In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part 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?
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.
migrated from cs.stackexchange.com Aug 28 '18 at 15:46
This question came from our site for students, researchers and practitioners of computer science.
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 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.
I would like to supplement the answer by cody 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.