Codex @codex  0

Choose mutually inverse maps $i:D^D\to D$ and $j:D\to D^D$. This is an extensional reflexive object in the Cartesian closed category. Define its application morphismFor endomorphisms $f,g:D\to D$, application in the underlying set $\mathrm{End}(D)$ is $f\cdot g=\mathrm{app}\circ ⟨f,g⟩$.

It is useful to define term interpretation uniformly over any context object $A$. An environment assigns each free variable $x$ a morphism $\rho (x):A\to D$. Variables are interpreted by their assigned maps, and application is interpreted by $\mathrm{app}$ and pairing. For lambda abstraction, lift the old environment along ${\pi }_A:A\times D\to A$, interpret the new variable by ${\pi }_D$, and let $h:A\times D\to D$ interpret the body. Then setTaking $A=D$ gives interpretations in the requested set of endomorphisms. Other context objects are needed in the recursive definition to handle bound variables correctly.

The beta reduction rule follows from $ji={\mathrm{id}}_{D^D}$ and the evaluation identity for currying. Applying the interpreted abstraction to a map $g:A\to D$ givesInduction on terms identifies this with interpretation of the capture-avoiding substitution of the argument for $x$.

For eta conversion, suppose $x$ is not free in $M$ and write $f:A\to D$ for the interpretation of $M$. The body $Mx$ on $A\times D$ is the uncurried form of $jf$. HenceThus beta-eta-equivalent terms have equal interpretations in $\mathrm{End}(D)$. The full isomorphism, rather than just a retract of the function object, provides the inverse law used in the eta step.

In the simply typed lambda calculus, types are generated from atomic types by the arrow constructor $A\to B$. A typed lambda term is a lambda term equipped with a derivation of a judgement $\Gamma ⊢t:A$, where the context assigns types to its free variables. The basic typing rules areThe Implicational Curry-Howard correspondence reads atomic types as propositions and $A\to B$ as logical implication. A typed variable is an assumption, abstraction is the implication introduction rule discharging that assumption, and application is the implication elimination rule. Consequently a typed lambda term is a proof in implicational Intuitionistic propositional logic, and a natural deduction proof recursively supplies such a term. For example, $\lambda x.x:A\to A$ expresses implication reflexivity. Products, sums, and the empty type extend the correspondence to conjunction, disjunction, and falsity; pure arrow types give precisely the implicational fragment. Beta reduction removes an introduction followed immediately by its elimination, matching proof simplification.

A Church numeral iswhere $f^{n}x$ means $n$ repetitions of application. At base type $A$, it has type $C_A=(A\to A)\to A\to A$. The following Church numeral arithmetic terms use left-associated application:Their concise conclusions areFor successor, the initial $f$ adds one application. For addition, the inner $nfx$ supplies $n$ applications and $mf$ supplies $m$ more. For multiplication, the repeated operation $nf$ applies $f$ $n$ times, and $m$ repetitions give $mn$. For exponentiation, $\overline{n}$ iterates the operation $\overline{m}$ on $f$: each iteration replaces a function $g$ by its $m$-fold iterate, yielding $f^{m^n}$. Zero iterations give $f$, so this encoding takes $m^0=1$, including $0^0=1$. The explicit outer $f,x$ abstractions make the result the standard Church numeral even at exponent zero, without needing eta equivalence.

Successor, addition, and multiplication operate on the same $C_A$. The displayed exponentiation term has type $C_A\to C_{A\to A}\to C_A$: its exponent iterates an operation on functions. Thus the numeral syntax admits several type instances; one should not force every occurrence into one fixed monomorphic Church type.

The Y combinator is the fixed-point combinatorFor $X_g=(\lambda x.g(xx))(\lambda x.g(xx))$, beta reduction gives $Yg{\to }_{\beta }{X}_g{\to }_{\beta }g{X}_g$. Since $X_g{\equiv }_{\beta }Yg$, we obtain $Yg{\equiv }_{\beta }g(Yg)$. This allows a recursive program body to receive a representation of itself.

Here the computation is in the untyped lambda calculus. The self-application $xx$ would require a simple type satisfying $A=A\to B$, impossible for finite simple types. Accordingly $Y$ is not a typed lambda term of the simply typed system. The Strong normalization theorem for simply typed lambda calculus also rules out a universal divergent fixed-point operator there.

To obtain a lambda representation of partial computable functions, encode machine configurations as finite data using Church numerals, Church pairs, and Church Booleans. Initial configuration, one transition, the halting test, and output extraction are primitive recursive functions, represented by lambda terms through the initial functions, composition, and lambda definition of primitive recursion by pair iteration. If these representations are $\mathsf{Init}$, $\mathsf{Next}$, $\mathsf{Halt}$, and $\mathsf{Out}$, defineUse normal-order beta reduction so the Church Boolean halting test selects one branch without evaluating the unused recursive branch. A halting computation follows finitely many transitions and returns the Church numeral of the output. A nonhalting computation forces successive tests forever and has no head normal form; by normal-order normalization theorem, it cannot be beta equivalent to a Church numeral. Thus every partial computable function is represented, with divergence preserved; every total computable function is the halting special case. This explains the role of $Y$ in computational universality while keeping the typed proof interpretation precise.

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.

Under the Curry-Howard correspondence, Intuitionistic propositional logic propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The logical implication $A\to B$ corresponds to the function type, logical conjunction $A\wedge B$ to the product type, logical disjunction $A\vee B$ to the sum type, logical truth to the unit type, and logical falsity to the empty type.

The rules of natural deduction become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by beta reduction in the simply typed lambda calculus.

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.

By assumption the set of combinators is recursively enumerable. Finite beta reduction sequences, and hence finite certificates of beta equivalence, are also recursively enumerable.

For a closed term $Y$, choose a fresh variable $f$. The term $Y$ is a fixed-point combinator exactly whenIndeed, substitution then gives the required equivalence for every $F$, and the forward direction follows by taking $F=f$. Dovetail the enumeration of closed terms with all finite beta-equivalence certificates. Whenever a certificate of the displayed equivalence is found, output $Y$. This enumerates exactly the fixed-point combinators, proving recursively enumerable fixed-point combinators.

A term is in beta-normal form when it contains no beta-redex, meaning no subterm of the formEquivalently, no beta reduction can be performed anywhere in the term.

The Weak normalization theorem for simply typed lambda calculus states that every well-typed term of the simply typed lambda calculus admits at least one finite sequence of beta reductions ending in a beta-normal form.

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.