クリーネの再帰定理

クリーネの再帰定理（クリーネのさいきていり、英: Kleene's recursion theorem）は再帰理論における2つの基本的な結果である。この定理によれば計算可能関数をそれ自身を用いて記述することができる。この定理は1938年にスティーブン・コール・クリーネによって最初に証明された。1952年の彼の著作 Introduction to Metamathematics において見られる。

2つの再帰定理は幾つかの計算可能関数の不動点の構成に利用できる。例えばクワインの生成や関数の帰納的定義などである。任意の再帰的関数の不動点構成への応用はロジャースの定理として知られる。これはハートレイ・ロジャース (Rogers, 1967) による。

記法

部分帰納的関数のアクセプタブル・ナンバリングを [math]\varphi[/math] とする。指標 [math]e[/math] に対応する帰納的関数を [math]\varphi_e[/math] と書く。プログラミングの言葉を用いれば、[math]e[/math] はプログラムで [math]\varphi_e[/math] は表示的意味である。

ロジャースの不動点定理

この文脈での関数 [math]F[/math] の不動点とは、指標 [math]e[/math] で [math]\varphi_e \simeq \varphi_{F(e)}[/math] を満たすものをいう。プログラミングの言葉を用いれば [math]e[/math] は [math]F(e)[/math] と意味論的に同値である.

ロジャースの不動点定理. [math]F[/math] が（全域）計算可能ならば不動点を持つ。

この定理は (Rogers, 1967: §11.2) のTheorem Iであり、クリーネの（第二）再帰定理の簡易版として記述されている。

不動点定理の証明

この証明では以下で定義される計算可能関数 [math]h[/math] を利用する。 自然数 [math]x[/math] が与えられたとき、関数 [math]h[/math] は次のような計算を行う部分計算可能関数の指標を出力する：

入力 [math]y[/math] が与えられると、 まず [math]\varphi_{x}(x)[/math] の計算を試行する。この計算が出力 [math]e[/math] を返したならば、そのときに限って [math]\varphi_e(y)[/math] を計算してその値を返す。

任意の [math]x[/math] について、 [math]\varphi_x(x)[/math] が停止するならば [math]\varphi_{h(x)} = \varphi_{\varphi_x(x)}[/math] であり、停止しないならば [math]\varphi_{h(x)}[/math] は停止しない。これは [math]\varphi_{h(x)} \simeq \varphi_{\varphi_x(x)}[/math] と書ける。関数 [math]h[/math] は部分計算可能関数 [math]g(x,y)=\varphi_{\varphi_x(x)}(y)[/math] からSmn定理を用いて構成できる： 各 [math]x[/math] に対して、[math]h(x)[/math] はプログラム [math]y \mapsto g(x,y)[/math] の指標である。

証明を完成させる為に、[math]F[/math] を任意の全域計算可能関数とする。また [math]h[/math] を上で構成した関数とする。いま [math]e[/math] を合成 [math]F \circ h[/math] の指標とする。これは全域計算可能関数である。すると [math]h[/math] の定義より [math]\varphi_{h(e)} \simeq \varphi_{\varphi_e(e)}[/math] が成り立つ。 ところが [math]e[/math] は [math]F \circ h[/math] の指標だったから、[math]\varphi_e(e) = (F \circ h)(e)[/math] であり、[math]\varphi_{\varphi_e(e)} \simeq \varphi_{F(h(e))}[/math]。 [math]\simeq[/math] の推移性により、これは [math]\varphi_{h(e)} \simeq \varphi_{F(h(e))}[/math] を意味する。すなわち [math]n = h(e)[/math] について [math]\varphi_n \simeq \varphi_{F(n)}[/math] が成り立つ。

不動点を持たない（fixed-point free）関数

関数 [math]F[/math] が任意の [math]e[/math] に対して [math] \varphi_e \not \simeq \varphi_{F(e)}[/math] を満たすときfixed point freeという。不動点定理によれば計算可能なfixed-point free関数は存在しない。しかし計算可能でないfixed-point free関数は幾つも存在する。アースラノフの完全性条件は、帰納的可算集合 [math]A[/math] に関する次の条件が同値であることを述べる：

1. [math]A[/math] はチューリング次数 [math]\boldsymbol{0}'[/math] つまり停止性問題の次数を持つ。
2. Fixed-point free関数 [math]f \leq_{T}A[/math] が存在する。

クリーネの第二再帰定理

第二再帰定理は直観的には自己参照的プログラムが可能であるということである。

第二再帰定理. 任意の部分帰納的関数 [math]Q(x,y)[/math] に対して指標 [math]p[/math] が存在して [math]\varphi_p \simeq \lambda y.Q(p,y)[/math] が成り立つ。

これは次のように使用される。いま次のような自己参照的プログラムを考える： 計算可能関数 [math]Q(x, y)[/math] の第1変数に自分自身の指標を、第2変数に入力を渡して計算する。第二再帰定理はこのような自己参照的プログラム [math]p[/math] が構成できることを示している。ここで [math]p[/math] は [math]y[/math] だけを入力とする。[math]p[/math] の自身の指標は入力に与えられないが、構成より自己参照的な方程式を満たす。

この定理は [math]F(p)[/math] を [math]\varphi_{F(p)}(y) = Q(p, y)[/math] を満たす関数（この構成にはSmn定理を用いる）とすることでロジャースの定理から証明できる。この関数の不動点が所望の [math]p[/math] であることが確かめられる。

この定理は Q から p が帰納的に計算できるという意味で構成的である。例えばロジャースの定理の証明をラムダ計算で再現すれば不動点を計算するラムダ項（不動点コンビネータ）が得られる。

ロジャースの定理との比較

クリーネの第二再帰定理とロジャースの定理は一方から他方を簡単に証明できる（Jones, 1997: p. 229-230）。ところが、クリーネの定理の直接証明（Kleene 1952: p. 352-353）は万能関数を使用しない。その意味するところは、万能関数を持たない幾つかの弱い計算模型に於いても同様の定理が成り立つということである。

再帰の除去への利用

いま [math]g[/math] と [math]h[/math] を全域計算可能関数とする。これらを用いて関数 [math]f[/math] を帰納的に次のように定義する：

[math]f(0,y) \simeq g(y),\,[/math]

[math]f(x+1,y) \simeq h(f(x,y),x,y),\,[/math]

第二再帰定理をこの等式が計算可能関数を定義することを示すことに利用できる。それには考えている計算模型にア・プリオリに帰納的定義が備わっている必要はない。したがって第二再帰定理（と万能関数の存在）が成立する計算模型であればμ-再帰的関数でもチューリング機械でも成り立つ。

この帰納的定義は次の計算可能関数 [math] (x, y) \mapsto \varphi_{F}(e,x,y)[/math] の指標が [math]e[/math] 自身となるような [math]e[/math] を求めることに帰着できる：

[math]\varphi_{F}(e,0,y) \simeq g(y),\,[/math]

[math]\varphi_{F}(e,x+1,y) \simeq h(\varphi_e(x,y),x,y).\,[/math]

再帰定理は [math]\varphi_f(x,y) \simeq \varphi_{F}(f,x,y)[/math] なる計算可能関数 [math]\varphi_f[/math] の存在を確立する。すると [math]\varphi_f[/math] は与えられた帰納的定義を満たす。

クワインへの応用

再帰定理の使用の古典的な例は [math]Q(x,y)=x[/math] に対するものである。この場合に対応する指標 [math]p[/math] は任意に値を入力すると出力が自分自身に一致する計算可能関数である(Cutland 1980: p. 204)。プログラミングの言葉を用いれば、これはクワインとして知られるプログラムの指標に他ならない。

以下ではLispを用いて指標 [math]p[/math] が関数 [math]Q[/math] からどのように実効的に得られるかを見る。関数 s11 はSmn定理に対応するLispコードである。

Q は任意の2引数の関数のLispコードに置き換えられる。

(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)))

次の2つの式の結果は等しくなる。p(nil) Q(p, nil)

(eval (list p nil))

(eval (list Q p nil))

自己反映計算

自己反映計算は自己参照を用いたプログラミングである。Jones (1997) は自己反映言語に基づいた第二再帰定理の見方を示した。

それは自己反映言語の計算能力は自己反映を持たない言語の計算能力よりも強くはないということである。（何故なら自己反映言語のインタプリタは自己反映を持たない言語によって実装できる）； 再帰定理は自己反映言語において明らかに実現できる。したがって自己反映を持たない言語（帰納的関数やチューリング機械などの計算模型）でも成り立つ。

第一再帰定理

第一再帰定理は帰納的な枚挙作用素の不動点に関するものである。枚挙作用素とは対 [math](A, n)[/math] の集合であって、 [math]A[/math] はコード化された有限集合、 [math]n[/math] は自然数である。 関数が枚挙作用素を通じて定義される場合など [math]n[/math] は自然数の対のコードと見做されることがある。枚挙作用素は枚挙還元性の研究で最も重要な概念のひとつである。

枚挙作用素 Φ は自然数の集合から自然数の集合への関数を定める：

[math]\Phi(X) = \{ n \mid \exists A \subseteq X [(A,n) \in \Phi]\}.[/math]

帰納作用素とは部分帰納的関数のグラフ（正確には部分関数のグラフを対のコードの集合と見做したもの）を常に部分帰納的関数（同様）に写すものをいう。このとき帰納作用素は部分帰納的関数から部分帰納的関数への関数を定めるものと考えられる。

枚挙作用素 [math]\Phi[/math] の不動点とは [math]\Phi(F)=F[/math] なる集合 [math]F[/math] をいう。同様に帰納作用素 [math]\Psi[/math] の不動点とは [math]\Psi(f)=f[/math] なる部分関数 [math]f[/math] をいう。第一再帰定理は枚挙作用素が計算可能ならば不動点が実効的に得られることを示す。

第一再帰定理 次の言明が成り立つ:

1. 任意の計算可能な枚挙作用素は帰納的可算な最小不動点を持つ。
2. 任意の帰納作用素は部分帰納的な最小不動点を持つ。

例

第二再帰定理と同様に、第一再帰定理は再帰方程式を満たす関数を構成する為に使える。第一再帰定理を使うためには再帰方程式系を帰納作用素を使って書き換える必要がある。

階乗関数 [math]f[/math] の再帰方程式系を考える：

[math]f(0)=1,[/math]

[math]f(n+1)=(n+1)\cdot f(n).[/math]

対応する帰納作用素 [math]\Phi[/math] は [math]f[/math] の前の値から次の値をどのように得るかを記述することで得られる。直感的にいうと [math]f[/math] の有限近似を [math]\Phi[/math] で写すとよりよい（定義域が拡大された）有限近似が得られるように [math]\Phi[/math] を定義すればよい。まず [math]\Phi[/math] に対 [math](\varnothing,(0, 1))[/math] を置く。これは [math]f(0)=1[/math] であることを示す。次に任意の [math](n,m)[/math] について [math]\Phi[/math] に対 [math](\{(n, m)\}, (n+1,(n+1)\cdot m)[/math] を置く。これは [math]f(n)=m[/math] ならば [math]f(n+1)=(n+1)\cdot m[/math] であることを示す。

第一再帰定理より帰納的可算集合 [math]F[/math] で [math]\Phi(F)=F[/math] なる最小なものが存在する。この集合 [math]F[/math] は自然数の対だけからなり、ちょうど所望の階乗関数 [math]f[/math] のグラフとなっている。

上のようにして再帰方程式系の解が必ず得られるとは限らない。次のような解を持たない再帰方程式系が考える：

[math]g(0)=1,[/math]

[math]g(n+1)=1,[/math]

[math]g(2n)=0.[/math]

この方程式をもとに枚挙作用素 [math]\Psi[/math] を作る。第一再帰定理より [math]\Psi[/math] は（帰納的可算な）不動点を持つ。ところがいかなる部分（帰納的）関数も上の方程式系を満足しえない。この再帰方程式に対応する作用素は帰納作用素ではないからである。

第一再帰定理の証明の概略

第一再帰定理の前半の証明は、空集合から始めて枚挙演算子 [math]\Phi[/math] の反復によって得られる。まず集合列 [math]F_k[/math] を次のように帰納的に定義する：

[math]F_0 = \varnothing,[/math]

[math]F_{k+1} = F_k \cup \Phi(F_k)[/math]

次に [math]F = \bigcup F_k[/math] とおく。[math]F_k[/math] は一様に帰納的な増大列であるので [math]F[/math] は帰納的可算である。さらに [math]F[/math] は [math]\Phi[/math] の最小不動点である。ここで構成した [math]F_k[/math] は完備半順序で定義された単調関数の不動点の存在を述べるクリーネの不動点定理のクリーネ鎖に対応している。

定理の後半は前半から従う。実際 [math]\Phi[/math] を帰納作用素とすると上の証明の [math]F[/math] が部分関数のグラフになることが [math]k[/math] に関する帰納法で確かめられる。

第二再帰定理との比較

第二再帰定理と比較すると、第一再帰定理は狭い前提条件を満たす場合に限りより強い帰結を与える。ロジャース[1967]では第一再帰定理を弱再帰定理（英: weak recursion theorem）、第二再帰定理を強再帰定理（英: strong recursion theorem）と表現している。

ひとつの相違は、第一再帰定理は最小不動点を与えるものであるが、第二再帰定理は最小不動点に限らないということである。いまひとつの相違は、第一再帰定理は再帰方程式を帰納作用素に書き換えられる再帰方程式系に対してのみ適用できるが、第二再帰定理は任意の全域帰納的関数に適用できるということである。この制限はクリーネの不動点定理の連続写像という制限と類似している。

A.I. Maltsevによる一般化された定理

アナトリー・マルツェフはプリコンプリート・ナンバリングを持つ任意の集合に対する一般化された再帰定理を示した。アクセプタブル・ナンバリングは計算可能関数の集合に対するプリコンプリート・ナンバリングであるから、クリーネの再帰定理は一般化された定理の特別な場合として得られる。

プリコンプリート・ナンバリング [math]\nu[/math] を所与とすると、任意の部分計算可能関数 [math]f:\mathbb{N}^2 \to \mathbb{N}[/math] に対して、全域計算可能関数 [math]t:\mathbb{N} \to \mathbb{N}[/math] が存在して、次を満たす：

[math]\nu \circ f(n, t(n)) = \nu \circ t(n).[/math]

関連項目

• 表示的意味論
• 不動点コンビネータ

参考文献

• Cutland, N.J., Computability: An introduction to recursive function theory, Cambridge University Press, 1980. ISBN 0-521-29465-7
• Stephen Cole Kleene (1938). “On Notation for Ordinal Numbers”. The Journal of Symbolic Logic 3: 150–155. http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Kleene%20-%20Ordinals.pdf. 
• Kleene, Stephen, Introduction to Metamathematics, North-Holland, 1952. ISBN 0-7204-2103-9
• Rogers, H. Theory of Recursive Functions and Effective Computability, MIT Press, 1967. ISBN 0-262-68052-1; ISBN 0-07-053522-1
• Jones, N.D.J., Computability and Complexity from a programming perspective, MIT Press, 1997. ISBN 0-262-10064-9

外部リンク

• Recursive Functions （英語） - スタンフォード哲学百科事典「Piergiorgio Odifreddi」の項目。.