Kleene's recursion theorem: Difference between revisions

Revision as of 10:00, 6 May 2020

Revision as of 10:07, 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 ''[[#CITEREFKleene1952|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 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. 229-230). However, a direct proof of Kleene's theorem ([[#CITEREFKleene1952|Kleene 1952]]: p. 352-{{ndash}}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 ===