康托爾、哥德爾、圖靈——永恆的金色對角線

——康托爾算法

計算機是數學家一次失敗思考的產物。編程

——無名氏編程語言

哥德爾的不完備性定理震撼了20世紀數學界的天空，其數學意義顛覆了希爾伯特的形式化數學的宏偉計劃，其哲學意義直到21世紀的今天仍然不斷被延伸到各個天然學科，深入影響着人們的思惟。圖靈爲了解決希爾伯特著名的第十問題而提出有效計算模型，進而做出了可計算理論和現代計算機的奠定性工做，著名的停機問題給出了機械計算模型的能力極限，其深入的意義和漂亮的證實使它成爲可計算理論中的標誌性定理之一。丘齊，跟圖靈同時代的天才，則從另外一個抽象角度提出了lambda算子的思想，與圖靈機抽象的傾向於硬件性不一樣，丘齊的lambda算子理論是從數學的角度進行抽象，不關心運算的機械過程而只關心運算的抽象性質，只用最簡潔的幾條公理便創建起了與圖靈機徹底等價的計算模型，其體現出來的數學抽象美開出了函數式編程語言這朵奇葩，Lisp、Scheme、Haskell… 這些以抽象性和簡潔美爲特色的語言至今仍然活躍在計算機科學界，雖然因爲其本質上源於lambda算子理論的抽象方式不符合人的思惟習慣從而註定沒法成爲主流的編程語言[2]，然而這仍然沒法妨礙它們成爲編程理論乃至計算機學科的最佳教本。而誕生於函數式編程語言的神奇的Y combinator至今仍然讓人們陷入深沉的震撼和反思當中…ide

然而，這一切的一切，看似不很相關卻又有點相關，認真思考其關係卻又有點一頭霧水的背後，其實隱隱藏着一條線，這條線把它們從本質上串到了一塊兒，而順着時光的河流逆流而上，咱們將會看到，這條線的盡頭，不是別人，正是隻手撥開被不嚴密性問題困擾的19世紀數學界陰沉天空的天才數學家康托爾，康托爾創造性地將一一對應和對角線方法運用到無窮集合理論的創建當中，這個被希爾伯特稱爲「誰也沒法將咱們從康托爾爲咱們創造的樂園中驅逐出去」、被羅素稱爲「19世紀最偉大的智者之一」的人，他在集合論方面的工做終於驅散了不嚴密性問題帶來的陰霾，彷彿一道金色的陽光刺破烏雲，19世紀的數學終於看到了真正嚴格化的曙光，數學終於得以站在了史無前例的堅固的基礎之上；集合論至今還是數學裏最基礎和最重要的理論之一。而康托爾當初在研究無窮集合時最具天才的方法之一——對角線方法——則帶來了極其深遠的影響，其純粹而直指事物本質的思想如洪鐘大呂般響徹數學和哲學的每個角落[3]。隨着本文的展開，你將會看到，剛纔提到的一切，歌德爾的不完備性定理，圖靈的停機問題，lambda算子理論中神奇的Y combinator、乃至著名的羅素悖論、理髮師悖論等等，其實都源自這個簡潔、純粹而同時又是最優美的數學方法，反過來講，從康托爾的對角線方法出發，咱們能夠垂手可得地推導出哥德爾的不完備性定理，而由後者又能夠輕易導出停機問題和Y combinator，實際上，咱們將會看到，後二者也能夠直接由康托爾的對角線方法導出。尤爲是Y combinator，這個形式上繞來繞去，本質上捉摸不透，看上去神祕莫測的算子，其實只是一個很是天然而然的推論，若是從哥德爾的不完備性定理出發，它甚至比停機問題還要來得直接簡單。總之，你將會看到這些看似深奧的理論是如何由一個至爲簡單而又至爲深入的數學方法得出的，你將會看到最純粹的數學美。函數式編程

圖靈的停機問題(The Halting Problem)函數

瞭解停機問題的能夠直接跳過這一節，到下一節「Y Combinator」，瞭解後者的再跳到下一節「哥德爾的不完備性定理」oop

咱們仍是從圖靈著名的停機問題提及，一來它相對來講是咱們要說的幾個定理當中最簡單的，二來它也最貼近程序員。實際上，我之前曾寫過一篇關於圖靈機的文章，有興趣的讀者能夠從那篇開始，那篇主要是從理論上闡述，因此這裏咱們打算避開抽象的理論，換一種符合程序員思惟習慣的直觀方式來加以解釋。ui

停機問題

不存在這樣一個程序（算法），它可以計算任何程序（算法）在給定輸入上是否會結束（停機）。

那麼，如何來證實這個停機問題呢？反證。假設咱們某一天真作出了這麼一個極度聰明的萬能算法（就叫God_algo吧），你只要給它一段程序（二進制描述），再給它這段程序的輸入，它就能告訴你這段程序在這個輸入上會不會結束（停機），咱們來編寫一下咱們的這個算法吧：

bool God_algo(char* program, char* input)

{

if(<program> halts on <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)：

<expr> ::= lambda <identifier-list>. <expr>

<expr> ::= (<expr> <expr>)

前兩條語法用於生成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)

如今<self>處不是缺乏「這個函數自身」嘛，既然不能直接填入「這個函數自身」，咱們能夠增長一個參數，也就是說，把<self>參數化：

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 = {X:X不屬於X};

這個悖論最初是從康托爾的無窮集合論裏面引伸出來的。當初康托爾在思考無窮集合的時候發現能夠稱「一切集合的集合」，這樣一個集合因爲它自己也是一個集合，因此它就屬於它自身。也就是說，咱們如今能夠稱世界上存在一類屬於本身的集合，除此以外固然就是不屬於本身的集合了。而咱們把全部不屬於本身的集合收集起來作成一個集合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)了。這個問題的證實更加可以體現對角線方法的運用。仍然留給你吧。

2. 負喧瑣話(http://blog.csdn.net/g9yuayon)是個很是不錯的blog:)。g9的文字輕鬆幽默，並且有不少名人八卦能夠養眼，真的灰常…灰常…不錯哦。此外g9老兄仍是個理論功底很是紮實的牛。因此，anyway，看了他的blog就知道啦！最初這篇文章的動機也正是看了上面的一篇關於Y Combinator的鑄造過程的介紹，因而想揭示一些更深的東西，因而便有了本文。

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內推出（證實）。