<p>I would like to supplement the answer by cody by a general observation conveying my understanding of <em>why</em> the type checking algorithms work.</p>

<p>For a wide class of type theories, type checking or inference is performed in such a way that we never attempt to normalize a term, unless we have established beforehand that it is well-typed. Similarly, we never attempt to normalize a type, unless we have already established that it is a type. Because of this, we can be sure that normalization will terminate (which requires a separate proof).</p>

<p>One has to look at specific algorithms and see that they really work this way, but they do. I just wanted to state what makes them tick. Or better, that's the reason they stop ticking.</p>

CC BY-SA 4.0
2018-08-29T12:34:36.787Z
2018-08-29T12:34:36.787Z
Andrej Bauer
<p>Certainly the decision problem</p>

<blockquote>
  <p>Given a (pre-)term $a$ Is there a type $A$ such that $\vdash a :A$ is derivable in MLTT?</p>
</blockquote>

<p>Sometimes written $\vdash a\ :\ ?$ (and called the <em>type inference problem</em>) is decidable, which is to say it doesn't matter whether $a$ is well-typed or not to get an answer. Indeed, all proof checkers based on MLTT implement some version of this decision algorithm!</p>

<p>Obviously, the problem in a non-empty context ($\Gamma\vdash a\ :\ ?$) is decidable as well, usually you need to solve the latter to solve the former.</p>

<p>This should answer questions 1 and 2. The algorithm does <strong>not</strong> involve normalizing $a$, which in general would be bad news, since it is undecidable whether an untyped term normalizes to anything. However the type checking algorithm <strong>does</strong> involve normalizing <em>types</em>, which are by construction well-typed themselves.</p>

<p>As a result, normalization of well-typed terms is a necessary condition for the type inference problem to be decidable.</p>

<p>You might want to check <a href="http://www.cse.chalmers.se/~smith/handbook.pdf" rel="noreferrer">Nordström, Petersson and Smith</a> for an introduction.</p>

<hr>

<p>I'm not aware of any <em>generic</em> description of a type inference algorithm for normalizing type theories, though Pollack gives a pretty good overview (though the state of the art has improved) in <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.1842&amp;rep=rep1&amp;type=pdf" rel="noreferrer">Typechecking in Pure Type Systems</a>.</p>

CC BY-SA 4.0
2018-08-29T09:09:58.307Z
How about pretypes (terms allgedly denoting a type)? It might be worth clarifying their status as well.
Andrej Bauer
CC BY-SA 4.0
2018-08-29T12:19:37.330Z
Thank you cody, are you referring to the type checking algorithms implemented by proof assistants like ALF and Coq? To my understanding those are algorithms for the specific variants of MLTT they are based on (CIC for Coq, something else for ALF), but it is unclear to me how these may be used to type check the specific MLTT of '73. In particular, if the universe hierarchy or other differences in detail there might change anything...
Josh
CC BY-SA 4.0
2018-08-29T12:19:43.893Z
...Or are the algorithms general enough to cover these differences? I am having trouble finding results in such generality; all I seem to be turning up in my literature search are very specific results, often particularly tailored to the underlying theory of some proof assistant.
Josh
CC BY-SA 4.0
2018-08-30T14:47:55.693Z
@JoshChen the algorithms are at their core very general, as they involve a type-directed search, alternating with normalization steps on well-typed terms, as Andrej explained. I'm not aware of a *generic* description of the algorithm, unfortunately, though I'll add a partial reference to my answer.
cody
CC BY-SA 4.0
2018-08-31T12:32:13.650Z
I apologize for adding question on question, but I am now not sure what to make of the statement in https://ncatlab.org/nlab/show/decidability#typability claiming that "dependent type theory has undecidable typeability", I wonder what is going on there..
Josh
CC BY-SA 4.0
2018-09-03T23:21:28.000Z
@JoshChen They don't clarify, but they may be referring to inferring types for "curry-style" terms, for which inference is undecidable. I go into more detail here: https://cs.stackexchange.com/a/12957/988
cody
CC BY-SA 4.0
2021-03-15T19:02:33.310Z
No; it's an untyped lambda term in the language of the system.
cody
CC BY-SA 4.0
2018-08-28T17:15:04.760Z
2018-08-30T14:50:28.183Z
2018-08-30T14:50:28.183Z
cody
<ol>
<li><p>In Martin-Löf's <a href="https://www.sciencedirect.com/science/article/pii/S0049237X08719451" rel="noreferrer"><em>An Intuitionistic Theory of Types: Predicative Part</em></a> it is proved that type checking $a \colon A$ is decidable <em>subject to $a$ being typeable</em> in the first place, by proving a normalization theorem for closed typeable terms.
On the other hand, I've seen it written in multiple places (Wikipedia, Nördstrom etc.) that type-checking in (intensional) MLTT is decidable; are they implicitly restricting to typeable terms?</p></li>
<li><p>Is anything known about the decidability of type inference or type checking in intensional MLTT if we do not restrict to the typeable terms?
For instance, perhaps there is a decision process that recognizes untypeable terms, say by normalizing to a form that doesn't correspond to any of the constructors, or by showing that there is no non-periodic sequence of reductions for any untypeable term.</p>

<p>I haven't been able to find very much in the literature.</p></li>
</ol>

<reference-request><type-theory><type-inference>
Decidability of type inference and type checking in MLTT
Josh
# Decidability of type inference and type checking in MLTT

(Asked by: username_0 on 2018-08-26)

1. In Martin-Löf's [*An Intuitionistic Theory of Types: Predicative Part*](https://www.sciencedirect.com/science/article/pii/S0049237X08719451) it is proved that type checking $a \colon A$ is decidable *subject to $a$ being typeable* in the first place, by proving a normalization theorem for closed typeable terms.
   On the other hand, I've seen it written in multiple places (Wikipedia, Nördstrom etc.) that type-checking in (intensional) MLTT is decidable; are they implicitly restricting to typeable terms?
2. Is anything known about the decidability of type inference or type checking in intensional MLTT if we do not restrict to the typeable terms?
   For instance, perhaps there is a decision process that recognizes untypeable terms, say by normalizing to a form that doesn't correspond to any of the constructors, or by showing that there is no non-periodic sequence of reductions for any untypeable term.

   I haven't been able to find very much in the literature.

**Tags:** reference-request, type-theory, type-inference


---

## 2 answers

### Answer by username_2 on 2018-08-28. Score: 10 | Accepted answer

Certainly the decision problem

> Given a (pre-)term $a$ Is there a type $A$ such that $\vdash a :A$ is derivable in MLTT?

Sometimes written $\vdash a\ :\ ?$ (and called the *type inference problem*) is decidable, which is to say it doesn't matter whether $a$ is well-typed or not to get an answer. Indeed, all proof checkers based on MLTT implement some version of this decision algorithm!

Obviously, the problem in a non-empty context ($\Gamma\vdash a\ :\ ?$) is decidable as well, usually you need to solve the latter to solve the former.

This should answer questions 1 and 2. The algorithm does **not** involve normalizing $a$, which in general would be bad news, since it is undecidable whether an untyped term normalizes to anything. However the type checking algorithm **does** involve normalizing *types*, which are by construction well-typed themselves.

As a result, normalization of well-typed terms is a necessary condition for the type inference problem to be decidable.

You might want to check [Nordström, Petersson and Smith](http://www.cse.chalmers.se/~smith/handbook.pdf) for an introduction.

---

I'm not aware of any *generic* description of a type inference algorithm for normalizing type theories, though Pollack gives a pretty good overview (though the state of the art has improved) in [Typechecking in Pure Type Systems](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.1842&rep=rep1&type=pdf).

> **Comments:**
> **username_1**: How about pretypes (terms allgedly denoting a type)? It might be worth clarifying their status as well.  
> **username_0**: Thank you username_2, are you referring to the type checking algorithms implemented by proof assistants like ALF and Coq? To my understanding those are algorithms for the specific variants of MLTT they are based on (CIC for Coq, something else for ALF), but it is unclear to me how these may be used to type check the specific MLTT of '73. In particular, if the universe hierarchy or other differences in detail there might change anything...  
> **username_0**: ...Or are the algorithms general enough to cover these differences? I am having trouble finding results in such generality; all I seem to be turning up in my literature search are very specific results, often particularly tailored to the underlying theory of some proof assistant.  
> **username_2**: @username_0Chen the algorithms are at their core very general, as they involve a type-directed search, alternating with normalization steps on well-typed terms, as Andrej explained. I'm not aware of a *generic* description of the algorithm, unfortunately, though I'll add a partial reference to my answer.  
> **username_0**: I apologize for adding question on question, but I am now not sure what to make of the statement in https://ncatlab.org/nlab/show/decidability#typability claiming that "dependent type theory has undecidable typeability", I wonder what is going on there..  
> **username_2**: @username_0Chen They don't clarify, but they may be referring to inferring types for "curry-style" terms, for which inference is undecidable. I go into more detail here: https://cs.stackexchange.com/a/12957/988  
> **username_2**: No; it's an untyped lambda term in the language of the system.  

---

### Answer by username_1 on 2018-08-29. Score: 9

I would like to supplement the answer by username_2 by a general observation conveying my understanding of *why* the type checking algorithms work.

For a wide class of type theories, type checking or inference is performed in such a way that we never attempt to normalize a term, unless we have established beforehand that it is well-typed. Similarly, we never attempt to normalize a type, unless we have already established that it is a type. Because of this, we can be sure that normalization will terminate (which requires a separate proof).

One has to look at specific algorithms and see that they really work this way, but they do. I just wanted to state what makes them tick. Or better, that's the reason they stop ticking.


---

