Church encoding

Church encoding represents data and operations as terms of the lambda calculus. A Church numeral represents a natural number by repeated function application; a Church Boolean selects one of two arguments.

The Church numeral $c_n=\lambda f.\lambda x.f^{n}x$ encodes the natural number $n$ by iteration.

Church numeral successor, addition, multiplication, and exponentiation are represented by $\lambda nfx.f(nfx)$, $\lambda mnfx.mf(nfx)$, $\lambda mnfx.m(nf)x$, and $\lambda mnfx.(nm)fx$. The last term takes the base first and the exponent second. Its outer abstractions preserve the usual numeral normal form at exponent zero, implementing $m^0=1$, including $0^0=1$. At base type $A$, exponentiation uses an exponent at Church type $C_{A\to A}$ and a base at $C_A=(A\to A)\to A\to A$.

The lambda termreturns the Church Boolean $\mathsf{T}$ on $c_0$ and $\mathsf{F}$ on every positive Church numeral. Zero iterations leave the initial true value, while at least one iteration replaces it by false. Normal-order beta reduction evaluates a numeral conditional without evaluating an unchosen branch.

With the Church Booleans $\mathsf{T}=\lambda ab.a$ and $\mathsf{F}=\lambda ab.b$, encode a pair byThen $\mathsf{Fst}(\mathsf{Pair}AB){\to }_{\beta }^{\ast }A$ and the second projection similarly returns $B$. Pairing an iteration counter with a computed value implements primitive recursion using only Church numeral iteration.

A function $g:{\mathbb{N}}^k\to \mathbb{N}$ is lambda-definable when some combinator $G$ satisfiesfor every tuple of natural numbers.

The successor function is lambda-defined on Church numerals bybecause $\mathrm{Succ}{c}_n{\equiv }_{\beta }{c}_{n+1}$.

Using a fixed-point combinator, Church Boolean conditionals, a zero test, and a predecessor term, lambda-definable $g$ and $h$ giveNormal-order beta reduction evaluates only the selected conditional branch, so this term implements primitive recursion on Church numerals.

If total functions $g$ and $h$ are represented by lambda terms $G,H$, defineandAfter $j$ iterations the Church pair holds $(c_j,c_{f(\mathbf{x},j)})$, proved by mathematical induction using the defining recursion equations. Consequently $R$ represents the total primitive recursive function $f$. This statement concerns total inputs and total recursion constituents; it is not an unguarded composition theorem for arbitrary partial functions.

A partial function is lambda-definable when one lambda term maps Church numerals in its domain to the numeral of the output and produces no numeral on inputs outside its domain.

Every partial computable function is represented on Church numerals by a closed untyped lambda calculus term. First represent all primitive recursive functions using zero, successor, projections, composition and lambda definition of primitive recursion by pair iteration. Apply the Kleene normal form theorem and search successive history codes with a fixed-point combinator. Test the represented total predicate using a Church numeral zero test; return the decoded output only on the true branch. If no history passes, normal-order head reduction continues the search indefinitely and the term has no head normal form, so cannot be in beta equivalence with a Church numeral. This avoids the incorrect assumption that a lazy outer function must evaluate a divergent argument in an unguarded composition.

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.

The term $\mathrm{Force}{c}_{m}K$ beta-reduces to $K$ for every Church numeral $c_m$. If its first argument has no head normal form, the whole application has no head normal form. Nesting this operation forces each represented inner computation before applying an outer function, implementing composition of partial functions even when an outer projection would discard an argument. The same guard makes lambda definition of primitive recursion strict in the preceding recursive value.

For a lambda-definable partial $g(\mathbf{x},n)$, a fixed-point search term tests $n=0,1,2,\dots$ and returns the first $n$ for which $g(\mathbf{x},n)=0$. If no such value is reached, reduction produces no Church numeral. This realizes unbounded minimization and therefore makes every partial recursive function lambda-definable.

At type $\sigma \to \sigma \to \sigma$, the Church Booleans are $\top =\lambda x.\lambda y.x$ and $\perp =\lambda x.\lambda y.y$.