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.

  • 7
    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 Oct 11 at 6:19
  • 7
    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 Oct 11 at 6:21
up vote 7 down vote accepted

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.

  • 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 Oct 12 at 20:31
  • 1
    @Ł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: cstheory.stackexchange.com/a/41457/3984 – cody Oct 12 at 22:01
  • I think it's worth mentioning Lennart Augustsson's Simpler, Easier!. 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. – Łukasz Lew Oct 12 at 22:17
  • 1
    @Ł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: pauillac.inria.fr/~herbelin/articles/… – cody Oct 12 at 22:40
  • What does it means $u≤t$? – jonaprieto Nov 14 at 13:21

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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