クリーネの再帰定理
帰納作用素とは部分帰納的関数のグラフ(正確には部分関数のグラフを対のコードの集合と見做したもの)を常に部分帰納的関数(同様)に写すものをいう。このとき帰納作用素は部分帰納的関数から部分帰納的関数への関数を定めるものと考えられる。
枚挙作用素 Φ {\displaystyle \Phi } の不動点とは Φ ( F ) = F {\displaystyle \Phi (F)=F} なる集合 F {\displaystyle F} をいう。同様に帰納作用素 Ψ {\displaystyle \Psi } の不動点とは Ψ ( f ) = f {\displaystyle \Psi (f)=f} なる部分関数 f {\displaystyle f} をいう。第一再帰定理は枚挙作用素が計算可能ならば不動点が実効的に得られることを示す。
第一再帰定理 次の言明が成り立つ: 任意の計算可能な枚挙作用素は帰納的可算な最小不動点を持つ。 任意の帰納作用素は部分帰納的な最小不動点を持つ。
再帰定理の使用の古典的な例は Q ( x , y ) = x {\displaystyle Q(x,y)=x} に対するものである。この場合に対応する指標 p {\displaystyle p} は任意に値を入力すると出力が自分自身に一致する計算可能関数である(Cutland 1980: p. 204)。プログラミングの言葉を用いれば、これはクワインとして知られるプログラムの指標に他ならない。
以下ではLispを用いて指標 p {\displaystyle p} が関数 Q {\displaystyle Q} からどのように実効的に得られるかを見る。関数 s11 はSmn定理に対応するLispコードである。
Q は任意の2引数の関数のLispコードに置き換えられる。
次の2つの式の結果は等しくなる。p(nil) Q(p, nil)