Proof of the fixed-point theorem

The proof uses a particular total computable function ${\displaystyle h}$, defined as follows. Given a natural number ${\displaystyle x}$, the function ${\displaystyle h}$ outputs the index of the partial computable function that performs the following computation:

Given an input ${\displaystyle y}$, first attempt to compute ${\displaystyle \varphi _{x}(x)}$. If that computation returns an output ${\displaystyle e}$, then compute ${\displaystyle \varphi _{e}(y)}$ and return its value, if any.

Thus, for all indices ${\displaystyle x}$ of partial computable functions, if ${\displaystyle \varphi _{x}(x)}$ is defined, then ${\displaystyle \varphi _{h(x)}\simeq \varphi _{\varphi _{x}(x)}}$. If ${\displaystyle \varphi _{x}(x)}$ is not defined, then ${\displaystyle \varphi _{h(x)}}$ is a function that is nowhere defined. The function ${\displaystyle h}$ can be constructed from the partial computable function ${\displaystyle g(x,y)}$ described above and the s-m-n theorem: for each ${\displaystyle x}$, ${\displaystyle h(x)}$ is the index of a program which computes the function ${\displaystyle y\mapsto g(x,y)}$.

To complete the proof, let ${\displaystyle F}$ be any total computable function, and construct ${\displaystyle h}$ as above. Let ${\displaystyle e}$ be an index of the composition ${\displaystyle F\circ h}$, which is a total computable function. Then ${\displaystyle \varphi _{h(e)}\simeq \varphi _{\varphi _{e}(e)}}$ by the definition of ${\displaystyle h}$. But, because ${\displaystyle e}$ is an index of ${\displaystyle F\circ h}$, ${\displaystyle \varphi _{e}(e)=(F\circ h)(e)}$, and thus ${\displaystyle \varphi _{\varphi _{e}(e)}\simeq \varphi _{F(h(e))}}$. By the transitivity of ${\displaystyle \simeq }$, this means ${\displaystyle \varphi _{h(e)}\simeq \varphi _{F(h(e))}}$. Hence ${\displaystyle \varphi _{n}\simeq \varphi _{F(n)}}$ for ${\displaystyle n=h(e)}$.

This proof is a construction of a partial recursive function which implements the Y combinator.

Fixed-point-free functions

A function ${\displaystyle F}$ such that ${\displaystyle \varphi _{e}\not \simeq \varphi _{F(e)}}$ for all ${\displaystyle e}$ is called fixed-point free. The fixed-point theorem shows that no total computable function is fixed-point free, but there are many non-computable fixed-point-free functions. Arslanov's completeness criterion states that the only recursively enumerable Turing degree that computes a fixed-point-free function is 0′, the degree of the halting problem.^[5]

Comparison to Rogers's theorem

Kleene's second recursion theorem and Rogers's theorem can both be proved, rather simply, from each other.^[6] However, a direct proof of Kleene's theorem^[7] does not make use of a universal program, which means that the theorem holds for certain subrecursive programming systems that do not have a universal program.

Application to quines

A classic example using the second recursion theorem is the function ${\displaystyle Q(x,y)=x}$. The corresponding index ${\displaystyle p}$ in this case yields a computable function that outputs its own index when applied to any value.^[8] When expressed as computer programs, such indices are known as quines.

The following example in Lisp illustrates how the ${\displaystyle p}$ in the corollary can be effectively produced from the function ${\displaystyle Q}$. The function s11 in the code is the function of that name produced by the S-m-n theorem.

Q can be changed to any two-argument function.

(setq Q '(lambda (x y) x))
(setq s11 '(lambda (f x) (list 'lambda '(y) (list f x 'y))))
(setq n (list 'lambda '(x y) (list Q (list s11 'x 'x) 'y)))
(setq p (eval (list s11 n n)))

The results of the following expressions should be the same. ${\displaystyle \varphi }$ p(nil)

(eval (list p nil))

Q(p, nil)

(eval (list Q p nil))

Application to elimination of recursion

Suppose that ${\displaystyle g}$ and ${\displaystyle h}$ are total computable functions that are used in a recursive definition for a function ${\displaystyle f}$:

${\displaystyle f(0,y)\simeq g(y),}$

${\displaystyle f(x+1,y)\simeq h(f(x,y),x,y),}$

The second recursion theorem can be used to show that such equations define a computable function, where the notion of computability does not have to allow, prima facie, for recursive definitions (for example, it may be defined by μ-recursion, or by Turing machines). This recursive definition can be converted into a computable function ${\displaystyle \varphi _{F}(e,x,y)}$ that assumes ${\displaystyle e}$ is an index to itself, to simulate recursion:

${\displaystyle \varphi _{F}(e,0,y)\simeq g(y),}$

${\displaystyle \varphi _{F}(e,x+1,y)\simeq h(\varphi _{e}(x,y),x,y).}$

The recursion theorem establishes the existence of a computable function ${\displaystyle \varphi _{f}}$ such that ${\displaystyle \varphi _{f}(x,y)\simeq \varphi _{F}(f,x,y)}$. Thus ${\displaystyle f}$ satisfies the given recursive definition.

Reflexive programming

Reflexive, or reflective, programming refers to the usage of self-reference in programs. Jones presents a view of the second recursion theorem based on a reflexive language.^[9] It is shown that the reflexive language defined is not stronger than a language without reflection (because an interpreter for the reflexive language can be implemented without using reflection); then, it is shown that the recursion theorem is almost trivial in the reflexive language.

Example

Like the second recursion theorem, the first recursion theorem can be used to obtain functions satisfying systems of recursion equations. To apply the first recursion theorem, the recursion equations must first be recast as a recursive operator.

Consider the recursion equations for the factorial function f:

$${\displaystyle {\begin{aligned}&f(0)=1\\&f(n+1)=(n+1)\cdot f(n)\end{aligned}}}$$

The corresponding recursive operator Φ will have information that tells how to get to the next value of f from the previous value. However, the recursive operator will actually define the graph of f. First, Φ will contain the pair ${\displaystyle (\varnothing ,(0,1))}$. This indicates that f(0) is unequivocally 1, and thus the pair (0,1) is in the graph of f.

Next, for each n and m, Φ will contain the pair ${\displaystyle (\{(n,m)\},(n+1,(n+1)\cdot m))}$. This indicates that, if f(n) is m, then f(n + 1) is (n + 1)m, so that the pair (n + 1, (n + 1)m) is in the graph of f. Unlike the base case f(0) = 1, the recursive operator requires some information about f(n) before it defines a value of f(n + 1).

The first recursion theorem (in particular, part 1) states that there is a set F such that Φ(F) = F. The set F will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function f, as desired.

The restriction to recursion equations that can be recast as recursive operators ensures that the recursion equations actually define a least fixed point. For example, consider the set of recursion equations:

$${\displaystyle {\begin{aligned}&g(0)=1\\&g(n+1)=1\\&g(2n)=0\end{aligned}}}$$

There is no function g satisfying these equations, because they imply g(2) = 1 and also imply g(2) = 0. Thus there is no fixed point g satisfying these recursion equations. It is possible to make an enumeration operator corresponding to these equations, but it will not be a recursive operator.

Proof sketch for the first recursion theorem

The proof of part 1 of the first recursion theorem is obtained by iterating the enumeration operator Φ beginning with the empty set. First, a sequence F_k is constructed, for ${\displaystyle k=0,1,\ldots }$. Let F₀ be the empty set. Proceeding inductively, for each k, let F_{k + 1} be ${\displaystyle F_{k}\cup \Phi (F_{k})}$. Finally, F is taken to be ${\textstyle \bigcup F_{k}}$. The remainder of the proof consists of a verification that F is recursively enumerable and is the least fixed point of Φ. The sequence F_k used in this proof corresponds to the Kleene chain in the proof of the Kleene fixed-point theorem.

The second part of the first recursion theorem follows from the first part. The assumption that Φ is a recursive operator is used to show that the fixed point of Φ is the graph of a partial function. The key point is that if the fixed point F is not the graph of a function, then there is some k such that F_k is not the graph of a function.

Comparison to the second recursion theorem

Compared to the second recursion theorem, the first recursion theorem produces a stronger conclusion but only when narrower hypotheses are satisfied. Rogers uses the term weak recursion theorem for the first recursion theorem and strong recursion theorem for the second recursion theorem.^[3]

One difference between the first and second recursion theorems is that the fixed points obtained by the first recursion theorem are guaranteed to be least fixed points, while those obtained from the second recursion theorem may not be least fixed points.

A second difference is that the first recursion theorem only applies to systems of equations that can be recast as recursive operators. This restriction is similar to the restriction to continuous operators in the Kleene fixed-point theorem of order theory. The second recursion theorem can be applied to any total recursive function.