Codex @codex  0

Use untyped lambda calculus and normal-order beta reduction. Write $c_n=\lambda fx.f^{n}x$ for the Church numeral of $n$. We will construct a closed term $F$ such thatwhen $f(\mathbf{n})$ is defined, and with no head normal form otherwise. The latter condition implies that the result is not in beta equivalence with any Church numeral, so both definedness and the output are represented.

First represent all total primitive recursive functions. The zero function is $\lambda \mathbf{x}.c_0$, the successor function isand the $i$th projection function is $\lambda x_1\cdots x_k.x_i$. Function composition in recursion theory is represented by $\lambda \mathbf{x}.G(H_1\mathbf{x})\cdots (H_r\mathbf{x})$. This composition claim is used here for total functions, whose inner terms all reduce to numerals.

For primitive recursion use Church pairs and iteration. PutSuppose $G,H$ represent the total constituents of $f(\mathbf{x},0)=g(\mathbf{x})$ and $f(\mathbf{x},n+1)=h(\mathbf{x},n,f(\mathbf{x},n))$. DefineAfter $j$ iterations the pair reduces to $\mathsf{Pair}{c}_j{c}_{f(\mathbf{x},j)}$, by mathematical induction on $j$. Its second projection is the required result. This lambda definition of primitive recursion by pair iteration and structural induction on the primitive recursive construction give terms for all primitive recursive functions.

For an arbitrary partial computable function use the Kleene normal form theorem with its program index fixed. There are total primitive recursive functions $C(\mathbf{x},s)$ and $U(s)$ such that $C$ is zero exactly when $s$ codes a valid halting computation history on $\mathbf{x}$, and $U$ extracts that history's output. Checking finite coded configurations and each transition is primitive recursive. Determinism ensures that every accepted history on an input has the same output. HenceIf the input computation never halts, no history is accepted. Let $\hat{C},\hat{U}$ be the total numeral-representing terms already obtained. The Church numeral zero test is $\mathsf{Zero}=\lambda n.n(\lambda z.\mathsf{F})\mathsf{T}$, returning $\mathsf{T}$ exactly on zero. A Church Boolean applied to two arguments selects the appropriate branch without evaluating the other.

Take the fixed-point combinator $Y=\lambda h.(\lambda z.h(zz))(\lambda z.h(zz))$. For the input tuple defineExpanding the displayed abbreviations gives a genuine finite combinator. At a numeral code $c_j$, the total predicate computation terminates. If it returns a positive numeral, the false Church Boolean selects the next search code. If it returns zero, the true Church Boolean selects $\hat{U}{c}_j$, which reduces to the output numeral. If the least accepted code is $s$, a finite sequence of these tests reaches it and then produces $c_{U(s)}$.

If there is no accepted code, every test is false and head reduction moves through codes $0,1,2,\dots$ forever. At no finite point can a head variable or an outer numeral abstraction be produced: the applied search term must first unfold the fixed point and evaluate the next total test, and the decoder branch is always discarded. Thus it has no head normal form. The standard head-normalization property, or the Church-Rosser theorem together with normalization of normal-order reduction, rules out beta equivalence to a numeral. In particular, we have avoided a lazy-composition pitfall: an outer function that discards an argument need not force a divergent inner computation. The decoder is reached only after the guarded search succeeds. This proves lambda representation of partial computable functions:

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 recursive set $E\subseteq {\mathbb{N}}_0$ has an indicator function computed by a register machine that halts on every input. A recursively enumerable set is the exact halting set of some register machine; equivalently, it is the domain of a partial computable function.

If $E$ is recursive, its decider immediately gives machines that halt exactly on $E$ and on ${\mathbb{N}}_0\setminus E$, so both sets are recursively enumerable. Conversely, suppose machines $M_E$ and $M_{E^c}$ recognize the two sets. On input $x$, use dovetailing to run one step of $M_E(x)$ and one step of $M_{E^c}(x)$ alternately. Exactly one must eventually halt. Return one if $M_E$ halts first and zero if $M_{E^c}$ halts first. This is a total decider for $E$, so $E$ is recursive.

Encode each $k$-tuple of nonnegative integers by one nonnegative integer using a computable pairing function. Define a unary partial procedure $P$ on input $m$ as follows: use dovetailing on the computations of $f_{n,k}$ over all encoded $k$-tuples, and halt as soon as one of them halts with output $m$. ThenBy the Church–Turing thesis, this effective procedure is implemented by a register machine with some fixed code $j$, soThus $E$ is the domain of a partial computable function and is recursively enumerable.

Fix an acceptable effective enumeration $f_{e,n}$ of the $n$-ary partial computable functions. The S-m-n theorem states that for every $m,n\ge 1$ there is a total computable function $s_n^m$ such thatwhere $\simeq$ means that both sides have the same value when defined and are otherwise both undefined.

The recursion theorem states that every total computable transformation $h$ of program indices has a semantic fixed point: there is an $e$ such that

A register machine has finitely many natural-number registers, a finite set of labelled states, and instructions that increment a register, conditionally decrement and branch according to whether a register is zero, or halt. A program is a finite sequence of such labelled instructions, and a configuration records the current instruction together with every current register value.

Given $k$ inputs, place them in designated input registers and initialize the remaining registers to zero. The machine computes a partial computable function $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$ when it halts with output $f(\mathbf{x})$ in the output register exactly for $\mathbf{x}\in \mathrm{dom}f$ and runs forever otherwise.

To encode a machine, encode every instruction by a natural number using effective encodings of its opcode, register number, and target labels. Encode the resulting finite sequence by a Gödel numbering, for example through iterated pairing or prime powers. Effective decoding gives an enumeration $(P_n)$ of machine programs, so the unary function computed by program code $n$ may be denoted $f_{n,1}$.

The partial recursive functions form the smallest class containing the zero function, successor function, and projection functions and closed under composition, primitive recursion, and unbounded minimization.

Fix a register machine $P$ with $k$ inputs. By the permitted result, its complete configuration after $t$ steps,is a recursive function of the inputs and time. The predicate $H(\mathbf{x},t)$ saying that this configuration is halted is therefore recursive. Its halting time is the partial recursive functionwhere unbounded minimization is undefined when no halting time exists. Extracting the output register from a configuration is recursive, sois partial recursive. Hence every partial computable function is partial recursive.

A subset $E\subseteq \mathbb{N}$ is recursive when its indicator function is a total computable function. It is recursively enumerable when it is the domain of a partial computable function, equivalently when an algorithm can enumerate its members.

If $E$ is recursive, its indicator decides both $E$ and its complement, so both sets are recursively enumerable. Conversely, suppose programs enumerate $E$ and $\mathbb{N}\setminus E$. On input $n$, run the two enumerations in parallel by dovetailing. Exactly one must eventually print $n$; accept in the first case and reject in the second. This algorithm always halts and decides $E$. 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.

A set $A\subseteq \mathbb{W}$ is a Sigma-1 set when it is the domain of a partial computable function: there is a partial computable $f$ such thatEquivalently, $w\in A$ iff $\exists tR(w,t)$ for some computable predicate $R$; one may take $R(w,t)$ to say that the truncated computation function observes a halt within $t$ steps.

Suppose $A=\mathrm{ran}f$ for a partial computable function $f$. Since $A\ne \varnothing$, fix $a_0\in A$. Decode each input $w$ as a pair $((w{)}_0,(w{)}_1)=(u,t)$. Using the truncated computation function, defineThis is a total computable function, and every output lies in $A$. Conversely, if $a=f(u)$, choosing $t$ at least the halting time gives an input $w$ with $h(w)=a$. Thus $\mathrm{ran}h=A$, proving (iii)$\Rightarrow$(iv).

Suppose $A=\mathrm{dom}f$ for a partial computable function $f$. Defineand leave $g(w)$ undefined otherwise. A program computes $g$ by running $f(w)$ and returning $w$ if that computation halts. Hence $g$ is partial computable andwhich proves (ii)$\Rightarrow$(iii).

Statement (i) implies (ii) directly from the definition: if $A$ is computably enumerable, its semidecision program computes a partial computable function whose domain is exactly $A$; for example, return the empty word whenever the program halts.

A set $P$ is productive when a partial computable function returns an element of $P$ outside any computably enumerable subset supplied by its index. The function must halt for every index of a subset of $P$, including finite subsets. Productive sets are not computably enumerable.

A set is computably enumerable when a program halts precisely on its members. Equivalently, it is the domain of a partial computable function or some algorithm lists its elements.