導入
計算可能性理論では、ライスの定理は、チューリング完全プログラミング言語の表示意味論に関する非自明な性質 (つまり、常に真または常に偽であるとは限らない) は決定不可能であると述べています。これは停止問題を一般化したものです。
この定理は、ライスによる最初の出版物 (1953 年) の系B を「直観的に」再定式化したものです。
説明と直感的な証明
まず第一に、 chビット文字列を入力としてprogプログラムが停止するかどうかを知ることができるhaltプログラムは存在しないことを覚えておいてください (証明については、halt 問題のページを参照してください)。より一般的な結果が得られます。
いくつかの表記を指定します。 prog(ch) は、入力としてch を使用したprogの実行が終了した場合に出力として取得される文字列です。 ch_prog はプログラムprog をエンコードする文字列として表し、 ch1,ch2 は2 つの文字列ch1とch2 を連結することによって得られる文字列を指定します。
たとえば、 prog(ch)の呼び出しが完了してchによってエンコードされた整数の2 乗をエンコードした場合にはsquare(ch_prog,ch) が1 を返し、そうでない場合には 0 を返すような平方プログラムが存在するとします。
次に、次のような無秩序なプログラムを構築できます。ここで、 progは任意のプログラム、 ch2 は任意の文字列です。
トラブル(ch1)
1.prog(ch2)を実行します
2. ch1でコード化された整数の 2 乗を返します。
prog が入力としてch2で停止した場合にのみ、 trouble(ch1)が存在し、 ch1によってコード化された整数の 2 乗をエンコードすることがわかります。したがって、 square が存在する場合、 halt が存在します。しかし私たちは停止が存在しないことを知っています。
上の例では、 square を任意の関数に置き換えることができ、ライスの定理を証明できます。任意の関数fおよび任意のプログラムprogについて、 progがfの移植であることを確認するプログラムはありません。
正式な定義
前編
ここでは、チューリング完全 プログラミング言語を使用していることを前提としています (直感的に計算できるすべての関数、チャーチ・チューリングの論文を参照、この言語でプログラムできます)。 φ( x , y ) を入力y ∈ ℕ に対するプログラムxの評価の結果とする。プログラムx が入力yに対して終了しない場合、関数 φ はこれらの入力に対して定義されていないため、必然的に部分関数となり、φ( x , y ) は必ずしも何かを指定する必要はありません (特別な値を示すために ⊥ を追加できます)。終了しません」）。 ℕ の ℕ の部分関数 (一部はどこでも定義できますが、以下では詳細は指定しません) を計算する一連のプログラムをP で表すことにします。 y ↦ φ( x , y ) がPに含まれるようなxの集合が再帰的であると仮定します。この場合、 P = ∅、またはP はすべてのプログラム (ℕ から ℕ への部分関数を計算する) の集合です。
言い換えれば、ライスの定理によれば、拡張プログラムのセット、つまり、与えられた部分関数が含まれるとすぐにその部分関数を計算するすべてのプログラムを含む、自明ではない、つまりプログラムのセットとは異なり、∅ 、は再帰セットではありません。
本当にそれを形式化したいのであれば、プログラムが何であるかを言わなければなりません。このタイプのプロパティの場合は、かなり大雑把な表現で十分です。クリーンによって始められた計算可能性(または再帰) の理論では、プログラムは整数によってコード化されます (コンピューター サイエンスでは、これらは実際に文字のシーケンスであり、したがってビットのシーケンスであり、したがって最終的には整数です)。関数 φ は、部分的なクリーネ列挙関数です。これは、ℕ ↦ ℕ のすべての部分再帰関数を列挙する ℕ × ℕ ↦ ℕ の部分再帰関数であり、したがって、関数 φ x : y ↦ φ( x , y ) になります。 。整数x は、関数 φ xのインデックス(またはコード) と呼ばれます。同じ関数を計算するプログラムが明らかに無数に存在するのと同様 (結果に影響を与えない命令をプログラムに好きなだけ追加できます)、部分再帰関数には無限の手掛かりがあります。
整数のセット (したがって部分再帰関数のインデックス) W は、同じ部分再帰関数のインデックスである 2 つの整数iとjが両方ともW内にあるか、両方ともWの外側にある場合に外延的であると言われます。
- ∀ i , j ∈ ℕ [( i ∈ Wおよび φ i = φ j ) ⇒ j ∈ W ]
ライスの定理は次のように述べています。
- ライスの定理。 ℕ の非自明な拡張サブセット(ℕ および ∅ とは異なります) は再帰的ではありません。
整数に関して厳密な意味で解釈されるこれらの概念はすべて、コーディングの影響を受けやすいことに注意してください。したがって、これらは計算可能な関数の結果です。
第二部
再帰的に列挙可能な集合の観点から見ると、ライスの定理は、これらの集合上の自明でない性質は決定不可能であると述べています。このような性質は、A が B に含まれるような再帰的に列挙可能なすべての集合 A および B について、P(A) -> P(B) が成立する場合に限り、単調であると言われます。たとえば、「A は有限集合である」は単調ではありませんが、「A には要素 x が含まれています」は単調です。したがって、再帰的に列挙可能なセット上の非単調プロパティは、再帰的に列挙可能(または半決定可能) ではありません。
