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 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.