Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions

• URL: http://arxiv.org/abs/2307.15543v1
• Date: Fri, 28 Jul 2023 13:16:46 GMT
• Title: Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
• Authors: Yannick Forster, Dominik Kirst, Niklas M\"uck
• Abstract summary: We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions. As usual in synthetic approaches, we employ a definition of oracle computations based on meta-level functions. We show that Turing reducibility forms an upper semilattice, transports decidability, and is strictly more expressive than truth-table reducibility.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof assistant. As usual in synthetic approaches, we employ a definition of oracle computations based on meta-level functions rather than object-level models of computation, relying on the fact that in constructive systems such as CIC all definable functions are computable by construction. Such an approach lends itself well to machine-checked proofs, which we carry out in Coq. There is a tension in finding a good synthetic rendering of the higher-order notion of oracle computability. On the one hand, it has to be informative enough to prove central results, ensuring that all notions are faithfully captured. On the other hand, it has to be restricted enough to benefit from axioms for synthetic computability, which usually concern first-order objects. Drawing inspiration from a definition by Andrej Bauer based on continuous functions in the effective topos, we use a notion of sequential continuity to characterise valid oracle computations. As main technical results, we show that Turing reducibility forms an upper semilattice, transports decidability, and is strictly more expressive than truth-table reducibility, and prove that whenever both a predicate $p$ and its complement are semi-decidable relative to an oracle $q$, then $p$ Turing-reduces to $q$.

Related papers

• On Computational Indistinguishability and Logical Relations [1.024113475677323]
  The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.
  arXiv  Detail & Related papers  (2024-08-30T15:08:51Z)
• On the Representational Capacity of Neural Language Models with Chain-of-Thought Reasoning [87.73401758641089]
  Chain-of-thought (CoT) reasoning has improved the performance of modern language models (LMs) We show that LMs can represent the same family of distributions over strings as probabilistic Turing machines.
  arXiv  Detail & Related papers  (2024-06-20T10:59:02Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  We propose complexity-impacted reasoning score (CIRS) to measure correlation between code and reasoning abilities. Specifically, we use the abstract syntax tree to encode the structural information and calculate logical complexity. Code will be integrated into the EasyInstruct framework at https://github.com/zjunlp/EasyInstruct.
  arXiv  Detail & Related papers  (2023-08-29T17:22:39Z)
• Efficient Computation of Counterfactual Bounds [44.4263314637532]
  We compute exact counterfactual bounds via algorithms for credal nets on a subclass of structural causal models. We evaluate their accuracy by providing credible intervals on the quality of the approximation.
  arXiv  Detail & Related papers  (2023-07-17T07:59:47Z)
• The vacuum provides quantum advantage to otherwise simulatable architectures [49.1574468325115]
  We consider a computational model composed of ideal Gottesman-Kitaev-Preskill stabilizer states. We provide an algorithm to calculate the probability density function of the measurement outcomes.
  arXiv  Detail & Related papers  (2022-05-19T18:03:17Z)
• Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
  We show that we can learn arbitrary logic in a single layer using an activation function of matching or greater arity. We represent belief tables using a basis that directly associates the number of nonzero parameters to the effective arity of the belief function. This opens optimization approaches to reduce logical complexity by inducing parameter sparsity.
  arXiv  Detail & Related papers  (2022-03-16T22:47:53Z)
• Resource Optimisation of Coherently Controlled Quantum Computations with the PBS-calculus [55.2480439325792]
  Coherent control of quantum computations can be used to improve some quantum protocols and algorithms. We refine the PBS-calculus, a graphical language for coherent control inspired by quantum optics.
  arXiv  Detail & Related papers  (2022-02-10T18:59:52Z)
• Statistically Meaningful Approximation: a Case Study on Approximating Turing Machines with Transformers [50.85524803885483]
  This work proposes a formal definition of statistically meaningful (SM) approximation which requires the approximating network to exhibit good statistical learnability. We study SM approximation for two function classes: circuits and Turing machines.
  arXiv  Detail & Related papers  (2021-07-28T04:28:55Z)
• Programming by Rewards [20.626369097817715]
  We formalize and study programming by rewards'' (PBR), a new approach for optimizing some quantitative metric such as performance, resource utilization, or correctness over a benchmark. A PBR specification consists of (1) input features $x$, and (2) a reward function $r$, modeled as a black-box component (which we can only run) We show that the framework is theoretically-founded ---in cases when the rewards satisfy nice properties, the synthesized code is optimal in a precise sense.
  arXiv  Detail & Related papers  (2020-07-14T05:49:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.