哥德爾的不完備性定理震撼了20世紀數學界的天空，其數學意義顛覆了希爾伯特的形式化數學的宏偉計劃，其哲學意義直到21世紀的今天仍然不斷被延伸到各個自然學科，深刻影響著人們的思維。圖靈為瞭解決希爾伯特著名的第十問題而提出有效計算模型，進而作出了可計算理論和現代計算機的奠基性工作，著名的停機問題給出了機械計算模型的能力極限，其深刻的意義和漂亮的證明使它成為可計算理論中的標誌性定理之一。丘齊，跟圖靈同時代的天才，則從另一個抽象角度提出了lambda算子的思想，與圖靈機抽象的傾向於硬件性不同，丘齊的lambda算子理論是從數學的角度進行抽象，不關心運算的機械過程而只關心運算的抽象性質，只用最簡潔的幾條公理便建立起了與圖靈機完全等價的計算模型，其體現出來的數學抽象美開出了函數式編程語言這朵奇葩，Lisp、Scheme、Haskell… 這些以抽象性和簡潔美為特點的語言至今仍然活躍在計算機科學界，雖然由於其本質上源於lambda算子理論的抽象方式不符合人的思維習慣從而注定無法成為主流的編程語言[2]，然而這仍然無法妨礙它們成為編程理論乃至計算機學科的最佳教本。而誕生於函數式編程語言的神奇的Y combinator至今仍然讓人們陷入深沉的震撼和反思當中…
然而，這一切的一切，看似不很相關卻又有點相關，認真思考其關係卻又有點一頭霧水的背後，其實隱隱藏著一條線，這條線把它們從本質上串到了一起，而順著時光的河流逆流而上，我們將會看到，這條線的盡頭，不是別人，正是隻手撥開被不嚴密性問題困擾的19世紀數學界陰沉天空的天才數學家康托爾，康托爾創造性地將一一對應和對角線方法運用到無窮集合理論的建立當中，這個被希爾伯特稱為「誰也無法將我們從康托爾為我們創造的樂園中驅逐出去」、被羅素稱為「19世紀最偉大的智者之一」的人，他在集合論方面的工作終於驅散了不嚴密性問題帶來的陰霾，彷彿一道金色的陽光刺破烏雲，19世紀的數學終於看到了真正嚴格化的曙光，數學終於得以站在了前所未有的堅固的基礎之上；集合論至今仍是數學裡最基礎和最重要的理論之一。而康托爾當初在研究無窮集合時最具天才的方法之一——對角線方法——則帶來了極其深遠的影響，其純粹而直指事物本質的思想如洪鐘大呂般響徹數學和哲學的每一個角落[3]。隨著本文的展開，你將會看到，剛才提到的一切，歌德爾的不完備性定理，圖靈的停機問題，lambda算子理論中神奇的Y combinator、乃至著名的羅素悖論、理髮師悖論等等，其實都源自這個簡潔、純粹而同時又是最優美的數學方法，反過來說，從康托爾的對角線方法出發，我們可以輕而易舉地推導出哥德爾的不完備性定理，而由後者又可以輕易導出停機問題和Y combinator，實際上，我們將會看到，後兩者也可以直接由康托爾的對角線方法導出。尤其是Y combinator，
這個形式上繞來繞去，本質上捉摸不透，看上去神秘莫測的算子，其實只是一個非常自然而然的推論，如果從哥德爾的不完備性定理出發，它甚至比停機問題還要來
得直接簡單。總之，你將會看到這些看似深奧的理論是如何由一個至為簡單而又至為深刻的數學方法得出的，你將會看到最純粹的數學美。
圖靈的停機問題(The Halting Problem)
瞭解停機問題的可以直接跳過這一節，到下一節「Y Combinator」，瞭解後者的再跳到下一節「哥德爾的不完備性定理」
我們還是從圖靈著名的停機問題說起，一來它相對來說是我們要說的幾個定理當中最簡單的，二來它也最貼近程序員。實際上，我以前曾寫過一篇關於圖靈機的文章，有興趣的讀者可以從那篇開始，那篇主要是從理論上闡述，所以這裡我們打算避開抽象的理論，換一種符合程序員思維習慣的直觀方式來加以解釋。
停機問題
不存在這樣一個程序（算法），它能夠計算任何程序（算法）在給定輸入上是否會結束（停機）。
那麼，如何來證明這個停機問題呢？反證。假設我們某一天真做出了這麼一個極度聰明的萬能算法（就叫God_algo吧），你只要給它一段程序（二進制描述），再給它這段程序的輸入，它就能告訴你這段程序在這個輸入上會不會結束（停機），我們來編寫一下我們的這個算法吧：
bool God_algo(char* program, char* input)
{
return true;
return false;
}
這裡我們假設if的判斷語句裡面是你天才思考的結晶，它能夠像上帝一樣洞察一切程序的宿命。現在，我們從這個God_algo出發導出一個新的算法：
bool Satan_algo(char* program)
{
if( God_algo(program, program) ){
while(1); // loop forever!
return false; // can never get here!
}
else
return true;
}
正如它的名字所暗示的那樣，這個算法便是一切邪惡的根源了。當我們把這個算法運用到它自身身上時，會發生什麼呢？
Satan_algo(Satan_algo);
我們來分析一下這行簡單的調用：
顯然，Satan_algo(Satan_algo)這個調用要麼能夠運行結束返回（停機），要麼不能返回（loop forever）。
如果它能夠結束，那麼Santa_algo算法裡面的那個if判斷就會成立（因為God_algo(Santa_algo,Santa_algo)將會返回true），從而程序便進入那個包含一個無窮循環while(1);的if分支，於是這個Satan_algo(Satan_algo)調用便永遠不會返回（結束）了。
而如果Satan_algo(Satan_algo)不能結束（停機）呢，則if判斷就會失敗，從而選擇另一個if分支並返回true，即Satan_algo(Satan_algo)又能夠返回（停機）。
總之，我們有：
Satan_algo(Satan_algo)能夠停機=> 它不能停機
Satan_algo(Satan_algo)不能停機=> 它能夠停機
所以它停也不是，不停也不是。左右矛盾。
於是，我們的假設，即God_algo算法的存在性，便不成立了。正如拉格朗日所說：「陛下，我們不需要（上帝）這個假設」[4]。
這個證明相信每個程序員都能夠容易的看懂。然而，這個看似不可捉摸的技巧背後其實隱藏著深刻的數學原理（甚至是哲學原理）。在沒有認識到這一數學原理之前，至少我當時是對於圖靈如何想出這一絕妙證明感到無法理解。但後面，在介紹完了與圖靈的停機問題「同構」的Y combinator之後，我們會深入哥德爾的不完備性定理，在理解了哥德爾不完備性定理之後，我們從這一同樣絕妙的定理出發，就會突然發現，離停機問題和神奇的Y combinator只是咫尺之遙而已。當然，最後我們會回溯到一切的盡頭，康托爾那裡，看看停機問題、Y combinator、以及不完備性定理是如何自然而然地由康托爾的對角線方法推導出來的，我們將會看到這些看似神奇的構造性證明的背後，其實是一個簡潔優美的數學方法在起作用。
Y Combinator
瞭解Y combinator的請直接跳過這一節，到下一節「哥德爾的不完備性定理」。
讓我們暫且擱下但記住繞人的圖靈停機問題，走進函數式編程語言的世界，走進由跟圖靈機理論等價的lambda算子發展出來的另一個平行的語言世界。讓我們來看一看被人們一代一代吟唱著的神奇的Y Combinator…
關於Y Combinator的文章可謂數不勝數，這個由師從希爾伯特的著名邏輯學家Haskell B.Curry（Haskell語言就是以他命名的，而函數式編程語言裡面的Curry手法也是以他命名）「發明」出來的組合算子（Haskell是研究組合邏輯(combinatory logic)的）彷彿有種神奇的魔力，它能夠算出給定lambda表達式（函數）的不動點。從而使得遞歸成為可能。事實上，我們待會就會看到，Y Combinator在神奇的表面之下，其實隱藏著深刻的意義，其背後體現的意義，曾經開出過歷史上最燦爛的數學之花，所以MIT的計算機科學系將它做成系徽也就不足為奇了[5]。
當然，要瞭解這個神奇的算子，我們需要一點點lambda算子理論的基礎知識，不過別擔心，lambda算子理論是我目前見過的最簡潔的公理系統，這個系統僅僅由三條非常簡單的公理構成，而這三條公理裡面我們又只需要關注前兩條。
以下小節——lambda calculus——純粹是為了沒有接觸過lambda算子理論的讀者準備的，並不屬於本文重點討論的東西，然而要討論Y combinator就必須先瞭解一下lambda（當然，以編程語言來瞭解也行，但是你會看到，丘齊最初提出的lambda算子理論才是最最簡潔和漂亮的，學起來也最省事。）所以我單獨準備了一個小節來介紹它。如果你已經知道，可以跳過這一小節。不知道的讀者也可以跳過這一小節去wikipedia上面看，這裡的介紹使用了wikipedia上的方式
lambda calculus
先來看一下lambda表達式的基本語法(BNF)：
::=
::= lambda .
::= ( )
前兩條語法用於生成lambda表達式（lambda函數），如：
lambda x y. x + y
haskell裡面為了簡潔起見用「」來代替希臘字母lambda，它們形狀比較相似。故而上面的定義也可以寫成：
x y. x + y
這是一個匿名的加法函數，它接受兩個參數，返回兩值相加的結果。當然，這裡我們為了方便起見賦予了lambda函數直觀的計算意義，而實際上lambda calculus裡面一切都只不過是文本替換，有點像C語言的宏。並且這裡的「+」我們假設已經是一個具有原子語義的運算符[6]，此外，為了方便我們使用了中綴表達（按照lambda calculus系統的語法實際上應該寫成「(+ x y)」才對——參考第三條語法）。
那麼，函數定義出來了，怎麼使用呢？最後一條規則就是用來調用一個lambda函數的：
((lambda x y. x + y) 2 3)
以上這一行就是把剛才定義的加法函數運用到2和3上（這個調用語法形式跟命令式語言(imperative language)慣用的調用形式有點區別，後者是「f(x, y)」，而這裡是「(f x y)」，不過好在順序沒變:) ）。為了表達簡潔一點，我們可以給(lambda x y. x + y)起一個名字，像這樣：
let Add = (lambda x y. x + y)
這樣我們便可以使用Add來表示該lambda函數了：
(Add 2 3)
不過還是為了方便起見，後面調用的時候一般用「Add(2, 3)」，即我們熟悉的形式。
有了語法規則之後，我們便可以看一看這個語言系統的兩條簡單至極的公理了：
Alpha轉換公理：例如，「lambda x y. x + y」轉換為「lambda a b. a + b」。換句話說，函數的參數起什麼名字沒有關係，可以隨意替換，只要函數體裡面對參數的使用的地方也同時注意相應替換掉就是了。
Beta轉換公理：例如，「(lambda x y. x + y) 2 3」轉換為「2 + 3」。這個就更簡單了，也就是說，當把一個lambda函數用到參數身上時，只需用實際的參數來替換掉其函數體中的相應變量即可。
就這些。是不是感覺有點太簡單了？但事實就是如此，lambda算子系統從根本上其實就這些東西，然而你卻能夠從這幾個簡單的規則中推演出神奇無比的Y combinator來。我們這就開始！
遞歸的迷思
敏銳的你可能會發現，就以上這兩條公理，我們的lambda語言中無法表示遞歸函數，為什麼呢？假設我們要計算經典的階乘，遞歸描述肯定像這樣：
f(n):
if n == 0 return 1
return n*f(n-1)
當然，上面這個程序是假定n為正整數。這個程序顯示了一個特點，f在定義的過程中用到了它自身。那麼如何在lambda算子系統中表達這一函數呢？理所當然的想法如下：
lambda n. If_Else n==0 1 n*<self>(n-1)
當然，上面的程序假定了If_Else是一個已經定義好的三元操作符（你可以想像C的「?:」操作符，後面跟的三個參數分別是判斷條件、成功後求值的表達式、失敗後求值的表達式。那麼很顯然，這個定義裡面有一個地方沒法解決，那就是<self>那個地方我們應該填入什麼呢？很顯然，熟悉C這類命令式語言的人都知道應該填入這個函數本身的名字，然而lambda算子系統裡面的lambda表達式（或稱函數）是沒有名字的。
怎麼辦？難道就沒有辦法實現遞歸了？或者說，丘齊做出的這個lambda算子系統裡面根本沒法實現遞歸從而在計算能力上面有重大的缺陷？顯然不是。馬上你就會看到Y combinator是如何把一個看上去非遞歸的lambda表達式像變魔術那樣變成一個遞歸版本的。在成功之前我們再失敗一次，注意下面的嘗試：
let F = lambda n. IF_Else n==0 1 n*F(n-1)
看上去不錯，是嗎？可惜還是不行。因為let F只是起到一個語法糖的作用，在它所代表的lambda表達式還沒有完全定義出來之前你是不可以使用F這個名字的。更何況實際上丘齊當初的lambda算子系統裡面也並沒有這個語法元素，這只是剛才為了簡化代碼而引入的語法糖。當然，瞭解這個let語句還是有意義的，後面還會用到。
一次成功的嘗試
在上面幾次失敗的嘗試之後，我們是不是就一籌莫展了呢？別忘了軟件工程裡面的一條黃金定律：「任何問題都可以通過增加一個間接層來解決」。不妨把它沿用到我們面臨的遞歸問題上：沒錯，我們的確沒辦法在一個lambda函數的定義裡面直接（按名字）來調用其自身。但是，可不可以間接調用呢？
我們回顧一下剛才不成功的定義：
lambda n. If_Else n==0 1 n*<self>(n-1)
現在處不是缺少「這個函數自身」嘛，既然不能直接填入「這個函數自身」，我們可以增加一個參數，也就是說，把參數化：
lambda self n. If_Else n==0 1 n*self(n-1)
上面這個lambda算子總是合法定義了吧。現在，我們調用這個函數的時候，只要加傳一個參數self，這個參數不是別人，正是這個函數自身。還是為了簡單起見，我們用let語句來給上面這個函數起個別名：
let P = lambda self n. If_Else n==0 1 n*self(n-1)
我們這樣調用，比如說我們要計算3的階乘：
P(P, 3)
也就是說，把P自己作為P的第一個參數（注意，調用的時候P已經定義完畢了，所以我們當然可以使用它的名字了）。這樣一來，P裡面的self處不就等於是P本身了嗎？自身調用自身，遞歸！
可惜這只是個美好的設想，還差一點點。我們分析一下P(P, 3)這個調用。利用前面講的Beta轉換規則，這個函數調用展開其實就是（你可以完全把P當成一個巨集來進行展開！）：
IF_Else n==0 1 n*P(n-1)
看出問題了嗎？這裡的P(n-1)雖然調用到了P，然而只給出了一個參數；而從P的定義來看，它是需要兩個參數的（分別為self和n）！也就是說，為了讓P(n-1)變成良好的調用，我們得加一個參數才行，所以我們得稍微修改一下P的定義：
let P = lambda self n. If_Else n==0 1 n*self(self, n-1)
請注意，我們在P的函數體內調用self的時候增加了一個參數。現在當我們調用P(P, 3)的時候，展開就變成了：
IF_Else 3==0 1 3*P(P, 3-1)
而P(P, 3-1)是對P合法的遞歸調用。這次我們真的成功了！
不動點原理
然而，看看我們的P的定義，是不是很醜陋？「n*self(self, n-1)」？什麼玩意？為什麼要多出一個多餘的self？DRY！怎麼辦呢？我們想起我們一開始定義的那個失敗的P，雖然行不通，但最初的努力往往是大腦最先想到的最直觀的做法，我們來回顧一下：
let P = lambda self n. If_Else n==0 1 n*self(n-1)
這個P的函數體就非常清晰，沒有冗餘成分，雖然參數列表裡面多出一個self，但我們其實根本不用管它，看函數體就行了，self這個名字已經可以說明一切了對不對？但很可惜這個函數不能用。我們再來回想一下為什麼不能用呢？因為當你調用P(P, n)的時候，裡面的self(n-1)會展開為P(n-1)而P是需要兩個參數的。唉，要是這裡的self是一個「真正」的，只需要一個參數的遞歸階乘函數，那該多好啊。為什麼不呢？乾脆我們假設出一個「真正」的遞歸階乘函數：
power(n):
if(n==0) return 1;
return n*power(n-1);
但是，前面不是說過了，這個理想的版本無法在lambda算子系統中定義出來嗎（由於lambda函數都是沒名字的，無法自己內部調用自己）？不急，我們並不需要它被定義出來，我們只需要在頭腦中「假設」它以「某種」方式被定義出來了，現在我們把這個真正完美的power傳給P，這樣：
P(power, 3)
注意它跟P(P, 3)的不同，P(P, 3)我們傳遞的是一個有缺陷的P為參數。而P(power, 3)我們則是傳遞的一個真正的遞歸函數power。我們試著展開P(power, 3):
IF_Else 3==0 1 3*power(3-1)
發生了什麼？？power(3-1)將會計算出2的階乘（別忘了，power是我們設想的完美遞歸函數），所以這個式子將會忠實地計算出3的階乘！
回想一下我們是怎麼完成這項任務的：我們設想了一個以某種方式構造出來的完美的能夠內部自己調用自己的遞歸階乘函數power，我們發現把這個power傳給P的話，P(power, n)的展開式就是真正的遞歸計算n階乘的代碼了。
你可能要說：廢話！都有了power了我們還要費那事把它傳給P來個P(power, n)幹嘛？直接power(n)不就得了？! 別急，之所以設想出這個power只是為了引入不動點的概念，而不動點的概念將會帶領我們發現Y combinator。
什麼是不動點？一點都不神秘。讓我們考慮剛才的power與P之間的關係。一個是真正可遞歸的函數，一個呢，則是以一個額外的self參數來試圖實現遞歸的偽遞歸函數，我們已經看到了把power交給P為參數發生了什麼，對吧？不，似乎還沒有，我們只是看到了，「把power加上一個n一起交給P為參數」能夠實現真正的遞歸。現在我們想考慮power跟P之間的關係，直接把power交給P如何？
P(power)
這是什麼？這叫函數的部分求值(partial evaluation)。換句話說，第一個參數是給出來了，但第二個參數還懸在那裡，等待給出。那麼，光給一個參數得到的是什麼呢？是「還剩一個參數待給的一個新的函數」。其實也很簡單，只要按照Beta轉換規則做就是了，把P的函數體裡面的self出現處皆替換為power就可以了。我們得到：
IF_Else n==0 1 n*power(n-1)
當然，這個式子裡面還有一個變量沒有綁定，那就是n，所以這個式子還不能求值，你需要給它一個n才能具體求值，對吧。這麼說，這可不就是一個以n為參數的函數麼？實際上就是的。在lambda算子系統裡面，如果給一個lambda函數的參數不足，則得到的就是一個新的lambda函數，這個新的lambda函數所接受的參數也就是你尚未給出的那些參數。換句話來說，調用一個lambda函數可以分若干步來進行，每次只給出一部分參數，而只有等所有參數都給齊了，函數的求值結果才能出來，否則你得到的就是一個「中間函數」。
那麼，這跟不動點定理有什麼關係？關係大了，剛才不是說了，P(power)返回的是一個新的「中間函數」嘛？這個「中間函數」的函數體我們剛才已經看到了，就是簡單地展開P(power)而已，回顧一遍：
IF_Else n==0 1 n*power(n-1)
我們已經知道，這是個函數，參數n待定。因此我們不妨給它加上一個「lambda n」的帽子，這樣好看一點：
lambda n. IF_Else n==0 1 n*power(n-1)
這是什麼呢？這可不就是power本身的定義？（當然，如果我們能夠定義power的話）。不信我們看看power如果能夠定義出來像什麼樣子：
let power = lambda n. IF_Else n==0 1 n*power(n-1)
一模一樣！也就是說，P(power)展開後跟power是一樣的。即：
P(power) = power
以上就是所謂的不動點。即對於函數P來說power是這樣一個「點」：當把P用到power身上的時候，得到的結果仍然還是power，也就是說，power這個「點」在P的作用下是「不動」的。
可惜的是，這一切居然都是建立在一個不存在的power的基礎上的，又有什麼用呢？可別過早提「不存在」這個詞，你覺得一樣東西不存在或許只是你沒有找到使它存在的正確方法。我們已經看到power是跟P有著密切聯繫的。密切到什麼程度呢？對於偽遞歸的P，存在一個power，滿足P(power)=power。注意，這裡所說的「偽遞歸」的P，是指這樣的形式：
let P = lambda self n. If_Else n==0 1 n*self(n-1) // 注意，不是self(self,n-1)
一般化的描述就是，對任一偽遞歸F（回想一下偽遞歸的F如何得到——是我們為瞭解決lambda函數不能引用自身的問題，於是給理想的f加一個self參數從而得到的），必存在一個理想f（F就是從這個理想f演變而來的），滿足F(f) = f。
那麼，現在的問題就歸結為如何針對F找到它的f了。根據F和f之間的密切聯繫（F就比f多出一個self參數而已），我們可以從F得出f嗎？假設我們可以（又是假設），也就是說假設我們找到了一根魔棒，把它朝任意一個偽遞歸的F一揮，眼前一花，它就變成了真正的f了。這根魔棒如果存在的話，它具有什麼性質？我們假設這個神奇的函數叫做Y，把Y用到任何偽遞歸的函數F上就能夠得到真正的f，也就是說：
Y(F) = f
結合上面的F(f) = f，我們得到：
Y(F) = f = F(f) = F(Y(F))
也就是說，Y具有性質：
Y(F) = F(Y(F))
性質倒是找出來了，怎麼構造出這個Y卻又成了難題。一個辦法就是使用抽象法，這是從工程學的思想的角度，也就是通過不斷迭代、重構，最終找到問題的解。然而對於這裡的Y combinator，接近問題解的過程卻顯得複雜而費力，甚至過程中的有些點上的思維跳躍有點如羚羊掛角無跡可尋。然而，在這整個Y combinator介紹完了之後我們將會介紹著名的哥德爾不完備性定理，然後我們就會發現，通過哥德爾不完備性定理證明中的一個核心構造式，只需一步自然的推導就能得出我們的Y combinator。而且，最美妙的是，還可以再往下歸約，把一切都歸約到康托爾當初提出的對角線方法，到那時我們就會發現原來同樣如羚羊掛角般的哥德爾的證明其實是對角線方法的一個自然推論。數學竟是如此奇妙，我們由簡單得無法再簡單的lambda calculus系統的兩條公理居然能夠導出如此複雜如此令人目眩神迷的Y Combinator，而這些複雜性其實也只是蕩漾在定理海洋中的漣漪，撥開複雜性的迷霧我們重又發現它們居然寓於極度的簡潔之中。這就是數學之美。
讓我們先來看一看Y combinator的費力而複雜的工程學構造法，我會儘量讓這個過程顯得自然而流暢[7]：
我們再次回顧一下那個偽遞歸的求階乘函數：
let P = lambda self n. If_Else n==0 1 n*self(n-1)
我們的目標是找出P的不動點power，根據不動點的性質，只要把power傳給P，即P(power)，便能夠得到真正的遞歸函數了。
現在，關鍵的地方到了，由於：
power = P(power) // 不動點原理
這就意味著，power作為一個函數（lambda calculus裡面一切都是函數），它是自己調用了自己的。那麼，我們如何實現這樣一個能夠自己調用自己的power呢？回顧我們當初成功的一次嘗試，要實現遞歸，我們是通過增加一個間接層來進行的：
let power_gen = lambda self. P(self(self))
還記得self(self)這個形式嗎？我們在成功實現出求階乘遞歸函數的時候不就是這麼做的？那麼對於現在這個power_gen，怎麼遞歸調用？
power_gen(power_gen)
不明白的話可以回顧一下前面我們調用P(P, n)的地方。這裡power_gen(power_gen)展開後得到的是什麼呢？我們根據剛才power_gen的定義展開看一看，原來是：
P(power_gen(power_gen))
看到了嗎？也就是說：
power_gen(power_gen) => P(power_gen(power_gen))
現在，我們把power_gen(power_gen)當成整體看，不妨令為power，就看得更清楚了：
power => P(power)
這不正是我們要的答案麼？
OK，我們總結一下：對於給定的P，只要構造出一個相應的power_gen如下：
let power_gen = lambda self. P(self(self))
我們就會發現，power_gen(power_gen)這個調用展開後正是P(power_gen(power_gen))。也就是說，我們的power_gen(power_gen)就是我們苦苦尋找的不動點了！
鑄造Y Combinator
現在我們終於可以鑄造我們的Y Combinator了，Y Combinator只要生成一個形如power_gen的lambda函數然後把它應用到自身，就大功告成：
let Y = lambda F.
let f_gen = lambda self. F(self(self))
return f_gen(f_gen)
稍微解釋一下，Y是一個lambda函數，它接受一個偽遞歸F，在內部生成一個f_gen（還記得我們剛才看到的power_gen吧），然後把f_gen應用到它自身（記得power_gen(power_gen)吧），得到的這個f_gen(f_gen)也就是F的不動點了（因為f_gen(f_gen) = F(f_gen(f_gen))），而根據不動點的性質，F的不動點也就是那個對應於F的真正的遞歸函數！
如果你還覺得不相信，我們稍微展開一下看看，還是拿階乘函數說事，首先我們定義階乘函數的偽遞歸版本：
let Pwr = lambda self n. If_Else n==0 1 n*self(n-1)
讓我們把這個Pwr交給Y，看會發生什麼（根據剛才Y的定義展開吧）：
Y(Pwr) =>
let f_gen = lambda self. Pwr(self(self))
return f_gen(f_gen)
Y(Pwr)的求值結果就是裡面返回的那個f_gen(f_gen)，我們再根據f_gen的定義展開f_gen(f_gen)，得到：
Pwr(f_gen(f_gen))
也就是說：
Y(Pwr) => f_gen(f_gen) => Pwr(f_gen(f_gen))
我們來看看得到的這個Pwr(f_gen(f_gen))到底是不是真有遞歸的魔力。我們展開它（注意，因為Pwr需要兩個參數，而我們這裡只給出了一個，所以Pwr(f_gen(f_gen))得到的是一個單參（即n）的函數）：
Pwr(f_gen(f_gen)) => If_Else n==0 1 n*f_gen(f_gen) (n-1)
而裡面的那個f_gen(f_gen)，根據f_gen的定義，又會展開為Pwr(f_gen(f_gen))，所以：
Pwr(f_gen(f_gen)) => If_Else n==0 1 n* Pwr(f_gen(f_gen)) (n-1)
看到加粗的部分了嗎？因為Pwr(f_gen(f_gen))是一個接受n為參數的函數，所以不妨把它令成f（f的參數是n），這樣上面的式子就是：
f => If_Else n==0 1 n*f(n-1)
完美的階乘函數！
哥德爾的不完備性定理
瞭解哥德爾不完備性定理的可以跳到下一節，「大道至簡——康托爾的天才」
然而，漫長的Y Combinator征途仍然並非本文的最終目的，對於Y combinator的構造和解釋，只是給不瞭解lambda calculus或Y combinator的讀者看的。關鍵是馬上你會看到Y combinator可以由哥德爾不完備性定理證明的一個核心構造式一眼瞧出來！
讓我們的思緒回到1931年，那個數學界風起雲湧的年代，一個名不經傳的20出頭的學生，在他的博士論文中證明了一個驚天動地的結論。
在那個年代，希爾伯特的數學天才就像太陽的光芒一般奪目，在關於數學嚴格化的
大紛爭中希爾伯特帶領的形式主義派系技壓群雄，得到許多當時有名望的數學家的支持。希爾伯特希望借助於形式化的手段，抽掉數學證明中的意義，把數學證明抽
象成一堆無意義的符號轉換，就連我們人類賴以自豪的邏輯推導，也不過只是一堆堆符號轉換而已（想起lambda calculus系統了吧：）)。
這樣一來，一個我們日常所謂的，帶有直觀意義和解釋的數學系統就變成了一個純粹由無意義符號表達的、公理加上推導規則所構成的形式系統，而數學證明呢，只
不過是在這個系統內玩的一個文字遊戲。令人驚訝的是，這樣一種做法，真的是可行的！數學的意義，似乎竟然真的可以被抽掉！另一方面，一個形式系統具有非常
好的性質，平時人們證明一個定理所動用的推導，變成了純粹機械的符號變換。希爾伯特希望能夠證明，在任一個無矛盾的形式系統中所能表達的所有陳述都要麼能
夠證明要麼能夠證偽。這看起來是個非常直觀的結論，因為一個結論要麼是真要麼是假，而它在它所處的領域/系統中當然應該能夠證明或證偽了（只要我們能夠揭示出該系統中足夠多的真理）。
然而，哥德爾的證明無情的擊碎了這一企圖，哥德爾的證明揭示出，任何足夠強到蘊含了皮亞諾算術系統（PA）的一致（即無矛盾）的系統都是不完備的，所謂不完備也就是說在系統內存在一個為真但無法在系統內推導出的命題。這在當時的數學界揭起了軒然大波，其證明不僅具有數學意義，而且蘊含了深刻的哲學意義。從那時起這一不完備性定理就被引申到自然科學乃至人文科學的各個角落…至今還沒有任何一個數學定理居然能夠產生這麼廣泛而深遠的影響。
哥德爾的證明非常的長，達到了200多頁紙，但其中很大的成分是用在了一些輔助性的工作上面，比如佔據超過1/3紙
張的是關於一個形式系統如何映射到自然數，也就是說，如何把一個形式系統中的所有公式都表示為自然數，並可以從一自然數反過來得出相應的公式。這其實就是
編碼，在我們現在看來是很顯然的，因為一個程序就可以被編碼成二進制數，反過來也可以解碼。但是在當時這是一個全新的思想，也是最關鍵的輔助性工作之一，
另一方面，這正是「程序即數據」的最初想法。
現在我們知道，要證明哥德爾的不完備性定理，只需在假定的形式系統T內表達出一個為真但無法在T內推導出（證明）的命題。於是哥德爾構造了這樣一個命題，用自然語言表達就是：命題P說的是「P不可在系統T內證明」（這裡的系統T當然就是我們的命題P所處的形式系統了），也就是說「我不可以被證明」，跟著名的說謊者悖論非常相似，只是把「說謊」改成了「不可以被證明」。我們注意到，一旦這個命題能夠在T內表達出來，我們就可以得出「P為真但無法在T內推導出來」的結論，從而證明T的不完備性。為什麼呢？我們假設T可以證明出P，而因為P說的就是P不可在系統T內證明，於是我們又得到T無法證明出P，矛盾產生，說明我們的假設「T可以證明P」是錯誤的，根據排中律，我們得到T不可以證明P，而由於P說的正是「T不可證明P」，所以P就成了一個正確的命題，同時無法由T內證明！
如果你足夠敏銳，你會發現上面這番推理本身不就是證明嗎？其證明的結果不就是P是正確的？然而實際上這番證明是位於T系統之外的，它用到了一個關於T系統的假設「T是一致（無矛盾）的」，這個假設並非T系統裡面的內容，所以我們剛才其實是在T系統之外推導出了P是正確的，這跟P不能在T之內推導出來並不矛盾。所以別擔心，一切都正常。
那麼，剩下來最關鍵的問題就是如何用形式語言在T內表達出這個P，上面的理論雖然漂亮，但若是P根本沒法在T內表達出來，我們又如何能證明「T內存在這個為真但無法被證明的P」呢？那一切還不是白搭？
於是，就有了哥德爾證明裡面最核心的構造，哥德爾構造了這樣一個公式：
N(n) is unprovable in T
這個公式由兩部分構成，n是這個公式的自由變量，它是一個自然數，一旦給定，那麼這個公式就變成一個明確的命題。而N則是從n解碼出的貨真價實的（即我們常見的符號形式的）公式（記得哥德爾的證明第一部分就是把公式編碼嗎？）。」is unprovable in T」則是一個謂詞，這裡我們沒有用形式語言而是用自然語言表達出來的，但哥德爾證明了它是可以用形式語言表達出來的，大致思路就是：一個形式系統中的符號數目是有限的，它們構成這個形式系統的符號表。於是，我們可以依次枚舉出所有長度為1的串，長度為2的串，長度為3的串… 此外根據形式系統給出的語法規則，我們可以檢查每個串是否是良構的公式（well formed formula，簡稱wff，其實也就是說，是否符合語法規則，前面我們在介紹lambda calculus的時候看到了，一個形式系統是需要語法規則的，比如邏輯語言形式化之後我們就會看到P->Q是一個wff，而->PQ則不是），因而我們就可以枚舉出所有的wff來。最關鍵的是，我們觀察到形式系統中的證明也不過就是由一個個的wff構成的序列（想想推導的過程，不就是一個公式接一個公式嘛）。而wff構成的序列本身同樣也是由符號表內的符號構成的串。所以我們只需枚舉所有的串，對每一個串檢查它是否是一個由wff構成的序列（證明），如果是，則記錄下這個wff序列（證明）的最後一個wff，也就是它的結論。這樣我們便枚舉出了所有的可由T推導出的定理。然後為了表達出」X is unprovable in T」，本質上我們只需說「不存在這樣一個自然數S，它所解碼出來的wff序列以X為終結」！這也就是說，我們表達出了「is unprovable in T」這個謂詞。
我們用UnPr(X)來表達「X is unprovable in T」，於是哥德爾的公式變成了：
UnPr( N(n) )
現在，到了最關鍵的部分，首先我們把這個公式簡記為G(n)——別忘了G內有一個自由變量n，所以G現在還不是一個命題，而只是一個公式，所以談不上真假：
G(n): UnPr( N(n) )
又由於G也是個wff，所以它也有自己的編碼g，當然g是一個自然數，現在我們把g作為G的參數，也就是說，把G裡面的自由變量n替換為g，我們於是得到一個真正的命題：
G(g): UnPr( G(g) )
用自然語言來說，這個命題G(g)說的就是「我是不可在T內證明的」。看，我們在形式系統T內表達出了「我是不可在T內證明的」這個命題。而我們一開始已經講過了如何用這個命題來推斷出G(g)為真但無法在T內證明，於是這就證明了哥德爾的不完備性定理[8]。
哥德爾的不完備性定理被稱為20世紀數學最重大的發現（不知道有沒有「之一」:) ）現在我們知道為真但無法在系統內證明的命題不僅僅是這個詭異的「哥德爾命題」，還有很多真正有意義的明確命題，其中最著名的就是連續統假設，此外哥德巴赫猜想也有可能是個沒法在數論系統中證明的真命題。
從哥德爾公式到Y Combinator
哥德爾的不完備性定理證明了數學是一個未完結的學科，永遠有需要我們以人的頭腦從系統之外去用我們獨有的直覺發現的東西。羅傑·彭羅斯在《The Emperor's New Mind》中
用它來證明人工智能的不可實現。當然，這個結論是很受質疑的。但哥德爾的不完備性定理的確還有很多很多的有趣推論，數學的和哲學上的。哥德爾的不完備性定
理最深刻的地方就是它揭示了自指（或稱自引用，遞歸調用自身等等）結構的普遍存在性，我們再來看一看哥德爾命題的絕妙構造：
G(n): UnPr( N(n) )
我們注意到，這裡的UnPr其實是一個形式化的謂詞，它不一定要說「X在T內可證明」，我們可以把它泛化為一個一般化的謂詞，P：
G(n): P( N(n) )
也就是說，對於任意一個單參的謂詞P，都存在上面這個哥德爾公式。然後我們算出這個哥德爾公式的自然數編碼g，然後把它扔給G，就得到：
G(g): P( G(g) )
是不是很熟悉這個結構？我們的Y Combinator的構造不就是這樣一個形式？我們把G和P都看成一元函數，G(g)可不正是P這個函數的不動點麼！於是，我們從哥德爾的證明裡面直接看到了Y Combinator！
至於如何從哥德爾的證明聯繫到停機問題，就留給你去解決吧:) 因為更重要的還在後面，我們看到，哥德爾的證明雖然巧妙至極，然而其背後的思維過程仍然飄逸而不可捉摸，至少我當時看到G(n)的時候，「乃大驚」「不知所從出」，他怎麼想到的？難道是某一個瞬間「靈光一現」？一般我是不信這一說的，已經有越來越多的科學研究表明一瞬間的「靈感」往往是潛意識乃至表層意識長期思考的結果。哥德爾天才的證明也不例外，我們馬上就會看到，在這個神秘的構造背後，其實隱藏著某種更深的東西，這就是康托爾在19世紀80年代研究無窮集合和超限數時引入的對角線方法。這個方法彷彿有種神奇的力量，能夠揭示出某種自指的結構來，而同時，這又是一個極度簡單的手法，通過它我們能夠得到數學裡面一些非常奇妙的性質。無論是哥德爾的不完備性定理還是再後來丘齊建立的lambda calculus，抑或我們非常熟悉的圖靈機理論裡的停機問題，其實都只是這個手法簡單推演的結果！
大道至簡——康托爾的天才
「大道至簡」這個名詞或許更多出現在文學和哲學裡面，一般用在一些模模糊糊玄玄乎乎的哲學觀點上。然而，用在這裡，數學上，這個名詞才終於適得其所。大道至簡，看上去最複雜的理論其實建立在一個最簡單最純粹的道理之上。
康托爾在無窮集合和超限數方面的工作主要集中在兩篇突破性的論文上，這也是我
所見過的最純粹最美妙的數學論文，現代的數學理論充斥了太多複雜的符號和概念，很多時候讓人看不到最本質的東西，當然，不否認這些東西很多也是有用的，然
而，要領悟真正的數學美，像集合論和數論這種純粹的東西，真的非常適合。不過這裡就不過多談論數學的細節了，只說康托爾引入對角線方法的動機和什麼是對角
線方法。
神奇的一一對應
康托爾在研究無窮集合的時候，富有洞察性地看到了對於無窮集合的大小問題，我們不能再使用直觀的「所含元素的個數」來描述，於是他創造性地將一一對應引入進來，兩個無窮集合「大小」一樣當且僅當它們的元素之間能夠構成一一對應。這是一個非常直觀的概念，一一對應嘛，當然個數相等了，是不是呢？然而這同時就是它不直觀的地方了。對於無窮集合，我們日常的所謂「個數」的概念不管用了，因為無窮集合裡面的元素個數本就是無窮多個。不信我們來看一個小小的例子。我們說自然數集合能夠跟偶數集合構成一一對應，從而自然數集合跟偶數集合裡面元素「個數」是一樣多的。怎麼可能？偶數集合是自然數集合的真子集，所有偶數都是自然數，但自然數里面還包含奇數呢，說起來應該是二倍的關係不是？不是！我們只要這樣來構造一一對應：
1 2 3 4 …
2 4 6 8 …
用函數來描述就是 f(n) = 2n。檢驗一下是不是一一對應的？不可思議對嗎？還有更不可思議的，自然數集是跟有理數集一一對應的！對應函數的構造就留給你解決吧，提示，按如下方式來挨個數所有的有理數：
1/1 1/2 2/1 1/3 2/2 3/1 1/4 2/3 3/2 4/1 …
用這種一一對應的手法還可以得到很多驚人的結論，如一條直線上所有的點跟一個平面上所有的點構成一一對應（也就是說複數集合跟實數集合構成一一對應）。以致於連康托爾自己都不敢相信自己的眼睛了，這也就是為什麼他在給戴得金的信中會說「我看到了它，卻不敢相信它」的原因。
然而，除了一一對應之外，還有沒有不能構成一一對應的兩個無窮集合呢？有。實數集合就比自然數集合要「大」，它們之間實際上無法構成一一對應。這就是康托爾的對角線方法要解決的問題。
實數集和自然數集無法構成一一對應？！
我們只需將實數的小數位展開，並且我們假設實數集能夠與自然數集一一對應，也就是說假設實數集可列，所以我們把它們與自然數一一對應列出，如下：
1 a10.a11a12a13…
2 a20.a21a22a23…
3 a30.a31a32a33…
4 …
5 …
（註：aij裡面的ij是下標）
現在，我們構造一個新的實數，它的第i位小數不等於aii。也就是說，它跟上面列出的每一個實數都至少有一個對應的小數位不等，也就是說它不等於我們上面列出的所有實數，這跟我們上面假設已經列出了所有實數的說法相矛盾。所以實數集只能是不可列的，即不可與自然數集一一對應！這是對角線方法的最簡單應用。
對角線方法——停機問題的深刻含義
對角線方法有很多非常奇妙的結論。其中之一就是文章一開始提到的停機問題。我想絕大多數人剛接觸停機問題的時候都有一個問題，圖靈怎麼能夠想到這麼詭異的證明，怎麼能構造出那個詭異的「說停機又不停機，說不停機又停機」的悖論機器。馬上我們就會看到，這其實只是對角線方法的一個直接結論。
還是從反證開始，我們假設存在這樣一個圖靈機，他能夠判斷任何程序在任何輸入上是否停機。由於所有圖靈機構成的集合是一個可列集（也就是說，我們可以逐一列出所有的圖靈機，嚴格證明見我以前的一篇文章《圖靈機雜思》），所以我們可以很自然地列出下表，它表示每個圖靈機分別在每一個可能的輸入（1,2,3,…）下的輸出，N表示無法停機，其餘數值則表示停機後的輸出：
1 2 3 4 …
M1 N 1 N N …
M2 2 0 N 0 …
M3 0 1 2 0 …
M4 N 0 5 N …
…
M1，M2，M3 … 是逐一列出的圖靈機，並且，注意，由於程序即數據，每個圖靈機都有唯一編碼，所以我們規定在枚舉圖靈機的時候Mi其實就代表編碼為i的圖靈機，當然這裡很多圖靈機將會是根本沒用的玩意，但這不要緊。此外，最上面的一行1 2 3 4 … 是輸入數據，如，矩陣的第一行代表M1分別在1，2，3，…上面的輸出，不停機的話就是N。
我們剛才假設存在這樣一個圖靈機H，它能夠判斷任何程序在任何輸入上能否停機，換句話說，H(i,j)（i是Mi的編碼）能夠給出「Mi(j)」是N（不停）呢還是給出一個具體的結果（停）。
我們現在來運用康托爾的對角線方法，我們構造一個新的圖靈機P，P在1上的輸出行為跟M1(1)「不一樣」，在2上的輸出行為跟M2(2)「不一樣」，…總之P在輸入i上的輸出跟Mi(i)不一樣。只需利用一下我們萬能的H，這個圖靈機P就不難構造出來，如下：
P(i):
if( H(i, i) == 1 ) then // Mi(i) halts
return 1 + Mi(i)
else // if H(i, i) == 0 (Mi(i) doesn't halt)
return 0
也就是說，如果Mi(i)停機，那麼P(i)的輸出就是Mi(i)+1，如果Mi(i)不停機的話，P(i)就停機且輸出0。這就保證了P(i)的輸出行為跟Mi(i)反正不一樣。現在，我們注意到P本身是一個圖靈機，而我們上面已經列出了所有的圖靈機，所以必然存在一個k，使得Mk = P。而兩個圖靈機相等當且僅當它們對於所有的輸入都相等，也就是說對於任取的n，有Mk(n) = P(n)，現在令n=k，得到Mk(k)=P(k)，根據上面給出的P的定義，這實際上就是：
Mk(k) = P(k) =
1+Mk(k) if Mk(k) halts
0 if Mk(k) doesn't halt
看到這個式子裡蘊含的矛盾了嗎？如果Mk(k)停機，那麼Mk(k)=1+Mk(k)；如果Mk(k)不停機，則Mk(k)=0（給出結果0即意味著Mk(k)停機）；不管哪種情況都是矛盾。於是我們得出，不存在那樣的H。
這個對角線方法實際上說明了，無論多聰明的H，總存在一個圖靈機的停機行為是它無法判斷的。這跟哥德爾定理「無論多『完備』的形式化公理系統，都存在一個『哥德爾命題』是無法在系統內推導出來的」從本質上其實是一模一樣的。只不過我們一般把圖靈的停機問題稱為「可判定問題」，而把數學的稱為「可證明問題」。
等等！如果我們把那個無法判定是否停機的圖靈機作為算法的特例納入到我們的H當中呢？我們把得到的新的判定算法記為H1。然而，可惜的是，在H1下，我們又可以相應地以同樣的手法從H1構造出一個無法被它（H1）
判定的圖靈機來。你再加，我再構造，無論你加多少個特例進去，我都可以由同樣的方式構造出來一個你無法夠到的圖靈機，以彼之矛，攻彼之盾。其實這也是哥德
爾定理最深刻的結論之一，哥德爾定理其實就說明了無論你給出多少個公理，即無論你建立多麼完備的公理體系，這個系統裡面都有由你的那些公理出發所推導不到
的地方，這些黑暗的角落，就是人類直覺之光才能照射到的地方！
本節我們從對角線方法證明了圖靈的停機問題，我們看到，對角線方法能夠揭示出某種自指結構，從而構造出一個「悖論圖靈機」。實際上，對角線方法是一種有深遠影響的方法，哥德爾的證明其實也是這個方法的一則應用。證明與上面的停機問題證明如出一轍，只不過把Mi換成了一個形式系統內的公式fi，具體的證明就留給聰明的你吧:)我們現在來簡單的看一下這個奇妙方法的幾個不那麼明顯的推論。
學過邏輯的人大約肯定是知道著名的羅素悖論的，羅素悖論用數學的形式來描述就是：
這個悖論最初是從康托爾的無窮集合論裡面引申出來的。當初康托爾在思考無窮集合的時候發現可以稱「一切集合的集合」，這樣一個集合由於它本身也是一個集合，所以它就屬於它自身。也就是說，我們現在可以稱世界上存在一類屬於自己的集合，除此之外當然就是不屬於自己的集合了。而我們把所有不屬於自己的集合收集起來做成一個集合R，這就是上面這個著名的羅素悖論了。
我們來看R是否屬於R，如果R屬於R，根據R的定義，R就不應該屬於R。而如果R不屬於R，則再次根據R的定義，R就應該屬於R。
這個悖論促使了集合論的公理化。後來策梅羅公理化的集合論裡面就不允許X屬於X（不過可惜的是，儘管如此還是沒法證明這樣的集合論不可能產生出新的悖論。而且永遠沒法證明——這就是哥德爾第二不完備性定理的結論——一個包含了PA的形式化公理系統永遠無法在內部證明其自身的一致（無矛盾）性。從而希爾伯特想從元數學推出所有數學系統的一致性的企圖也就失敗了，因為元數學的一致性又得由元元數學來證明，後者的一致性又得由元元元數學來證明…）。
這裡我們只關心羅素是如何想出這個絕妙的悖論的。還是對角線方法！我們羅列出所有的集合，S1,S2,S3 …
S1 S2 S3 …
S1 0 1 1 …
S2 1 1 0 …
S3 0 0 0 …
… …
右側縱向列出所有集合，頂行橫向列出所有集合。0/1矩陣的(i,j)處的元素表示Si是否包含Sj，記為Si(j)。現在我們只需構造一個新的0/1序列L，它的第i位與矩陣的(i,i)處的值恰恰相反：L(i) = 1-Si(i)。我們看到，這個新的序列其實對應了一個集合，不妨也記為L，L(i)表示L是否包含Si。根據L的定義，如果矩陣的(i,i)處值為0（也就是說，如果Si不包含Si），那麼L這個集合就包含Si,否則就不包含。我們注意到這個新的集合L肯定等於某個Sk（因為我們已經列出了所有的集合），L = Sk。既然L與Sk是同一集合，那麼它們肯定包含同樣的元素，從而對於任意n，有L(n) = Sk(n)。於是通過令n=k，得到L(k) = Sk(k)，而根據L的定義，L(k) = 1- Sk(k)。這就有Sk(k) = 1-Sk(k)，矛盾。
通過抽象簡化以上過程，我們看到，我們構造的L其實是「包含了所有不包含它自身的集合的集合」，用數學的描述正是羅素悖論！
敏銳的你可能會注意到所有集合的數目是不可數的從而根本不能S1,S2…的一一列舉出來。沒錯，但通過假設它們可以列舉出來，我們發現了一個與可列性無關的悖論。所以這裡的對角線方法其實可以說是一種啟發式方法。
同樣的手法也可以用到證明P(A)（A的所有子集構成的集合，也叫冪集）無法跟A構成一一對應上面。證明就留給聰明的你了:)
希爾伯特第十問題結出的碩果
希爾伯特是在1900年巴黎數學家大會上提出著名的希爾伯特第十問題的，簡言之就是是否存在一個算法，能夠計算任意丟番圖方程是否有整根。要解決這個問題，就得先嚴格定義「算法」這一概念。為此圖靈和丘齊分別提出了圖靈機和lambda calculus這兩個概念，它們從不同的角度抽象出了「有效（機械）計算」的概念，著名的圖靈——丘齊命題就是說所有可以有效計算出來的問題都可以由圖靈機計算出來。實際上我們已經看到，丘齊的lambda calculus其實就是數學推理系統的一個形式化。而圖靈機則是把這個數學概念物理化了。而也正因為圖靈機的概念隱含了實際的物理實現，所以馮·諾依曼才據此提出了奠定現代計算機體系結構的馮·諾依曼體系結構，其遵循的，正是圖靈機的概念。而「程序即數據」的理念，這個發端於數學家哥德爾的不完備性定理的證明之中的理念，則早就在黑暗中預示了可編程機器的必然問世。
對角線方法——回顧
我們看到了對角線方法是如何簡潔而深刻地揭示出自指或遞歸結構的。我們看到了著名的不完備性定理、停機問題、Y Combinator、羅素悖論等等等等如何通過這一簡潔優美的方法推導出來。這一誕生於康托爾的天才的手法如同一條金色的絲線，把位於不同年代的偉大發現串聯了起來，並且將一直延續下去…
P.S
1. lambda calculus裡面的「停機問題」
實際上lambda calculus裡面也是有「停機問題」的等價版本的。其描述就是：不存在一個算法能夠判定任意兩個lambda函數是否等價。所謂等價當然是對於所有的n,有f(n)=g(n)了。這個問題的證明更加能夠體現對角線方法的運用。仍然留給你吧。
3. 文章起名《康托爾、哥德爾、圖靈——永恆的金色對角線》其實是為了紀念看過的一本好書GEB，即《Godel、Escher、Bach-An Eternal Golden Braid》中文譯名《哥德爾、埃舍爾、巴赫——集異璧之大成》——商務印書館出版。對於一本定價50元居然能夠在douban上賣到100元的二手舊書，我想無需多說。另，幸福的是，電子版可以找到:)
4. 其實很久前想寫的是一篇《從哥德爾到圖靈》，但那篇寫到1/3不到就擱下了，一是由於事務，二是總覺得少點什麼。呵呵，如今把康托爾扯進來，也算是完成當時扔掉的那一篇吧。
5. 這
恐怕算是寫得最曲折的一篇文章了。不僅自己被這些問題搞得有點暈頭轉向（還好總算走出來），更因為要把這些東西自然而然的串起來，也頗費周章。很多時候是
利用吃飯睡覺前或走路的時間思考本質的問題以及如何表達等等，然後到紙上一氣呵成。不過同時也鍛鍊了不拿紙筆思考數學的能力，呵呵。
6. 關於圖靈的停機問題、Y Combinator、哥德爾的不完備性定理以及其它種種與康托爾的對角線之間的本質聯繫，幾乎查不到完整系統的深入介紹，一些書甚至如《The Emperor's New Mind》也只是介紹了與圖靈停機問題之間的聯繫（已經非常的難得了），google和baidu的結果也是基本沒有頭緒。很多地方都是一帶而過讓人幹著急。所以看到很多地方介紹這些定理和構造的時候都是弄得人暈頭轉向的，絕大部分人在面對如Y Combinator、不完備性定理、停機問題的時候都把注意力放在力圖理解它是怎麼運作的上面了，卻使人看不到其本質上從何而來，於是人們便對這些東東大為驚嘆。這使我感到很不痛快，如隔靴搔癢般。這也是寫這篇文章的主要動機之一。
Reference
[1] 《數學——確定性的喪失》
[2] 也有觀點認為函數式編程語言之所以沒有廣泛流行起來是因為一些實際的商業因素。
[3] Douglas R.Hofstadter的著作《Godel, Escher, Bach: An Eternal Golden Braid》（《哥德爾、艾舍爾、巴赫——集異璧之大成》）就是圍繞這一思想寫出的一本奇書。非常建議一讀。
[4] 《數學——確定性的喪失》
[5] 雖然我覺得那個系徽做得太複雜，要表達這一簡潔優美的思想其實還能有更好的方式。
[6] 關於如何在lambda calculus系統裡實現「+」操作符以及自然數等等，可參見這裡，這裡，和這裡。
[7] g9的blog（負暄瑣話）http://blog.csdn.net/g9yuayon/ 上有一系列介紹lambda calculus的文章（當然，還有其它好文章:)），非常不錯，強烈推薦。最近的兩篇就是介紹Y combinator的。其中有一篇以javaScript語言描述了迭代式逐步抽象出Y Combinator的過程。
[8]
實際上這只是第一不完備性定理，它還有一個推論，被稱為第二不完備性定理，說的是任一個系統T內無法證明這個系統本身的一致性。這個定理的證明核心思想如
下：我們前面證明第一不完備性定理的時候用的推斷其實就表明 Con/T -> G(g)
（自然語言描述就是，由系統T的無矛盾，可以推出G(g)成立），而這個「Con/T ->
G(g)」本身又是可以在T內表達且證明出來的（具體怎麼表達就不再多說了）——只需要用排中律即可。於是我們立即得到，T裡面無法推出Con/T，因為
一旦推出Con/T就立即推出G(g)從而推出UnPr(G(g))，這就矛盾了。所以，Con/T無法在T內推出（證明）。 | 
留言列表
留言列表