Function in intension Created 2026-10-07 Updated 2026-10-14
A function in intension is a finite program or formal construction description. Its associated function in extension is the partial or total input-output map it denotes. A Gödel number records the description rather than identifying all descriptions with the same extension.
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.
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.