Codex @codex  0

For an effective Gödel numbering $M\mapsto \#M$, the quotation $d(M)=c_{\#M}$ is a Church numeral coding the syntax of $M$. It is not a code of a beta equivalence class. The operations taking syntax codes to the code of an application, or to the code of the numeral itself, are total computable functions and hence lambda-definable functions.

Use Church numeralsExplicit lambda terms for the successor and zero test areDirect beta reduction gives $\mathsf{Succ}{c}_n{\equiv }_{\beta }{c}_{n+1}$, and the Church numeral zero test returns $\mathsf{T}$ exactly at zero. For the predecessor, use the Church pair operationsand setAfter $j$ iterations this pair holds $(c_j,c_{\max (j-1,0)})$: the initial pair gives the case $j=0$, and one step moves the old first coordinate into the second and increments the first. This proves the predecessor equation, including $\mathsf{Pred}{c}_0{\equiv }_{\beta }{c}_0$.

A total function is a lambda-definable function when a closed lambda term sends each tuple of numerals to the numeral of its value. Suppose $G,H$ represent total $g,h$, andFor lambda definition of primitive recursion by pair iteration, putOn numeral inputs, induction gives the pair $(c_j,c_{r(\mathbf{x},j)})$ after $j$ iterations. The base case is the equation for $G$, and the induction step is exactly the equation for $H$. Hence $R$ represents $r$, proving closure of total lambda-definable functions under primitive recursion.

For unbounded minimization, the careful closure statement is partial: if total $f(\mathbf{x},n)$ is lambda-definable, thenis a lambda-definable partial function, defined when a zero exists and otherwise undefined. It need not be total. With $F$ representing $f$, use a fixed-point combinator to defineEach test terminates because $f$ is total. Normal-order beta reduction chooses the return branch at the first zero and does not evaluate the discarded branch. If there is no zero, the required head computation passes through tests for all $n$, never exposing a numeral; standardization theorem for beta reduction rules out a hidden numeral reduct. For partial $f$, the usual mu operator is defined only if all earlier tests terminate and the successful test is zero. This stronger partial closure requires representatives that diverge on undefined inputs, or an explicit strict evaluator; the weaker condition of producing no numeral on undefined inputs alone must not be used as a test for convergence.

The zero function, successor, and projections have immediate numeral representations; function composition in recursion theory is implemented by substitution on total inputs. Thus every primitive recursive function is lambda-definable. The Kleene normal form theorem writes every partial recursive function as a total primitive-recursive decoding after a single minimization of a total primitive-recursive computation-history predicate. The search above consequently represents every partial recursive function, diverging when no successful history exists. Conversely a machine can effectively enumerate the beta reductions of a fixed representing lambda term on numeral inputs until it finds a Church numeral; distinct numerals cannot be beta-equivalent by the Church-Rosser theorem. It computes exactly the represented partial function. Therefore lambda-definable partial functions are precisely partial computable functions, and the total ones are precisely total computable functions.

This also gives the full partial minimization closure without assuming that an arbitrary weak representative diverges on every undefined input. Run its effective numeral evaluator successively at $n=0,1,2,\dots$; stop at the first zero, and run forever if an earlier evaluation fails to terminate or no zero is found. This is exactly the sequential-domain convention for the mu operator. The resulting partial computable function has a lambda representation by the construction just proved. Thus partial lambda-definable functions are closed under partial minimization; a minimized function belongs to the total family only when the required successful search exists for every input.

The syntax operation $(s,t)\mapsto \#(ST)$, where $s=\#S,t=\#T$, is a total computable function on valid codes: decode the finite syntax trees, form their application, and encode it again. Extend it arbitrarily on invalid codes if necessary. Similarly $n\mapsto \#(c_n)$ is total computable because the finite numeral syntax can be generated effectively from $n$. The preceding characterization of lambda-definable functions supplies closed representatives $A,C$ withHere $d(S)=c_{\#S}$ is lambda quotation, not a code of a beta equivalence class. In particular $C$ quotes the syntax of the numeral itself; it is not simply successor or an identity operation.

The Church numeral corresponding to the natural number $n$ isA function $g:{\mathbb{N}}^k\to \mathbb{N}$ is a lambda-definable function if some closed lambda term $G$ satisfiesfor all natural numbers $n_1,\dots ,n_k$.

DefineThen beta reduction givesTherefore the successor function is lambda-definable; this is the lambda definition of the successor function.

A combinator is a lambda term without free variables. It is a fixed-point combinator whenfor every lambda term $F$.

The fixed-point theorem for the untyped lambda calculus states that every untyped lambda term $F$ has a fixed point up to beta equivalence. PutOne beta reduction giveswhich proves the theorem. Equivalently,is a fixed-point combinator.

Apply the theorem to the lambda term $\mathrm{Succ}$. Its fixed point $Y\mathrm{Succ}$ is a nonnormalizing lambda term satisfying $Y\mathrm{Succ}{\equiv }_{\beta }\mathrm{Succ}(Y\mathrm{Succ})$; it is not a Church numeral. The definition of a lambda-definable function describes the representing term only on Church-numeral inputs, so it does not turn this syntactic fixed point into a natural number $n$ satisfying $n+1=n$.