Kleene's recursion theorem: Difference between revisions

Revision as of 09:41, 6 May 2020

Revision as of 10:00, 6 May 2020

Line 1:

{{distinguish|text=[[Kleene's theorem]] for regular languages}}

In [[computability theory]], '''Kleene's recursion theorems''' are a pair of fundamental results about the application of [[computable function]]s to their own descriptions. The theorems were first proved by [[Stephen Cole Kleene|Stephen Kleene]] in 1938 and appear in his 1952 book ''Introduction to Metamathematics''. A related theorem which constructs fixed points of a computable function is known as '''Rogers's theorem''' and is due to [[Hartley Rogers, Jr.]] ([[#CITEREFRogers1967|Rogers 1967]]).

The recursion theorems can be applied to construct [[fixed point (mathematics)|fixed points]] of certain operations on [[computable function]]s, to generate [[quine (computing)|quines]], and to construct functions defined via [[recursive definition]]s.

Line 11:

== Rogers's fixed-point theorem ==

Given a function <math>F</math>, a '''fixed point''' of <math>F</math> is an index <math>e</math> such that <math>\varphi_e \simeq \varphi_{F(e)}</math>. Rogers ([[#CITEREFRogers1967|Rogers 1967]]: §11.2) describes the following result as "a simpler version" of Kleene's (second) recursion theorem.

:'''Rogers's fixed-point theorem'''. If <math>F</math> is a total computable function, it has a fixed point.

Line 28:

=== Fixed-point free functions ===

A function <math>F</math> such that <math> \varphi_e \not \simeq \varphi_{F(e)}</math> for all <math>e</math> 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&prime;''', the degree of the [[halting problem]] ([[#CITEREFSoare1987|Soare 1987,]]: p.&nbsp;88)

== Kleene's second recursion theorem ==

Line 39:

=== Comparison to Rogers's theorem ===

Kleene's second recursion theorem and Rogers's theorem can both be proved, rather simply, from each other ([[#CITEREFJones1997|Jones, 1997]]: p.&nbsp;229-230). However, a direct proof of Kleene's theorem ([[#CITEREFKleene1952|Kleene 1952]]: p.&nbsp;352-353) 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 ([[#CITEREFCutland1980|Cutland 1980,]]: p.&nbsp;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]].

Line 80:

=== Reflexive programming ===

Reflexive, or [[Reflection (computer programming)|reflective]], programming refers to the usage of self-reference in programs. Jones ([[#CITEREFJones1997|Jones 1997]]) presents a view of the second recursion theorem based on a reflexive language.

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.

Line 131:

=== 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 ([[#CITEREFRogers1967|Rogers 1967]]) uses the term '''weak recursion theorem''' for the first recursion theorem and '''strong recursion theorem''' for the second recursion theorem.

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.