1936 - 判定問題不可判定性#
案件摘要#
1936 年，Church 證明 Hilbert 的判定問題（Entscheidungsproblem）不可判定： 不存在任何演算法，能對任意一階邏輯語句機械地判定真假。 同年，英國的年輕人 Alan Turing 用完全不同的機器（圖靈機）獨立證明同一結果 —— 兩條線索指向同一個結論，「可計算」從此有了精確的邊界。
前因 -- 為什麼會有這個案子#
- Hilbert 綱領的最後希望：Gödel（1931）已證明數學不完備，但 Hilbert 仍期望「判定問題」有解 —— 若存在機械程序判定任意數學語句的真假，數學至少還能「自動化」。
- 判定問題（Entscheidungsproblem）的定義：給定一階邏輯（狹謂詞演算）的語句 \(\varphi\) ，是否存在有效程序（effective procedure），有限步內判定 \(\varphi\) 是否普遍有效（valid）？
- Church 手中已有工具：λ 演算 + Kleene 證明的「λ 可定義 = 一般遞迴」。
- Turing 劍橋受訓，獨立構思出「圖靈機」—— 一台只有紙帶、讀寫頭與有限狀態的極簡機器。
線索與推理 -- 數學式、程式、理論#
1. Church 的證明策略（λ 演算版）#
第一步：把「有效程序」精確化為「λ 可定義函數」。 Church 命題：可有效計算 \(\Leftrightarrow\) λ 可定義。於是「是否存在判定程序」變成「是否存在 λ 項 \(D\) 判定普遍有效性」。
第二步：把邏輯語句算術化（Gödel numbering）。 每個一階邏輯語句編碼為自然數： \(\ulcorner\varphi\urcorner \in \mathbb{N}\) 。「 \(\varphi\) 普遍有效」變成數論性質：
第三步：反證 —— 若 \(D\) 存在，就能造出不可解的函數。 假設判定器 \(D\) 存在（ \(D\) 是 λ 可定義的）。定義對角線函數：
其中 \(\varphi_n\) 是「編號為 \(n\) 的表達式 \(\psi_n\) 滿足『 \(\psi_n\) 應用於編號 \(n\) 不普遍有效』」的語句。
Kleene 已證明 \(g\) 是一般遞迴的，因此 λ 可定義。但「 \(g\) 在名單上」與對角線構造矛盾 —— 與 Kleene–Rosser 案同款手法。結論：
第四步：等價的停機問題式論證（λ 演算的自我指涉）。 核心洞察：λ 演算中「歸約是否停機」本身不可判定。反證：假設存在 λ 項
則可構造對角線項：
問 \(\Delta\ \Delta\) 停機嗎？ - 若 \(\Delta\,\Delta\) 停機： \(Halt\ (\Delta\,\Delta) = \top\) ，則 \(\Delta\,\Delta \to \neg\top\ (\Delta\,\Delta) \to \bot\) -分支，繼續歸約不停 —— 矛盾。 - 若不停： \(Halt\ (\Delta\,\Delta) = \bot\) ，則 \(\Delta\,\Delta \to \bot\) -分支即停機 —— 矛盾。
無論如何矛盾，故 \(Halt\) 不存在。這與 Turing 的停機問題（halting problem）在結構上完全同構 —— 自我指涉 + 對角線，是所有不可判定性證明的共同指紋。
# 停機問題的 Python 類比（對角線構造）
def halts(prog, inp): ... # 假設存在萬能停機判定器
def trouble(prog):
if halts(prog, prog): # 若 prog 對自己的輸入會停機
while True: pass # 就故意不停機
else:
return "done" # 否則停機
trouble(trouble) # 停機嗎？兩種答案都矛盾 —— 故 halts 不存在
2. Church–Turing 命題#
兩位主角各自提出（並被對方證明等價）的命題：
Church–Turing 命題：一個函數是「可有效計算的」，若且唯若它由圖靈機計算，若且唯若它是一般遞迴函數，若且唯若它是 λ 可定義的。
這是命題而非定理 —— 因為「可有效計算」是直覺概念，無法形式化證明；但所有合理的計算模型（圖靈機、λ 演算、遞迴函數、隨機存取機器……）都被證明彼此等價，使命題獲得壓倒性支持。
3. Turing 機器簡述#
Turing 的機器只有： 1. 一條無限長的紙帶，每格寫一個符號（0/1/空白） 2. 一個讀寫頭，可讀、寫、左右移動 3. 一個有限狀態控制器與轉移規則表
計算 = 依規則表一步步操作，直到 halt 或永不停。
4. 兩種模型的對照表#
| 面向 | λ 演算（Church） | 圖靈機（Turing） |
|---|---|---|
| 原子 | 函數（λ 項） | 符號與狀態 |
| 計算 | β-歸約 \((\lambda x.M)\,N \to M[N/x]\) | 轉移規則 \(\delta\) |
| 資料 | Church 數字 \(\bar{n} = \lambda f.\lambda x.f^n x\) | 紙帶上的 0/1 串 |
| 風格 | 重寫（rewriting）、宣告式 | 操作（step-by-step）、命令式 |
| 不停機 | Ω 組合子、對角線項 | 停機問題 |
| 後裔 | Lisp、Haskell、JS/Python 函數 | 所有現代電腦、馮紐曼架構 |
5. 模型互譯（等價性）#
Church（1937）與 Turing（1937）互相證明：λ 可定義函數 = 圖靈可計算函數。互譯的關鍵： - λ 演算 → 圖靈機：把 β-歸約實作為符號串重寫（Turing 機可模擬任何重寫系統） - 圖靈機 → λ 演算：把紙帶編碼為 λ 項（配對/串列），把狀態轉移編碼為遞迴函數
結案 -- 後果與影響#
- Hilbert 綱領正式落幕：判定問題不可判定 + 不完備定理，宣告數學無法被完全機械化。
- 1936 年 5 月 Church 論文先發表；1936 年底 Turing 論文提交（1937 年刊出），同年 Church 成為 Turing 的博士導師 —— 兩位「對手」成為師生。
- Church–Turing 命題成為電腦科學的公理級基石：一切「演算法」的定義都以此為準。
- 圖靈機成為「可計算性」的直觀標準模型與複雜度理論（P/NP）的基礎；λ 演算成為函數式程式設計的理論基礎 —— 一體兩面，殊途同歸。
- 停機問題成為所有「不可判定」證明的模板：程式分析、型別推斷、定理證明中的不可判定結果，全是它的後裔。
關鍵人物與文獻#
- Alonzo Church：以 λ 演算證明判定問題不可判定。
- Alan Turing（1912–1954）：以圖靈機獨立證明，並提出停機問題。
- David Hilbert & Wilhelm Ackermann：《Grundzüge der theoretischen Logik》(1928) 提出判定問題。
- A. Church, An unsolvable problem of elementary number theory, American Journal of Mathematics 58 (1936)；A note on the Entscheidungsproblem, JSL 1 (1936)。
- A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proc. London Math. Soc. 42 (1936–37)。
- S. C. Kleene, Introduction to Metamathematics (1952)：三大模型等價性的標準整理。