数学の基礎
再帰関数とチューリング機械
アルゴリズムで計算可能な関数を正確に定義する形式的モデル。
直観機械は何を計算できるか?
電卓は足し算と掛け算ができ、コンパイラは型検査ができ、AIは(時に)質問に答えられる。しかし、どんなに賢いアルゴリズムでも決して計算できない関数は存在するだろうか?アラン・チューリングの答えは「ある」——それは「アルゴリズム」の精密な数学的モデル、すなわちテープ、読み書きヘッド、有限の規則表からなるチューリング機械から得られた。一見異なる2つの形式化、再帰関数(合成と再帰によって単純な部品から構成される)とチューリング機械(機械的な段階的過程)は、まったく同じ関数のクラスを計算することが判明した——これはチャーチ–チューリングの提唱、すなわちこれこそが「計算可能なものすべて」であるという主張の強力な証拠である。
大学原始再帰関数と -再帰関数
定義: 原始再帰関数
原始再帰関数とは、零関数、後続関数 、およびすべての射影を含み、合成と原始再帰の下で閉じている、 の関数の最小のクラスである: と が与えられたとき、再帰 、 は新しい原始再帰関数 を定義する。加法、乗法、冪乗、そして固定された上限を持つあらゆる「forループ」プログラムはすべて原始再帰的である——そしてすべての原始再帰関数は全域的(すべての入力に対して定義される)であり、各入力について有界なステップ数で停止する。
すべての計算可能関数——停止しないかもしれないものも含めて——を捉えるには、もう一つの演算子を加える。**-再帰(一般再帰)関数は非有界最小化**を加える: は となる最小の を返し、 と探索する——そしてそのような が存在しなければ単に決して返らない。これこそが -再帰関数に停止しない能力を与えるものであり、クリーネの定理はそれらがチューリング機械とまったく同じ(部分)関数のクラスを計算することを示している。
| クラス | 構成要素 | 必ず停止するか? | 例 |
|---|---|---|---|
| 原始再帰 | 合成+有界再帰 | はい、常に全域的 | 冪乗 |
| 一般(-)再帰 | 原始再帰+非有界 | いいえ、無限に回る場合がある | アッカーマン関数 |
| チューリング計算可能(部分的) | 状態+テープ+遷移規則 | いいえ、-再帰と厳密に一致 | あらゆるアルゴリズム |
すべてのプログラム索引 と入力 について、(プログラム を入力 で実行すること)が停止するかどうかを常に停止して正しく出力するアルゴリズム は存在しない。
なぜ正しいのか?
これは、どのアンチウイルスソフト、コンパイラ、IDEも、無限ループ、デッドコード、「この関数は常にクラッシュする」といったことを完全に一般的な形で検出できない数学的理由である——今日の工学の限界ではなく、揺るぎない数学の壁である。
証明
背理法で、そのような判定器 が存在すると仮定する:(停止する)なら 、(永遠に走る)なら であり、 自身は常に停止し正しい答えを出す。
を用いて、入力 に対し次のように動作する新しいプログラム を作る: を計算し、 なら は無限ループに入り、 なら は直ちに停止する。 は から実効的に構成される(単に に if 文とループを加えただけ)ので、あるプログラム索引 を持つ、すなわち 。
ここで自己言及的な問いを立てる: は停止するか?
場合1: が停止するなら、 の正しさにより 。しかし の定義により は を入力 で無限ループさせる——すなわち は停止しない。矛盾。
場合2: が停止しないなら、 の正しさにより 。しかし の定義により は を入力 で停止させる——すなわち は停止する。矛盾。
どちらの場合も矛盾するので、 が存在するという仮定は偽である。停止問題は決定不可能である。
発展ライスの定理
停止問題は、より広い現象のほんの一例に過ぎない。部分計算可能関数の性質 が、プログラム が計算する関数 のみに依存し、ソースコード自体には依存しないとき意味論的と呼び、ある計算可能関数がそれを持ちある関数が持たないとき非自明と呼ぶ。
部分計算可能関数のすべての非自明な意味論的性質 について、集合 は決定不可能である。
なぜ正しいのか?
この一つの定理は、「このプログラムはゼロ関数を計算するか」「このプログラムは全域関数を計算するか」「これら2つのプログラムは等価か」といった、プログラムの振る舞いに関する無数の自然な問いに対するアルゴリズムを、それぞれ別々の対角線論法なしに、一挙に排除する。
証明
一般性を失うことなく、いかなる入力に対しても決して停止しないプログラムが計算する至る所未定義の関数 が性質 を持たないと仮定する——そうでなければ、 が決定可能であることとちょうど同値な補性質 で議論する。 は非自明なので、その関数 が性質 を持つプログラム を一つ固定する。
背理法で、 がある判定アルゴリズム によって決定可能であると仮定する(プログラム索引が与えられると、 は停止し、そのプログラムの関数が性質 を持つかどうかを正しく報告する)。 に停止問題を還元し、定理1と矛盾させる。
任意の組 に対し、実効的に(単純な文字列操作——クリーネの s-m-n 定理により)新しいプログラム を構成する。 は任意の入力 について:まずプログラム を入力 で実行するシミュレーションを行い、そのシミュレーションが停止したら、次にプログラム を入力 でシミュレーションしてその出力を出力する。
2つの場合を調べる。 が で停止する場合: を で実行するシミュレーションは終了するので、 はその後すべての入力で とまったく同じように振る舞う、すなわち ——これは性質 を持つ( は意味論的なので計算される関数のみに依存し、 は を持つ)。 が で停止しない場合: を で実行するシミュレーションは決して終わらないので、 はいかなる入力 についても のシミュレーション段階に決して到達しない。したがって は至る所未定義の関数 であり、仮定によりこれは性質 を持たない。
よって: が で停止する が性質 を持つ が「はい」と答える。 は計算可能なので、「 から を計算し、 を実行する」というアルゴリズムは停止問題を決定してしまう——定理1と矛盾する。したがってそのような は存在しない: は決定不可能である。
大学実世界での応用と具体例
コンパイラの最適化器は「このコードは到達可能か」「この変数の値は意味を持つか」といったことを判定しなければならない——ライスの定理により、これらは完全に一般的な形では決定不可能であり、まさにそれゆえ実際のコンパイラは保守的な近似を用いる(生きたコードを削除する危険を冒すより、本当に死んでいるコードの一部を残しておく)。ビジービーバー関数 ——状態の停止するチューリング機械が停止するまでにとりうる最大のステップ数——は具体的で計算不可能な関数である:既知の値は 、、、 であり、2024年には共同プロジェクト Busy Beaver Challenge(Tristan Stérin らが主導し、「mxdys」という偽名の貢献者による Coq 検証済みの証明を伴う)が を確立した——この「単純」に見える組合せ論的問いですら、一般的なアルゴリズムでは決して計算できず、場合ごとにしか計算できないことを示している。
例: アッカーマン関数 を展開する
規則 、 に対し 、 に対し を用いて を段階的に計算し、アッカーマン関数が全域的でありながら原始再帰的ではない理由を説明せよ。
解答
第三の規則により 。まず が必要で、第二の規則により 。
(第二と第一の規則で2回展開)。よって なので 。
であり、。よって 。したがって 。
最上位に戻る:; と展開;よって 。したがって 。
アッカーマン関数は全域的であることが証明されている(最終的に必ず の場合に帰着する)ので、一般再帰関数のクラスに属する——しかしあらゆる原始再帰関数より速く増大する(例えば 、 はすでに指数のタワーである)。あらゆる原始再帰関数が最終的にある固定された によって支配されることが示せるので、原始再帰関数が 自身に等しくなることはあり得ない—— 演算子ではなく、この対角線論法風の支配論法こそが、全域的であるにもかかわらずアッカーマン関数を原始再帰の外に置く理由である。
例: 停止問題を「このプログラムはhelloを出力するか?」に還元する
「プログラム が与えられたとき、 を(入力なしで)実行すると文字列 `hello` が出力されることがあるか?」という問題が、ライスの定理を使わずに、停止問題からの直接還元により決定不可能であることを示せ。
解答
背理法で、 を実行すると `hello` が出力されるかどうかを決定するアルゴリズム が存在すると仮定する。 を用いて停止問題を決定し、定理1と矛盾させる。
任意のプログラム と入力 が与えられたとき、実効的に新しいプログラム (入力不要)を構成する: を で実行するシミュレーションを行い、それが停止したら は `hello` を出力して停止する。
が で停止する場合:シミュレーションは終了するので は出力段階に到達し `hello` を出力する。 が で停止しない場合:シミュレーションは決して終わらないので は出力段階に決して到達せず `hello` を決して出力しない。
よって が で停止する が「はい」と答える。 は計算可能なので、「 を構成し を実行する」ことで停止問題が決定できてしまう——定理1と矛盾する。よって は存在し得ない:「helloを出力する」問題は決定不可能である。(これはまさにコンパイラ解析のパターンである:「このコード行は到達可能か」も同じ形をしている。)
を用いると はいくつか?
コンパイラ設計にとって停止問題の決定不可能性がもたらす帰結はどれか?
ライスの定理が適用されない性質はどれか?
停止問題の決定不可能性の対角線論法による証明で、何が矛盾を引き起こすか?
参考文献
- Wikipedia contributors (2024). Halting problem
- Wikipedia contributors (2024). Rice's theorem
- Wikipedia contributors (2024). Ackermann function