Lambda演算(二)歸約!歸約!歸約!
阿新 • • 發佈:2018-04-28
求值 返回 替換 span 什麽 不同 運算 表示 三種 (一)
這裏先不列出λ項的正式定義,只記住λ表達式語義上的構造方式為:
第二種表達式的值表示這個函數本身;
因此,在討論求值時,我們只關心第三種,即將一個函數應用於另一個λ表達式時,如何計算它的值。
如上所述,λ表達式的應用等效於一次函數調用。我們知道,調用函數的時候,會將所有的形參替換用實參的值,並返回計算結果。因此,我們說在表達式 λ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。
在這個例子中,不同的歸約順序得出了相同的結果,然而,這並不是普遍現象。這裏面暗藏了一個計算機程序中常見的概念:作用域。
- x
- (λx.M)
- (M N)
Lambda演算(二)歸約!歸約!歸約!