I understand the diagonalization argument against implementing an eval function in a total language, and that typechecking in a dependently typed language requires evaluation, so implementing a typechecker for a total dependently typed language in itself is out. But is it possible to write a typechecker T for total dependently typed language A in (possibly non-total) language B, formalize B in A, and prove the correctness/termination/etc. of T in that formalization (without relying on cheats like including a primitive operation in B that does typechecking)? If not, is it possible to add some (presumably non-computable?) axiom to A that is not included in T and allows the proof to go through without allowing verifying incorrect implementations?

More concretely, suppose I have some formalization of turing machines in Coq and write a turing machine that takes a finite text stream (encoded in some reasonable format) and outputs a 1 if it represents a well-typed Gallina fragment and a 0 otherwise. Could I prove termination and correctness of that turing machine in Coq itself?

  • $\begingroup$ So theoretically, how could you prove correctness? It seems you would have to formalize Coq in Coq? Maybe I'm missing something $\endgroup$ – pdexter Jul 26 '16 at 22:24

As often in these matters, the encodings are important: you could have some silly encoding of Turing machines or Gallina terms or both where an input string $\langle n\rangle$ represents "the $n$-th well-typed term in Gallina". The TM that accepts this is trivial, and you'd be able to prove correctness and termination of the machine easily.

See e.g. this Mathoverflow question: https://mathoverflow.net/questions/223109/does-the-notion-of-provably-total-function-depend-on-the-chosen-representation

However, for any reasonable representation, any proof that the "usual" type checking algorithm terminates implies termination of reduction for well-typed terms, which in turn implies consistency of the underlying logic as suggested here. This is impossible if Coq/Gallina is actually consistent, per the second incompleteness theorem.

Two obvious fixes:

  • Add consistency of Coq (or some equivalent or stronger statement) to your list of axioms. One possible axiom is: consistency of ZFC + $\omega$-many inaccessible cardinals. If you want something more computational, you can add a strong enough form of induction-recursion. I don't think anyone's worked out the details for the CiC yet, but I imagine they're very similar to those for (for instance) Agda.

  • Add some constraints on the representation of well-typed terms to be checked. In Gallina, terms carry implicit computational content, to be executed as the usual type-checking algorithm runs. However one could imagine an explicit form of the language, where each term comes with a natural number representing the "gas" it is allowed to use, aka the number of steps it must not exceed during reduction. Then the correctness proof for the type-checking algorithm would be conditional on not exceeding this explicit limit of computation.

Note that talking about computability of these axioms doesn't make much sense: a single axiom on it's own is always computable in the sense of computable sets which is usually what we mean when we talk about computable theories.

However an axiom may or may not have computational content, for example an axiom $\exists x,\ P$ may cause a theory to lose the existence property, if there is no closed term $t$ which satisfies $P[t/x]$. However, an axiom that asserts that a Turing machine $T$ halts on all inputs is always correct from a computable (constructive) point of view if $T$ does indeed always halt in the "true" world.

| cite | improve this answer | |
  • $\begingroup$ Thanks! Some followup questions:1. I'm familiar with induction-recursion as it appears in Idris and have skimmed the linked slides, but how does adding it translate to the consistency of Coq (presumably consistency of Coq without induction-recursion?) $\endgroup$ – Shea Levy Jul 28 '16 at 9:44
  • $\begingroup$ 2. If constraints on the number of steps were added, I assume it wouldn't be possible to prove that for any statement, there is some number of steps above which it will always return either type-correct or type-incorrect? $\endgroup$ – Shea Levy Jul 28 '16 at 9:46
  • $\begingroup$ I suppose if 2 were possible then you could just define an algorithm that runs the constrained algorithm and increases the size one by one until it doesn't return out-of-gas, so never mind on that one :) $\endgroup$ – Shea Levy Jul 28 '16 at 9:51
  • 1
    $\begingroup$ 1. The first few lines of this post outline how to create a model for a type theory using I-R, and this paper by Dybjer and Setzer expand on the idea. Again, this has never been done for Coq, per se. $\endgroup$ – cody Jul 28 '16 at 11:58
  • 1
    $\begingroup$ 2. You are correct, it's not possible in general to prove that such a number exists. $\endgroup$ – cody Jul 28 '16 at 11:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.