語言特徵與模式- λ演算

時間 2019-12-05

標籤語言特徵模式演算简体版

原文原文鏈接

語言特徵與模式- λ演算

λ演算

wiki定義javascript

Lambda演算能夠被稱爲最小的通用程序設計語言。它包括一條變換規則（變量替換）和一條函數定義方式，Lambda演算之通用在於，任何一個可計算函數都能用這種形式來表達和求值。於是，它是等價於圖靈機的。儘管如此，Lambda演算強調的是變換規則的運用，而非實現它們的具體機器。能夠認爲這是一種更接近軟件而非硬件的方式。java

λ 表達式通俗定義

$λ$表達式所屬空間$Λ$描述爲：算法

$變量 a ∈ Λ$編程
$對於任何 M ∈ Λ，若變量a ∈ Λ，則λa . M ∈ Λ$函數式編程
$對於 F，M ∈ Λ，有 (FM) ∈ Λ$函數

規則一中說明了$a$是一個標識符，表明了一個元素。工具

規則二中說明了能夠從$ λ$ 表達式中構造出一個函數$f(a)$，這個函數以參數$a$爲自變量，以$λ$表達式描述映射關係，構造出的函數$f$也同屬於$λ $表達式.net

規則三中說明了$M$能夠做用在$F$上，也即以$M$做爲函數$F$的實參數進行計算，返回的值也屬於$λ$表達式翻譯

三條規則說明了定義了從$Λ$空間到$Λ$空間的映射關係的函數做爲$λ $表達式，其全部表達式的集合構成了$Λ$空間。設計

λ 表達式描述了這樣的集合$E$，對於函數$y = f(x)$, 其輸入$x$，映射關係$f$，輸出$y$均屬於集合$E$

在函數式編程思想中，說明了這麼一個理念，變量和函數等同，能夠做爲變量參與運算，運算結果也但是函數。這就是高階函數的定義。

咱們須要以lambda演算爲基礎構建出可用的基本編程語句模式：包括簡單的天然數及其運算、布爾運算、條件語句和循環（遞歸）語句，由此體現出lambda演算的圖靈完備性。lambda演算的圖靈完備性須要更爲嚴謹的證實，故此做「體現」兩字。

α-變換和 β-規約

對應於程序函數中的入參聲明和實參替入概念，不衝突的狀況下，入參名稱的改變不影響函數的描述，而應用函數時將實參代入形參進行計算。

單位元

類比實數集合中的$1$，對任意$a∈R$，均有 $ 1 * a= a$
λ 表達式的單位元爲
$$
e = λx.x
$$
有 $e a = ( λx.x) a = a$,特別的，有$ e e = ( λx.x)( λx.x) = ( λx.x) = e$

η-變換

$$
f = λx.(f x)
$$
這個等價變換有個好處，若$f = g y$，則能夠延遲到須要調用函數$f$的時候再計算$g(y)$

柯里化

純粹的λ 表達式不支持多個參數的函數表達式，能夠經過逐步經過返回接受一個參數的函數間接表達多參數函數。如：

function add(a, b) { return a + b; };
var $add = function (a) { return function (b) {return a + b;};};

這樣，經過這種轉換（翻譯），從原理上λ 表達式能夠支持多參數函數表達式，咱們可使用多參數函數表達式簡化表達。

做用：

描述λ 表達式支持多參數函數表達式的機制。
能夠解耦函數中的各個參數，在調用時沒必要一次性所有將各個參數值給出，能夠將未給出所有實參的「不徹底」表達式看成變量使用。
封裝和信息隱藏，將一些參數進行隱藏，僅給出須要傳參的參數，而內部已經綁定的實參對於調用者說不可見。
組裝，經過各個算子的組合構建出更高層次的函數，提升函數的複用性。

布爾類型構建

布爾變量

布爾全集僅有 true 和 false 兩個，考慮設計一個二元組描述整個全集，並將第一個設爲false，第二個設爲true

(define true  (lambda (x y) x))
(define false (lambda (x y) y))

布爾運算-或

注意到true和false有選擇功能，對於OR(x, y), 當x爲真時選擇x，不然選擇y，故能夠這樣定義OR

(define OR (lambda (x y) (x true y)))

布爾運算-與

對於AND(x, y), 當x爲真時選擇y，不然選擇false

(define AND (lambda (x y) (x y false)))

布爾運算-非

當x爲真時選擇false，不然選擇true

(define NOT (lambda (x) (x false true)))

天然數類型構建

零

考慮這一函數，其表明的數字和參數f被應用的次數相同

(define ZERO  (lambda (f x) x))

則有

(define ONE  (lambda (f x) (f x)))
(define TWO  (lambda (f x) (f (f x))))
(define N    (lambda (f x) (f (f (....  (f x))))))

遞增算子

咱們須要一個從$N$遞推到$N+1$的函數$ INC$，有

INC N = N + 1

咱們須要解出INC算子，嘗試經過遞推解決

每次都是經過一個lambda表達式來表達一種類型，由於lambda表達式是函數，故一個類型的特徵一般表如今調用該lambda表達式描述的函數後所體現的行爲，那麼要了解天然數$N$的特徵，則看看調用N的函數所表現出的行爲：

(TWO f x) = (f (f x))
(N   f x) = (f (f (....  (f x))))

注意到$N$應用到$ (f x)$後是將參數$x$應用到函數$f N$次, 故$N+ 1 $應該是在$N$的基礎上多調用$f$一次，固有

((INC N) f x) =  (f (N f x))

利用η-變換解出INC算子，須要將參數$f$、$x$ 柯里化，隱藏到內部lambda的參數列表中，由於$f$、$x$ 是N的參數，不該是INC的參數

((INC N) f x) = (f (N f x))
(lambda (N f x) ((INC N) f x)) = (lambda (N f x)(f (N f x)))
INC = (lambda (N f x)(f (N f x)))
INC = (lambda N (lambda (f x)(f (N f x))))
INC = (lambda N (lambda f (lambda x (f ((N f) x)))))

加法算子

如今定義兩個整數的加法ADD，明顯有

(define ADD (lambda (N M) (lambda (f x) (N f (M f x)))))

乘法算子

顯然，有

(define MUL (lambda (N M) (lambda (f x) (N (M f) x))))

遞減算子

相似於求鏈表中一個節點的前置節點，在單鏈表的狀況下，能夠經過設置兩個指針p，q，每次走時p緊跟q後面，當q到達某節點時，p即指向該節點的前置節點。故咱們須要定義二元組存放這樣的兩個指針，同時預留一個參數f以即可以編寫關於PAIR實例操做的方法。

(define (PAIR a b)(lambda f (f a b)))

以及訪問第一個元素和第二個元素的方法

(define L (lambda (a b) (a)))
(define R (lambda (a b) (b)))

還有一個後驅算法Trans使得
$$(lastNumber,currentNumber)⇒(currentNumber,SuccNumber)$$
有

(define TRANS (lambda (p) (PAIR (p R) (INC (p R)))))

故遞減算子PRED爲

(define PRED (lambda (N) ((N TRANS (PAIR 0 0)) L)))

減法算子

因而減法就很簡單了，將PRED調用M次應用在N上獲得N - M
$$Subt:=λnm.m Pred n$$

謂語和條件語句

在條件語句中，if (condition) then {...} else {...},condition稱爲謂語，謂語是一個依據其變量的值來斷定真或假的方法。

從判斷一個數是不是零的謂語開始，利用天然數的性質，當函數f被應用時（即數大於等於1）當即返回false，x爲初始值true，有

(define (isZero N) (N (lambda (x) false) true))

等於、不等於、大於、小於也能從isZero 和以前的布爾運算構建出，再也不敘述。

而條件語句其實就是單位元e。

(define (IF condition then else) (condition then else))

遞歸（循環）語句和Y組合子

在數學上，若對於一個函數$f(x)$,存在一個$x = x0$,使得$f(x) = x$,則稱$x = x0$爲函數$f$的一個不動點。

而在lambda函數上，對於任意一個函數$f$，咱們均能找到一個由$f$推導出來的一個不動點$x =Y(f)$，使得$f(Y(f))=Y(f)$，這個$Y$被稱做$Y$組合子，咱們試求出這樣的函數$Y$，使得對於任意一個函數都能經過$Y$獲得$f$的不動點。

Y組合子用於實現函數的可遞歸特性。舉例，爲了完成以下的函數的定義：

(define (fac n) (if (= n 1)
                    1
                    (+ n (fac (- n 1)))))

按照lambda表達式的語法來講，函數體裏的fac是未定義的，沒有出如今參數列表中，也不支持對函數命名，咱們想借助一個以下的環境爲函數提供可遞歸的定義：

$$ g:=λf x.M(f, x)$$

$f$爲本身定義的可遞歸函數，在函數體$M$內對$f$的調用如同遞歸調用自身，而$x$則是本來定義遞歸函數$f$的參數，因爲$f$出如今參數列表中，故能夠在函數體內使用函數$f$。咱們根據這樣的規則定義了函數$g$用來實現遞歸語義，則還須要一個工具把具體的$f$算出來以便代入到$g$的參數中實現遞歸的功能，而這樣的一個工具即是組合子$Y$，它知足$Y g = f$。

關於Y的定義以下:
$$Y = λ f. (λ x. f (x x)) (λ x. f (x x))$$

* Y組合子的推導

以斐波那契數列項推導公式爲例，目標是消除名字fac

(define (fac n) (if (= n 1)
                1
                (+ n (fac (- n 1)))))

將函數fac放入參數以完成遞歸調用

(define (fac f n) (if (= n 1)
                  1
                  (+ n (f f (- n 1)))))

柯里化，解耦函數f和參數n

(define (fac f) (lambda (n) (if (= n 1)
                        1
                        (+ n ((f f) (- n 1))))))
;; 調用
((fac fac) 5) ;;15

將w = (f f)抽象出來有

(define (w x) (x x))
(define (fac f) (lambda (n) (if (= n 1)
                       1
                       (+ n ((w f) (- n 1))))))
;; 調用
((w fac) 5) ;;15

將g = (w f) 提取爲參數，並根據η-變換處理g延遲g的計算

(define (w x) (x x))
(define (fac f) ((lambda (g) (lambda (n) (if (= n 1)
                         1
                         (+ n (g (- n 1))))))
             (lambda (x) ((w f) x))))
;; 調用
((w fac) 5) ;;15

提取自定義的匿名遞歸函數表達式做爲參數，參數名爲h，重構後的函數名爲Y0，同時命名斐波那契的匿名遞歸函數表達式爲fac，fac實現了在函數體內不調用fac自身。
```
(define (w x) (x x))
(define fac (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1)))))))
(define Y0 (lambda (h) (lambda (f) (h (lambda (x) ((w f) x))))))
;; 調用
((w (Y0 fac)) 5) ;;15
```

對於調用表達式，將fac從函數w中提出做爲參數f

(define (w x) (x x))
(define fac (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1)))))))
(define Y0 (lambda (h) (lambda (f) (h (lambda (x) ((w f) x))))))
;; 調用
(((lambda (f) (w (Y0 f))) fac) 5) ;;15

記Y = (lambda (f) (w (Y0 f)))

(define (w x) (x x))
(define fac (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1)))))))
(define Y0 (lambda (h) (lambda (f) (h (lambda (x) ((w f) x))))))
(define Y  (lambda (f) (w (Y0 f))))
;; 調用
((Y fac) 5) ;;15

至此，只要將fac的定義代入調用式中便可消除名字fac，對於Y，將Y0 展開，把Y0 中的變量f替換爲g以避免與函數Y中的f產生歧義(α-變換)，有

(define (w x) (x x))
(define Y  (lambda (f) (w ((lambda (h) (lambda (g) (h (lambda (x) ((w g) x))))) f))))
;; 調用
((Y (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1))))))) 5) ;;15

對於Y，展開最裏面的w，並將實參f代入到參數h，有

(define (w x) (x x))
(define Y  (lambda (f) (w (lambda (g) (f (lambda (x) ((g g) x)))))))

展開餘下的w，即爲最後的結果

(define Y  (lambda (f) ((lambda (g) (f (lambda (x) ((g g) x))))
                    (lambda (g) (f (lambda (x) ((g g) x)))))))
;; 調用
((Y (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1))))))) 5) ;;15

另外，在第6步中，能夠將參數h放在f的後面（而不是前面）做爲參數，調用時優先與w結合，有

(define (w x) (x x))
(define (fac f) (lambda (h)
                        (h (lambda (x) (((w f) h) x)))))
(((w fac) (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1))))))) 5)

將fac直接代入到調用式中，得出

(define Θ (w (lambda (f) (lambda (h) (h (lambda (x) (((f f) h) x)))))))

這實際上 Θ與以前推導出的Y算子等價，說明不一樣的變換和規約順序能夠得出不一樣的結果。

拓展

更深刻的主題：

負數、有理數的構造。（思路：和前驅算子同樣，設計一個二元組，如 -5 == 0 - 5，0.5 = 1 / 2）
實數的構造，涉及到實數理論。

參考

λ演算，https://zh.wikipedia.org/wiki...
神奇的λ演算，http://www.jianshu.com/p/e7db...
A Tutorial Introduction to the Lambda Calculu，http://www.inf.fu-berlin.de/i...
Fixed-point combinators in JavaScript: Memoizing recursive functions，http://matt.might.net/article...
Lambda Calculus: Subtraction is hard, http://gettingsharper.de/2012...

相關標籤/搜索

每日一句

每一个你不满意的现在，都有一个你没有努力的曾经。

語言特徵與模式- λ演算

語言特徵與模式- λ演算

λ演算

λ 表達式通俗定義

α-變換 和 β-規約

單位元

η-變換

柯里化

布爾類型構建

布爾變量

布爾運算-或

布爾運算-與

布爾運算-非

天然數類型構建

零

遞增算子

加法算子

乘法算子

遞減算子

減法算子

謂語和條件語句

遞歸（循環）語句和Y組合子

* Y組合子的推導

拓展

參考

α-變換和 β-規約