ライスの定理

索引トップ用語の索引ランキングカテゴリー

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/09/20 08:37 UTC 版)

直観的説明

Aが関数fを計算するプログラムであるとき、f_A=fと定義する。たとえばAが「a=x+yを計算した後、a+zを出力する」という趣旨のプログラムであると、 f_A(x,y,z)=x+y+zである。ただし、Aにxを入力しても(無限ループにはまる等の理由で)有限時間で停止しない場合は、f_A(x)=⊥と定義する。ここで「⊥」はプログラムが停止しない事を表す特殊な記号。

なお、2つのプログラムA、Bに対し、AとBがプログラムとしては別物であっても f_Aとf_Bが同じになる事がある事に注意されたい。たとえばBを「b=x+zを計算した後、b+yを出力する」という趣旨のプログラムとすると、 Bの見掛けは前述のAのそれとは異なるが、明らかにf_A(x,y,z)=f_B(x,y,z)=x+y+zである。

Fを関数に関する何らかの性質^[1]とする。たとえばFは「関数f_Aは恒等的に0である」とか「f_A(x)≧x³である」のようなものである。注意しなければならないのは、Fは関数f_Aに関する性質であってプログラムAに関する性質ではない事である。よってFは「プログラムAは300行以下である」のようなものであってはならない。

そして「Aが与えられたとき、f_Aは性質Fを満たすかを決定せよ」という問題を考える。ライスの定理は、Fが自明なものでない限り、この問題を常に正しく解く事できるプログラムは存在しない、というものである。ここで自明な性質とは、「全てのf_Aが満たす性質」と「いかなるf_Aも満たさない性質」の事である。 ^[2]

ライスの定理をより厳密に記述するため、記号を導入する。プログラム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は存在しない、というものである。

f_AがFを満たす ⇒ M(A)はYESを出力して停止する。
f_AがFを満たさない ⇒ M(A)はNOを出力して停止する。

ライスの定理でFの選び方を変える事で、以下の問題が全て決定不能な事が分かる。ここで「問題XXXが決定不能」とは、「問題XXXを解くプログラムは存在しない」の意。

与えられたプログラムが全ての入力に対して 0 を返すか
与えられたプログラムが少なくとも1つの入力に対して 0 を返すか
与えられたプログラムの出力は常に10ビット以下か

停止性問題の決定不能性定理との関係

ライスの定理は「停止性問題の決定不能性定理」の一般化である。ここで停止性問題とは、「プログラムAとデータxが与えられたとき、A(x)が有限時間で停止するかどうかを決定せよ」という問題である。また「停止性問題の決定不能性定理」とは、停止性問題を常に正しく解くプログラムは存在しない、という定理である。すなわち次のようなプログラムHは存在しない、という定理である。

A(x)が停止する ⇒ H(A,x)はYESを出力して停止する。
A(x)は停止しない ⇒ H(A,x)はNOを出力して停止する。

ライスの定理のFを「f_Aは⊥を出力しない」にした場合が「停止性問題の決定不能性定理」に一致する事を簡単に確かめられる。

脚注

^ 厳密には、Fは関数空間の部分集合Yを使って「f_AはYの元である」の形に書ける性質。
^ あるプログラムAが存在してf=f_Aと書ける関数fの事を計算可能関数という。Fが自明であるとは、厳密には、「任意の計算可能関数fに対し、fはFを満たす」と「任意の計算可能関数fに対し、fはFを満たさない」の事である。
^ $C$ を帰納的可算集合のクラスとするとき、計算可能な関数にたいするライスの定理で、 $\{\phi _{e}:{\textrm {dom}}\,\phi _{e}\in C\}$ というクラスを考えればよい。ただし ${\textrm {dom}}\,\phi _{e}:=\{x:\phi _{e}(x)\downarrow \}$ は $\phi _{e}$ の定義域であり、あらゆる帰納的可算集合は適当な $e$ を選ぶことにより ${\textrm {dom}}\,\phi _{e}$ と書くことが出来る。
^ Kreisel, G., Lacombe, D., Shoenﬁeld, J.R., 1959. Partial recursive functionals and effective operations. In: Heyting, A. (Ed.), Constructivity in Mathematics. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, pp. 290–297.
^ ^a ^b Kumabe, Masahiro; Mihara, H. Reiju (2008). “Computability of simple games: A characterization and application to the core”. Journal of Mathematical Economics 44 (3-4): 348–366. doi:10.1016/j.jmateco.2007.05.012. ISSN 03044068.
^ Kumabe, Masahiro; Mihara, H. Reiju (2008). “The Nakamura numbers for computable simple games”. Social Choice and Welfare 31 (4): 621–640. doi:10.1007/s00355-008-0300-5. ISSN 0176-1714.