Content deleted Content added
No edit summary |
ref to 'Further reading' | {{reflist|refs}} | from parenthetical referencing (deprecated) to short footnote | -{{Use parenthetical referencing}} | +{{Use shortened footnotes}} |
||
Line 1:
{{distinguish|text=[[Kleene's theorem]] for regular languages}}
{{Use shortened footnotes|date=May 2021}}
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{{r|Kleene1938}} and appear in his 1952 book ''
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.
== Notation ==
The statement of the theorems refers to an [[admissible numbering]] <math>\varphi</math> of the [[partial recursive function]]s, such that the function corresponding to index <math>e</math> is <math>\varphi_e</math>. In programming terms, <math>e</math> represents a program and <math>\varphi_e</math> represents the function computed by this program.
Line 13 ⟶ 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
:'''Rogers's fixed-point theorem'''. If <math>F</math> is a total computable function, it has a fixed point.
Line 29 ⟶ 27:
=== 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′''', the degree of the [[halting problem]]
▲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′''', the degree of the [[halting problem]] {{harv|Soare|1987|p=88}}.
== 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.
Line 41 ⟶ 37:
=== Comparison to Rogers's theorem ===
Kleene's second recursion theorem and Rogers's theorem can both be proved, rather simply, from each other
=== 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
▲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 {{harv|Cutland|1980|p=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 82 ⟶ 77:
=== Reflexive programming ===
Reflexive, or [[Reflection (computer programming)|reflective]], programming refers to the usage of self-reference in programs. Jones
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.
== The first recursion theorem ==
While the second recursion theorem is about fixed points of computable functions, the first recursion theorem is related to fixed points determined by enumeration operators, which are a computable analogue of inductive definitions. An '''enumeration operator''' is a set of pairs (''A'',''n'') where ''A'' is a ([[Gödel number|code]] for a) finite set of numbers and ''n'' is a single natural number. Often, ''n'' will be viewed as a code for an ordered pair of natural numbers, particularly when functions are defined via enumeration operators. Enumeration operators are of central importance in the study of [[enumeration reducibility]].
Line 100 ⟶ 94:
=== 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.
Line 126 ⟶ 119:
=== 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''<sub>''k''</sub> is constructed, for <math>k = 0, 1, \ldots</math>. Let ''F''<sub>0</sub> be the empty set. Proceeding inductively, for each ''k'', let ''F''<sub>''k'' + 1</sub> be <math>F_k \cup \Phi(F_k)</math>. Finally, ''F'' is taken to be <math>\bigcup F_k</math>. The remainder of the proof consists of a verification that ''F'' is recursively enumerable and is the least fixed point of Φ. The sequence ''F''<sub>''k''</sub> used in this proof corresponds to the Kleene chain in the proof of the [[Kleene fixed-point theorem]].
Line 132 ⟶ 124:
=== 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.
▲Compared to the second recursion theorem, the first recursion theorem produces a stronger conclusion but only when narrower hypotheses are satisfied. Rogers {{harv|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.
Line 140 ⟶ 131:
== Generalized theorem ==
In the context of his theory of numberings, [[Yury Yershov|Ershov]] showed that Kleene's recursion theorem holds for any [[precomplete numbering]]
Given a precomplete numbering <math>\nu</math>, then for any partial computable function <math>f</math> with two parameters there exists a total computable function <math>t</math> with one parameter such that
Line 151 ⟶ 142:
== References ==
* {{Cite book |last=Ershov |first=Yuri L. |author-link=Yury Yershov |date=1999 |chapter=Part 4: Mathematics and Computability Theory. 14. Theory of numbering |editor-last=Griffor |editor-first=Edward R. |title=Handbook of Computability Theory |series=Studies in logic and the foundations of mathemtics |volume=140 |___location=Amsterdam |publisher=[[Elsevier]] |pp=473-503 |isbn=9780444898821 |oclc=162130533 |access-date=6 May 2020 |url=https://books.google.com/books?id=KqeXZ4pPd5QC
* {{Cite journal|last1=Barendregt|first1=Henk|author-link1=Henk Barendregt|last2=Terwijn|first2=Sebastiaan A.|date=2019|title=Fixed point theorems for precomplete numberings|url=http://www.sciencedirect.com/science/article/pii/S016800721930048X|journal=Annals of Pure and Applied Logic|language=en|volume=170|issue=10|pages=1151{{ndash}}1161|doi=10.1016/j.apal.2019.04.013|hdl=2066/205967|s2cid=52289429|issn=0168-0072|access-date=6 May 2020|url-access=subscription|hdl-access=free}}▼
}}
* {{Cite book|last=Cutland|first=Nigel J.|author-link=Nigel Cutland|date=1980|title=Computability: An Introduction to Recursive Function Theory|url=https://books.google.com/books?id=wAstOUE36kcC|publisher=[[Cambridge University Press]]|language=en|doi=10.1017/cbo9781139171496|isbn=9781139935609|oclc=488175597|access-date=6 May 2020}}▼
* {{Cite book |last=
}}
* {{Cite journal|last=Kleene|first=S. C.|author-link=Stephen Cole Kleene|date=1938|title=On notation for ordinal numbers|url=http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Kleene%20-%20Ordinals.pdf|journal=[[Journal of Symbolic Logic]]|language=en|volume=3|issue=4|pages=150{{ndash}}155|doi=10.2307/2267778|jstor=2267778|issn=0022-4812|access-date=6 May 2020}}▼
* {{Cite book |last=Kleene |first=
}}
* {{Cite journal|last1=Jockusch|first1=C. G.|author-link1=Carl Jockusch|last2=Lerman|first2=M.|last3=Soare|first3=R. I.|author-link3=Robert I. Soare|last4=Solovay|first4=R. M.|author-link4=Robert M. Solovay|date=1989|title=Recursively enumerable sets modulo iterated jumps and extensions of Arslanov's completeness criterion|journal=[[The Journal of Symbolic Logic]]|language=en|volume=54|issue=4|pages=1288{{ndash}}1323|doi=10.1017/S0022481200041104|jstor=2274816|issn=0022-4812}}▼
* {{Cite book |last=
'''Footnotes'''
* {{Cite book|last=Soare|first=R. I.|author-link=Robert I. Soare|title=Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets|series=Perspectives in Mathematical Logic|date=1987|publisher=[[Springer-Verlag]]|isbn=9780387152998|___location=Berlin; New York|language=en|oclc=318368332}}▼
{{reflist|refs=
▲
▲
▲
▲
}}
==Further reading==
▲* {{Cite journal |last1=Jockusch |first1=C. G. |author-link1=Carl Jockusch |last2=Lerman |first2=M. |last3=Soare |first3=R.
== External links ==
| |||