<p>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.</p>

<p>See e.g. this Mathoverflow question: <a href="https://mathoverflow.net/questions/223109/does-the-notion-of-provably-total-function-depend-on-the-chosen-representation">https://mathoverflow.net/questions/223109/does-the-notion-of-provably-total-function-depend-on-the-chosen-representation</a></p>

<p>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 <a href="http://progress-preservation.blogspot.com/2010/05/weak-normalization-cut-elimination-and.html" rel="nofollow noreferrer">here</a>. This is impossible if Coq/Gallina is actually consistent, <em>per</em> the second incompleteness theorem.</p>

<p>Two obvious fixes:</p>

<ul>
<li><p>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 <a href="http://www.cs.swan.ac.uk/~csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf" rel="nofollow noreferrer">induction-recursion</a>. 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.</p></li>
<li><p>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 <em>explicit</em> 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.</p></li>
</ul>

<p>Note that talking about <em>computability</em> of these axioms doesn't make much sense: a single axiom on it's own is always computable in the sense of <a href="https://en.wikipedia.org/wiki/Computability_theory#Computable_and_uncomputable_sets" rel="nofollow noreferrer">computable sets</a> which is usually what we mean when we talk about <em>computable theories</em>.</p>

<p>However an axiom may or may not have <em>computational content</em>, 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 <em>always correct</em> from a computable (constructive) point of view if $T$ does indeed always halt in the "true" world.</p>

CC BY-SA 3.0
2016-07-28T09:44:58.573Z
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?)
Shea Levy
CC BY-SA 3.0
2016-07-28T09:46:26.027Z
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?
Shea Levy
CC BY-SA 3.0
2016-07-28T09:51:39.087Z
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 :)
Shea Levy
CC BY-SA 3.0
2016-07-28T11:58:31.287Z
1. The first few lines of [this post](http://fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html) outline how to create a *model* for a type theory using I-R, and [this paper by Dybjer and Setzer](http://www.sciencedirect.com/science/article/pii/S0168007202000969) expand on the idea. Again, this has never been done for Coq, *per se*.
cody
CC BY-SA 3.0
2016-07-28T11:58:56.177Z
2. You are correct, it's not possible in general to prove that such a number exists.
cody
CC BY-SA 3.0
2016-07-27T22:03:02.663Z
2016-07-27T22:03:02.663Z
2017-04-13T12:57:54.777Z
cody
<p>I understand the diagonalization argument against implementing an <code>eval</code> 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 <code>T</code> for total dependently typed language <code>A</code> in (possibly non-total) language <code>B</code>, formalize <code>B</code> in <code>A</code>, and prove the correctness/termination/etc. of <code>T</code> in that formalization (without relying on cheats like including a primitive operation in <code>B</code> that does typechecking)? If not, is it possible to add some (presumably non-computable?) axiom to <code>A</code> that is not included in <code>T</code> and allows the proof to go through without allowing verifying incorrect implementations?</p>

<p>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?</p>

CC BY-SA 3.0
2016-07-26T22:24:13.367Z
So theoretically, how could you prove correctness? It seems you would have to formalize Coq in Coq? Maybe I'm missing something
pdexter
<type-theory><dependent-type><program-verification>
Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?
Shea Levy
# Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?

(Asked by: username_0 on 2016-07-26)

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?

**Tags:** type-theory, dependent-type, program-verification

> **Comments:**
> **username_1**: So theoretically, how could you prove correctness? It seems you would have to formalize Coq in Coq? Maybe I'm missing something  

---

## 1 answers

### Answer by username_2 on 2016-07-27. Score: 4 | Accepted answer

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](http://progress-preservation.blogspot.com/2010/05/weak-normalization-cut-elimination-and.html). 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](http://www.cs.swan.ac.uk/~csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf). 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](https://en.wikipedia.org/wiki/Computability_theory#Computable_and_uncomputable_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.

> **Comments:**
> **username_0**: 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?)  
> **username_0**: 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?  
> **username_0**: 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 :)  
> **username_2**: 1. The first few lines of [this post](http://fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html) outline how to create a *model* for a type theory using I-R, and [this paper by Dybjer and Setzer](http://www.sciencedirect.com/science/article/pii/S0168007202000969) expand on the idea. Again, this has never been done for Coq, *per se*.  
> **username_2**: 2. You are correct, it's not possible in general to prove that such a number exists.  

---

