Lambda演算（二）歸約！歸約！歸約！

（一）

這裏先不列出λ項的正式定義，只記住λ表達式語義上的構造方式爲：

1. x

一個單獨的變量名是一個λ項表達式；

2. (λx.M)

該λ表示一個函數。 其中 M 是這個函數的函數體，M 自己也是一個 λ項。

除了 x 以外，M 中可能還有其餘變量名，λ 這個符號用於指示函數體 M 的參數爲 x。

了便於理解，能夠將 M 看做函數體，x 看做形參，即變量名。

 

例如：λx.x+3 即表示一個函數 f(x) = x+3，該函數會返回x與3相加的結果

要注意的是，我這裏的寫法並不規範，在λ表達式中，二元運算符是做爲前綴的。x+3 應該寫做 (+ x 3)。因此這個表達式的正規寫法是 λx.(+ x 3)。至於爲何，咱們以後再講。

3. (M N)

其中 M，N 均爲λ項表達式。

若是 M 自己是一個函數，咱們說將函數 M 應用於 N。若是 M 不是函數，不接受參數，N 將在求值的過程當中被忽略。

例如：（λx.(+ x 3) 4），其中M爲表達式 λx.x+3，N 爲 4。這個表達式表示將函數應用於 4，即f(4) 

 

因此一個典型的λ表達式具備以下形式：

 (λx.M) N，爲了方便去掉括號寫做 λx.M N

 

其中 M 是函數體，x 能夠看做形參，即變量名， N 能夠看做實參，即變量值。

 

函數自己也能夠做爲參數，例如（λx.x）（λx.(+x 3)),  表達式左邊就是一個函數，這個函數將返回它本身的參數，將這個函數應用於咱們以前說的函數 f，參數是 f，那麼這個函數將返回 f。

 

如此一來，第一種形式的λ表達式表明一個變量；

第二種表達式表明一個函數；

第三種表達式則表明將函數應用於一個值，即一次函數調用。

 

（二）歸約

第一種表達式的值即它自己；

第二種表達式的值表示這個函數自己；

所以，在討論求值時，咱們只關心第三種，即將一個函數應用於另外一個λ表達式時，如何計算它的值。

 

如上所述，λ表達式的應用等效於一次函數調用。咱們知道，調用函數的時候，會將全部的形參替換用實參的值，並返回計算結果。所以，咱們說在表達式 λx.M N 中，函數體 M 裏的 x 與表達式 N 綁定，M 中剩下未綁定的變量則是自由變量。

 

對 λx.M N 進行求值時，M 中全部的 x 都將被替換爲 N。這一過程稱爲歸約，歸約後獲得簡化的λ表達式，能夠進一步歸約直至沒法再歸約，此時的表達式就是對原表達式進行求值的結果。

 

考慮一個函數 f(x)=x+3，寫做λ表達式就是 (λx.(+x 3))。

如前所述，當咱們想計算 f(4) 時，將函數應用於 4，表達式爲 λx.(+ x 3) 4。

按照歸約的法則，函數體 (+ x 3) 中的 x 被 4 替換，函數表達式變爲 (+ 4 3)，結果爲 7。

 

考慮另外一個函數 g(y)=y*2，λ表達式 λy.(* y 2)。

若是咱們想將函數 g 應用於 f(4) 的計算結果，即 g(f(4))，咱們能夠將 g 的λ表達式應用於上述表達式，即 λy.(* y 2)  (λx.(+ x 3) 4)

 

而後咱們進行歸約，這裏有兩種歸約順序。

 

一種是同以前同樣，先計算右邊表達式的值，即歸約爲 λy.(* y 2) 7。

而後將函數體 (* y 2) 中的 y 替換爲 7，獲得 (* 7 2)。

最終結果是 14。

 

另外一種歸約順序是先計算最外層的應用，即將y替換爲右邊的表達式(λx.(+ x 3) 4)，獲得歸約後的表達式(* (λx.(+ x 3) 4) 2)。

再歸約內層的應用，替換 x 獲得 (* (+ 4 3) 2)。

最終結果爲(* 7 2)=14。

 

在這個例子中，不一樣的歸約順序得出了相同的結果，然而，這並非廣泛現象。這裏面暗藏了一個計算機程序中常見的概念：做用域。