計算可能性理論では、ライスの定理は、チューリング完全プログラミング言語の表示意味論に関する非自明な (つまり、常に真または常に偽であるとは限らない) 特性は決定不可能であると述べています。これは停止問題を一般化したものです。
この定理は、Rice (1953) による最初の出版物からの系B を「直観的に」再定式化したものです。
説明と直感的な証明
まず第一に、 chビット文字列を入力としてprogプログラムが停止するかどうかを知ることができるhaltプログラムは存在しないことを覚えておいてください (証明については、halt 問題のページを参照してください)。より一般的な結果が得られます。
いくつかの表記法を指定しましょう。 prog(ch) は、 chを入力としてprog を起動してループしない場合に出力として取得される文字列です。 ch_prog はプログラムprog をエンコードする文字列であり、 ch1,ch2 は、 2 つの文字列ch1とch2 。
たとえば、ループしない場合にはsquare(ch_prog,ch)が 1 を返し、 prog(ch)はchによってエンコードされた整数の2 乗をエンコードし、それ以外の場合は 0 を返すような平方プログラムが存在するとします。
次に、次のような無秩序なプログラムを構築できます。ここで、 progは任意のプログラム、 ch2 は任意の文字列です。
トラブル(ch1)
1.prog(ch2)を実行します
2. ch1でコード化された整数の 2 乗を返します。
prog が入力としてch2で停止した場合にのみ、 trouble(ch1)が存在し、 ch1によってコード化された整数の 2 乗をエンコードすることがわかります。したがって、 square が存在する場合、 halt が存在します。しかし私たちは停止が存在しないことを知っています。
上の例では、 square を任意の関数に置き換えることができ、ライスの定理を証明できます。どの関数fおよびプログラムprogについても、 progがfの移植であることを確認するプログラムはありません。
実用的な影響
この定理の実際的な定式化は、プログラムの最終結果に関連する興味深い (自明ではない) 特性に対して、プログラムのソース コードが与えられた場合に、この特性を満たすかどうかを決定できるアルゴリズムは存在しないということです。このような決定不可能なプロパティには次のようなものがあります。
- 「プログラムは実行時エラーで終了しません」
- 「プログラムは仕様と比較して正しい結果を計算します」
言い換えれば、静的プログラム分析の方法では、すべてのプログラムがどのようなものであっても、またテストされるプロパティがどのようなものであっても、有限時間内に信頼できる結果を与えることはできません。ただし、この制限は、必ずしも特定のサイズのプログラムにのみ適用されるわけではありません。
たとえば、最適かつ安全なガベージ コレクション (未使用のメモリを解放するソフトウェア) は不可能です。実際、メモリを解放するかどうかは、システムの将来の動作に依存しており、予測することは不可能です。これは、すべてのガベージ コレクション技術が保守的であり、メモリ内に不要なブロックを保持し、メモリ リークを引き起こす可能性がある理由を説明しています。
したがって、次の C 言語プログラム ( p が他の場所に介入しないと仮定します) では、メモリ ブロックを割り当てた直後に解放する必要があるかどうかを決定することは、 f()で停止する問題を決定することと同じです。
char *p = malloc(1000); f(); *p = 1;
正式な定義
前編
ここでは、チューリング完全 プログラミング言語を使用していることを前提としています (直感的に計算できるすべての関数、チャーチ・チューリングの論文を参照、この言語でプログラムできます)。 φ( x , y ) を、入力y ∈ ? に対するプログラムxの評価の結果とする。プログラムx が入力yに対して終了しない場合、関数 φ はこれらの入力に対して定義されていないため、必然的に部分関数となり、φ( x , y ) は必ずしも何かを指定する必要はありません (特別な値を示すために ⊥ を追加できます)。終了しません」）。の部分関数（一部はどこでも定義できますが、以下では詳しくは説明しません）を計算する一連のプログラムをP で表すことにします。で ？。 xの集合が y を満たすと仮定します。 φ( x , y ) はPに再帰的に含まれます。この場合、 P = ∅ となります。ここで、 P はすべてのプログラムの集合です (? の ? から部分関数を計算します)。
言い換えれば、ライスの定理によれば、拡張プログラムのセット、つまり、与えられた部分関数が 1 つ含まれるとすぐにその部分関数を計算するすべてのプログラムを含む、そして自明ではない、つまりプログラムのセットとは異なります。および ∅ は再帰集合ではありません。
本当にそれを形式化したいのであれば、プログラムが何であるかを言わなければなりません。このタイプのプロパティの場合は、かなり大雑把な表現で十分です。クリーンによって始められた計算可能性(または再帰) の理論では、プログラムは整数によってコード化されます (コンピューター サイエンスでは、これらは実際に文字のシーケンスであり、したがってビットのシーケンスであり、したがって最終的には整数です)。関数 φ は部分的な Kleene 列挙関数です。これは ? の部分的な再帰関数です。 × ? ? ?これは ? のすべての部分再帰関数をリストします。 ? ?、関数 φ x : y はどれですか? φ( x , y )。整数x は、関数 φ xのインデックス(またはコード) と呼ばれます。同じ関数を計算するプログラムが明らかに無数に存在するのと同様 (結果に影響を与えない命令をプログラムに好きなだけ追加できます)、部分再帰関数には無限の手掛かりがあります。
整数のセット (したがって部分再帰関数のインデックス) W は、同じ部分再帰関数のインデックスである 2 つの整数iとjが両方ともW内にあるか、両方ともWの外側にある場合に外延的であると言われます。
- ∀ i , j ∈ ? [( i ∈ Wおよび φ i = φ i ) ⇒ j ∈ W ]
ライスの定理は次のように述べています。
- ライスの定理。 ? の拡張サブセットnon-trivial (? や ∅ とは異なります) は再帰的ではありません。
整数に関して厳密な意味で解釈されるこれらの概念はすべて、コーディングの影響を受けやすいことに注意してください。したがって、これらは計算可能な関数の結果です。
第二部
再帰的に列挙可能な集合の観点から見ると、ライスの定理は、これらの集合上の自明でない性質は決定不可能であると述べています。このような性質は、A が B に含まれるような再帰的に列挙可能なすべての集合 A および B について、P(A) -> P(B) が成立する場合に限り、単調であると言われます。たとえば、「A は有限集合である」は単調ではありませんが、「A には要素 x が含まれています」は単調です。したがって、再帰的に列挙可能なセット上の非単調プロパティは、再帰的に列挙可能(または半決定可能) ではありません。
ライスの定理の証明
停止問題の決定は、再帰的に列挙可能な集合上の自明でないプロパティの決定に帰着できることが示されています。私たちは、それを受け入れるチューリングマシンによって再帰的に列挙可能なセットを表します。 P を、再帰的に列挙可能なセット上の決定可能かつ自明ではないプロパティとする。 P(∅)=”False” とします (そうでない場合は、P の否定を使って同じように推論します)。したがって、P を満たす再帰的に列挙可能な集合 A が存在します。K を A を受け入れるチューリング マシンとしましょう。P は決定可能であるため、チューリング マシン MP が存在します。チューリング マシン MP は、チューリング マシンの任意の表現に対して、次のことを決定します。本機が受け付けたセットがPを満たすか否か。
それ以降、入力 x が後に続くチューリング マシン M の表現を入力として受け取るチューリング マシン H を構築します。 H のアルゴリズムは次のとおりです。
- 1. 入力 d に対して次のようなチューリング マシン T の表現を構築します。
- x に対する M の実行をシミュレートします。
- d に対する K の実行をシミュレートし、結果を返します。
- 2. T の表現で MP の実行をシミュレートし、結果を返します。
M が x で停止した場合、T によって受け入れられるセットは A です。このセットは P を満たすため、アルゴリズムの第 2フェーズは「True」を返します。 M が x で停止しない場合、T によって受け入れられる集合は ∅ です。このセットは P を満たさないため、アルゴリズムの第 2 フェーズは「False」を返します。
したがって、マシン H は停止問題を完全に計算します。これは決定不可能であるため、矛盾により、P は決定不可能です。
第二部のデモンストレーション
同様に、停止問題の否定の半決定は、再帰的に列挙可能な集合上の任意の非単調特性の半決定に帰着できることを示します。
P を非単調で半決定可能な特性とする。したがって、次のようにチューリング マシン MA および MB によってそれぞれ計算される 2 つの再帰的に列挙可能なセット A および B が存在します。
- AはBに含まれる
- 満足P
- B は P を満たしません。
さらに、チューリング マシン MP が存在します。チューリング マシン MP は、チューリング マシンの任意の表現に対して、このマシンによって受け入れられる再帰的に列挙可能な集合が P を満たす場合に停止して受け入れます。
それ以降、チューリング マシン M の表現とそれに続く入力 x を入力として受け取るチューリング マシン H を構築できます。そのアルゴリズムは次のとおりです。
- 1 入力 y に対して次のようなチューリング マシン T の表現を構築します。
- 1 並列実行
- MA オン y
- y の MB
- M以上x
- 2 y を受け入れる
- MA は y または else を受け入れます
- MB は y を受け入れ、かつ M は x で停止します
- 1 並列実行
- 2 T の表現に対して MP を実行し、結果を返します。
「並列実行」とは、マシン T が y でステップ MA を実行し、次に y で MB のステップを実行し、次に x で M のステップを実行し、次に y で MA の 2 番目のステップを実行することを意味します。言い換えれば、あるマシンの計算ステップを他のマシンの計算ステップと「インターリーブ」します。
M が x で停止する場合、MA または MB が y を受け入れる場合に限り、T は y を受け入れます。また、A は B に含まれるため、これは、y が B に属する場合に限り、ということになります。 したがって、T は集合 B を正確に受け入れます。仮説により、P は検証されません。その結果、MP は T を受け入れません。(P は半分決定可能であると想定されているため、MP はまったく停止しない可能性もあります) M が x で停止しない場合、T は次の場合にのみ y を受け入れます。 y は A に属します。したがって、T は、仮説により P を満たす集合 A を正確に受け入れます。その結果、MP は T を受け入れます (したがって、半決定可能性の定義により停止することになります)。したがって、マシン H は停止問題の否定を計算します。これは半決定可能ではありません。矛盾により、P は半決定可能ではありません。