4.1 停機問題與對角線法#

前言：那個「檢查程式會不會當掉」的夢#

每個工程師都夢想過一個完美的工具：餵入任何程式與輸入，它告訴你「這會不會當機/跑不完」。靜態分析工具、linter、模型檢查器都在逼近這個夢，但 1936 年圖靈證明：這個夢在一般形式下數學上不可能。這就是停機問題（halting problem）的不可判定性——本書全部「不可能定理」的原型。

對角線法（diagonalization）則是證明的技術核心，血統上承自 Cantor 1891 年證明實數不可數，經哥德爾 1931 年的自指句，被圖靈改造成機器世界的武器。

對角線法：從 Cantor 講起#

Cantor 要證明：正整數到實數之間不存在一一對應（實數「更多」）。反證：設列出所有實數

\[ \begin{aligned} r_1 &= 0.\,3\,1\,4\,1\,5\,9\ldots\\ r_2 &= 0.\,2\,7\,1\,8\,2\,8\ldots\\ r_3 &= 0.\,1\,4\,1\,4\,2\,1\ldots\\ &\;\;\vdots \end{aligned} \]

構造 \(d\) ：第 \(i\) 位取與 \(r_i\) 第 \(i\) 位不同的數字。 \(d\) 與每一個 \(r_i\) 至少在第 \(i\) 位不同，故不在列表中——列表必不完備。這個「沿對角線反轉」的動作是通用模板：任何自稱完備的清單，都能被對角線構造打破。

停機問題：定理與證明#

定義： \(A_{TM} = \{\langle M, w\rangle \mid M \text{ 是圖靈機且 } M \text{ 在輸入 } w \text{ 上接受}\}\)

定理（Turing 1936）： \(A_{TM}\) 不可判定。

證明（反證 + 對角線）：假設存在判定器 \(H(\langle M,w\rangle)\) 總是停機並正確回答。構造「攪局機」 \(D\) ：

D(⟨M⟩):
    if H(⟨M, ⟨M⟩⟩) == accept  then  reject
    else                           accept

現在餵入 \(D\) 自己的編碼：

\[ D(\langle D \rangle) \text{ 接受} \iff H(\langle D, \langle D\rangle\rangle) \text{ 拒絕} \iff D(\langle D \rangle) \text{ 不接受} \]

自相矛盾。故 \(H\) 不存在。 \(\blacksquare\)

flowchart LR
    H["假設的判定器 H(M,w)"] --> D["攪局機 D: H說會接受我就拒絕"]
    D -- "D(⟨D⟩)?" --> X["自我矛盾: 接受 iff 不接受"]
    X --> C["故 H 不存在; A_TM 不可判定"]

注意證明中 \(H\) 可以是任意慢的——我們沒有假設效率，只假設「總會給出正確答案」。因此不可判定性比任何 NP 難度都更根本。

半可判定性：r.e. 與 co-r.e. 的鴻溝#

\(A_{TM}\) 雖不可判定，但可半判定：模擬 \(M(w)\) ，接受就接受——不拒絕就跑到天荒地老。所以：

\(A_{TM}\) 是遞迴可枚舉（r.e.）的；
\(\overline{A_{TM}}\) 不是 r.e. 的（若兩者皆 r.e.，交錯模擬可判定 \(A_{TM}\) ，矛盾）。

這給出兩個極有用的判準：

補語技巧： \(L\) 可判定 \(\iff\) \(L\) 與 \(\bar{L}\) 皆 r.e.。 歸約技巧：若 \(A \le_m B\) 且 \(B\) 可判定，則 \(A\) 可判定。逆否： \(A\) 不可判定 \(\Rightarrow\) \(B\) 不可判定。

Rice 定理（4.3 節）把歸約技術系統化，使我們不再需要每題重新對角線。

停機問題的實務面目#

工程中「不可判定」以各種偽裝出現，以下問題全部互歸約於停機問題：

死碼偵測：if (false) { ... } 之外的任何不可達碼判定；
空語言問題：這個正則表達式/程式會不會接受任何輸入？（正則可判定、任意程式不可判定）；
測試覆蓋的完備性：能否自動確認「所有路徑都測過」？路徑數可能無窮；
無限迴圈偵測：正好就是停機問題；
病毒/惡意行為判定：對任意程式判定「是否會執行惡意動作」不可判定（4.3 節 Rice 定理的直接推論）——防毒軟體因此必然是啟發式的，這不是工程不努力，是數學的牆。

理論也給出建設性的對策：限定問題的範圍就能重獲可判定性——

① 限定模型:    正則/CFG 的成員與空性 → 可判定 (第2、3章)
② 限定資源:    限時 n 步內是否接受 → 可判定 (直接模擬 n 步)
③ 限定結構:    有限狀態程式 / 存取受限 (pushdown) 系統 → 模型檢查可判定
④ 限定驗證義務: 不判定正確性, 改為「給定斷言, 找反例」(bounded model checking → SAT)

這張對策表是形式驗證工業（SPIN、CBMC、TLA+、AWS 的 formal methods 團隊）的設計哲學：在不可判定的汪洋中圈出可判定的島嶼。

虛擬碼：對角線結構的實作示範#

def halting_problem_solver_fake(M_code, w):
    """這個函式不可能被實作 (僅示意其簽名)"""
    ...

def diagonal_program(M_code):
    """攪局機 D 的現代寫法"""
    if halting_problem_solver_fake(M_code, M_code) == "accept":
        while True: pass          # reject: 無限迴圈
    else:
        return                    # accept: 立即停止

def self_test():
    try:
        return diagonal_program(code_of(diagonal_program))
    except RecursionError:
        pass   # 任何「實作」都會在這裡或無限迴圈中露出馬腳

「模擬器無法判定自己是否停機」（1.2 節的 timeout 分支）在此得到解釋：不是模擬器寫得不夠好，而是問題本身無解。

歷史意義與後續發展#

判定問題的落幕：停機問題不可判定 + 歸約到一階邏輯有效性（ \(A_{TM} \le\) validity）⇒ Church 的判定問題負解（1936）。圖靈的論文最後一節完成了這一步。
Goedel–Turing 對照：哥德爾的不完備可以從停機問題直接導出——若算術一致且完備，我們就能機械判定所有真命題，進而解停機問題（程式停機對應一個算術命題），矛盾。兩大定理實為一體兩面。
Kolmogorov 複雜性與 Chaitin： \(\Omega\) 常數（停機機率的編碼）是不可計算的實數，其位元序列等價於停機問題——不可判定性滲入「資訊壓縮的極限」（沒有萬能壓縮器）。
複雜性理論的起點：停機問題問「能否計算」，時間階層定理（5.1 節）問「計算多快」——對角線法經精緻化（延遲對角線）證明 \(P \subsetneq \mathrm{EXPTIME}\) 等結果。對角線法至今仍是唯一的「分離類別」技術，也是 P vs NP 進展受挫的原因之一（5.3 節 relativity 障礙）。

重點整理#

停機問題不可判定：對角線構造 \(D\) 使任何假想的判定器 \(H\) 自我瓦解。
\(A_{TM}\) 是 r.e. 但其補不是——r.e./co-r.e. 的不對稱是所有歸約證明的杠杆。
工程對策：限定模型、資源、結構或驗證義務，即可重獲可判定性；防毒/靜態分析的啟發式本質由此而來。
對角線法譜系：Cantor→哥德爾→圖靈→階層定理，是「自指產生不可能性」的通用模板。