Kleene's recursion theorem

In computability theory Kleene's recursion theorem, first proved by Stephen Kleene in 1938, is a fundamental result about the application of computable functions to their own descriptions.

Suppose that φ is a scheme for describing partial recursive functions (e.g. a Gödel numbering or programming language), and that the function corresponding to description p is φ_p. If Q is a partial recursive function of two arguments, then there is a description p of a function of one argument such that

$\varphi _{p}=\lambda y.Q(p,\,y)$

In other words, for any computable function of two arguments, there is a program that takes one argument and evaluates the function in question, with its own description as the first argument and the given argument as the second. Note that this program does not have to read its description from an external source, such as a file; It can generate the required information about its description, in the chosen description scheme, by itself.

Proof: Let s₁₁ be given by the S-m-n theorem, and let n be a description of the function λx,y.Q(s₁₁(x, x), y). Let p = s₁₁(n, n). Then,

$\phi _{p}=\phi _{s_{11}(n,\,n)}=\lambda y.\phi _{n}(n,y)=\lambda y.Q(s_{11}(n,\,n),\,y)=\lambda y.Q(p,\,y)$

A classic example is the function Q(x, y) = x. The corresponding program p in this case generates its own description when applied to any value. Such programs are known as quines. Although the proof of the theorem shows how to construct one quine, students sometimes challenge themselves to find simpler ones.

Generalized theorem by A.I. Mal'tsev

A.I. Mal'tsev proved a generalized version of the recursion theorem for any set with a precomplete numbering. A Gödel numbering is a precomplete numbering on the set of computable functions so the generalized theorem yields the Kleene recursion theorem as a special case.

Given a precomplete numbering $\nu$ then for any partial computable function $f$ with two parameters there exists a total computable function $r$ with one parameter so that

$\nu \circ f(n,t(n))=\nu \circ t(n)\quad n\in \mathbb {N} .\,$

Example

With a Lisp interpreter, it is straightforward to implement the construction in the proof.

; 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.
; φp(nil)
(eval (list p nil)    

; Q(p,nil)
(eval (list Q p nil))

References

• Kleene, Stephen, "On notation for ordinal numbers," The Journal of Symbolic Logic, 3 (1938), 150-155.