<p>There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why things work out all right when type-checking in a &quot;standard&quot; dependent type theory (I'll be deliberately vague, since these issues tend to crop up regardless):</p>
<p>Fact 1: If <span class="math-container">${\cal D}$</span> is a derivation of <span class="math-container">$\Gamma\vdash t:A$</span>, then there is a derivation <span class="math-container">${\cal D}'$</span> of <span class="math-container">$\Gamma \vdash A:s$</span> for some kind <span class="math-container">$s$</span>, and for every subterm <span class="math-container">$u\leq t$</span>, there is some type <span class="math-container">$B$</span>, a context <span class="math-container">$\Delta$</span> and a derivation <span class="math-container">$\cal D''$</span> of <span class="math-container">$\Delta\vdash u:B$</span>.</p>
<p>This nice fact is somewhat hard to prove, and offset by a pretty nasty counter-fact:</p>
<p>Fact 2: In general, <span class="math-container">$\cal D'$</span> and <span class="math-container">$\cal D''$</span> <strong>are not</strong> sub-derivations of <span class="math-container">$\cal D$</span>!</p>
<p>This depends a bit on the precise formulation of your type system, but most &quot;operational&quot; systems implemented in practice do satisfy Fact 2.</p>
<p>This means that you cannot &quot;pass to sub-terms&quot; when reasoning by induction on derivations, or conclude that the inductive statement is true about the type of the term you're trying to prove something about.</p>
<p>This fact bites you quite harshly when trying to prove seemingly innocent statements, e.g. that systems with typed conversion are equivalent to those with untyped conversion.</p>
<p><strong>However</strong>, in the case of type inference, you can give a simultaneous type and sort (the type of the type) inference algorithm by induction on the structure of the term, which may involve a type-directed algorithm as Andrej suggests. For a given term <span class="math-container">$t$</span> (and context <span class="math-container">$\Gamma$</span>, you either fail or find <span class="math-container">$A, s$</span> such that <span class="math-container">$\Gamma\vdash t:A$</span> and <span class="math-container">$\Gamma\vdash A : s$</span>. You do not need to use the inductive hypothesis to find the latter derivation, and so in particular you avoid the problem explained above.</p>
<p>The crucial case (and the only case which really requires conversion) is application:</p>
<pre><code>infer(t u):
   type_t, sort_t &lt;- infer(t)
   type_t' &lt;- normalize(type_t)
   type_u, sort_u &lt;- infer(u)
   type_u' &lt;- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail
</code></pre>
<p>Every call to normalize was done on well-typed terms, as this is the invariant for <code>infer</code>'s success.</p>
<hr />
<p>By the way, as it is implemented, Coq does not have decidable type checking, as it normalizes the body of <code>fix</code> statements before attempting to type check them.</p>
<p>At any rate, the bounds on the normal forms of well-typed terms are so astronomical, that the decidability theorem is mostly academic at this point anyways. In practice, you run the type checking algorithm for as long as you have patience for, and try a different route if it hasn't finished by then.</p>

CC BY-SA 4.0
2018-10-12T20:31:03.113Z
I found your answer very useful, thank you. I have two questions: 1. What does it mean "operational systems"? What's the alternative? 2. Can you be more explicit on with the example: what it means (what fact are we trying to prove?) "systems with typed conversion are equivalent to those with untyped conversion."? Thanks!
Łukasz Lew
CC BY-SA 4.0
2018-10-12T22:01:41.313Z
@ŁukaszLew The alternative to an operational system (one implemented in practice in e.g. the Coq or Agda software) would be a theoretical system, which is useful to prove meta-theoretic properties, but is inefficient or inconvenient to use in practice. Proving the equivalence of an operational and a theoretical system is often an important part of a system design. I talk more about this here: https://cstheory.stackexchange.com/a/41457/3984
cody
CC BY-SA 4.0
2018-10-12T22:17:58.793Z
I think it's worth mentioning Lennart Augustsson's [Simpler, Easier!](http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html). This is a minimal Haskell implementation of type checking and some inference for dependently typed lambda calculus. There is code that closely corresponds to cody's `infer(t u):`; to find it, search for "`tCheck r (App f a) =`". For a more complete but still simple implementation you can check [Morte's `typeWith`](https://github.com/Gabriel439/Haskell-Morte-Library/blob/262c695292abe3396e83810de4b612a712ba1ddf/src/Morte/Core.hs#L567).
Łukasz Lew
CC BY-SA 4.0
2018-10-12T22:40:42.977Z
@ŁukaszLew The typed vs untyped conversion problem is a well-known open question that relates 2 formulations of type theories, and was resolved rather recently: http://pauillac.inria.fr/~herbelin/articles/jfp-SilHer11-pts-typed-conv-all.pdf
cody
CC BY-SA 4.0
2018-11-14T13:21:06.230Z
What does it means $u≤t$?
Jonathan Prieto-Cubides
CC BY-SA 4.0
2018-11-14T14:52:42.937Z
@jonaprieto it's just the subterm order on (raw) terms.
cody
CC BY-SA 4.0
2018-10-11T22:51:18.140Z
2018-10-11T22:51:18.140Z
2020-06-17T09:38:08.363Z
cody
<p>I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and thus that definitional equality is decidable.</p>

<p>In many references I read, the decidability of typechecking is listed as a corollary of strong normalization, and I believe it in those cases, but I'm wondering how one goes about actually showing this.</p>

<p>In particular, I'm stuck on the following: </p>

<ul>
<li>Just because well typed terms are strongly normalizing, doesn't mean that the algorithm won't loop forever on non-well typed inputs</li>
<li>Since logical relations are usually used to show strong normalization, there's not a convenient decreasing metric as we progress typechecking terms. So even if my type rules are syntax directed, there's no guarantee that applying the rules will eventually terminate.</li>
</ul>

<p>I'm wondering, does anyone have a good reference to a proof of decidability of typechecking for a dependently typed language? If it's a small core calculus, that's fine. Anything that discusses proof techniques for showing decidability would be great.</p>

CC BY-SA 4.0
2018-10-11T06:19:51.503Z
The usual bidirectional type-checking algorithms never attempt to normalize a term (or a type) without first checking that it is well-typed (or well-formed). You need not worry about normalizing untyped terms.
Andrej Bauer
CC BY-SA 4.0
2018-10-11T06:21:49.820Z
Regarding applying the rules: all term and type rules decrease the goal, except type conversion. Thus we need to control type conversion, which we do by using a bi-directional approach.
Andrej Bauer
<reference-request><pl.programming-languages><type-theory><dependent-type><typed-lambda-calculus>
Proof techniques for showing that dependent type checking is decidable
Joey Eremondi
# Proof techniques for showing that dependent type checking is decidable

(Asked by: username_0 on 2018-10-11)

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and thus that definitional equality is decidable.

In many references I read, the decidability of typechecking is listed as a corollary of strong normalization, and I believe it in those cases, but I'm wondering how one goes about actually showing this.

In particular, I'm stuck on the following:

* Just because well typed terms are strongly normalizing, doesn't mean that the algorithm won't loop forever on non-well typed inputs
* Since logical relations are usually used to show strong normalization, there's not a convenient decreasing metric as we progress typechecking terms. So even if my type rules are syntax directed, there's no guarantee that applying the rules will eventually terminate.

I'm wondering, does anyone have a good reference to a proof of decidability of typechecking for a dependently typed language? If it's a small core calculus, that's fine. Anything that discusses proof techniques for showing decidability would be great.

**Tags:** reference-request, pl.programming-languages, type-theory, dependent-type, typed-lambda-calculus

> **Comments:**
> **username_1**: The usual bidirectional type-checking algorithms never attempt to normalize a term (or a type) without first checking that it is well-typed (or well-formed). You need not worry about normalizing untyped terms.  
> **username_1**: Regarding applying the rules: all term and type rules decrease the goal, except type conversion. Thus we need to control type conversion, which we do by using a bi-directional approach.  

---

## 1 answers

### Answer by username_2 on 2018-10-11. Score: 9 | Accepted answer

There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why things work out all right when type-checking in a "standard" dependent type theory (I'll be deliberately vague, since these issues tend to crop up regardless):
Fact 1: If ${\cal D}$ is a derivation of $\Gamma\vdash t:A$, then there is a derivation ${\cal D}'$ of $\Gamma \vdash A:s$ for some kind $s$, and for every subterm $u\leq t$, there is some type $B$, a context $\Delta$ and a derivation $\cal D''$ of $\Delta\vdash u:B$.
This nice fact is somewhat hard to prove, and offset by a pretty nasty counter-fact:
Fact 2: In general, $\cal D'$ and $\cal D''$ are not sub-derivations of $\cal D$!
This depends a bit on the precise formulation of your type system, but most "operational" systems implemented in practice do satisfy Fact 2.
This means that you cannot "pass to sub-terms" when reasoning by induction on derivations, or conclude that the inductive statement is true about the type of the term you're trying to prove something about.
This fact bites you quite harshly when trying to prove seemingly innocent statements, e.g. that systems with typed conversion are equivalent to those with untyped conversion.
However, in the case of type inference, you can give a simultaneous type and sort (the type of the type) inference algorithm by induction on the structure of the term, which may involve a type-directed algorithm as Andrej suggests. For a given term $t$ (and context $\Gamma$, you either fail or find $A, s$ such that $\Gamma\vdash t:A$ and $\Gamma\vdash A : s$. You do not need to use the inductive hypothesis to find the latter derivation, and so in particular you avoid the problem explained above.
The crucial case (and the only case which really requires conversion) is application:
infer(t u):
   type_t, sort_t <- infer(t)
   type_t' <- normalize(type_t)
   type_u, sort_u <- infer(u)
   type_u' <- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail

Every call to normalize was done on well-typed terms, as this is the invariant for infer's success.

By the way, as it is implemented, Coq does not have decidable type checking, as it normalizes the body of fix statements before attempting to type check them.
At any rate, the bounds on the normal forms of well-typed terms are so astronomical, that the decidability theorem is mostly academic at this point anyways. In practice, you run the type checking algorithm for as long as you have patience for, and try a different route if it hasn't finished by then.

> **Comments:**
> **username_3**: I found your answer very useful, thank you. I have two questions: 1. What does it mean "operational systems"? What's the alternative? 2. Can you be more explicit on with the example: what it means (what fact are we trying to prove?) "systems with typed conversion are equivalent to those with untyped conversion."? Thanks!  
> **username_2**: @ŁukaszLew The alternative to an operational system (one implemented in practice in e.g. the Coq or Agda software) would be a theoretical system, which is useful to prove meta-theoretic properties, but is inefficient or inconvenient to use in practice. Proving the equivalence of an operational and a theoretical system is often an important part of a system design. I talk more about this here: https://cstheory.stackexchange.com/a/41457/3984  
> **username_3**: I think it's worth mentioning Lennart Augustsson's [Simpler, Easier!](http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html). This is a minimal Haskell implementation of type checking and some inference for dependently typed lambda calculus. There is code that closely corresponds to username_2's `infer(t u):`; to find it, search for "`tCheck r (App f a) =`". For a more complete but still simple implementation you can check [Morte's `typeWith`](https://github.com/Gabriel439/Haskell-Morte-Library/blob/262c695292abe3396e83810de4b612a712ba1ddf/src/Morte/Core.hs#L567).  
> **username_2**: @ŁukaszLew The typed vs untyped conversion problem is a well-known open question that relates 2 formulations of type theories, and was resolved rather recently: http://pauillac.inria.fr/~herbelin/articles/jfp-SilHer11-pts-typed-conv-all.pdf  
> **username_4**: What does it means $u≤t$?  
> **username_2**: @jonaprieto it's just the subterm order on (raw) terms.  

---

