Content deleted Content added
m Adding local short description: "Theorem in computability theory", overriding Wikidata description "also called the fixed point theorem, in computability theory" |
|||
Line 98:
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}
&f(0) = 1 \\
&f(n+1) = (n + 1) \cdot f(n)
\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''.▼
▲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 {{nowrap|''f''(''n'' + 1)}} is {{nowrap|(''n'' + 1)''m''}}, so that the pair {{nowrap|(''n'' + 1, (''n'' + 1)''m'')}} is in the graph of ''f''. Unlike the base case {{nowrap|1=''f''(0) = 1}}, the recursive operator requires some information about ''f''(''n'') before it defines a value of {{nowrap|''f''(''n'' + 1)}}.
Line 110 ⟶ 108:
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:<math display="block">\begin{align}
&g(0) = 1\\
&g(n + 1) = 1\\
&g(2n) = 0
\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.▼
▲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 ===
Line 141 ⟶ 136:
* [[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 ==
| |||