クリーネの第二再帰定理
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/10/03 01:23 UTC 版)
「クリーネの再帰定理」の記事における「クリーネの第二再帰定理」の解説
第二再帰定理は直観的には自己参照的プログラムが可能であるということである。 第二再帰定理. 任意の部分帰納的関数 Q ( x , y ) {\displaystyle Q(x,y)} に対して指標 p {\displaystyle p} が存在して φ p ≃ λ y . Q ( p , y ) {\displaystyle \varphi _{p}\simeq \lambda y.Q(p,y)} が成り立つ。 これは次のように使用される。いま次のような自己参照的プログラムを考える： 計算可能関数 Q ( x , y ) {\displaystyle Q(x,y)} の第1変数に自分自身の指標を、第2変数に入力を渡して計算する。第二再帰定理はこのような自己参照的プログラム p {\displaystyle p} が構成できることを示している。ここで p {\displaystyle p} は y {\displaystyle y} だけを入力とする。 p {\displaystyle p} の自身の指標は入力に与えられないが、構成より自己参照的な方程式を満たす。 この定理は F ( p ) {\displaystyle F(p)} を φ F ( p ) ( y ) = Q ( p , y ) {\displaystyle \varphi _{F(p)}(y)=Q(p,y)} を満たす関数（この構成にはSmn定理を用いる）とすることでロジャースの定理から証明できる。この関数の不動点が所望の p {\displaystyle p} であることが確かめられる。 この定理は Q から p が帰納的に計算できるという意味で構成的である。例えばロジャースの定理の証明をラムダ計算で再現すれば不動点を計算するラムダ項（不動点コンビネータ）が得られる。
※この「クリーネの第二再帰定理」の解説は、「クリーネの再帰定理」の解説の一部です。
「クリーネの第二再帰定理」を含む「クリーネの再帰定理」の記事については、「クリーネの再帰定理」の概要を参照ください。
- クリーネの第二再帰定理のページへのリンク
