is a co-recursively enumerable language, is not a recursively enumerable language, and is not a decidable language. The stipulated order on halting times includes .
First, failure has a finite witness. For valid machine descriptions,
Indeed, a strict inequality forces the first halting time to be finite. The second can be either a larger finite time or infinity. Whether the displayed condition holds for fixed is decidable by a finite simulation, including the initial configurations when .
Enumerate all pairs and perform these finite tests by dovetailing, accepting the complement of a set of on finding a witness. Equivalently, at stage , inspect all inputs of length at most through transitions. A genuine violation eventually appears; if there is no violation, the procedure never accepts. Malformed descriptions or differing input alphabets can be recognized and accepted as nonmembers immediately. Thus the complement is a recursively enumerable language, proving that is a co-recursively enumerable language.
For non-enumerability, use the standard result that the complement of a set of the halting problem
is not a recursively enumerable language. Given , effectively construct two Turing machines over the same fixed input alphabet. On every input , let ignore and simulate on the fixed word , halting precisely when that simulation halts. Let loop forever on every input.
If does not halt on , both halting times are infinity for every , so the pair belongs to . If halts on , the first halting time is finite while the second is infinity, so the pair does not belong to . Therefore
This is a many-one reduction from non-halting to the pointwise running-time domination problem. Were a recursively enumerable language, constructing the pair and running its recognizer would recognize non-halting, contradicting the stated result. Hence is not a recursively enumerable language. Since every decidable language is a recursively enumerable language, is also undecidable.
The halting problem asks whether program halts on input , given effective codes for both. Suppose a total decision algorithm returned one exactly when that computation halts. Construct a program which, on input , computes and then loops forever if the answer is one, but halts if it is zero. Let be the code of . If , the specification of makes it diverge, while if the same specification makes it halt. Both alternatives contradict correctness. Therefore the halting problem is . This is a diagonal argument, not merely the observation that individual simulations can run forever.
Let . Simulating the specified program semidecides membership, or dovetailing all simulations enumerates , so is a recursively enumerable set. The same diagonal program rules out a total decision algorithm for . Thus . Encoding a pair also gives an enumerable nonrecursive set of all halting program-input pairs.
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 algebraic characterization is the Boone-Higman theorem:
Here need not be finitely generated or finitely presented. We prove the equivalence using the Higman embedding theorem, Britton's lemma and the normal form theorem for a free product. The original characterization is Theorem I of An algebraic characterization of groups with soluble word problem.
First suppose the embeddings exist. Choose a word in representing some fixed , and fixed words in representing the finite generators of . Given a word in those generators, one search enumerates proofs that in the finite group presentation of . A second search enumerates all finite products of conjugates in of , and all proofs that any such product equals . All these searches are effective: a proof of equality is a finite product of conjugates of defining relators, checked in the free group, and dovetailing handles the countably many candidates.
If , simplicity gives , so is such a finite product with conjugators in , which are also elements of . The second search eventually succeeds. If , every such product is trivial, so it cannot equal , but the first search succeeds. Running the two searches in parallel thus decides the word problem for a group in . This is semidecision of nonidentity in simple subgroups; no enumeration of or word algorithm for is required. The choice of the fixed word for is an existence choice of a finite string, not an algorithm for discovering from an arbitrary presentation.
Conversely suppose the word problem for a group in is soluble. We construct a recursive simple envelope by cyclic HNN extensions, keeping all effectiveness requirements explicit. Start with , where has infinite order. Reduced free product words give a word algorithm for and an algorithm testing membership in and recovering its exponent. The original null words of are decidable and therefore enumerable, so has a recursive presentation of a group.
Inductively assume has an effectively enumerable generating set, a recursive presentation, a word algorithm, and an algorithm for membership and exponent in . Form . For each nonidentity word in , introduce distinct stable letters , and introduce another letter , with relations
Let be this multiple HNN extension of . A computable enumeration of all words of , filtered by its word algorithm, indexes the nonidentity used here. Repeated representatives of the same element cause no difficulty: their stable letters are simply distinct.
Every associated subgroup in these relations is infinite cyclic. For , the words and are cyclically reduced free product words with respectively two and four syllables; their nonzero th powers have lengths and . Therefore the reduced syllable length of an input bounds the finitely many possible exponents needed to decide membership in each subgroup and find the exponent. Membership in is immediate, and membership in is inherited from . This proves effective cyclic membership in a free product, including the crucial point that the order of is never needed.
By Britton's lemma, embeds in . To solve its word problem, repeatedly find a pinch in an HNN extension using these membership algorithms, transport the known exponent across its defining isomorphism, and remove two stable letters. With no pinch left, a word retaining stable letters is nontrivial and not in the base; otherwise the base word algorithm applies. The same reduction decides whether an input lies in : if stable letters remain it does not, and if none remain use the base cyclic-membership algorithm. This verifies the inductive effectiveness claims rather than asserting that HNN extensions automatically preserve decidable word problem. Only the finitely many stable letters in the input need inspection.
The union is nontrivial, since retains infinite order under every embedding, and has an effective countable recursive presentation: enumerate each stage's relators and dovetail the enumerations. We now prove simplicity. Let contain , and take a stage with . The commutator belongs to , so its displayed conjugation forces . Conversely, in the quotient by the normal closure of , the relation for forces ; then the relation for forces every nonidentity to be one. Thus the normal closure of contains each . All newly adjoined stable letters belong to a later , so this normal closure is all of . Hence , proving that is a simple group containing .
Finally apply the explicit two-generator HNN embedding from Question 3 to an effective countable list of generators of . Its same free-conjugate-basis argument works for every finite word, and its relations are recursively enumerable, so it embeds in a two-generated recursively presented group . The Higman embedding theorem embeds in a finitely presented group . Composing the inclusions gives , completing the proof of both directions.
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 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 recursive set 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 is recursive, its decider immediately gives machines that halt exactly on and on , so both sets are recursively enumerable. Conversely, suppose machines and recognize the two sets. On input , use dovetailing to run one step of and one step of alternately. Exactly one must eventually halt. Return one if halts first and zero if halts first. This is a total decider for , so is recursive.
Encode each -tuple of nonnegative integers by one nonnegative integer using a computable pairing function. Define a unary partial procedure on input as follows: use dovetailing on the computations of over all encoded -tuples, and halt as soon as one of them halts with output . Then
By the Church–Turing thesis, this effective procedure is implemented by a register machine with some fixed code , so
Thus is the domain of a partial computable function and is recursively enumerable.
A subset 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 is recursive, its indicator decides both and its complement, so both sets are recursively enumerable. Conversely, suppose programs enumerate and . On input , run the two enumerations in parallel by dovetailing. Exactly one must eventually print ; accept in the first case and reject in the second. This algorithm always halts and decides . Hence
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 , choose a fresh variable . The term is a fixed-point combinator exactly when
Indeed, substitution then gives the required equivalence for every , and the forward direction follows by taking . Dovetail the enumeration of closed terms with all finite beta-equivalence certificates. Whenever a certificate of the displayed equivalence is found, output . This enumerates exactly the fixed-point combinators, proving recursively enumerable fixed-point combinators.