ライスの定理

計算可能性理論において、ライスの定理は、プログラムの非自明な意味的特性はすべて決定不可能であると述べている。意味的特性は、構文的特性 (たとえば、「プログラムにはif-then-else文が含まれているか?」) とは異なり、プログラムの動作に関する特性 (たとえば、「すべての入力に対してプログラムは終了するか?」) である。非自明な特性は、すべてのプログラムに対して真でも偽でもない特性である。

この定理は、停止問題の決定不可能性について一般化しています。これは、プログラムの静的解析の実現可能性に広範囲な影響を及ぼします。これは、たとえば、特定のプログラムが正しいかどうかをチェックするツールを実装したり、エラーなしで実行したりすることは不可能であることを意味します (たとえば、プログラムの正確さを常に過大評価したり、常に過小評価したりするツールを実装することは可能ですが、実際には、何がそれほど問題ではないかを決定する必要があります)。

この定理は、1951 年にシラキュース大学の博士論文でこの定理を証明したヘンリー・ゴードン・ライスにちなんで名付けられました。

ライスの定理は、どのタイプの静的解析を自動的に実行できるかについて理論的な限界を定めています。プログラムの構文と意味論を区別することができます。構文は、プログラムの記述方法の詳細、つまり「意図」であり、意味論は、プログラムの実行時の動作、つまり「拡張」です。ライスの定理は、その特性が自明 (すべてのプログラムに当てはまるか、すべてのプログラムに当てはまらない) でない限り、構文ではなく意味論のみに依存するプログラムの特性を決定することは不可能であると主張しています。

ライスの定理によれば、プログラムと仕様を入力として受け取り、プログラムが仕様を満たしているかどうかをチェックして、他のプログラムにバグがないことを自動的に検証するプログラムを作成することは不可能です。

これは、特定の種類のバグを防ぐことが不可能であることを意味するものではありません。たとえば、ライスの定理は、チューリング完全な動的型付けプログラミング言語では、型エラーがないことを検証することが不可能であることを意味します。一方、静的型付けプログラミング言語は、静的に型エラーを防ぐ型システムを備えています。本質的には、これはそれらの言語の構文（広い意味で）の特徴として理解されるべきです。プログラムの型チェックを行うには、そのソースコードを検査する必要があります。この操作は、プログラムの仮説的なセマンティクスにのみ依存するわけではありません。

一般的なソフトウェア検証の観点から言えば、これは、特定のプログラムが特定の仕様を満たしているかどうかをアルゴリズム的にチェックすることはできないが、プログラムが正しいことを証明する追加情報で注釈を付けること、または検証を可能にする特定の制限された形式でプログラムが記述されることを要求し、このように検証されたプログラムのみを受け入れることができることを意味します。型安全性の場合、前者は型注釈に対応し、後者は型推論に対応します。型安全性を超えて、この考え方は、ホーア論理などの証明注釈を通じてプログラムの正しさの証明につながります。

ライスの定理を回避する別の方法は、完全ではないものの、多くのバグをキャッチする方法を探すことです。これが抽象解釈の理論です。

検証のさらに別の方向性はモデル検査ですが、これは有限状態プログラムにのみ適用でき、チューリング完全な言語には適用できません。

φ を部分計算可能関数の許容番号とする。P を のサブセットとする。次のことを仮定する。 ${\displaystyle \mathbb {N} }$

1. Pは非自明です。つまり、Pは空でもそれ自体でもありません。${\displaystyle \mathbb {N} }$
2. P は外延的です。つまり、すべての整数mとnに対して、φ _m = φ _nであれば、m ∈ P ⟺ n ∈ Pです。

そうするとPは決定不能となる。

インデックス セットの観点から、より簡潔な記述を行うことができます。決定可能なインデックス セットは ∅ と のみです。 ${\displaystyle \mathbb {N} }$

自然数nを受け取り、自然数P ( n )を返すプログラムPが与えられた場合、以下の質問は決定不可能である。

• P は与えられたnで終了するか？（これが停止問題です。）
• P は0 で終了しますか?
• P はすべての nで終了しますか(つまり、P は 合計ですか)?
• P はすべての入力で終了し、0 を返しますか?
• P は何らかの入力で終了し、0 を返しますか?
• P はすべての入力に対して終了し、同じ値を返しますか?
• P は与えられたプログラムQと同等でしょうか?

矛盾に対して、 は非自明で、外延的で、計算可能な自然数の集合であると仮定します。自然数と自然数があります。およびのとき、によって関数を定義します。クリーネの再帰定理により、となる が存在します。すると、 の場合、 となり、 であるための外延性と矛盾します。また逆に、 の場合、 となり、 であるためこれも外延性と矛盾します。 ${\displaystyle P}$${\displaystyle a\in P}$${\displaystyle b\notin P}$${\displaystyle Q}$${\displaystyle Q_{e}(x)=\varphi _{b}(x)}$${\displaystyle e\in P}$${\displaystyle Q_{e}(x)=\varphi _{a}(x)}$${\displaystyle e\notin P}$${\displaystyle e}$${\displaystyle \varphi _{e}=Q_{e}}$${\displaystyle e\in P}$${\displaystyle \varphi _{e}=\varphi _{b}}$${\displaystyle P}$${\displaystyle b\notin P}$${\displaystyle e\notin P}$${\displaystyle \varphi _{e}=\varphi _{a}}$${\displaystyle a\in P}$

具体的には、プログラムpを調べ、p が整数d を受け取ってd ²を返す平方関数の実装であるかどうかを間違いなく判断するアルゴリズムがあるとします。この証明は、プログラムの動作に関するその他の重要な特性 (つまり、意味的かつ重要な特性) を判断するアルゴリズムがある場合でも同様に機能し、以下に一般的な説明を示します。

主張は、平方プログラムを識別するアルゴリズムを停止する関数を識別するアルゴリズムに変換できるというものです。入力aとi を受け取り、入力iが与えられたときにプログラムa が停止するかどうかを判定するアルゴリズムについて説明します。

これを決定するアルゴリズムは概念的に単純です。引数nを取る新しいプログラムt (の記述) を構築します。このプログラム t は、(1) 最初に入力iでプログラムaを実行し( aとi は両方ともtの定義にハードコードされています)、(2) 次にnの二乗を返します。 a ( i ) が永久に実行される場合、nに関係なく、 t はステップ (2) に到達することはありません。したがって、 ステップ (1) が終了した場合にのみ、 t は二乗を計算する関数であることがわかります。二乗を計算するプログラムを確実に識別できると仮定しているため、 aとiに依存するtがそのようなプログラムかどうかを判断できます。つまり、プログラムa が入力iで停止するかどうかを決定するプログラムを取得しました。停止決定アルゴリズムはt を実行せず、その記述を二乗識別プログラムに渡すだけであり、このプログラムは仮定により常に終了することに注意してください。 tの記述の構築も常に終了する方法で実行できるため、停止決定も必ず停止します。

停止 (a,i) {
   t(n) を定義する {
     a(i)
     n×nを返す
   }
   is_a_squaring_function(t)を返す
 }

この方法は、平方を計算する関数を認識できるかどうかに特に依存しているわけではありません。認識しようとしていることを実行できるプログラムがあれば、 a への呼び出しを追加してtを取得できます。平方根を計算するプログラム、月々の給与を計算するプログラム、または入力 が与えられたときに停止するプログラムを認識する方法があったかもしれません"Abraxas"。いずれの場合も、停止問題を同様に解決できます。

正式な証明では、アルゴリズムは文字列上の部分関数を定義し、それ自体が文字列で表現されると仮定します。文字列aで表されるアルゴリズムによって計算される部分関数は、 F _aで示されます。この証明は、背理法によって行われます。つまり、アルゴリズムによって決定される重要な特性があると仮定し、停止問題を決定できることを示しますが、これは不可能であり、したがって矛盾です。

ここで、P ( a ) はF _aの重要なプロパティを決定するアルゴリズムであると仮定します。一般性を失うことなく、P ( no-halt ) = "no"と仮定できます。ここで、 no-halt は停止しないアルゴリズムの表現です。これが正しくない場合、プロパティPの否定を計算するアルゴリズムPに当てはまります。ここで、P は重要なプロパティを決定するため、アルゴリズムF _bとP ( b ) = "yes" を表す文字列bが存在することになります。次に、アルゴリズムH ( a , i ) を次のように 定義できます。

1.アルゴリズムT ( j ) を表す文字列tを構築し、

• TはまずF _a ( i )の計算をシミュレートし、
• TはF _b ( j )の計算をシミュレートし、その結果を返します。

2. P ( t )を返す。

ここで、 H が停止問題を決定することを 示すことができます。

• aで表されるアルゴリズムが入力iで停止すると仮定します。この場合、F _t = F _bであり、P ( b ) = "yes" であり、 P ( x )の出力はF _xのみに依存するため、 P ( t ) = "yes"となり、したがってH ( a , i ) = "yes" となります。
• aで表されるアルゴリズムが入力iで停止しないと仮定します。この場合、F _t = F _no-halt、つまり定義されない部分関数です。P ( no-halt ) = "no" であり、 P ( x )の出力はF _xのみに依存するため、P ( t ) = "no" となり、したがってH ( a , i ) = "no" となります。

停止問題は決定不可能であることが知られているので、これは矛盾であり、 aによって表される関数の非自明な特性を決定するアルゴリズムP ( a ) が存在するという仮定は誤りでなければなりません。

• 停止の問題
• ライス・シャピロ定理とクライゼル・ラコンブ・ショーンフィールド・ツィーティン定理、ライスの定理の一般化
• スコット・カリー定理、ラムダ計算におけるライスの定理の類似物
• チューリングの証明

• ホップクロフト、ジョン E. ;ウルマン、ジェフリー D. (1979)、『オートマトン理論、言語、計算入門』、アディソン・ウェズレー、pp. 185–192
• ライス、HG（1953）、「再帰的に列挙可能な集合のクラスとその決定問題」、アメリカ数学会誌、74（2）：358–366、doi：10.1090/s0002-9947-1953-0053041-6、JSTOR  1990888
• ロジャース、ハートリー・ジュニア（1987）、再帰関数と実効計算可能性の理論（第2版）、マグロウヒル、§14.8