計算可能性理論 において、 クリーネの再帰定理は、計算可能関数をそれ自身の記述に適用することに関する一対の基本的な結果である。この定理は、1938年にスティーブン・クリーネによって初めて証明され[1]、1952年の著書「メタ数学入門」に掲載されている。[2]計算可能関数の不動点を構成する関連する定理はロジャースの定理として知られ、ハートリー・ロジャース・ジュニアによるものである[3]。
再帰定理は、計算可能関数に対する特定の演算の不動点の構築、クインの生成、再帰定義によって定義された関数の構築に適用できます。
表記
定理の記述は、部分再帰関数の許容される番号付け を参照しており、インデックス に対応する関数はです。
およびが自然数上の部分関数である場合、表記は、各nについて、およびが両方とも定義されていて等しいか、または、およびが両方とも未定義であることを示します。
ロジャースの不動点定理
関数 が与えられた場合、の不動点はとなるインデックスです。ここでの入力と出力の比較は数値ではなく、関連する関数に基づいていることに注意してください。
ロジャーズは、次の結果をクリーネの(第二)再帰定理の「より単純なバージョン」と表現している。[4]
ロジャースの不動点定理 — が全計算可能関数である場合、それは上記の意味で不動点を持ちます。
これは本質的に、プログラムに効果的な変換 (たとえば、後続、ジャンプ、行の削除などの命令の置き換え) を適用すると、変換によって動作が変更されないプログラムが常に存在することを意味します。したがって、この定理は次のように解釈できます。「プログラムを変換するための効果的な手順が与えられれば、その手順によって変更されたときに、以前とまったく同じ動作をするプログラムが常に存在する」、または「すべてのプログラムの拡張動作を変更するプログラムを作成することは不可能である」。
不動点定理の証明
証明では、次のように定義される特定の全体計算可能関数 を使用します。自然数 が与えられると、関数は次の計算を実行する部分計算可能関数のインデックスを出力します。
- 入力 が与えられた場合、まず を計算します。その計算によって出力 が返された場合は、 を計算し、その値があればそれを返します。
したがって、部分計算可能関数のすべてのインデックスについて、が定義されている場合は となります。が定義されていない場合は、 はどこにも定義されていない関数です。 関数 は、上記の部分計算可能関数とsmn 定理から構築できます。各 について、は関数 を計算するプログラムのインデックスです。
証明を完了するには、 を任意の全計算可能関数とし、を上記のように構築します。を合成 のインデックスとします。これは全計算可能関数です。の定義により、 となります。 しかし、は のインデックスであるため、となり、 となります。 の推移性により、これは を意味します。 したがって について となります。
この証明は、 Y コンビネータを実装する部分再帰関数の構築です。
固定小数点フリー関数
すべての に対してとなる関数は、固定小数点フリーと呼ばれます。固定小数点定理は、全計算可能関数は固定小数点フリーではないが、計算不可能な固定小数点フリー関数は多数存在することを示しています。アルスラノフの完全性基準は、固定小数点フリー関数を計算する唯一の再帰的に列挙可能なチューリング次数は、停止問題の次数である0′であるとしています。[5]
クリーネの第二再帰定理
第 2 再帰定理は、関数に 2 番目の入力を持つロジャースの定理の一般化です。第 2 再帰定理の非公式な解釈の 1 つは、自己参照プログラムを構築できるというものです。以下の「クインへの適用」を参照してください。
- 第二再帰定理。任意の部分再帰関数には、となるようなインデックスが存在します。
この定理は、を となる関数とすることでロジャースの定理から証明できます( Smn 定理によって記述される構成)。次に、この の不動点が要求どおりにインデックスであることを検証できます。この定理は、固定された計算可能関数がのインデックスを のインデックスにマッピングするという意味で構成的です。
ロジャースの定理との比較
クリーネの第二再帰定理とロジャースの定理は、どちらもお互いからかなり簡単に証明できます。[6]しかし、クリーネの定理[7]の直接的な証明では普遍的なプログラムを使用していません。つまり、この定理は普遍的なプログラムを持たない特定の部分再帰プログラミングシステムにも当てはまります。
クインへの応用
第二再帰定理を使った典型的な例は関数 です。この場合の対応するインデックスは、任意の値に適用すると独自のインデックスを出力する計算可能な関数を生成します。 [8]コンピュータプログラムとして表現される場合、このようなインデックスはクインと呼ばれます。
次のLispの例は、系の が関数 から効果的に生成される方法を示しています。コード内の関数 は、 Smn 定理によって生成されたその名前の関数です。
s11
Q任意の 2 つの引数を持つ関数に変更できます。
( 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 )))
次の式の結果は同じになるはずです。 p(nil)
( eval (リストp nil ))
Q(p, nil)
( eval (リストQ p nil ))
再帰の除去への応用
およびが関数 の再帰定義で使用される全計算可能関数であると仮定します。
2 番目の再帰定理は、このような方程式が計算可能な関数を定義することを示すために使用できます。計算可能性の概念は、一見、再帰的な定義を許容する必要はありません (たとえば、μ 再帰やチューリング マシンによって定義される場合があります)。この再帰的な定義は、が自分自身のインデックスである と想定する計算可能な関数に変換して、再帰をシミュレートできます。
再帰定理は、となる計算可能な関数の存在を確立します。したがって、 は与えられた再帰定義を満たします。
反射プログラミング
再帰的プログラミング、またはリフレクティブプログラミングとは、プログラム内で自己参照を使用することを指します。ジョーンズは、再帰言語に基づく第2再帰定理の見解を提示しています。[9] 定義された再帰言語は、リフレクションのない言語よりも強力ではないことが示されています(再帰言語のインタープリタはリフレクションを使用せずに実装できるため)。次に、再帰定理は再帰言語ではほとんど自明であることが示されています。
第一再帰定理
第二再帰定理が計算可能関数の不動点に関するものであるのに対し、第一再帰定理は、帰納的定義の計算可能な類似物である列挙演算子によって決定される不動点に関連しています。列挙演算子は、ペア ( A、n )の集合です。ここで、 Aは有限の数値集合(のコード) であり、n は単一の自然数です。多くの場合、特に関数が列挙演算子によって定義されている場合、 n は自然数の順序付きペアのコードと見なされます。列挙演算子は、列挙の還元可能性の研究において中心的な重要性を持っています。
各列挙演算子Φは、自然数の集合から自然数の集合への関数を決定する。
再帰演算子は、部分再帰関数のグラフが与えられた場合に、常に部分再帰関数のグラフを返す列挙演算子です。
列挙演算子 Φ の不動点は、Φ( F ) = Fとなる集合Fである。第一列挙定理は、列挙演算子自体が計算可能であれば、不動点を効果的に取得できることを示しています。
- 第一再帰定理。次の命題が成り立つ。
- 任意の計算可能な列挙演算子 Φ に対して、 Φ( F ) = Fとなるような再帰的に列挙可能な集合Fが存在し、F はこの性質を持つ最小の集合です。
- 任意の再帰演算子 Ψ に対して、Ψ(φ) = φ となるような部分計算可能関数 φ が存在し、φ はこの特性を持つ最小の部分計算可能関数です。
第一再帰定理は、不動点定理(再帰理論)とも呼ばれます。[10]再帰関数に適用できる定義も次のように存在します。
を帰納的関数とする。すると、最小不動点が計算可能となる。 すなわち
1)
2)次のように成り立つ
3)計算可能である
例
2 番目の再帰定理と同様に、1 番目の再帰定理は、再帰方程式のシステムを満たす関数を取得するために使用できます。1 番目の再帰定理を適用するには、まず再帰方程式を再帰演算子として書き直す必要があります。
階乗関数fの再帰方程式を考えてみましょう。対応する再帰演算子 Φには、 fの前の値から次の値に到達する方法を示す情報が含まれます。ただし、再帰演算子は実際にfのグラフを定義します。まず、 Φ にはペアが含まれます。これは、f (0) が明確に 1 であることを示しており、したがってペア (0,1) はfのグラフ内にあります。
次に、各nとmについて、 Φ にはペアが含まれます。これは、f ( n ) がmの場合、f ( n + 1)は( n + 1) mであり、ペア( n + 1, ( n + 1) m )がfのグラフ内にあることを示しています。基本ケースf (0) = 1とは異なり、再帰演算子はf ( n + 1)の値を定義する前にf ( n ) に関するいくつかの情報を必要とします。
最初の再帰定理(特にパート 1)は、Φ( F ) = Fとなる集合Fが存在することを述べています。集合F は、完全に自然数の順序付きペアで構成され、必要に応じて階乗関数fのグラフになります。
再帰演算子として書き直すことができる再帰方程式への制限は、再帰方程式が実際に最小不動点を定義することを保証します。たとえば、再帰方程式のセットを検討してください。これらの方程式はg (2) = 1を意味し、またg (2) = 0 を意味するため、これらの方程式を満たす関数 g は存在しません。したがって、これらの再帰方程式を満たす不動点gは存在しません。これらの方程式に対応する列挙演算子を作成することは可能ですが、それは再帰演算子にはなりません。
第一再帰定理の証明スケッチ
最初の再帰定理のパート 1 の証明は、空集合から始めて列挙演算子 Φ を反復することによって得られます。まず、 に対してシーケンスF kが構築されます。F 0 を空集合とします。帰納的に進めて、各kに対して、F k + 1をとします。最後に、Fを とします。証明の残りの部分は、 Fが再帰的に列挙可能であり、 の最小の不動点であることの検証で構成されます。この証明で使用されるシーケンスF k は、クリーネの不動点定理の証明のクリーネ連鎖に対応します。
最初の再帰定理の 2 番目の部分は、最初の部分から導かれます。Φ が再帰演算子であるという仮定は、Φ の不動点が部分関数のグラフであることを示すために使用されます。重要な点は、不動点Fが関数のグラフでない場合、F k が関数のグラフではない ようなk が存在するということです。
第二再帰定理との比較
第二再帰定理と比較すると、第一再帰定理はより強い結論を導きますが、それはより狭い仮説が満たされた場合に限られます。ロジャーズは第一再帰定理を弱い再帰定理、第二再帰定理を強い再帰定理と呼んでいます。 [3]
最初の再帰定理と 2 番目の再帰定理の違いの 1 つは、最初の再帰定理によって取得される不動点は最小不動点であることが保証されているのに対し、2 番目の再帰定理によって取得される不動点は最小不動点ではない可能性があることです。
2 つ目の違いは、最初の再帰定理は再帰演算子として書き直すことができる方程式のシステムにのみ適用されることです。この制限は、順序理論のクリーネの不動点定理における連続演算子への制限に似ています。2 番目の再帰定理は、任意の全再帰関数に適用できます。
一般化された定理
エルショフは数論の文脈において、クリーネの再帰定理が任意の前完全数に対して成り立つことを示した。[11]ゲーデル数とは計算可能関数の集合上の前完全数であるため、一般化された定理はクリーネの再帰定理を特別なケースとして導く。[12]
完全前番号付けが与えられた場合、2つのパラメータを持つ任意の部分計算可能関数に対して、1つのパラメータを持つ 全計算可能関数が存在し、
参照
- 表示的意味論では、別の最小不動点定理が最初の再帰定理と同じ目的で使用されます。
- 固定小数点コンビネータ。ラムダ計算では、第一再帰定理と同じ目的で使用されます。
- 対角線の補題は数学論理における密接に関連した結果です。
参考文献
- Ershov, Yuri L. (1999)。「第 4 部: 数学と計算可能性理論。14. 番号付けの理論」。Griffor, Edward R. (編)。計算可能性理論ハンドブック。論理学と数学の基礎の研究。第 140 巻。アムステルダム: Elsevier。pp . 473–503。ISBN 9780444898821. OCLC 162130533 . 2020年5月6日閲覧。
- ジョーンズ、ニール・D. (1997)。計算可能性と複雑性:プログラミングの観点から。マサチューセッツ州ケンブリッジ: MITプレス。ISBN 9780262100649. OCLC 981293265.
- クリーネ、スティーブン C. (1952)。メタ数学入門。Bibliotheca Mathematica。ノースホランド出版。ISBN 9780720421033. OCLC 459805591 . 2020年5月6日閲覧。
- ロジャース、ハートリー(1967年)。再帰関数の理論と実効計算可能性。マサチューセッツ州ケンブリッジ:MITプレス。ISBN 9780262680523. OCLC 933975989 . 2020年5月6日閲覧。
脚注
- ^ Kleene, Stephen C. (1938). 「序数の表記法について」(PDF) . Journal of Symbolic Logic . 3 (4): 150–155. doi :10.2307/2267778. ISSN 0022-4812. JSTOR 2267778. S2CID 34314018 . 2020年5月6日閲覧。
- ^ クリーネ 1952年。
- ^ロジャース 1967より。
- ^ ロジャース 1967、§11.2。
- ^ Soare, RI (1987).再帰的に列挙可能な集合と次数: 計算可能な関数と計算可能に生成された集合の研究。数理論理学の展望。ベルリンおよびニューヨーク市: Springer-Verlag。p . 88。ISBN 9780387152998. OCLC 318368332.
- ^ ジョーンズ1997年、229-230頁。
- ^ クリーネ 1952、352-353ページ。
- ^ Cutland, Nigel J. (1980). 計算可能性: 再帰関数理論入門.ケンブリッジ大学出版局. p. 204. doi :10.1017/cbo9781139171496. ISBN 9781139935609. OCLC 488175597 . 2020年5月6日閲覧。
- ^ ジョーンズ 1997.
- ^ Cutland, Nigel.計算可能性:再帰関数理論入門。
- ^ ヘンク・バレンドレグト;テルワイン、セバスティアン A. (2019)。「事前完全な番号付けに対する不動点定理」。純粋論理と応用論理の年代記。170 (10): 1151–1161。土井:10.1016/j.apal.2019.04.013。hdl : 2066/205967。ISSN 0168-0072。S2CID 52289429 。2020 年5 月 6 日に取得。1151ページ。
- ^ 英語の概要については、Ershov 1999、§4.14 を参照してください。
さらに読む
- Jockusch, CG ; Lerman, M.; Soare, RI ; Solovay, RM (1989). 「反復ジャンプを法とする再帰的に列挙可能な集合と Arslanov の完全性基準の拡張」. The Journal of Symbolic Logic . 54 (4): 1288–1323. doi :10.1017/S0022481200041104. ISSN 0022-4812. JSTOR 2274816. S2CID 32203705.
外部リンク
- スタンフォード哲学百科事典、 2012 年、 Piergiorgio Odifreddiによる「再帰関数」の項目。
