Editing Kleene's recursion theorem (section)

== Kleene's second recursion theorem ==
The second recursion theorem is a generalization of Rogers's theorem with a second input in the function. One informal interpretation of the second recursion theorem is that it is possible to construct self-referential programs; see "Application to quines" below.

:'''The second recursion theorem'''.  For any partial recursive function <math>Q(x,y)</math> there is an index <math>p</math> such that <math>\varphi_p \simeq \lambda y.Q(p,y)</math>.

The theorem can be proved from Rogers's theorem by letting <math>F(p)</math> be a function such that <math>\varphi_{F(p)}(y) = Q(p,y)</math> (a construction described by the [[Smn theorem|S-m-n theorem]]). One can then verify that a fixed-point of this <math>F</math> is an index <math>p</math> as required. The theorem is constructive in the sense that a fixed computable function maps an index for <math>Q</math> into the index <math>p</math>.

=== Comparison to Rogers's theorem ===
Kleene's second recursion theorem and Rogers's theorem can both be proved, rather simply, from each other.{{sfn|Jones|1997|pp=229-30}} However, a direct proof of Kleene's theorem{{sfn|Kleene|1952|pp=352-3}} 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 <math>Q(x,y)=x</math>. The corresponding  index <math>p</math> in this case yields a computable function that outputs its own index when applied to any value.{{r|Cutland1980_204}} When expressed as computer programs, such indices are known as '''[[Quine (computing)|quine]]s'''.

The following example in [[Lisp programming language|Lisp]] illustrates how the <math>p</math> in the corollary can be effectively produced from the function <math>Q</math>.   The function <code>s11</code> in the code is the function of that name produced by the [[S-m-n theorem]].

<code>Q</code> can be changed to any two-argument function.
<syntaxhighlight lang="lisp">
(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)))
</syntaxhighlight>

The results of the following expressions should be the same. <math>\varphi</math> <code>p(nil)</code>
<syntaxhighlight lang="lisp">
(eval (list p nil))
</syntaxhighlight>
<code>Q(p, nil)</code>
<syntaxhighlight lang="lisp">
(eval (list Q p nil))
</syntaxhighlight>

=== Application to elimination of recursion ===
Suppose that <math>g</math> and <math>h</math> are total computable functions that are used in a recursive definition for a function <math>f</math>:

:<math>f(0,y) \simeq g(y),</math>

:<math>f(x+1,y) \simeq h(f(x,y),x,y),</math>

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 [[M-recursive function|&mu;-recursion]], or by [[Turing machine]]s). This recursive definition can be converted into a computable function <math>\varphi_{F}(e,x,y)</math> that assumes <math>e</math> is an index to itself, to simulate recursion:

:<math>\varphi_{F}(e,0,y) \simeq g(y),</math>

:<math>\varphi_{F}(e,x+1,y) \simeq h(\varphi_e(x,y),x,y).</math>

The recursion theorem establishes the existence of a computable function <math>\varphi_f</math> such that <math>\varphi_f(x,y) \simeq \varphi_{F}(f,x,y)</math>. Thus  <math>f</math> satisfies the given recursive definition.

=== Reflexive programming ===
Reflexive, or [[Reflection (computer programming)|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.{{sfn|Jones|1997}}
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.