停止問題
CONCEPT → BOOK
この概念を本でたどる
『チューリング——コンピュータ科学の父』で「停止問題」を読む
アンドリュー・ホッジス
ホッジスはこの証明を、チューリングの最初の偉大な発見として詳述する。数学的直観と厳密な証明が融合した瞬間として描かれ、ヒルベルトの決定問題(Entscheidungsproblem)への否定的回答として位置づけられる。
この本とのつながりを見る停止問題とは、任意のプログラムとその入力が与えられたとき、そのプログラムが最終的に停止するか、それとも永遠に動き続けるかを一般的に判定するアルゴリズムは存在しない、と主張する定理である。1936年にアラン・チューリングが対角線論法を用いて証明した。一見素朴な問いに見えるが、その否定的な答えは計算という営みそのものに内在する限界を明らかにし、以後のコンピュータ科学の土台の一つとなった。
ヒルベルトの決定問題から
停止問題の背景には、数学者ダフィット・ヒルベルトが1928年に提起した「決定問題」(Entscheidungsproblem)がある。与えられた数学的命題が真か偽かを、有限の手続きで機械的に判定するアルゴリズムは存在するか、という問いである。チューリングは1936年の論文「計算可能数について、その決定問題への応用」でこれに答えるため、「計算」そのものを数学的に定義し直す必要に迫られた。そこで考案されたのが、後にチューリングマシンと呼ばれる抽象的な計算模型である。
対角線論法による証明
証明は背理法で進む。任意のプログラムとその入力を受け取り、そのプログラムが停止するかどうかを常に正しく判定するプログラムHが存在すると仮定する。このHを使えば、任意のプログラムを受け取り、「Hがそのプログラムに自分自身を入力したとき停止すると判定すれば無限ループに入り、停止しないと判定すれば直ちに停止する」という新しいプログラムQを作ることができる。ではQにQ自身を入力として与えるとどうなるか。Hが停止すると判定すればQは無限ループに入ってしまい判定と食い違い、停止しないと判定すればQは直ちに停止して、これもまた食い違う。どちらの場合も矛盾が生じるため、そのようなHは存在しえない。カントールの対角線論法を計算の世界に応用したこの構成により、決定問題は決定不可能性を持つことが示された。ほぼ同時期にアロンゾ・チャーチもラムダ計算を用いて独立に同じ結論へ到達しており、両者の符合はのちにチャーチ=チューリングのテーゼとして定式化されることになる。
ソフトウェアという現実への反響
停止問題は抽象数学だけの話ではない。あるプログラムが無限ループに陥るかどうかを完璧に見抜く汎用ツールは、原理的に作れないということを意味するからだ。静的解析やコンパイラの警告、バグ検出ツールがどれほど洗練されても、あらゆるコードに対して「停止する/しない」を確実に判定することはできない。実務のツールはこの限界を織り込んだ上で、判定を保留するか、型付けされた言語のサブセットなど制限された対象領域で近似的な保証にとどめる設計を取っている。停止問題は、ソフトウェア検証という営みが抱える宿命的な不完全性の出発点である。
なぜ今も停止問題なのか
自動生成されたコードや自律的に動くエージェントの安全性を機械的に保証したいという要求は、チューリングの時代よりむしろ切実になっている。だが停止問題が示すのは、どんなプログラムの振る舞いも事前に完全には予測できないという原理的な壁が今も変わらず存在するという事実だ。チューリング——コンピュータ科学の父が描くように、この証明は若き日のチューリングが成し遂げた最初の大きな発見であり、直観の閃きと論理の厳密さが融合した瞬間だった。計算に何ができないかを知ることは、計算に何ができるかを正しく理解するための出発点でもある。
概念ネットワーク
左右にスワイプして全体を見られます。 線の太さは共通する本の数を表しています。ノードをクリックすると概念ページに移動します。
この概念を扱う本(1冊)
アンドリュー・ホッジス
ホッジスはこの証明を、チューリングの最初の偉大な発見として詳述する。数学的直観と厳密な証明が融合した瞬間として描かれ、ヒルベルトの決定問題(Entscheidungsproblem)への否定的回答として位置づけられる。
隣の概念から、別の本へ
知脈でいま「停止問題」に結びついているのは『チューリング——コンピュータ科学の父』の1冊です。 ただしこの本のなかで隣り合う概念をたどると、別の本へ出られます。