ライスの定理

ライスの定理は、計算機科学における計算可能関数の理論に関する定理で、 定められた性質Fを満たすかどうかを任意の部分計算可能関数について判定する方法は存在しない、というもの。 名称の由来は Henry Gordon Rice から。

1. 直観的説明
--------

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

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

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

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

ライスの定理をより厳密に記述するため、記号を導入する。 プログラム//A//にデータ//x//を入力して実行する事を//A//と書き、//A//が//y//を出力するとき//y//=//A//と書く。

コンピュータではいかなるデータも0と1の数字で表し、したがってプログラム自身も0と1の数字で表せる。 以下記号を簡単にする為、プログラム//A//を数字で表したものも、//A//と書く。 よって例えばプログラム//A//、//B//に対し、「//A//」は、「プログラム//B//を表す数字を//b//とし、//A//に//b//を入力して実行する」の意である。

ライスの定理は、//F//を自明でない任意の性質とするとき、次のようなプログラム//M//は存在しない、というものである。

//f////A//が//F//を満たす ⇒ //M//はYESを出力して停止する。
//f////A//が//F//を満たさない ⇒ //M//はNOを出力して停止する。ライスの定理で//F//の選び方を変える事で、以下の問題が全て決定不能な事が分かる。 ここで「問題XXXが決定不能」とは、「問題XXXを解くプログラムは存在しない」の意。

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

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

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

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

3. ライスの定理の証明
------------

ライスの定理を停止性問題の決定不能性定理に帰着する。 証明は背理法による。

ライスの定理が成り立たなかったとすると、ある非自明な性質//F//が存在し、//f////A//が//F//を満たすかどうかを決定できるプログラム//M//が存在する。 すなわち、//f////A//が//F//を満たすとき//M//=YESで、 そうでないとき//M//=NOである。

//F//は関数//f////A//の性質であって//A//自身の性質では無かった。 したがって//f////A//=//f////B//を満たす任意のプログラム//A//、//B//に対し、//f////A//が//F//を満たす必要十分条件は//f////B//が//F//を満たす事である。 よって//M//の定義より、次の命題が成り立つ。

//f////A//=//f////B//なら//M//=//M//。無限ループを利用するなどして停止しないプログラム意図的に作るのは簡単である。 そこで//U//を、いかなる入力に対しても停止しないプログラムとする。 すると明らかに、//f//Uは恒等的に⊥を出力する。

//F'//を、「//F//を満たさない」という性質とする。 必要なら//F//を//F'//と取り換える事で、//M//=NOと仮定してよい。

//F//は非自明な性質なので、//F//を満たす//f//Vが存在する。//M//の性質より、//M//=YESである。

//A//を任意のプログラムとし//x//を任意のデータとするとき、//T////A//,//x//を以下のようなプログラムとする。
0. 入力//y//を受け取る。
1. //s//=//A//を計算する。
2. //t//=//V//を計算する。
3. //t//を出力する。

さらに//H//を、プログラム//A//と//x//とを入力されると、//M//を実行するアルゴリズムとする。

//H//は停止性問題を解く。というのも、前述した命題より、

//A//が停止すれば、//T////A//,//x//はステップ1を抜けて先に進み、//V//を実行する。よって。したがって//H//=//M//=//M//=YES。
//A//が停止しなければ、//T////A//,//x//はステップ1が停止しないので、は恒等的に⊥。よって。したがって//H//=//M//=//M//=NO。

4. ライスの定理の厳密な記述
---------------

を計算可能関数全体の集合とし、 をアクセプタブル・ナンバリングとする：

は全射である；
対応 は計算可能である；
上の条件を満たす任意の に対して、計算可能関数 が存在して が成り立つ。 は計算可能関数へのゲーデル数割り当てであると解釈できる。

の部分集合と、計算可能関数の属性を同一視する。 すなわち集合 に対し、 であるときだけ計算可能関数 が属性 //F// を持つと解釈する。

に対し、「自然数 が与えられたとき、 であるかどうかを決定せよ」という決定問題を と書く。

ライスの定理の主張は次の通り：

決定問題 が決定可能である必要十分条件は、 または である。
が非自明ならば もしくはその補集合はm-困難である。すなわち任意の帰納的可算集合を多対一還元可能である。ライスの定理はアクセプタブルでないナンバリングに対しては必ずしも成立しないことに注意しなければならない。例えばフリードバーグ・ナンバリングは単射であるから「自然数 は定数関数 の指標である」という性質は決定可能である。このことはライスの定理の結論に反する。

5. ライスの定理に類する結果
---------------

ライスの定理は、帰納的可算集合  を決定可能なやりかたで二分することの不可能性について述べたものと考えられる。 この定理のバリエーションとして、帰納的可算集合のかわりに帰納的集合  を考えたものもある。 これらの結果の類似性はそれぞれの定理が以下の主張をしていることから言える。

もともとのライスの定理は、「ある帰納的可算集合のクラスが"決定可能"ならば、与えられた帰納的可算集合がそのクラスに属するかどうかを判定するためには、ゼロ個の について、 がその集合に属するかどうかを調べればよい」ことを主張する。
帰納的集合にかんする定理は、「ある帰納的集合のクラスが"決定可能"ならば、与えられた帰納的集合がそのクラスに属するかどうかを判定するためには、有限個の について、 がその集合に属するかどうかを調べればよい」ことを主張する。類似定理のフォーマルな記述は省略する。 

この結果は、 協力ゲーム理論あるいは社会選択理論といった分野において、シンプルゲームの中村ナンバーの考察などに応用されている 。

ライスの定理を精緻化したものとしてライス＝シャピロの定理がある。この定理はインデックス集合が帰納的可算である為にはある種の有限性を持つことが必要であることを示す。

6. 脚注
-----

7. 参考文献
-------

Rice, H. G. "Classes of Recursively Enumerable Sets and Their Decision Problems." Trans. Amer. Math. Soc. 74, 358-366, 1953.

8. 関連項目
-------

停止性問題
ライス＝シャピロの定理

9. 外部リンク
--------

Eric W. Weisstein, [1] at MathWorld.