constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
basic constructions:
strong axioms
further
A partial recursive function (often “computable function”, but see there for disambiguation) is a partial function of natural numbers which can be defined by an algorithm or computer program (e.g., a Turing machine), taking finitely many natural numbers as inputs, and which on input may run forever, but otherwise eventually halts and returns a natural number as output.
This idea as described is vague until it is circumscribed by a specific notion of computer program (Turing machines, register machines, abaci, etc.). There is a standard article of faith called the “Church-Turing thesis”, identifying functions on natural numbers that are algorithmically computable with those that are computable using a Turing machine (or some variant class of machines that is Turing-complete).
A purely mathematical definition of the intended class of functions is given below.
A partial recursive function is a partial function from to (where is the set of natural numbers and is finite) that belongs to the smallest class of partial functions that
includes all constant functions ;
includes all projection maps , ;
includes the successor function ;
is closed under composition: if and belong to , then so does ;
is closed under primitive recursion: if and belong to , then the function defined recursively by the equations (for and )
also belongs to ;
is closed under minimization: given any total function belonging to , the partial function , defined by iff and whenever , also belongs to .
A primitive recursive function is a function that belongs to the smallest class of functions of the form that contains constants, projection maps, the successor map, is closed under composition, and is closed under primitive recursion.
Clearly the primitive recursive functions are a subclass of partial recursive functions. Notice that primitive recursive functions are not merely partial functions, but actual (total) functions.
Both the class of partial recursive functions and the class of primitive recursive functions yield Lawvere theories and , where a morphism of the Lawvere theory is a function belonging to the class. It is straightforward to check that in either case, the generating object of the Lawvere theory (or if you prefer) is a parametrized NNO in that category: this is the essence of primitive recursion.
A recursive relation (or what is more usual nowadays, a computable relation) is a subset of whose characteristic function is recursive. Similarly, a primitive recursive relation is a relation whose characteristic function is primitive recursive.
We may build up a stock of functions and relations that are primitive recursive as follows. (All closure properties mentioned will clearly also apply to partial recursive functions and relations.)
Addition, multiplication, and exponentiation on . The factorial function is primitive recursive. Binomial coefficients.
The predecessor function , defined by the recursion , .
Truncated subtraction, where if , else , is primitive recursive. It is defined by the recursion , .
The distance function . The function ; this is the characteristic function of the unary relation or predicate “equals zero”. So “equals zero” is a computable relation. So is “doesn’t equal zero”, since this has characteristic function .
Therefore the equality relation is a primitive recursive relation. So is , being the relation “ doesn’t equal zero”. If is a (primitive) recursive function, then its graph defined by the relation is a (primitive) recursive relation.
(Boolean combinations) Similarly, if is a primitive recursive relation (so that its characteristic function is primitive recursive), then so is its negation , since . If , are primitive recursive relations, so is , since . Hence Boolean combinations of primitive recursive relations are primitive recursive.
If and are primitive recursive, so is
and similarly with the sum replaced by a product. It follows that primitive recursive predicates are closed under bounded quantification; e.g., if is a primitive recursive predicate and is a primitive recursive function, then the predicate defined by
is primitive recursive since .
(Bounded least choice operator) If is a primitive recursive relation and is a primitive recursive function, then the function defined to be “the least such that if such exists, else ” is primitive recursive. Indeed,
(Pairing and unpairing) There is an isomorphism in the Lawvere theory , i.e., there is a primitive recursive function with a primitive recursive inverse . For example, take to be the function
Its inverse takes to the pair
where is the least element less than such that . By the aforementioned properties, this is manifestly primitive recursive.
As a consequence of this last property, there exist primitive recursive isomorphisms between and for any . Since partial/primitive recursive functions are closed under composition, it is sufficient (and sometimes convenient) to consider only partial/primitive recursive functions on itself. (The exception is the case , but this is trivial, since every partial function is recursive.)
To show that in the category of primitive recursive functions, it is not enough just to exhibit a primitive recursive bijection , because it is not true that every primitive recursive bijection possesses a primitive recursive inverse. In other words, it is not true that the forgetful functor (see Remark ) reflects isomorphisms. See Example below.
Similarly, it is not always true that if a graph of a function is a primitive recursive relation, then the function itself is primitive recursive. (For example, the graph of the Ackermann function, discussed below, is a primitive recursive relation.) However, we do have a sample theorem as follows.
If a graph of a function is a primitive recursive relation, and if for some primitive recursive , then is itself primitive recursive.
The proof can be roughly expressed as follows: if is the functional computable relation, then let be the least such that . The bounded least choice property shows that is primitive recursive.
The point hovering in the background is that there are some computable functions which grow faster (in fact, much much much faster) than any primitive recursive function. This underscores the important role of the minimization axiom for partial recursive functions, which allows unboundedly large searches to take place. Indeed, we have the following crucial fact:
If is a graph of a function and is a recursive relation, then is a (total) recursive function. (The converse holds by one of the properties listed above.)
According to the minimization axiom in Definition , given that is a recursive function, the function that takes to the least such that is also recursive. But this function is simply . This completes the proof.
The inverse of a recursive bijection is also recursive.
The graph of is a recursive relation, and so is the opposite graph, which is the graph of the function . Apply the preceding theorem.
Before passing on to general recursive functions, it is good to have some idea of the scope of primitive recursive functions. Some examples:
For each , we define a function by
;
where denotes the composition of copies of . The Ackermann function is defined by .
(The function is named after Wilhelm Ackermann. There are several variations of this function around, and one common version actually puts and .)
We show that while each is primitive recursive, the function grows faster than any primitive recursive function on , hence is not itself primitive recursive. It does however belong to the class of partial recursive functions.
By property 1 above, is primitive recursive. Supposing that is primitive recursive, is also primitive recursive because it satisfies the recursion , .
By induction one may easily show for all and for all . We have for all . The function gives powers of , the function gives tetrations (iterated exponentials stacked high) of , the function gives iterated tetrations, and so on.
Some routine inductions establish the following facts:
If is primitive recursive, then there exists such that for all . (We say is dominated by , for short.)
In the case where is constant with value , take . For the successor, use . For each projection , again use :
Now proceed by induction on the construction of primitive recursive functions. Given that is dominated by and are dominated by , we calculate that is dominated by :
And given that is dominated by and is dominated by , if we define by recursion by and , we calculate that is dominated by , in two steps. First we claim
Indeed, this is true by assumption for . And then
which justifies the claim. Finally, we have
so that is dominated by . This completes the proof.
The Ackermann function is not primitive recursive.
If were recursive, then so would be the function . In that case, is dominated by for some . We then arrive at the contradiction
The graph of the Ackermann function is a primitive recursive relation.
The rough idea is to let bound the search for solutions to . For we have where . We have . Starting with , iterate this procedure so that
with each less than . (Explicitly, the iteration is .)
Thus, after disposing of some trivial low number cases, WLOG we may take , where the ternary predicate
is equivalent to
where the quantifications are manifestly bounded by . This shows that the ternary predicate is primitive recursive.
From this it follows that the binary relation is also primitive recursive, as claimed.
Combining this result with Theorem , we have
The Ackermann function is recursive.
Here we exhibit a primitive recursive bijection whose inverse is not primitive recursive. The graph of the Ackermann function is primitive recursive binary predicate, and the image is a primitive recursive unary predicate, because the existential quantifier is a bounded quantifier applied to a primitive recursive relation:
Observe that both and its complement in are infinite.
For any infinite set , let be the function taking to the element of (with respect to the usual order ). For example, . Now define a function by
Then and the graph of is primitive recursive, so by Theorem , is a primitive recursive function. It is a bijection by construction. But is not primitive recursive, because , and is not primitive recursive.
type I computability | type II computability | |
---|---|---|
typical domain | natural numbers | Baire space of infinite sequences |
computable functions | partial recursive function | computable function (analysis) |
type of computable mathematics | recursive mathematics | computable analysis, Type Two Theory of Effectivity |
type of realizability | number realizability | function realizability |
partial combinatory algebra | Kleene's first partial combinatory algebra | Kleene's second partial combinatory algebra |
A standard textbook in recursive functions is
Quite a bit of the arrangement and proofs above were taken from clear and useful lecture notes of Stephen Simpson,
Of course, there is always good old Wikipedia:
Last revised on May 9, 2022 at 20:42:36. See the history of this page for a list of all contributions to it.