Bounded halting predicate Created 2026-10-06 Updated 2026-10-07
For a fixed effective machine coding, the predicate that program on input halts within steps is primitive recursive. Code finite configurations, iterate a total single-step function by primitive recursion, and test for the halt state. This supplies a bounded simulation even though the unrestricted halting problem is undecidable.
Bounded minimization 2026-10-06
Search over the finite interval for the least witness to a primitive recursive predicate, with an explicitly chosen default if there is none. The result is a primitive recursive function, by scanning this finite interval using primitive recursion. This differs from unbounded minimization, which may fail to terminate.
Church pair 2026-10-05
With the Church Booleans and , encode a pair by
Then and the second projection similarly returns . Pairing an iteration counter with a computed value implements primitive recursion using only Church numeral iteration.
Finite witness array coding Created 2026-10-06 Updated 2026-10-07
In a primitive recursion, an existential representation of the step function may need a different witness tuple at every time. Code each coordinate of the finite witness array by a separate beta-function code pair. All row witnesses then have bounded remainder quantifiers under the bounded time quantifier, while the finitely many code pairs remain in the outer unrestricted existential block.
A partial computable function is the function computed by a finite program, with an undefined value when its computation never terminates. A total computable function terminates on every input. Fix an effective enumeration of the partial computable functions, with a universal partial computable function . Composition, primitive recursion and unbounded minimization give a machine-independent description of this class. Unbounded minimization is allowed to diverge. The S-m-n theorem permits parameters in a program to be specialized effectively: an algorithm described uniformly in has an index obtained computably from .
The halting set is computably enumerable: simulate all computations in parallel and enumerate each index whose diagonal computation terminates. It is not a computable set. Otherwise the program which terminates exactly when the proposed decision procedure says its own diagonal computation does not terminate gives a contradiction. There is also no effective enumeration consisting exactly of all total computable functions: from such an enumeration the total computable function differs from every listed function. Thus the effective enumeration of partial programs cannot be replaced by a decidable catalogue of total ones.
For the Rice theorem, let be a nontrivial property of partial computable functions, depending on the computed function rather than the program text. First suppose the nowhere-defined function is not in , and choose a program computing some . Uniformly in , define a program which, on input , first waits for to terminate and then runs the computation of . The S-m-n theorem gives a computable index map , and
Consequently a decision procedure for membership in would decide the halting set. If the nowhere-defined function belongs to , apply the same argument to its complement. Every nontrivial extensional property of partial computable functions has an undecidable index set. Syntactic properties of program descriptions are outside this assertion, and the theorem concerns unrestricted program indices, not merely an assumed list of terminating programs.
Here is an explicit Jockusch triple coloring computing the halting set. Choose computable increasing finite stages with union . For , put
This is a computable colouring. An infinite monochromatic set cannot have color : fix its first element and choose two later elements beyond the stage at which stabilizes. Their triple has color .
Suppose is infinite and homogeneous of color . To decide whether using , find with , and then with . For every above , homogeneity gives . Such are unbounded, so . Testing therefore decides . Hence every homogeneous set computes the halting set, and there is no infinite recursive monochromatic set. The infinity qualification is essential: finite homogeneous sets are recursive.
A recursive function is a total computable function: an algorithm halts on every input and returns the specified value. Equivalently it is an everywhere-defined member of the partial recursive functions, obtained from the initial zero, successor and projection functions by composition, primitive recursion and unbounded minimization. In minimization , the sequential search must find a zero after all earlier tests have been defined; otherwise the result is undefined. The Church–Turing thesis allows the algorithmic formulation here.
A recursively enumerable set is the domain of a partial computable function. Thus an algorithm halts and accepts exactly on members of , and may run forever on nonmembers. Equivalently an algorithm lists exactly its elements, allowing repetition and allowing an empty output for the empty set. To pass from a listing to a membership semidecision, wait for the input to appear. To pass back, use dovetailing on all inputs and list each whose recognizing computation halts. This differs from a recursive set, whose zero-one characteristic function is total recursive and decides both membership and nonmembership.
The primitive recursive functions are the smallest collection containing zero functions, successor , and coordinate projections, and closed under composition and primitive recursion. The recursion scheme forms from already constructed functions by
Constants follow by composing successor with zero. Define addition, multiplication and exponentiation successively by
At each stage the initial and step functions are compositions of primitive recursive functions already available. Induction on gives , , and , with the recursive convention . Composition with the second projection now gives
A partial computable function may return a natural-number output or diverge. One concrete definition uses finite deterministic Turing machines; code the finite transition table by an integer . Every single transition and every bounded simulation is computable, and the universal simulation gives a universal partial computable function
The symbol means equal outputs when defined and simultaneous divergence otherwise. A total computable function is a partial computable function defined on every input. Different program codes may compute the same partial function; this distinction between syntax and computed behavior is crucial.
The equivalent recursive description starts with zero, successor and projections and closes under composition and primitive recursion, giving the primitive recursive functions. Add unbounded minimization: search for the first at which a predicate returns zero, requiring every preceding tested computation to have converged. This gives the partial recursive functions. To see the connection with machines, encode finite configurations and histories. Checking a proposed halting history is a primitive recursive predicate , and a primitive recursive function extracts its output. Thus a machine computation has the normal form . Conversely a machine can implement composition, primitive recursion and this successive search. This proves equivalence of the formal definitions. The Church–Turing thesis identifying them with informal effective calculability is a thesis, not an additional formal theorem used in the proof.
A computably enumerable set is one enumerated by a program, equivalently the domain of a partial computable function. For the forward implication wait until the given input is enumerated; for the reverse implication run all input computations by dovetailing, outputting those that halt. A set is decidable if its characteristic function is total computable. It is decidable exactly when both it and its complement are computably enumerable: dovetail their enumerators and stop when one lists the input.
The S-m-n theorem supplies effective specialization of parameters. Given a code for a program on , compile the constant into a wrapper that writes it and then calls that program. The wrapper's transition table is computably produced from the original table and , yielding a total computable function with . This elementary code-construction proof is all the specialization machinery needed below.
The diagonal halting problem is computably enumerable by universal simulation but not decidable. If a total decider existed, the program that halts on precisely when would have an index . Evaluating it at gives exactly when , a contradiction.
For Rice theorem, let be a nontrivial collection of partial computable functions, and let its index set be . Membership must depend only on the computed function, not on its code. Let be the nowhere-defined function. First suppose , and choose a computable partial function with a fixed program. Uniformly from , produce the following program on input : first simulate ; if it halts, then simulate and return that output. Its index is total computable by specialization, and
Therefore iff , so a decider for would decide . If instead , apply the same argument to the nontrivial complement collection, whose index set would also be decidable if were. We conclude
For computably enumerable languages, use the same waiting program before beginning a fixed enumeration, taking the empty language as the bottom object. Properties such as having finite domain, computing a total function or recognizing a particular nontrivial language are therefore undecidable. Purely syntactic properties such as the parity of the code are excluded: they are not extensional. Rice's conclusion is undecidability, not that every such index set must fail to be computably enumerable.
The arrow in the original PDF permits partial functions. A partial computable function is computed by a finite program which halts with the specified value on every input in its domain and diverges on inputs outside the domain. A total computable function is the special case with full domain. Coding finite tuples by a primitive recursive pairing function identifies the different finite arities effectively, without identifying total and partial computability.
One precise machine model is a Turing machine. Its finite transition rules and configurations admit effective numerical coding. Bounded simulation is primitive recursive, and unbounded execution gives the partial result. Equivalently, start from zero, successor and projections and close under composition, primitive recursion and unbounded minimization. The Kleene normal form theorem makes the equivalence concrete:
where is a primitive recursive predicate checking a coded halting computation and reads its output. If no computation exists, the minimum and hence the value are undefined. Checking a finite history is effective because every consecutive configuration must obey one of the finitely many transition rules.
The universal partial computable function evaluates the program indexed by on an input. The S-m-n theorem says that fixing finitely many input parameters can be done by a total computable operation on program Gödel numbers: a new program stores those parameters and calls the original universal evaluator. These facts explain both universal simulation and uniform reductions. A set is computably enumerable when it is the domain of a partial computable function, equivalently the range of an effective enumeration. It is recursive when its characteristic function is total computable. A set is recursive precisely when it and its complement are computably enumerable: dovetail the two enumerations to decide each input.
The diagonal halting problem is computably enumerable but not recursive. A total decider would yield a program which, on , diverges if the decider says and halts otherwise. Applying this program to its own index gives a contradiction. There is likewise no total computable universal listing of all total computable functions: the diagonal function would be total and absent from the listing.
Here is a full proof of the Rice theorem. Let be a nonempty proper class of partial computable functions whose property depends only on the function, not its program. First suppose the everywhere-undefined function is not in , and choose a program for a function . Given an index , construct uniformly a program which on first waits for to halt and, only then, simulates . The S-m-n theorem gives a total computable index map . If , then ; if , then . Thus
A decision procedure for the property would decide , impossible. If , apply the same argument to its nontrivial complement. Every nontrivial extensional property of partial computable functions has an undecidable index set. Totality, having finite domain, and taking a particular value somewhere are examples. A syntactic property such as program length is not covered; nor does the theorem say that no individual program's behaviour can be established.
Self-reference can also be made effective. For a total computable index transformation , let be an index for the program which first computes and then runs the program with that resulting index on its own input. The S-m-n theorem makes total computable. Choose an index for the total function , and put . Then
This proves the recursion theorem: every effective transformation of programs has a fixed point at the level of the function computed, though not necessarily at the level of its numerical code.
Finally, consider the Jockusch triple coloring computing the halting set. Fix computable finite approximations with union . For , define
This is a total recursive two-coloring because both stages are finite computations. Suppose is infinite and homogeneous. Its color cannot be one: fix , wait until every enumeration below has stabilized, and choose later from beyond that stage. Their color is zero.
If has color zero, it computes . On input , use to find and in . For arbitrarily large with , homogeneity gives . Taking stages sufficiently large to reach the final finite approximation gives . Consequently membership of in is decided by the finite stage . A recursive would therefore make recursive, a contradiction. There is a recursive partition of triples with no infinite recursive homogeneous set. This is the nontrivial finite-color meaning of the partition of an infinite domain; if “infinite partition” meant infinitely many colors, the coloring by the least member would already give a trivial example. Ramsey's theorem still guarantees infinite homogeneous sets for the displayed two-coloring, but every such set is computationally nontrivial.
The printed arrow is a partial-function arrow. Thus the central objects are partial computable functions , with total computable functions as the special case in which every input has an output. Here includes zero; changing this convention by a computable shift changes none of the results. A program computing must halt with output exactly on its domain, and run forever elsewhere. A finite program is a function in intension, whereas its possibly partial input-output map is a function in extension; many programs have the same extension.
A precise machine model is a register machine with finitely many instructions to increment a register, decrement it conditionally, jump, and halt. Registers hold natural numbers. A Turing machine instead uses a finite transition table, a finite alphabet and an unbounded tape. These models simulate one another: encode the finite nonblank tape, state and head position as numbers for the register simulation; conversely represent each register by a finite tape block and implement its increment and decrement by finite scans. Tuple inputs can be encoded by a primitive recursive pairing function. The equivalence of these formal models is a mathematical result. Their identification with every informal effective procedure is the Church–Turing thesis, rather than an additional mathematical theorem about an already formal notion.
There is also an algebraic description. Begin with zero, successor and projections, close under composition of partial functions and primitive recursion, and then under unbounded minimization. The primitive recursion scheme is
Applied within the primitive recursive class it produces only total functions, by mathematical induction on . Unbounded minimization searches for the first zero of ; its output is defined only if that search reaches such a zero with every preceding necessary computation defined. Composition is likewise strict about the intermediate values it requires. These schemes compile into machine programs using finite subroutines, loops and an unbounded search loop.
For the converse, encode a machine's finite configurations and finite computation histories using Gödel numbering. Testing that a history starts with the specified input, that every adjacent pair follows the transition table, and that its final configuration halts is primitive recursive: all the tests are bounded by the finite code. Extracting the final output is primitive recursive too. For a suitable checking predicate and output decoder this proves the Kleene normal form theorem:
The symbol means equality of values and of definedness. A halting computation has a passing history code and every passing history has its actual output; a nonhalting computation has none. This proves that the partial recursive and machine-computable functions coincide, including their domains of divergence.
Finite programs can be effectively listed. Simulating the program with index gives a universal partial computable function . Fixing some inputs is effective syntactically: prepend instructions writing those constants and then call the original program. This proves the S-m-n theorem in this machine presentation. In particular, reductions that construct a program from numerical parameters really do produce its index effectively.
The primitive recursive functions are a proper subclass of the total computable functions. Enumerate all valid unary primitive recursive descriptions, interpreting invalid descriptions as zero. Evaluating any fixed valid description terminates by structural induction. Thus the diagonal map is total and computable, but cannot be one of the enumerated primitive recursive maps, since . This is a total computable diagonal over primitive recursive syntax. The evaluator can terminate on every particular description without itself being primitive recursive.
In contrast, one cannot effectively enumerate exactly the programs for all total computable functions. If such an infinite enumeration were available, wait for its th program and run it on , then add one. Totality makes this another total computable function, while its diagonal disagrees with every listed function. Equivalently, there is no total computable universal evaluator listing precisely all total computable maps.
The halting problem is undecidable. If decided whether program halts on , construct a program which halts on input exactly when says that it does not halt. Taking to be 's own index gives a contradiction. The halting relation is nevertheless computably enumerable, since finite halting histories can be searched for.
More generally, a set is computably enumerable exactly when it is the domain of a partial computable function. From an enumeration, halt on when appears; in the other direction use dovetailing over all inputs of a partial program to enumerate its halting inputs. A set is a computable set exactly when both it and its complement are computably enumerable: dovetail the two searches and return the answer from the one that succeeds. Neither a semidecision procedure nor an unbounded search supplies a uniform negative answer.
Finally, the Rice theorem explains the scope of this obstruction. Let be a nontrivial property of the extension of a partial computable program. Choose a partial computable whose -status differs from that of the nowhere-defined function. Given a program and input , effectively form the program which, on , first waits for to halt and then computes . If never halts its extension is nowhere defined; otherwise its extension is . A decision procedure for would therefore decide the halting problem. Effective descriptions allow universal simulation and positive verification, but not a decision procedure for every semantic property or for termination.
A function in intension is a finite description of a computation, such as a program or a formal construction expression. A function in extension is the resulting input-output map, including its domain if it is partial. Different descriptions may have the same extension: the programs that return directly and that compute describe the same function. Finite descriptions have Gödel numbers; equality of the resulting partial computable functions is a separate semantic question.
The primitive recursive functions are the smallest class of numerical functions containing the zero functions, the successor function and all projection functions, and closed under function composition in recursion theory and primitive recursion. More explicitly, from and the latter operation forms
For function composition in recursion theory, an -ary and -ary give . Zero functions of all allowed arities can be included, with nullary zero included if arity is part of the coding convention. Every resulting function is total: the initial functions are total, function composition in recursion theory preserves totality, and mathematical induction on verifies totality of primitive recursion. Applying structural induction for primitive recursive functions then covers all construction expressions.
Use a fixed effective Gödel numbering of finite tagged construction trees with decidable decoding. A node is tagged as zero, successor, projection, composition, or recursion. The primitive recursive syntax and arity checking algorithm first checks that the input decodes as a finite tree, then works upwards from its leaves. A projection tag is legal exactly when , with output arity . A composition node declares its output arity and is legal when its outer child has arity , there are exactly inner children, and each has arity ; its arity is . The declared arity also handles the case . A recursion node is legal when its base child has arity and its step child has arity ; its arity is . Zero and successor tags have their declared arities. Ill-formed nodes are rejected. The process terminates because there are only finitely many nodes. Thus, for each fixed ,
This is a syntactic assertion about functions in intension. It does not assert that arbitrary machine indices computing primitive recursive functions form a decidable set. That extensional property is nontrivial, hence undecidable by Rice theorem. For an explicit reduction, given a program construct a program that, on every input, waits for to halt and then returns . Its extension is a primitive recursive function if , and otherwise is nowhere defined and so is not a primitive recursive function. A decision procedure for this latter semantic set would decide the diagonal halting set.
Enumerate the decidable syntax set in increasing code order as . There are infinitely many such descriptions; iterating successor after a unary zero expression already supplies infinitely many. Let be the extension of a valid construction and define
To compute , find by the syntax test and interpret its finite construction tree. Evaluate function composition in recursion theory by evaluating the children, and evaluate primitive recursion by the prescribed finite loop of length equal to its final input. Termination follows from the totality argument above, so and are total computable functions.
If were a unary primitive recursive function, some construction would have extension . Then the diagonal argument gives
which is impossible. The displayed is total and computable but not primitive recursive. Repetitions of extensions in the enumeration cause no problem: every possible extension is represented, which is all the diagonal argument needs. The same argument shows that the two-variable interpreter cannot itself be primitive recursive.
We prove closure under the defining schemes for primitive recursive functions, keeping all unbounded existential variables outside a bounded arithmetic formula. A bounded quantifier means or , where does not contain . All formulas are interpreted in the standard natural numbers.
First we need a finite sequence code using only the permitted language of ordered rings. Define the bounded arithmetic formula
For given , it specifies the unique remainder of modulo . In particular the quotient and remainder variables are bounded by arithmetic terms; division is not a new language symbol.
Every finite list can be coded by some pair . Choose larger than every list entry and divisible by every integer from to . The moduli are pairwise coprime. Indeed a prime dividing both cannot divide , but then divides ; since and is divisible by that integer, this is impossible. The Chinese remainder theorem gives with for every . Since , each holds. This is Gödel beta-function sequence coding. The external choice of a divisible proves that codes exist; factorial and exponentiation do not occur in the existential bounded representation of a primitive recursive function.
For the zero function, successor function and projections use , and . These formulas need no auxiliary variables. For function composition in recursion theory, suppose have representations with bounded arithmetic formulas . A bounded arithmetic formula for is
Treat every as an auxiliary variable in the outer existential block. The logical conjunction is true for some such variables exactly when is the desired output.
Now suppose
By structural induction for primitive recursive functions, assume and are bounded arithmetic formulas representing . We code the values with . For finite witness array coding, give each component of the step witness another code pair , so that the witness at step is the remainder specified by .
With these code pairs and as free auxiliary variables, take the following bounded arithmetic formula:
The displayed line breaks are only for readability: the bounded quantifiers on the last three lines bind the entire bracket. If , their empty block and logical conjunction are omitted. Expanding every occurrence of leaves only bounded quantifiers, logical conjunctions, the bounded arithmetic formulas already obtained, and the symbols .
If , take the actual finite computation values and select witnesses for the finitely many true instances of , together with witnesses for . The Gödel beta-function sequence coding provides and the finitely many . These make true. Conversely, suppose some code pairs and initial witnesses make true. The unique remainders of give values . The initial clause makes . Every step clause makes , since its coded witnesses satisfy the representing matrix for . Induction on gives , and the final remainder clause gives . This argument includes , when the step condition is empty.
Closure under the initial functions of recursion theory, composition and primitive recursion proves
Coding the step witnesses is essential: leaving an unrestricted existential witness block inside would not give the required syntactic form.
We use untyped lambda calculus and normal-order beta reduction. The Church numeral for is . A lambda term represents a partial function if on numeral inputs it has the correct numeral normal form exactly when the function is defined. We use a lambda simulation of a Turing machine; this also ensures that undefined computations do not accidentally produce an output through an ignored argument.
First all total primitive recursive functions are lambda-definable. The initial functions of recursion theory are represented by
Composition is obtained by substitution of representing terms. For primitive recursion use Church pairs:
If represent the total functions in and , define
After iterations the pair has components . Thus the Church numeral executes exactly the required recursion steps. Since these functions are total on numeral inputs, substitution for composition causes no undefined-argument issue.
Now fix a deterministic Turing machine computing the given partial computable function. Encode a configuration by its finite control state and two natural numbers for the tape portions on the two sides of the head, allowing blank bits beyond the finite nonblank tape. For the two-stack encoding of a Turing tape with a binary alphabet, let have the immediately-left cell as its low bit and have the current cell as its low bit. Reading and removing a bit use remainder and quotient by two. If the machine writes , the updates are
The new state is obtained from a finite transition table. These operations, the initial configuration, the halting test, and output decoding are total primitive recursive functions on configuration codes. For instance parity alternates by primitive recursion, and the quotient by two satisfies , . A fixed finite alphabet can be handled by the same stack construction in a larger base. Choose a standard delimited input and output convention, for example unary words in a finite tape alphabet with a distinct blank symbol. Initialization is primitive recursive. On a halting configuration the output is a finite word; decoding can be implemented by a bounded scan of the encoded tape, with a default output for malformed words. This is total primitive recursive and introduces no additional unbounded search. Use nested Church pairs to carry the three fields, and the preceding primitive recursive representations to obtain lambda terms .
Represent Church Booleans by and . A Church numeral zero test is . Use a numerical test equal to zero on halting configurations and one otherwise; applying this zero test gives the required Boolean halting test. With the fixed-point combinator
put
Normal-order reduction evaluates the halting test on the current configuration. If it is true, it selects the output branch without evaluating the recursive branch. Otherwise it advances the configuration and repeats. Induction on the number of machine steps shows that a computation halting with output makes reduce to .
If the machine never halts, the normal-order beta reduction repeatedly takes the recursive branch. Each individual configuration transition and test terminates, but there is always another required transition; hence the reduction never reaches a normal form. The normal-order normalization theorem says that a lambda term with a beta-normal form is normalized by normal-order beta reduction. Therefore in the nonhalting case there is no numeral normal form at all. We have proved
Confluence of beta reduction ensures uniqueness of the resulting numeral. This handles genuinely partial computations. Simply composing terms for partial subcomputations would need extra care, because lambda reduction can discard an unevaluated argument.
For (1)(a), a primitive recursive function is obtained by a finite construction from the zero function, successor function and projection functions, using function composition in recursion theory and primitive recursion. The recursion rule, with parameters , is
Here have already been constructed. All these functions are total on nonnegative integers: the initial functions are total, composition preserves totality, and ordinary mathematical induction proves totality of each recursion.
For (1)(b), use a shifted hyperoperation sequence, beginning with addition. Define
and, for each fixed , define
The first three members are therefore addition, multiplication and exponentiation:
The exponentiation convention includes , hence . The next member iterates exponentiation, with ; there is no need for an exceptional domain restriction at .
For (1)(c), is a primitive recursive function by its displayed recursion. If is a primitive recursive function, then
are primitive recursive functions, using constants, projection functions and function composition in recursion theory. Primitive recursion applied to gives . Mathematical induction on the fixed rank proves every member of the sequence is primitive recursive. This does not assert that the joint three-variable evaluator is a primitive recursive function.
For (2), as written, the answer is no: the empty set is semidecidable, whereas a total computable function from to always has a nonempty range. This is the only obstruction. To prove the stronger useful statement, suppose is a nonempty computably enumerable set and choose . Fix a Turing machine which halts exactly on the inputs in . Its bounded halting predicate
is primitive recursive: encode configurations arithmetically, iterate its total single-step operation times by primitive recursion, and check the halt state. A halted configuration is kept fixed. This is a bounded simulation, not unbounded waiting.
Fix a primitive recursive pairing function with primitive recursive inverse coordinate functions. For example, the Cantor pairing function has inverses obtained by bounded minimization. Define
The two coordinate functions, the bounded predicate, and the finite case distinction are primitive recursive functions, so is a primitive recursive function. Its values always lie in . Conversely, if , its computation halts within some finite , and . Thus
The range need not be a computable set; deciding whether a value occurs anywhere in this total enumeration is an unbounded search.
Represent a nonnegative integer by the Church numeral
A closed lambda term represents a partial computable function if, on inputs in its domain, 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 , the projection functions by , and the successor function by
For 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 represent the total functions defining a recursion, put
and
After iterations the Church pair contains the counter and the recursively computed value at , 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 , there are total primitive recursive functions such that
with undefined precisely when no such exists. The predicate checks codes of valid finite halting histories for the chosen program; extracts their common output. This expresses unbounded minimization of a total predicate, so no earlier undefined test can interfere with the search.
Let be the represented total functions. The Church numeral zero test and a fixed-point combinator are
Define the search lambda term
All displayed abbreviations expand to finite closed lambda terms; stands for the fixed finite tuple of input variables. Because , normal-order beta reduction tests . At the first successful test the Church Boolean selects , 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:
Use untyped lambda calculus and normal-order beta reduction. Write for the Church numeral of . We will construct a closed term such that
when 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 , the successor function is
and the th projection function is . Function composition in recursion theory is represented by . This composition claim is used here for total functions, whose inner terms all reduce to numerals.
For primitive recursion use Church pairs and iteration. Put
Suppose represent the total constituents of and . Define
After iterations the pair reduces to , by mathematical induction on . 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 and such that is zero exactly when codes a valid halting computation history on , and 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. Hence
If the input computation never halts, no history is accepted. Let be the total numeral-representing terms already obtained. The Church numeral zero test is , returning exactly on zero. A Church Boolean applied to two arguments selects the appropriate branch without evaluating the other.
Take the fixed-point combinator . For the input tuple define
Expanding the displayed abbreviations gives a genuine finite combinator. At a numeral code , 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 , which reduces to the output numeral. If the least accepted code is , a finite sequence of these tests reaches it and then produces .
If there is no accepted code, every test is false and head reduction moves through codes 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 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: is defined only when every inner value is defined and is defined on the resulting tuple. Likewise primitive recursion requires all preceding recursive values. The partial minimization is defined when such a 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 satisfying
On 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 . Church Booleans encode a conditional by , with and . Put
Iteration takes to for , proving that encodes the predecessor function and that correctly tests zero.
Use a fixed-point combinator and the strict sequencing operation
For any numeral , reduces to . If the first argument has no head normal form, neither does the whole expression. Thus composition is implemented by nesting 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 already represented by , take
The tuple notation abbreviates successive abstractions and applications. On numeral inputs, induction on 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, use
This 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 , stopping when a result is a Church numeral in beta-normal form. If , 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
Let be the successor function. Define by primitive recursion
Induction gives . Then define
by composition. Initial functions, composition, and primitive recursion produce primitive recursive functions, so and are partial recursive functions and are visibly defined for every . Both functions are total.
Fix a register machine with inputs. By the permitted result, its complete configuration after steps,
is a recursive function of the inputs and time. The predicate saying that this configuration is halted is therefore recursive. Its halting time is the partial recursive function
where unbounded minimization is undefined when no halting time exists. Extracting the output register from a configuration is recursive, so
is partial recursive. Hence every partial computable function is partial recursive.