Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?

Question

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?

Answer 1

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.