= Lambda simulation of a Turing machine
{title2=$\mathsf{Run}=Y(\lambda r c.\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.
Back to article page
