永恆的金色對角線

知識 08-18

永恆的金色對角線

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

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

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

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

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

停機問題

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

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

bool God_algo(char* program, char* input){

if(

halts on )

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演算法的存在性，便不成立了。正如拉格朗日所說：「陛下，我們不需要（上帝）這個假設」。

這個證明相信每個程序員都能夠容易的看懂。然而，這個看似不可捉摸的技巧背後其實隱藏著深刻的數學原理（甚至是哲學原理）。在沒有認識到這一數學原理之前，至少我當時是對於圖靈如何想出這一絕妙證明感到無法理解。但後面，在介紹完了與圖靈的停機問題「同構」的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的計算機科學系將它做成系徽也就不足為奇了。

當然，要了解這個神奇的運算元，我們需要一點點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*(n-1)

當然，上面的程序假定了If_Else是一個已經定義好的三元操作符（你可以想像C的「?:」操作符，後面跟的三個參數分別是判斷條件、成功後求值的表達式、失敗後求值的表達式。那麼很顯然，這個定義裡面有一個地方沒法解決，那就是那個地方我們應該填入什麼呢？很顯然，熟悉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*(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)