# 停止性問題 ## 定義 停止性問題(Halting Problem)とは、与えられた任意のプログラムが、中断されない限り永遠に実行し続けるか、それとも停止するかを判定する一般的な procedure を求める問題である。本書は文字列 procedure(ASCII文字列を入力に取るprocedure)に限定した特別な形で扱う。ASCII文字列sをそのままprocedure Ps(sをコンパイルした結果)とみなす規約のもとで、No-halt := {s ∈ ASCII | Ps を s に適用すると停止しない} と定義し(定義7.2.1)、集合Sが「認識可能(recognizable)」とは、Sに属する文字列に適用すると停止し、属さない文字列に適用すると停止しないような procedure が存在することと定義する。定理7.2.2は No-halt が認識可能でないことを主張し、証明はCantorの定理(§7.1.3)と同型の対角線論法による: f(s) := {t ∈ ASCII | Ps がtに適用されると停止する} という総関数fを考えると、定義より s ∈ No-halt iff s ∉ f(s) が成り立つ。No-haltを認識するprocedure Ps0が存在すると仮定すると No-halt = f(s0) となり、s = s0 を代入して s0 ∈ f(s0) iff s0 ∉ f(s0) という矛盾が生じる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 7 Infinite Sets]] ch.7 §7.2) この結果から、任意のプログラミング言語について、その言語で書かれた完全な静的型検査器・最適化器・実行時解析 procedure は存在しないことが導かれる(型検査器が完全であれば、それを使って停止性を判定できてしまうため)。また、ある言語(例: C++)で書かれたprocedureが別の言語(例: Java)向けの解析を完全に行えるという逃げ道もない。なぜなら、一方の言語で他方の仮想機械を書けるならば、その仮想機械を通じて同じ矛盾に帰着するからである。(Source: ch.7 §7.2) ## 横断的知見 (この concept は本 ingest が初出のため、複数ソースの突き合わせによる横断的知見はまだない。決定不能性・計算可能性理論に触れる他章・他ソースが ingest された際にここへ追記する。) ## 未解決の問い - 本章は「実行時挙動全体(overall run-time behavior)」に関する性質のみ認識不可能だとし、脚注で「最初の100命令以内に停止するプログラムの集合」のような部分的な性質は認識可能だと注記している(§7.2 脚注3)。「overall」の境界を厳密に特徴づける一般的な基準(Riceの定理に相当するもの)は本章では示されていない。後続の計算理論の文献でこの一般化がどう定式化されるか。 - 本書はこの章で「停止性問題」という名前をAlan Turingに帰属させていない(第8章 Number Theory で Turing の生涯と計算可能性理論への貢献が別途紹介される)。歴史的にはTuringの1936年論文が停止性問題の起源とされるが、本章の記述だけからはその関連は追えない。第8章の [[Alan Turing]] エントリとの接続を確認する必要がある。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 7 Infinite Sets]] / [[@2015__MIT__Mathematics for Computer Science - Chapter 8 Number Theory]](Alan Turingの生涯と計算可能性理論への貢献) - 概念: [[対角線論法]] —— 停止性問題の非認識可能性の証明技法そのもの。 / [[濃度]] —— 同じ対角線論法がCantorの定理の証明に使われる姉妹概念。 - 実体: [[Alan Turing]] ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 7, §7.2.