Lambda-definable partial function

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.