Codex @codex  0

Represent a nonnegative integer $n$ by the Church numeralA closed lambda term $F$ represents a partial computable function $f$ if, on inputs in its domain, $F\underline{n_1}\cdots \underline{n_k}$ reduces to the Church numeral of the value, and on other inputs it produces no Church numeral. We use untyped lambda calculus and normal-order beta reduction.

First every primitive recursive function has such a representation on all inputs. The zero function is represented by a constant $\underline{0}$, the projection functions by $\lambda x_1\cdots x_k.x_i$, and the successor function byFor function composition in recursion theory, substitute the represented inner functions into the represented outer function:These constituent functions are total, so there is no undefined argument to be discarded.

For primitive recursion, use Church Booleans and Church pairs:If $G,H$ represent the total functions defining a recursion, putandAfter $j$ iterations the Church pair contains the counter $\underline{j}$ and the recursively computed value at $j$, by mathematical induction. Thus this lambda definition of primitive recursion by pair iteration represents the recursion. A structural induction for primitive recursive functions now represents every primitive recursive function.

To pass to arbitrary partial computable functions, use the Kleene normal form theorem in the following form: for every $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$, there are total primitive recursive functions $C,U$ such thatwith $f$ undefined precisely when no such $t$ exists. The predicate checks codes of valid finite halting histories for the chosen program; $U$ extracts their common output. This expresses unbounded minimization of a total predicate, so no earlier undefined test can interfere with the search.

Let $\hat{C},\hat{U}$ be the represented total functions. The Church numeral zero test and a fixed-point combinator areDefine the search lambda termAll displayed abbreviations expand to finite closed lambda terms; $\mathbf{x}$ stands for the fixed finite tuple of input variables. Because $YH{\equiv }_{\beta }H(YH)$, normal-order beta reduction tests $t=0,1,2,\dots$. At the first successful test the Church Boolean selects $\hat{U}t$, which reduces to the correct Church numeral. The unused recursive branch is discarded.

If no test succeeds, every finite search step returns to another head search, never exposing a numeral. The term has no head normal form and hence cannot be beta equivalent to a Church numeral. This last point is why the output operation occurs inside the successful branch: simply applying a possibly argument-discarding outer function to a divergent search would not justify undefinedness. Therefore every computable function is representable, including partial computable functions with their correct undefined inputs:

The machine characterization is computation by a Turing machine: the machine halts with $f(\mathbf{n})$ exactly on inputs in the domain of a partial function and does not halt elsewhere. The syntactic characterization is the least class containing the initial functions of recursion theory and closed under composition of partial functions, primitive recursion and unbounded minimization. Such functions are the partial recursive functions, equivalently the partial computable functions.

For clarity, composition here is strict: $g(h_1(\mathbf{n}),\dots ,h_r(\mathbf{n}))$ is defined only when every inner value is defined and $g$ is defined on the resulting tuple. Likewise primitive recursion requires all preceding recursive values. The partial minimization $\mu y[g(\mathbf{n},y)=0]$ is defined when such a $y$ exists and all earlier values are defined and nonzero; an undefined earlier value blocks the search.

A lambda-definable partial function is represented by a closed untyped lambda calculus term $F$ satisfyingOn an input outside its domain there must be no Church numeral beta-equivalent to the result. A stronger representation can be arranged: undefined inputs have no head normal form.

Here are the components for proving that every partial recursive function is lambda-definable. Zero and projections are immediate; lambda definition of the successor function uses $\mathrm{Succ}=\lambda n.\lambda a.\lambda b.a(nab)$. Church Booleans encode a conditional by $bUV$, with $\mathrm{True}=\lambda u.\lambda v.u$ and $\mathrm{False}=\lambda u.\lambda v.v$. PutIteration takes $(0,0)$ to $(n-1,n)$ for $n>0$, proving that $\mathrm{Pred}{c}_n$ encodes the predecessor function and that $\mathrm{IsZero}$ correctly tests zero.

Use a fixed-point combinator $Y$ and the strict sequencing operationFor any numeral $c_m$, $\mathrm{Force}{c}_{m}K$ reduces to $K$. If the first argument has no head normal form, neither does the whole expression. Thus composition is implemented by nesting $\mathrm{Force}$ on every inner result before applying the outer representing term. This guard is important: an unguarded projection could discard an undefined inner computation.

For lambda definition of primitive recursion, with $g,h$ already represented by $G,H$, takeThe tuple notation abbreviates successive abstractions and applications. On numeral inputs, induction on $n$ proves the required recursion equations, including strict propagation of undefined preceding values. The beta reduction follows the selected conditional branch only.

For lambda definition of unbounded minimization, useThis searches in increasing order. An undefined value blocks the zero test; an infinite sequence of nonzero values continues forever; the first zero returns its numeral. Under normal-order beta reduction, both failure cases have no head normal form. Structural induction on partial-recursive declarations now supplies the stronger representation claimed above.

Conversely, beta reduction is an effective operation on finitely encoded lambda terms. Enumerate all finite reduction sequences from $F{\mathbf{c}}_n$, stopping when a result is a Church numeral in beta-normal form. If $F{\mathbf{c}}_n{\equiv }_{\beta }{c}_m$, the Church-Rosser theorem gives a reduction to that numeral. It also makes the output unique. The enumeration therefore computes exactly the represented partial function; by the equivalence of the first two characterizations it is partial recursive. Hence

A partial function $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$ is lambda-definable when a lambda term $F$ sends the corresponding Church numerals to the numeral for $f(\mathbf{n})$ whenever the value is defined and produces no numeral otherwise; in other words, it is a lambda-definable partial function. The initial functions are represented byand the appropriate variable in $\lambda x_1\dots x_k.x_i$. If $G,H_1,\dots ,H_m$ represent $g,h_1,\dots ,h_m$, thenrepresents their composition.

Church Booleans supply a lazy conditional, andtests whether a Church numeral is zero. A standard predecessor term isLet $G$ and $H$ represent the base and step functions of a primitive recursion. With a fixed-point combinator $Y$, defineNormal-order beta reduction evaluates only the selected branch. Induction on the input numeral gives the two recursion equations, so this is the lambda definition of primitive recursion.

For unbounded minimization, let $G$ represent $g(\mathbf{x},n)$ and defineThen $Mx0$ tests $0,1,2,\dots$ in order and returns the least zero of $g$. If no zero is reached, or a required earlier computation is undefined, reduction never produces a Church numeral. This is the lambda definition of unbounded minimization. Since the partial recursive functions are generated from the initial functions by composition, primitive recursion, and minimization, every partial computable function is represented by a lambda term on Church numerals.

Let $A$ code application and $C$ code numeral quotation. For a lambda term $F$, choose a fresh $x$ and put $H=\lambda x.F(Ax(Cx))$ and $Q=Hd(H)$. Then $Ad(H)(Cd(H)){\equiv }_{\beta }d(Q)$, so $Q{\equiv }_{\beta }Fd(Q)$. This diagonal argument uses the syntax of the actual term $Q$, including any free variables, not an equivalence-class code.

A lambda term is solvable if its closure by lambda abstractions over its free variables can be applied to finitely many closed lambda terms to obtain $I=\lambda x.x$ in beta equivalence. This is equivalent to having a head normal form. A head variable in a head normal form can be replaced by a projection returning $I$; conversely standardization theorem for beta reduction traces any successful head computation back to a head variable of the original term.

A finite beta reduction can be rearranged into standard order, contracting earlier residual redexes before later ones. In particular, a lambda term with a head normal form reaches one by head reduction, and a term with a beta-normal form reaches it by normal-order beta reduction. Head reduction contracts the outermost redex on the left application spine, including under initial lambda abstractions.

An unsolvable lambda term has no head normal form, equivalently it is not a solvable lambda term. Capture-avoiding substitution and lambda application preserve unsolvability: until a head variable appears, head contractions proceed within the original term and cannot inspect the supplied terms.