ライスの定理の一般化
計算可能性理論において、ライス=シャピロの定理はライスの定理の一般化であり、ヘンリー・ゴードン・ライスとノーマン・シャピロにちなんで名付けられました。これは、部分計算可能関数の半決定可能性質が特定の部分関数上で真である場合、その性質が依然として真となる有限部分関数を抽出できることを述べています。
この定理の非公式な考え方は、プログラムの動作に関する情報を取得する「唯一の一般的な方法」はプログラムを実行することであり、計算は有限であるため、有限の数の入力に対してのみプログラムを試すことができるというものです。
これに密接に関連する定理としてクライゼル・ラコーム・ショーンフィールド・ツィティン定理(KLST定理)があり、これはゲオルク・クライゼル、ダニエル・ラコーム、ジョセフ・R・ショーンフィールド [1]とグリゴリ・ツィティン[2]によって独立に導かれたものである。
ライス・シャピロの定理。[3] : 482 [4] [5]を部分計算可能関数の集合とし、の添字集合(つまり、ある固定された許容番号付け に対してとなる添字の集合)が半決定可能 であるとする。すると、任意の部分計算可能関数 に対して、 が の有限部分関数(つまり、有限個の点で定義され、それらの点で と同じ値をとる部分関数)を含む場合のみ、が成り立つ。










クライゼル・ラコンブ・ショーンフィールド・ツィティンの定理。[3] : 362 [1] [2] [6] [ 7] [8] : 440 を 全計算可能関数の集合とし、のインデックス集合は、入力が全計算可能関数のインデックスであると約束して決定可能とする(すなわち、 が全であるようなインデックスを与えられたときに、であれば 1 を返し、そうでない場合は 0 を返す部分計算可能関数が存在する。 が全でない場合は定義する必要がない)。 2 つの全計算関数 は、がすべて に対して成り立つ場合、が「 まで一致する」という。すると、任意の全計算可能関数 に対して、 が存在し、 がまで と一致するすべての全計算可能関数 に対して、 が成り立つ。



















例
ライス・シャピロ定理によれば、与えられたプログラムが以下のいずれであるかは半決定可能でも半決定可能でもありません。
- すべての入力で終了する(普遍停止問題)。
- 有限個の入力で終了します。
- 固定された他のプログラムと同等です。
クライゼル・ラコンブ・ショーンフィールド・ツァイティンの定理によれば、常に終了すると仮定されるプログラムが、
- 常に偶数を返します。
- 常に終了する固定された他のプログラムと同等です。
- 常に同じ値を返します。
議論
これら2つの定理は密接に関連しており、ライスの定理とも関連しています。具体的には、
- ライスの定理は、部分計算可能関数の決定可能集合に適用され、それらは必ず自明であると結論付けられます。
- ライス・シャピロの定理は、部分計算可能関数の半決定可能集合に適用され、有限の数の値に基づいて要素のみを認識できると結論付けています。
- クライゼル・ラコンブ・ショーンフィールド・ツィティンの定理は、全計算可能関数の決定可能集合に適用され、ライス・シャピロの定理に類似した結論を導きます。
全計算可能関数の半決定可能集合について何が言えるのか疑問に思うのは当然である。驚くべきことに、これらはライス・シャピロ定理とクライゼル・ラコンブ・ショーンフィールド・ツァイティン定理の結論を検証する必要がない。以下の反例はリチャード・M・フリードバーグによるものである[9] [8] : 444
が定数ゼロ関数ではない計算可能関数全体の集合とし、がゼロとなる最大のインデックスを と定義すると、が定義され、各 に対してに等しいようなコードプログラムが存在する。定数ゼロ関数が追加された
集合を とする。










一方、定義により定数零関数を含むが、全 が計算可能であれば、 までは定数零関数と一致するような関数は存在しない。実際、 が与えられれば、が定義されるような任意のに対してよりも大きい値を に設定することで全関数を定義でき、に対してとなる。関数は値 を除いて零であり、したがって計算可能であり、 までは零関数と一致するが、構成上 には属さない。

















一方、プログラムと完全な約束が与えられた場合、 1つのタスクを実行して を半決定し(これは明らかに実行可能です)、別のタスクを実行してすべてのについて を半決定することで、 を半決定することが可能です。これは、ゼロ関数が2番目のタスクによって検出され、逆に2番目のタスクがtrueを返す場合、 がゼロであるか、インデックス までしかゼロではないかのいずれかであり、インデックス は を満たす必要があり、 の定義により が成り立つため、正しいと言えます。












ライス・シャピロ定理の証明
半決定可能な添え字集合を持つ部分計算可能関数の集合を とする。2つの含意を別々に証明する
。
上向きの閉鎖性
まず、が の有限部分関数であることを証明し、次にが有限であるという仮説は実際には役に立たない。





証明には、計算可能性定理に典型的な対角線論法を用いる。以下のようにプログラムを構築する。このプログラムは入力を受け取り、標準的なダブテール技法を用いて2つのタスクを並列に実行する。



- 最初のタスクは、自身について半決定する半アルゴリズムを実行します(クリーネの再帰定理により、自身のソースコードにアクセスできます)。この結果が最終的に true を返す場合、この最初のタスクは( への入力)について半計算する半アルゴリズムの実行を継続し、それが終了した場合、タスク全体として を返します。








- 2番目のタスクは、を半計算する半アルゴリズムを実行します。これが true を返す場合、タスク全体として を返します。




の場合、最初のタスクは決して完了しないため、 の結果は2番目のタスクによって完全に決定されます。したがって、は単純に となり、矛盾が生じます。これは であることを示しています。





したがって、両方のタスクは関連していますが、は のサブ関数であり、 が定義されている場合、 2 番目のタスクは を返しますが、 が定義されている場合、1 番目のタスクは を返すため、プログラムは実際には、つまりを計算し、したがって となります。








逆に、 が部分計算可能関数 を含む場合、 は の有限部分関数 を含むことを証明します。 を固定しましょう。入力を受け取り、以下のステップを実行する
プログラムを構築します。





- を半決定する半アルゴリズムの計算ステップを、自身を入力として実行します。この半アルゴリズムが終了して true を返す場合、無限ループします。



- それ以外の場合は、について半計算し、これが終了した場合は結果 を返します。



と仮定する。これは、最初のステップで使用される半決定の半アルゴリズムが決して真を返さないことを意味する。すると、は を計算し、これは仮定 と矛盾する。したがって、 が成り立ち、半決定のアルゴリズムは、あるステップ数 の後に で真を返す。部分関数 は、となる入力に対してのみ定義でき、そのような入力に対して を返すため、に属するの有限部分関数である。















クライゼル・ラコム・ショーンフィールド・ツェイティン定理の証明
予選
全関数が有限個の点を除いて常にゼロの値を取る場合、つまりすべての に対してとなる関数が存在する場合、その関数は究極的にゼロであると言われます。このような関数は常に計算可能であることに注意してください(入力が特定の定義済みリストに含まれているかどうかを確認し、含まれていない場合はゼロを返すだけで計算できます)。




最終的にゼロになるすべての全関数の計算可能な列挙を固定します。つまり、次のようになります。


- すべての に対して、関数は最終的にゼロになります。


- 最終的にゼロになるすべての全関数に対して、が存在する。



- 関数自体は完全に計算可能です。

標準的な手法で構築できます(たとえば、 を増やす場合、 によって制限され、より大きい入力に対して 0 となる最終的に 0 の関数を列挙します)。




最終的にゼロ関数による近似
を定理の文の とします。つまり、インデックスと完全である約束が与えられたときに、であるかどうかを決定するアルゴリズムが存在するような、完全計算可能関数の集合です。




まず、補題を証明します。すべての全計算可能関数、およびすべての整数に対して、 、およびまでと一致するような最終的にゼロとなる関数 が存在します。







この補題を証明するには、全計算可能関数と整数を固定し、ブール値をとします。入力を受け取り、以下の手順を実行する
プログラムを構築します。





- その場合は、 ;を返します。


- それ以外の場合は、を決定するアルゴリズムの計算ステップを実行し、 が返された場合はゼロを返します。




- それ以外の場合は、 を返します。

明らかに、は常に終了する、つまり は完全である。したがって、実行し続けるという約束は果たされる。




矛盾として、 と の一方が に属し、もう一方が に属していない、すなわち であると仮定します。すると、は を計算することがわかります。これは、 は何ステップ行っても では を返さないためです。したがって が得られ、これはとの一方が に属し、もう一方が に属していないという事実と矛盾します。この議論は であることを証明します。次に、2 番目のステップにより、 は十分に大きい に対して 0 を返すため、 は最終的に 0 になります。また、構築により (最初のステップにより) はまでと一致します。したがって、 を取ることができ、補題は証明されます。





















主な証拠
前の補題を用いて、クライゼル・ラコンブ・ショーンフィールド・ツァイティンの定理を証明できます。ここでも、定理の文と同様に、 を全計算可能関数、 をブール値 " " とします。入力を受け取り、以下のステップを実行する
プログラムを作成してください。





- を決定するアルゴリズムの計算ステップを実行します。



- これが特定のステップ数(最大)でを返す場合、およびになるまでと一致するを並列に検索します。そのような が見つかったら、 を返します。










- それ以外の場合 (ステップでを返さなかった場合) は、 を返します。





まず、がでを返すことを証明します。矛盾により、これが当てはまらない(が を返す、またはが終了しない)と仮定します。次に、 は実際に を計算します。特に、は完全であるため、で実行した場合に となるという約束は満たされ、ブール値 を返します。これは、つまり となり、仮定と矛盾します。















が に戻るのに必要なステップ数を とします。は定理の結論を満たすと主張します。つまり、までと一致するすべての計算可能関数に対して、が成り立ちます。矛盾点として、までと一致する計算可能関数が存在し、となると仮定します。













補題を再度適用すると、が までおよびと一致するような が存在する。 と は両方ともまでと一致するため、もまでと一致する。また、とより、 が成り立つ。したがって、 はプログラム の並列探索ステップの条件、すなわちが まで およびと一致するという条件を満たす。これは、2番目のステップの探索が常に終了することを証明している。が発見する値を に固定する。






















であることが分かります。確かに、 の2番目のステップがを返すか、3番目のステップが を返しますが、後者のケースは の場合にのみ発生し、までは がと一致することがわかります。








特に、は合計です。これにより、 で実行されるという約束が満たされ、でが返されます。






矛盾を発見しました。一方では、 のブール値は の戻り値であり、これは ですが、他方では があり、 であることがわかっています。






有効位相からの視点
整数上の任意の有限単項関数について、 の定義域で と一致する、定義済みのすべての部分再帰関数の「錐台」を で表します。




すべての部分再帰関数の集合に、これらの錐台 によって生成される位相を基底として付与する。すべての錐台 について、添字集合は再帰的に列挙可能であることに注意されたい。より一般に、すべての
部分再帰関数の
集合に対して、以下の式が成り立つ。


は、
frusta の再帰的に列挙可能な和集合である場合に限り、再帰的に列挙可能です。

アプリケーション
クライゼル・ラコンブ・ショーンフィールド・ツィーティン定理は、計算論的社会選択(より広義にはアルゴリズムゲーム理論)の基礎問題に応用されてきた。例えば、隈部と三原[10] [11]は、この結果を協力ゲーム理論と社会選択理論における単純ゲームにおけるナカムラ数の検討に適用している。
注記
- ^ ab クライゼル, ゲオルク;ラコム, ダニエル; ショーンフィールド, ジョセフ R. (1959). 「部分再帰関数と実効演算」.アーレンド・ヘイティング編. 『数学における構成性』 . 論理学と数学の基礎研究. アムステルダム: 北ホラント. pp. 290– 297.
- ^ ab Tseitin, Grigori (1959). 「構成的完全分離計量空間におけるアルゴリズム演算子」. Doklady Akademii Nauk . 128 : 49-52.
- ^ ab Rogers Jr., Hartley (1987). 『再帰関数の理論と実効計算可能性』 MIT Press. ISBN
0-262-68052-1。
- ^ Cutland, Nigel (1980).計算可能性:再帰関数理論入門. ケンブリッジ大学出版局.
; 定理7-2.16。
- ^ Odifreddi, Piergiorgio (1989).古典的再帰理論. 北ホラント.
- ^ Moschovakis, Yiannis N. (2010年6月). 「クリーネの驚くべき第二再帰定理」(PDF) . The Bulletin of Symbolic Logic . 16 (2): 189– 239. doi :10.2178/bsl/1286889124.
- ^ Royer, James S. (1997年6月). 「意味論 vs 構文 vs 計算:タイプ2多項式時間有界関数の機械モデル」. Journal of Computer and System Sciences . 54 (3): 424– 436. doi : 10.1006/jcss.1997.1487 .
- ^ ab Longley, John; Normann, Dag (2015).高階計算可能性. 計算可能性の理論と応用. Springer. doi :10.1007/978-3-662-47992-6. ISBN
978-3-662-47991-9。
- ^ フリードバーグ、リチャード M. (1958)。 「相対的な反例の再帰的表現」。科学アカデミーのコンテス。247 : 852–854 .
- ^ 隈部正之; 三原弘之 (2008). 「計算可能単純ゲームにおける中村数」.社会選択と福祉. 31 (4): 621. arXiv : 1107.0439 . doi :10.1007/s00355-008-0300-5. S2CID 8106333.
- ^ 隈部 正之; 三原 HR (2008). 「単純ゲームの計算可能性:その特徴づけと核心への応用」. Journal of Mathematical Economics . 44 ( 3–4 ): 348– 366. arXiv : 0705.3227 . doi :10.1016/j.jmateco.2007.05.012. S2CID 8618118.