如何猜出 Y combinator

先約定幾個記号:

定義用一個冒号加等号表示“:=”，

表達式全等用兩個等号表示“==”，

歸約意義上的相等用一個等号表示“=”，“==”蘊涵“=”。

由于lambda演算不能定義符号，是以像這樣的遞歸定義是不能被求值的：

如何在lambda驗算中實作遞歸？從最簡單的遞歸函數開始。希望能帶來一些啟發。

首先，我們的目标是找出一個無限循環的lambda表達式。另外額外要求這個表達式最短。

一個lambda表達式隻可能有三種形式：

符号（x, y, z等等），

函數（如(lambda (x) x)），

應用（英文application，即函數調用，如調用函數func，參數x寫作：(func x)）。

第1、2種形式又稱為值（value），因為他們不能被歸約了。一個無限循環的表達式隻能是第3種形式：

考慮exp1。exp1是個函數，或者能被歸約成函數的應用。如果exp1是應用，那麼exp1要麼會歸約到一個函數，要麼無限循環。如果exp1無限循環，就和我們的最短假設沖突，是以exp1會歸約到一個函數。如果exp1會歸約到一個函數，那麼和exp1是一個函數沒什麼差別。簡單考慮，假設exp1是個函數：

那麼

為了讓表達式無限循環，我們希望：

是以body應該是個應用:

從最後一個條件可以推出：

另外還能看出，表達式exp1中包含了一個和exp2相等的子表達式。滿足這個條件的最簡單的exp1就是和exp2相等的exp1。

綜合幾個條件：

于是我們要找的無限循環的表達式是:

這個表達式就是lambda演算裡的\(\Omega\)表達式。\(\Omega\)表達式循環的關鍵在于(f f)形式的表達式，即自己應用到自己。\(\Omega\)包含了三個(f f)形式的表達式。

一般來說，遞歸函數長這個樣子：

body[target]的意思是一個包含target這個符号的表達式，args表示這是一個任意個數參數的函數。在這個表達式中，target是一個無限制的符号。一個包含無限制符号的表達式不能被求值。Lambda演算中限制一個符号的方法是用lambda關鍵字，為了讓target變成限制符号，我們改寫表達式：

為了避免混淆，上面将target改名成f（\(\alpha\)歸約），target仍然表示我們想要的遞歸函數的表達式。target和p有如下關系：

順便一提，可以看出我們在尋找的target是p的一個不動點。

接下來考慮如何找target。記得尋找\(\Omega\)的啟發嗎？我們猜測target是一個(g g)形式的表達式：

根據最後一個條件可以看出：

把p提取到參數位置：

這個Y就是Y combinator。

最簡單的無限循環函數是：

利用Y combinator來生成這個函數的lambda表達式看看會得到什麼？

呼，要對齊這麼多括弧真不容易。注意到（\(\eta\)歸約）：

是以: