# Proving program termination in the $\lambda$-calculus

Turing's Checking a large routine:

Finally the checker has to verify that the process comes to an end. Here again he should be assisted by the programmer giving a further definite assertion to be verified. This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops. To the pure mathematician it is natural to give an ordinal number.

How do you apply this to a program written in the untyped $$\lambda$$-calculus?

Such a quantity exists if and only if the lambda-term is normalizable (according to a chosen reduction strategy $$\to$$). Proof: suppose there is a function $$f : \mathbf{\Lambda}(M_0) \to \mathbb{N}$$ where $$\mathbf{\Lambda}(M_0)$$ is the set of lambda-terms $$M$$ such that $$M_0 \to^\star M$$, such that if $$M \to M'$$ then $$f(M) \lt f(M')$$. Then the length of a reduction chain from $$M_0$$ is bounded by $$f(M_0)$$ and in particular cannot be infinite, so $$M_0$$ is strongly normalizable. Conversely, if $$M_0$$ is strongly normalizable, define $$f(M)$$ as the length of the longest reduction starting at $$M$$.