Search

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$.

In synthetic computability, pioneered by Richman, Bridges, and Bauer, one develops computability theory without an explicit model of computation. This is enabled by assuming an axiom equivalent to postulating a function $\phi$ to be universal for the space $\mathbb{N}\to\mathbb{N}$ ($\mathsf{CT}_\phi$, a consequence of the constructivist axiom $\mathsf{CT}$), Markov's principle, and at least the axiom of countable choice. Assuming $\mathsf{CT}$ and countable choice invalidates the law of excluded middle, thereby also invalidating classical intuitions prevalent in textbooks on computability. On the other hand, results like Rice's theorem are not provable without a form of choice. In contrast to existing work, we base our investigations in constructive type theory with a separate, impredicative universe of propositions where countable choice does not hold and thus a priori $\mathsf{CT}_{\phi}$ and the law of excluded middle seem to be consistent. We introduce various parametric strengthenings of $\mathsf{CT}_{\phi}$, which are equivalent to assuming $\mathsf{CT}_\phi$ and an $S^m_n$ operator for $\phi$ like in the $S^m_n$ theorem. The strengthened axioms allow developing synthetic computability theory without choice, as demonstrated by elegant synthetic proofs of Rice's theorem. Moreover, they seem to be not in conflict with classical intuitions since they are consequences of the traditional analytic form of $\mathsf{CT}$. Besides explaining the novel axioms and proofs of Rice's theorem we contribute machine-checked proofs of all results in the Coq proof assistant.

"Church's thesis" ($\mathsf{CT}$) as an axiom in constructive logic states that every total function of type $\mathbb{N} \to \mathbb{N}$ is computable, i.e. definable in a model of computation. $\mathsf{CT}$ is inconsistent in both classical mathematics and in Brouwer's intuitionism since it contradicts Weak K\"onig's Lemma and the fan theorem, respectively. Recently, $\mathsf{CT}$ was proved consistent for (univalent) constructive type theory. Since neither Weak K\"onig's Lemma nor the fan theorem are a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that $\mathsf{CT}$ is inconsistent only with a combination of classical logic and choice axioms. We study consequences of $\mathsf{CT}$ and its relation to several classes of axioms in Coq's type theory, a constructive type theory with a universe of propositions which does neither prove classical logical axioms nor strong choice axioms. We thereby provide a partial answer to the question which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.

We implement three Coq plugins regarding inductive types in MetaCoq. The first plugin is a simple syntax transformation generating alternative constructors for inductive types by abstracting over concrete indices in the types of the constructors. The second plugin re-implements Coq's $\texttt{Scheme Induction}$ command in MetaCoq, and extends it to nested inductive types, e.g. types like rose trees which use $\texttt{list}$ in their definition, similar to the Elpi-plugin by Tassi. The third plugin implements the $\texttt{Derive Subterm}$ command provided by the Equations package in MetaCoq., Comment: accepted for presentation at the Coq Workshop 2020

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics \`a la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov's Principle and Weak K\"onig's Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper., Comment: extended version of https://link.springer.com/chapter/10.1007/978-3-030-36755-8_4

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem -- in our case by a Minsky machine -- is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer. Additionally, we prove the reverse direction and show that every Diophantine relation is recognisable by $\mu$-recursive functions and give a certified compiler from $\mu$-recursive functions to Minsky machines.

We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for \L, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.

We study the weak call-by-value $\lambda$-calculus as a model for computational complexity theory and establish the natural measures for time and space -- the number of beta-reductions and the size of the largest term in a computation -- as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas [STOC~84]. More precisely, we show that, using those measures, Turing machines and the weak call-by-value $\lambda$-calculus can simulate each other within a polynomial overhead in time and a constant factor overhead in space for all computations that terminate in (encodings) of 'true' or 'false'. We consider this result as a solution to the long-standing open problem, explicitly posed by Accattoli [ENTCS~18], of whether the natural measures for time and space of the $\lambda$-calculus are reasonable, at least in case of weak call-by-value evaluation. Our proof relies on a hybrid of two simulation strategies of reductions in the weak call-by-value $\lambda$-calculus by Turing machines, both of which are insufficient if taken alone. The first strategy is the most naive one in the sense that a reduction sequence is simulated precisely as given by the reduction rules; in particular, all substitutions are executed immediately. This simulation runs within a constant overhead in space, but the overhead in time might be exponential. The second strategy is heap-based and relies on structure sharing, similar to existing compilers of eager functional languages. This strategy only has a polynomial overhead in time, but the space consumption might require an additional factor of $\log n$, which is essentially due to the size of the pointers required for this strategy. Our main contribution is the construction and verification of a space-aware interleaving of the two strategies, which is shown to yield both a constant overhead in space and a polynomial overhead in time.

We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.

We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verifications include a reduction of a string rewriting problem generalising the halting problem for Turing machines to PCP, and reductions of PCP to the intersection problem and the palindrome problem for context-free grammars. Interestingly, rigorous correctness proofs for some of the reductions are missing in the literature.

We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.