8.2 停止性問題

どこまでも大きくなる無限が積み上がった塔はせいぜい情報科学者にとってのロマンチックな研究対象でしかないものの、無限に関する結果を導いた議論は計算の理論で非常に重要な役割を果たす。対角線論法を使うと、どうやっても計算で解けない問題がいくつも存在することが示せる。

まず、プログラムを操作する手続きは情報科学の技術として一般的である事実を思い出してほしい。例えばコンパイル (compilation) と呼ばれる処理は Java, C++ , Python といった高レベルプログラミング言語で書かれたテキスト形式のプログラムを受け取り、そのプログラムに記述された処理を現実のハードウェアで高速に実行する低レベル命令で書いたプログラムを生成する。同様に、インタープリタ (interpreter) や仮想マシン (virtual machine) と呼ばれるプログラムは特定のコンピューター用のプログラムを受け取り、その動作を別種のコンピューターでシミュレートする。コンパイラには、特定の実行時エラーが起こらないことを確認する型検査 (type-checking) や、生成されるプログラムを高速にする最適化 (optimizing) といった処理が組み込まれている。

不可能なことが知られている基礎的な処理として、プログラムの実行時における全体的な振る舞いの完全な解析 (例えば型検査や最適化) がある。本節では、この事実を停止性問題 (halting problem) と呼ばれる標準的な例を使って説明する。以降の文章に含まれる「プログラム」は読者が知っている好きなプログラミング言語 ── Python, Java, C++, \(\ldots\) ── で書かれたプログラムだと思って読んでほしい。

実行が開始されたプログラムが何らかの理由で実行を止める ── 最終的な値が生成された、入力待ちの状態になった、エラーによる割り込みを受けた、あるいは単にフリーズした ── とき、プログラムは停止 (halt) したと言うことにする。つまり停止しないプログラムは永遠に実行続け、CPU サイクルと電力を (OS から割り込みを受けない限り) 消費し続ける。停止性問題は、任意のプログラムを受け取って「そのプログラムが停止するかどうか」を判定する一般的な問題である。

停止するプログラムを検出する単純な方法は、少なくとも理論上は存在する: 停止するまで実行すればいい。ただし、実際には普通に実行するだけでは十分でない: プログラムが「静かに」フリーズする状況を検出できない。そのため、インタープリタや仮想マシンで実行をシミュレートして、フリーズを含む全ての種類の停止を認識できる形でプログラムを実行する必要がある。任意のプログラムの実行をシミュレートできるインタープリタや仮想マシンは珍しくない技術なので、プログラムの停止を検出する一般的な方法は確かに存在する。

難しいのはプログラムが停止しないことの検出である。プログラムの実行をシミュレートしている任意の時点において、その実行がいつ停止するかは当然分からない。そのため、どれだけ実行のシミュレートを続けてもプログラムが停止しないと確実に言えることはない。

停止しないプログラムを確実に検出する方法は存在するだろうか？ 任意のプログラムを解析し、それが停止するかどうかを正しく言い当てるプログラム解析ツールは書けるだろうか？ 答えは「No」である。これから見るように、そういった「非停止検出」ツールは書けないことが標準的な対角線論法で証明できる。停止しないプログラムを検出する任意の手法は必ず不完全となる運命にある。停止するプログラムを誤って「停止しない」と認識するか、一部のプログラムに対して解答を生成できない (入力すると無限ループとなるプログラムが存在する)。

対角線論法を使うための準備として、ここからは文字列手続き (string procedure) と呼ばれる処理だけを考える。文字列手続きは 256 個の ASCII アルファベットが並んだ単一の文字列 \(s \in \text{ASCII}^{\ast}\) を受け取る。単純な例として、任意の文字が二つ連続で使われる二重文字列 (double letter string) を受け取ったときにだけ停止する文字列手続きが考えられる。例えば、この手続きは \(\texttt{aaCC33}\), \(\texttt{zz++ccBB}\) を受け取ると停止し、\(\texttt{aa;bb}\), \(\texttt{b33}\), \(\texttt{AAAAA}\) を受け取ると停止しない。

文字列を受け取った手続きが停止するとき、その手続きは受け取った文字列を認識 (recognize) すると言う。この用語を使う文脈では、文字列の集合を (形式formal) 言語 (language) と呼ぶ。手続き \(P\) が認識する言語を \(\operatorname{lang}(P)\) と表す:

何らかの手続き \(P\) に対する \(\operatorname{lang}(P)\) に等しい言語を認識可能 (recognizable) な言語と呼ぶ。例えば、上記の例では二重文字列が認識可能だと仮定していた。

あらゆるプログラムが \(\text{ASCII}^{\ast}\) に属する文字列として書けると仮定することには何の問題もない ── 多くのプログラムは ASCII 文字列としてコンピューターに入力される。文字列 \(s \in \text{ASCII}^{\ast}\) が文字列手続きを表すとき、その手続きを \(P_{s}\) で表す。文字列 \(s\) をコンパイルした結果の実行可能形式を表すのが \(P_{s}\) だと考えても構わない¹。また、\(\text{ASCII}^{\ast}\) に属する任意の文字列が何らかの文字列手続きを表すとした方が議論の都合がいいので、\(s \in \text{ASCII}^{\ast}\) が文字列手続きとして正しくパースできないときは何らかのデフォルトの文字列手続き (例えば、任意の入力に対して停止しない手続き) を \(P_{s}\) と定める。

文字列手続きだけを考えるとき、一般的な停止性問題は「文字列 \(s\), \(t\) が与えられたとき、手続き \(P_{s}\) が \(t\) を認識するかどうかを判定せよ」と表現できる。標準的な対角線論法のアプローチに従い、言語 \(\text{No-halt}\) を定義する:

任意の文字列 \(s \in \text{ASCII}^{\ast}\) に対して、\(P_{s}\) が認識する言語と \(\text{No-halt}\) は \(s\) を含むかどうかが異なる。よって \(\text{No-halt}\) を認識する手続きは存在しない:

もう少し丁寧に定理 8.2.2 の証明を追ってみよう。まず \(\text{No-halt}\) の定義より、全ての文字列 \(s \in \text{ASCII}^{\ast}\) で次の関係が成り立つと分かる:

ここから背理法を使って \(\text{No-halt}\) が認識可能でないと示す。\(\text{No-halt}\) が認識可能だと仮定する。このとき、\(\text{No-halt}\) を認識する手続き \(P_{s_{0}}\) が存在する:

これと関係 \(\text{(8.4)}\) から次の関係を得る:

ここで \(s \in \text{ASCII}^{\ast}\) は任意だから、\(s = s_{0}\) とすれば次の明らかな矛盾が得られる:

これで停止性問題が説明できた: 以上の議論はあらゆるプログラミングに適用できる。入力に受け取った Java プログラムが停止するかどうかを判定する Java プログラムを書くことは不可能である。同様に、入力に受け取った Python プログラムが停止するかどうかを判定する Python はどうやっても書けない。他の言語に関しても同じことが言える。

入力に受け取るプログラムと異なる言語でプログラムを書けば、この論理的な制限を受けずに済むのではないかと思ったかもしれない。言い換えれば、Java プログラムの停止性を判定する手続きは C++ でなら書けるのではないだろうか？ C++ を使えばコンピューターのメモリを Java より細かく操作できるので、これはありそうな話に思える。しかし、この「抜け穴」は存在しない。プログラミング言語の実装を学んだ経験があるなら、C++ プログラムのシミュレーターを Java で書けることを理解できるだろう。つまり、もし Java プログラムの停止性を判定する手続きを C++ で書けたなら、その手続きは Java で書かれた C++ シミュレーターを通して Java でも実行できてしまう。よって、そのような手続きは C++ でも書けはしない。どんなプログラミング言語を使ったとしても、あなたのお気に入りの言語で書かれたプログラムの停止性を判定する手続きは絶対に書けない。\(\text{No-halt}\) の認識は純粋に計算で可能な処理の範疇に収まっていないのである。

さらに、認識できないのは \(\text{No-halt}\) だけではない。プログラムを実行したときの完全な振る舞いに依存する任意の性質²を漏れなく認識する手続きが存在すれば、それを利用して \(\text{No-halt}\) を認識する手続きが作れてしまう。この事実に対する証明は示さないものの、いくつかの例を問題 8.35 に示してある。

例えば、多くのコンパイラは「静的」な型検査をコンパイル時に実行し、プログラムが実行時に型エラーを起こさないことを確かめる。型検査を通過したプログラムは実行時に型エラーを起こさないことが保証される。しかし、「型エラーが起こらない」というプログラムを実行したときの振る舞いを完全に認識するのは不可能なので、型検査は型エラーを本当は起こさないプログラムを拒否すると分かる。つまり結論は「完璧な型検査は存在しない」である ── あなたは必ず型検査を上回れる！

一方で、プログラムを解析する現実的な手続きを考えるときは話が別になる。任意の、ありとあらゆるプログラムの解析は論理的に不可能だとしても、現実に書かれる興味深いプログラムを上手く解析するプログラムを書くことが不可能と示されたわけではない。実際、そういった「興味深い」プログラムの多くは自身の処理を確認しやすいように解析が容易な形で書かれる。

実のところ、本節で説明した理論的制限が現実のプログラム解析に課すハードルの高さは現在でもはっきりと分かっていない。しかし、一般的なプログラム解析手法に関する一つの視点がこの理論から提供されるのは確かである。つまり、誰かが「私たちの手法はプログラムを完璧に解析できます」と発言した場合、その人物は次のいずれかである可能性が高い:

• 売り上げや研究費のために、考案手法の強みを誇張 (または捏造) している。

• 本当は認識している技術的制限に触れないことで、話を単純化している。

• おそらくもっとも多いのは、現実的なケースに対する考案手法の高い有用性に目がくらんで、必ず存在する理論的限界について考察するのを忘れている。

今後プログラムの解析・検証・最適化の手法に関して都合が良すぎる話を聞いたときは、まだ聞いてない話が必ずあると思った方がよい。