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?

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$.

StackExchange Computer Science Q#138208, answer score: 4