-
Notifications
You must be signed in to change notification settings - Fork 94
11b Unsolvable
Church 在論文中證明
THEOREM XVIII, There is no recursive function of a formula C, whose value is 2 or 1according as C has a normal form or not.
這是什麼意思？
如何證明的
ChatGPT: https://chatgpt.com/c/674bcf55-76e4-8012-9a40-60f7a0bb790a
定理 XVIII 是 Alonzo Church 在論文中關於不可判定性的結果之一，其結論大致可以翻譯為：
「不存在遞歸函數可以判定一個 λ 演算公式 ( C ) 是否具有正常形式。」
在 λ 演算中，正常形式（Normal Form, NF） 是指一個 λ 表達式經過 β-簡化後，無法再被進一步簡化的形式。換句話說：
- 如果一個 λ 表達式具有正常形式，則不存在任何 β-簡化規則可以應用。
- 如果一個 λ 表達式沒有正常形式，它可能會：
- 無限簡化（產生 β-簡化的無窮序列）。
- 卡在一個無法達到正常形式的結構。
這個定理表明：對於任意的 λ 表達式 ( C )，不存在一個遞歸函數（即可計算的算法）能夠保證回答這樣的問題：「這個表達式是否有正常形式？」
這是 λ 演算中不可判定性的一個結果，類似於圖靈機不可判定問題的特徵。
定理 XVIII 的證明是基於 不可判定性和對角化論證 的思想，具體如下：
假設存在一個遞歸函數 ( f(C) )，其滿足：
- ( f(C) = 1 ) 如果 ( C ) 具有正常形式；
- ( f(C) = 2 ) 如果 ( C ) 沒有正常形式。
構造一個特殊的 λ 表達式 ( D )（基於 ( f )），其定義如下：
- ( D = (\lambda x. x x) (\lambda x. x x) ) 這是著名的 Ω 表達式，它的 β-簡化會無限展開，永遠無法達到正常形式。
將 ( D ) 傳遞給 ( f )，我們發現：
- 如果 ( f(D) = 1 )，表示 ( D ) 具有正常形式，這與 ( D ) 的無限簡化矛盾。
- 如果 ( f(D) = 2 )，表示 ( D ) 沒有正常形式，這看似正確，但 ( f ) 無法在有限時間內保證判定這一點，因為 ( D ) 的簡化是無限的。
對 ( f ) 的每種假設情況，都無法保證 ( f ) 是有限的遞歸函數，這導致假設不成立。因此，這樣的 ( f ) 不可能存在。
Church 的證明依賴於以下幾個觀點：
- 遞歸函數的有限性：遞歸函數在有限步驟內計算出結果，但對於具有無限簡化序列的表達式，這無法實現。
- Ω 表達式的特性：它是一個典型的無限簡化表達式，用於說明某些 λ 表達式的正常形式不可判定。
- 不可判定性結果：這個結論類似於圖靈機停機問題的不可判定性，表明某些 λ 演算問題超出了計算的範圍。
Church 的定理 XVIII 與圖靈的停機問題有直接聯繫：
- 停機問題問：「一個程序是否會在有限步內結束運行？」
- 定理 XVIII 問：「一個 λ 表達式是否具有正常形式？」
兩者都涉及到無法在有限時間內確定某些性質，這展示了 λ 演算和圖靈機模型的等價性。
當然可以！以下是定理 XVIII（不可判定性）的詳細證明過程。這個證明基於 λ 演算和遞歸函數理論的基本概念。
不存在遞歸函數 ( f(C) )，其能判定一個 λ 表達式 ( C ) 是否具有正常形式。
我們將使用 反證法 和 對角化方法。具體步驟如下：
假設存在一個遞歸函數 ( f(C) )，使得：
- ( f(C) = 1 ) 當且僅當 ( C ) 具有正常形式；
- ( f(C) = 2 ) 當且僅當 ( C ) 沒有正常形式（即無法達到正常形式，可能是因為它會無限簡化）。
我們構造一個特殊的 λ 表達式 ( D )，該表達式的行為依賴於 ( f ) 本身。這類似於對角化論證中的「自反性」方法。
令： [ D = (\lambda x. f(x x)) (\lambda x. f(x x)) ]
- ( D ) 是 ( (\lambda x. f(x x)) (\lambda x. f(x x)) )，它會觸發自身的遞歸調用（即 ( x x )）。
- 如果 ( f ) 嘗試對 ( D ) 判定其是否具有正常形式，則它會面臨無限展開： [ D \to f(D) ] 這導致遞歸調用本身無法完成，因為 ( D ) 的結構無法穩定。
如果 ( f(C) ) 可以正確判定 ( C ) 是否具有正常形式，則：
- 若 ( f(D) = 1 )，表示 ( D ) 具有正常形式。但實際上，( D ) 是無限展開的，並無法達到正常形式。
- 若 ( f(D) = 2 )，表示 ( D ) 沒有正常形式。但 ( f ) 無法在有限步內確定 ( D ) 沒有正常形式，因為它需要無限簡化的結果。
因此，無論 ( f(D) ) 給出 ( 1 ) 或 ( 2 )，我們都能導致矛盾。
假設 ( f ) 存在：
- 如果 ( f(D) = 1 )，則 ( D ) 的簡化是有限的，這與 ( D ) 的無限展開矛盾。
- 如果 ( f(D) = 2 )，則 ( D ) 沒有正常形式，但 ( f ) 必須在有限步內得出結論，這不可能。
因此，( f ) 無法存在，假設不成立。
由於 ( f(C) ) 不可能同時滿足有限性和正確性，故 不存在遞歸函數可以判定 λ 表達式是否具有正常形式。
這個證明與圖靈的停機問題的證明非常類似：
- 停機問題問：「是否存在一個算法可以判定任意程序是否會停止？」
- 定理 XVIII問：「是否存在一個遞歸函數可以判定任意 λ 表達式是否具有正常形式？」
二者都表明某些性質（停機或正常形式）是不可判定的，從而揭示了遞歸函數理論的極限。
哥德爾不完備定理、圖靈停機問題（Halting Problem），以及 Church 定理 XVIII（正常形式判定不可解） 都揭示了數學邏輯和計算理論中的 不可判定性 和 不可解性，它們之間具有深刻的內在聯繫：
這三個理論都描述了某些系統中的極限，即在特定條件下，存在一些問題是不可解的或不可判定的。
-
哥德爾不完備定理：
- 系統內部無法證明自身的一致性，並且在足夠強的數學系統中，總存在不能被證明為真或假（不可決定）的命題。
- 揭示：在邏輯系統中，某些性質不可證。
-
圖靈停機問題：
- 無法設計一個算法來判定任意程序是否會停止。
- 揭示：在計算系統中，某些性質不可判定。
-
Church 定理 XVIII：
- λ 演算中，無法設計遞歸函數來判定一個 λ 表達式是否具有正常形式。
- 揭示：在形式系統中，某些性質不可計算。
這些理論共同反映了數學邏輯和計算理論中的根本限制。
它們都關注形式系統的性質，並強調形式化方法的局限性。
- 哥德爾不完備定理 是基於一階邏輯和皮亞諾算術的，這些系統可以用 λ 演算或圖靈機來模擬。
- 因此，哥德爾的不可證性（某些命題無法證明）與 λ 演算的不可判定性（某些性質無法判定）在邏輯上是等價的。
- λ 演算和圖靈機是等價的計算模型（Church-Turing 假設）。
- 圖靈停機問題 是圖靈機模型下的不可解性問題，而 定理 XVIII 是 λ 演算模型下的不可解性問題。這兩者本質上是同一問題在不同語境中的表達。
這三個理論都涉及到 遞歸性（recursion） 和 自參考（self-reference），而這正是不可解性的根源。
- 哥德爾構造了一個「自指命題」：「這個命題無法在系統內證明。」
- 系統內的證明結構無法處理這樣的自指命題，導致了不可證性。
- 圖靈在停機問題的證明中構造了一個「自我模擬程序」：「如果這個程序停止，那就讓它進入無限迴圈；如果它不停止，那就讓它停止。」
- 這樣的自模擬結構導致了停機問題的不可判定。
- 在 λ 演算中，我們可以構造一個像 ( (\lambda x. x x) (\lambda x. x x) ) 這樣的「自遞歸」表達式，導致無限簡化序列。
- 因此，正常形式的判定問題等價於停機問題。
從抽象層次看，這些理論的結論實際上描述了數學與計算系統中的三個側面：
| 理論 | 系統範圍 | 無法解決的問題 | 本質 |
|---|---|---|---|
| 哥德爾不完備定理 | 數學邏輯（形式系統） | 系統內命題的真或假 | 某些命題不可證 |
| 圖靈停機問題 | 計算模型（圖靈機） | 程序是否會停止 | 某些程序行為不可判定 |
| Church 定理 XVIII | λ 演算 | 表達式是否有正常形式 | 某些表達式性質不可計算 |
它們展示了形式系統的限制，說明了數學真理與計算模型的能力是有界的。
- 哥德爾不完備定理（1931） 奠定了形式系統研究的基石，指出數學系統的自我局限性。
- Church 的 λ 演算（1936） 和 圖靈的停機問題（1936-1937） 在不完全相同的框架下擴展了這一結論，並指出不可判定性在計算模型中的具體表現。
它們共同形成了現代理論計算機科學的核心基礎，揭示了數學邏輯與計算理論的統一性。
從希爾伯特到圖靈的那些故事
-- 以 Python 展現這些故事背後的程式