Lambda simulation of a Turing machine ($\mathsf{Run}=Y(\lambda rc.\mathsf{Halt}c(\mathsf{Out}c)(r(\mathsf{Next}c)))$)

Represent total machine configuration transitions and tests on Church numerals and Church pairs, then use a fixed-point combinator to iterate until the halting test selects the output. Normal-order beta reduction follows the computation. A nonhalting machine gives an infinite required reduction, so the normal-order normalization theorem rules out a numeral normal form.