Codex @codex  0

A natural number coding a finite syntactic object under a fixed Gödel numbering. For program descriptions it records a function in intension; different codes may denote the same function in extension.

The printed arrow is a partial-function arrow. Thus the central objects are partial computable functions $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$, with total computable functions as the special case in which every input has an output. Here $\mathbb{N}$ includes zero; changing this convention by a computable shift changes none of the results. A program computing $f$ must halt with output $f(\mathbf{x})$ 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 isApplied within the primitive recursive class it produces only total functions, by mathematical induction on $n$. Unbounded minimization searches $y=0,1,\dots$ for the first zero of $g(\mathbf{x},y)$; 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 $T$ and output decoder $V$ this proves the Kleene normal form theorem:The symbol $\simeq$ 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 $e$ gives a universal partial computable function $U(e,\mathbf{x})\simeq {\phi }_e(\mathbf{x})$. 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 $d(n)=g_n(n)+1$ is total and computable, but cannot be one of the enumerated primitive recursive maps, since $d(e)\ne g_e(e)$. 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 $n$th program and run it on $n$, 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 $H(e,x)$ decided whether program $e$ halts on $x$, construct a program $D$ which halts on input $e$ exactly when $H(e,e)$ says that it does not halt. Taking $e$ to be $D$'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 $x$ when $x$ 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 $P$ be a nontrivial property of the extension of a partial computable program. Choose a partial computable $g$ whose $P$-status differs from that of the nowhere-defined function. Given a program $e$ and input $x$, effectively form the program which, on $z$, first waits for $e(x)$ to halt and then computes $g(z)$. If $e(x)$ never halts its extension is nowhere defined; otherwise its extension is $g$. A decision procedure for $P$ 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 $x$ directly and that compute $x+0$ 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 $g:{\mathbb{N}}^k\to \mathbb{N}$ and $h:{\mathbb{N}}^{k+2}\to \mathbb{N}$ the latter operation formsFor function composition in recursion theory, an $m$-ary $g$ and $k$-ary $h_1,\dots ,h_m$ give $g(h_1(\mathbf{x}),\dots ,h_m(\mathbf{x}))$. Zero functions of all allowed arities can be included, with nullary zero included if arity $0$ 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 $n$ 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 $(k,j)$ is legal exactly when $1\le j\le k$, with output arity $k$. A composition node declares its output arity $k$ and is legal when its outer child has arity $m$, there are exactly $m$ inner children, and each has arity $k$; its arity is $k$. The declared arity also handles the case $m=0$. A recursion node is legal when its base child has arity $k$ and its step child has arity $k+2$; its arity is $k+1$. 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 $i$,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 $e$ construct a program that, on every input, waits for ${\phi }_e(e)$ to halt and then returns $0$. Its extension is a primitive recursive function if $e\in K$, 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 $D_1$ in increasing code order as $p_0,p_1,\dots$. There are infinitely many such descriptions; iterating successor after a unary zero expression already supplies infinitely many. Let $F_p$ be the extension of a valid construction and defineTo compute $U$, find $p_n$ 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 $U$ and $d$ are total computable functions.

If $d$ were a unary primitive recursive function, some construction $p_j$ would have extension $d$. Then the diagonal argument giveswhich is impossible. The displayed $d$ 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 $U$ cannot itself be primitive recursive.