Content deleted Content added
Gricharduk (talk | contribs) →References: Consistency: Now using templates in the references |
Link suggestions feature: 3 links added. |
||
| (40 intermediate revisions by 25 users not shown) | |||
Line 1:
{{Short description|Theorem in computability theory}}
{{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 ''Introduction to Metamathematics''.{{sfn|Kleene|1952}} A related theorem, which constructs fixed points of a computable function, is known as '''Rogers's theorem''' and is due to [[Hartley Rogers, Jr.]]
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>
▲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.
If <math>F</math> and <math>G</math> are [[partial function]]s on the natural numbers, the notation <math>F \simeq G</math> indicates that, for each ''n'', either <math>F(n)</math> and <math>G(n)</math> are both defined and are equal, or else <math>F(n)</math> and <math>G(n)</math> are both undefined.
== 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 describes the following result as "a simpler version" of Kleene's (second) recursion theorem.{{sfn|Rogers|1967|loc=§11.2}}
This essentially means that if we apply an [[Effectiveness|effective]] transformation to programs (say, replace instructions such as successor, jump, remove lines), there will always be a program whose behaviour is not altered by the transformation. This theorem can therefore be interpreted in the following manner: “given any effective procedure to transform programs, there is always a program that, when modified by the procedure, does exactly what it did before”, or: “it’s impossible to write a program that changes the extensional behaviour of all programs”.
▲:'''Rogers's fixed-point theorem'''. If <math>F</math> is a total computable function, it has a fixed point.
=== Proof of the fixed-point theorem ===
The proof uses a particular total computable function <math>h</math>, defined as follows. Given a natural number <math>x</math>, the function <math>h</math> outputs the index of the partial computable function that performs the following computation:
:Given an input
Thus, for all indices <math>x</math> of partial computable functions, if <math>\varphi_x(x)</math> is defined, then <math>\varphi_{h(x)} \simeq \varphi_{\varphi_x(x)}</math>. If <math>\varphi_x(x)</math> is not defined, then <math>\varphi_{h(x)}</math> is a function that is nowhere defined. The function <math>h</math> can be constructed from the partial computable function <math>g(x,y)</math> described above and the [[s-m-n theorem]]: for each <math>x</math>, <math>h(x)</math> is the index of a program which computes the function <math>y \mapsto g(x,y)</math>.
Line 26 ⟶ 30:
This proof is a construction of a [[partial recursive function]] which implements the [[Fixed-point combinator|Y combinator]].
=== Fixed-point
A function <math>F</math> such that <math> \varphi_e \not \simeq \varphi_{F(e)}</math> for all <math>e</math> is called '''fixed
▲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]] (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.
:'''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
=== 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 (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]].
<code>Q</code> 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)))
</syntaxhighlight>
The results of the following expressions should be the same. <math>\varphi</math> <code>p(nil)</code>
<
(eval (list p nil))
</syntaxhighlight>
<code>Q(p, nil)</code>
<
(eval (list Q p nil))
</syntaxhighlight>
=== Application to elimination of recursion ===
Line 71 ⟶ 72:
:<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,
:<math>\varphi_{F}(e,0,y) \simeq g(y),</math>
Line 80 ⟶ 81:
=== 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]].▼
▲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]].
Each enumeration operator Φ determines a function from sets of naturals to sets of naturals given by
Line 96:
:# For any computable enumeration operator Φ there is a recursively enumerable set ''F'' such that Φ(''F'') = ''F'' and ''F'' is the smallest set with this property.
:# For any recursive operator Ψ there is a partial computable function φ such that Ψ(φ) = φ and φ is the smallest partial computable function with this property.
The first recursion theorem is also called Fixed point theorem (of recursion theory).<ref>{{Cite book |last=Cutland |first=Nigel |title=Computability: an introduction to recursive function theory}}</ref> There is also a definition which can be applied to [[Primitive recursive functional|recursive functionals]] as follows:
Let <math>\Phi: \mathbb{F}(\mathbb{N}^k) \rightarrow (\mathbb{N}^k)</math> be a recursive functional. Then <math>\Phi</math> has a least fixed point <math>f_{\Phi}: \mathbb{N}^k \rightarrow \mathbb{N}</math> which is computable i.e.
=== Example ===▼
1) <math>\Phi(f_{\phi})=f_{\Phi}</math>
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.▼
2) <math>\forall g \in \mathbb{F}(\mathbb{N}^k)</math> such that <math>\Phi(g)=g</math> it holds that <math>f_{\Phi}\subseteq g</math>
Consider the recursion equations for the [[factorial]] function ''f'':▼
3) <math>
▲=== Example ===
<math>f(n+1) = (n + 1) \cdot f(n)</math>▼
▲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.
▲Consider the recursion equations for the [[factorial]] function ''f'':<math display="block">\begin{align}
The corresponding recursive operator Φ will have information that tells how to get to the next value of ''f'' from the previous value. However, the recursive operator will actually define the graph of ''f''. First, Φ will contain the pair <math>( \varnothing, (0, 1))</math>. This indicates that ''f''(0) is unequivocally 1, and thus the pair (0,1) is in the graph of ''f''.▼
&f(0) = 1 \\
▲\end{align}</math>The corresponding recursive operator Φ will have information that tells how to get to the next value of ''f'' from the previous value. However, the recursive operator will actually define the graph of ''f''. First, Φ will contain the pair <math>( \varnothing, (0, 1))</math>. This indicates that ''f''(0) is unequivocally 1, and thus the pair (0,1) is in the graph of ''f''.
Next, for each ''n'' and ''m'', Φ will contain the pair <math>( \{ (n, m) \}, (n+1, (n+1)\cdot m))</math>. This indicates that, if ''f''(''n'') is ''m'', then ''f''(''n'' + 1) is (''n'' + 1)''m'', so that the pair (''n'' + 1, (''n'' + 1)''m'') is in the graph of ''f''. Unlike the base case ''f''(0) = 1, the recursive operator requires some information about ''f''(''n'') before it defines a value of ''f''(''n'' + 1).▼
▲Next, for each ''n'' and ''m'', Φ will contain the pair <math>( \{ (n, m) \}, (n+1, (n+1)\cdot m))</math>. This indicates that, if ''f''(''n'') is ''m'', then {{nowrap|''f''(''n''
The first recursion theorem (in particular, part 1) states that there is a set ''F'' such that Φ(''F'') = F. The set ''F'' will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function ''f'', as desired.▼
▲The first recursion theorem (in particular, part 1) states that there is a set ''F'' such that {{nowrap|1=Φ(''F'') = F}}. The set ''F'' will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function ''f'', as desired.
The restriction to recursion equations that can be recast as recursive operators ensures that the recursion equations actually define a least fixed point. For example, consider the set of recursion equations:▼
▲The restriction to recursion equations that can be recast as recursive operators ensures that the recursion equations actually define a [[least fixed point]]. For example, consider the set of recursion equations:<math display="block">\begin{align}
&g(0) = 1\\
\end{align}</math>There is no function ''g'' satisfying these equations, because they imply ''g''(2) = 1 and also imply ''g''(2) = 0. Thus there is no fixed point ''g'' satisfying these recursion equations. It is possible to make an enumeration operator corresponding to these equations, but it will not be a recursive operator.▼
▲<math>g(2n) = 0</math>
▲There is no function ''g'' satisfying these equations, because they imply ''g''(2) = 1 and also imply ''g''(2) = 0. Thus there is no fixed point ''g'' satisfying these recursion equations. It is possible to make an enumeration operator corresponding to these equations, but it will not be a recursive operator.
=== 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 display="inline">\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]].▼
▲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]].
The second part of the first recursion theorem follows from the first part. The assumption that Φ is a recursive operator is used to show that the fixed point of Φ is the graph of a partial function. The key point is that if the fixed point ''F'' is not the graph of a function, then there is some ''k'' such that ''F''<sub>''k''</sub> is not the graph of a function.
=== 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 (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 138:
== 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
:<math>\forall n \in \mathbb{N} : \nu \circ f(n,t(n)) = \nu \circ t(n).</math>
Line 147:
* [[Denotational semantics]], where another least fixed point theorem is used for the same purpose as the first recursion theorem.
* [[Fixed-point combinator]]s, which are used in [[lambda calculus]] for the same purpose as the first recursion theorem.
* [[Diagonal lemma]] a closely related result in mathematical logic.
== References ==
* {{Cite book |last=Ershov |first=Yuri L. |author-link=Yury Yershov
* {{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=English|volume=170|issue=10|pages=1151{{ndash}}1161|doi=10.1016/j.apal.2019.04.013|issn=0168-0072|access-date=6 May 2020|url-status=live|url-access=subscription}}▼
}}
* {{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&printsec=frontcover|publisher=[[Cambridge University Press]]|language=English|doi=10.1017/cbo9781139171496|isbn=0-521-29465-7|oclc=488175597|access-date=6 May 2020|url-status=live}}▼
* {{Cite book |last=Jones |first=Neil D. |author-link=Neil D. Jones |date=1997 |title=Computability and complexity: From a Programming Perspective |___location=[[Cambridge, Massachusetts]] |publisher=[[MIT Press]] |isbn=9780262100649 |oclc=981293265
▲* {{Cite book|last=Ershov|first=Yuri L|author-link=Yury Yershov|editor-last=Griffor|editor-first=Edward R|url=https://books.google.com/books?id=KqeXZ4pPd5QC&printsec=frontcover|title=Handbook of Computability Theory|chapter=Part 4: Mathematics and Computability Theory. 14. Theory of numbering|series=Studies in logic and the foundations of mathemtics|date=1999|volume=140|pages=473-503|publisher=[[Elsevier]]||___location=Amsterdam|language=English|oclc=162130533|isbn=978-0-444-89882-1|access-date=6 May 2020|url-status=live}}
}}
* {{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=English|volume=3|issue=4|pages=150{{ndash}}155|doi=10.2307/2267778|issn=0022-4812|access-date=6 May 2020|url-status=live}}▼
* {{Cite book |last=Kleene |first=
}}
* {{Cite journal|last=Jockusch|first=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=English|volume=54|issue=4|pages=1288{{ndash}}1323|doi=10.1017/S0022481200041104|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=978-0-387-15299-8|___location=Berlin; New York|language=English|oclc=318368332}}▼
{{reflist|refs=
▲
▲
▲
▲
}}
==Further reading==
▲* {{Cite journal |
== External links ==
| |||