1950-Rice 定理#

案件摘要#

1950 年（論文 1951 年正式發表），Henry Gordon Rice 證明一個驚人的「全面性結論」：對圖靈機可計算枚舉語言而言，任何非平凡的語義性質都不可判定。停機問題只是冰山一角——整座冰山都沈在不可判定的海底。

前因 -- 為什麼會有這個案子#

• 1936 年 Turing 證明「此機器會停嗎？」不可判定。
• 但工程師與數學家想問更多：「此機器會輸出 42 嗎？」「此機器接受的語言是空的嗎？」「此程式有無窮迴圈 bug 嗎？」
• 當時已知的不可判定結果零散，每個都要個別證明。Rice 的偵探手法：找出所有這類問題的共同犯罪模式——它們全都可從停機問題歸約而來。

線索與推理 -- 數學式、程式、理論#

定理內容#

Rice 定理：設 \(\mathcal{S}\) 為部分可計算函數（等價地：r.e. 語言）的一個性質，即一個由程式指標定義的集合：

若 \(\mathcal{S}\) 非平凡（non-trivial），即存在 \(e_1, e_2\) 使 \(\varphi_{e_1} \in \mathcal{C}\) 且 \(\varphi_{e_2} \notin \mathcal{C}\) ，則 \(\mathcal{S}\) 不可判定。

換句話說：任何「只看程式做什麼、不看程式怎麼寫」的非平凡問題都不可判定。注意性質必須是語義的（extensional）：只依賴 \(\varphi_e\) 這個函數本身，不依賴指標 \(e\) 。

證明概述（歸約自停機問題）#

不失一般性，設 \(\mathcal{C}\) 中有一個指標 \(a\) （即 \(\varphi_a \in \mathcal{C}\) ），並設存在 \(b\) 使 \(\varphi_b \notin \mathcal{C}\) 。對任意輸入 \(e\) ，構造程式 \(g_e\) ：

實作方式： \(g_e\) 先模擬 \(M_e(e)\) ，若停機再執行 \(\varphi_a(x)\) 。

• 若 \(e \in K\) （ \(M_e(e)\) 停機），則 \(g_e \equiv \varphi_a\) ，故 \(g_e \in \mathcal{C}\) 。
• 若 \(e \notin K\) ，則 \(g_e\) 處處不停，其函數是「空函數」，由建構可取其 \(\notin \mathcal{C}\) （若空函數在 \(\mathcal{C}\) 中則對 \(b\) 的補集做同樣論證）。

由 s-m-n 定理， \(e \mapsto \langle g_e \rangle\) 是可計算函數，故 \(K \leq_m \mathcal{S}\) 。因 \(K\) 不可判定， \(\mathcal{S}\) 亦不可判定。 \(\blacksquare\)

語法性質 vs 語義性質的對照#

關鍵分界線：性質是否是 extensional 的。兩個行為完全相同的程式（一個用 while、一個用 for），語法性質可能不同，但語義性質必須相同。

實務應用：靜態分析與編譯器優化的極限#

• 靜態程式分析：任何「精確回答程式行為」的分析器都不存在。實務工具（如 Coverity、ESLint、型別系統）必須做保守近似（conservative approximation）：寧可誤報（false positive）也不漏報，或反之。
• 編譯器優化：判斷「這段程式碼是否為死碼（dead code）」是語義性質，精確判定不可能。編譯器只能用可判定的近似（如控制流圖分析、資料流分析）。
• 病毒偵測 / 等價性檢查：「此程式是否等價於已知病毒」不可判定（程式等價性是語義性質）。
• 這解釋了為何型別系統、抽象解譯（abstract interpretation）、模型檢查等領域存在：它們都是在 Rice 定理劃下的紅線內，用可判定的近似換取可用性。

Python 演示：「判斷程式是否永遠輸出 42」不可判定#

# 假設存在 halts(f) 判定「f 是否對所有輸入輸出 42」
# 我們用它解決停機問題 -> 矛盾
from functools import partial

def never_42(x):
    while True:   # 永不停，故不輸出 42
        pass

def always_42(x):
    return 42

def halts_42(f):
    # 假設這是 Rice 定理否定的「神奇分析器」
    raise NotImplementedError("不存在這種函數（Rice 定理）")

def solve_halt(e):
    """用假想的 halts_42 解決停機問題：M_e(e) 是否停機？"""
    def g(x):
        simulate(e, e)   # 先模擬 M_e(e)
        return 42        # 若停機，輸出 42
    # 若 M_e(e) 停機：g 輸出恆為 42 -> halts_42(g) 為 True
    # 若不停機：g 永不輸出 42   -> halts_42(g) 為 False
    return halts_42(g)   # == 停機問題的答案！

def simulate(e, x):
    # 模擬器存在（通用圖靈機），此處省略實作
    pass

# 結論：若 halts_42 存在，則 solve_halt 解決了不可判定的停機問題。
# 矛盾！所以「判斷程式是否永遠輸出 42」不可判定。

實際可驗證的部分：Python 的 exec/eval 無法判定任意程式碼的行為；任何 linter 只能靠規則與近似。

結案 -- 後果與影響#

• 結案：Rice 定理一次判決所有語義性質問題不可判定——停機問題不是特例而是通例。
• 它成為「不可能性結果」的標準武器：證明某分析不可判定時，通常只需指出它包含一個 Rice 性質。
• 實務影響：確立了靜態分析、驗證、優化必須走「近似 + 保守性」的路線；催生了抽象解譯（Cousot 夫婦 1977）等理論。
• 深遠影響：Rice 定理是 Rice–Shapiro 定理、 effective version 的起點，也與 Rice 定理在 AI 安全（AI 對齊的不可判定性論證）中被反覆引用。

關鍵人物與文獻#

• Henry Gordon Rice（1920–2003）：美國邏輯學家，《Classes of recursively enumerable sets and their decision problems》, Trans. AMS, 1951（1950 年博士論文）。
• Alan Turing：1936 年停機問題，Rice 定理的歸約源頭。
• Stephen Kleene：s-m-n 定理，證明的技術基礎。
• Patrick Cousot / Radhia Cousot：1977 年抽象解譯，在 Rice 定理紅線內的實務解法。
• Hartley Rogers：《Theory of Recursive Functions and Effective Computability》, 1967，Rice 定理的標準教科書表述。