求值 返回 替換 span 什麽 不同 運算 表示 三種

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

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。 在這個例子中，不同的歸約順序得出了相同的結果，然而，這並不是普遍現象。這裏面暗藏了一個計算機程序中常見的概念：作用域。

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