ライスの定理
ここで自明な性質とは、「全てのfAが満たす性質」と「いかなるfAも満たさない性質」の事である。
ライスの定理をより厳密に記述するため、記号を導入する。 プログラムAにデータxを入力して実行する事をA(x)と書き、A(x)がyを出力するときy=A(x)と書く。
コンピュータではいかなるデータも0と1の数字で表し、したがってプログラム自身も0と1の数字で表せる。 以下記号を簡単にする為、プログラムAを数字で表したものも、Aと書く。 よって例えばプログラムA、Bに対し、「A(B)」は、「プログラムBを表す数字をbとし、Aにbを入力して実行する」の意である。
ライスの定理は、Fを自明でない任意の性質とするとき、次のようなプログラムMは存在しない、というものである。
fAがFを満たす ⇒ M(A)はYESを出力して停止する。
fAがFを満たさない ⇒ M(A)はNOを出力して停止する。
ライスの定理でFの選び方を変える事で、以下の問題が全て決定不能な事が分かる。 ここで「問題XXXが決定不能」とは、「問題XXXを解くプログラムは存在しない」の意。
与えられたプログラムが全ての入力に対して 0 を返すか
与えられたプログラムが少なくとも1つの入力に対して 0 を返すか
与えられたプログラムの出力は常に10ビット以下か
ライスの定理の主張は次の通り:
決定問題 D F {\displaystyle D_{F}} が決定可能である必要十分条件は、 F = ∅ {\displaystyle F=\emptyset } または F = P ( 1 ) {\displaystyle F=\mathbf {P} ^{(1)}} である。
D F {\displaystyle D_{F}} が非自明ならば D F {\displaystyle D_{F}} もしくはその補集合はm-困難である。すなわち任意の帰納的可算集合を多対一還元可能である。
ライスの定理はアクセプタブルでないナンバリングに対しては必ずしも成立しないことに注意しなければならない。例えばフリードバーグ・ナンバリングは単射であるから「自然数 e {\displaystyle e} は定数関数 x ↦ 0 {\displaystyle x\mapsto 0} の指標である」という性質は決定可能である。このことはライスの定理の結論に反する。
ライスの定理を停止性問題の決定不能性定理に帰着する。 証明は背理法による。
ライスの定理が成り立たなかったとすると、ある非自明な性質Fが存在し、 fAがFを満たすかどうかを決定できるプログラムMが存在する。 すなわち、fAがFを満たすときM(A)=YESで、 そうでないときM(A)=NOである。
Fは関数fAの性質であってA自身の性質では無かった。 したがってfA=fBを満たす任意のプログラムA、Bに対し、 fAがFを満たす必要十分条件はfBがFを満たす事である。 よってMの定義より、次の命題が成り立つ。
fA=fBならM(A)=M(B)。
無限ループを利用するなどして停止しないプログラム意図的に作るのは簡単である。 そこでUを、いかなる入力に対しても停止しないプログラムとする。 すると明らかに、fUは恒等的に⊥を出力する。
F'を、「Fを満たさない」という性質とする。 必要ならFをF'と取り換える事で、M(U)=NOと仮定してよい。
Fは非自明な性質なので、Fを満たすfVが存在する。 Mの性質より、M(V)=YESである。