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?
This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops.
Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda calculus (with or without types: types don't affect evaluation), you want a quantity (a positive integer) that decreases at each reduction step.
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$.
