λ 演算學習

最近爲了學習Lambda表達式，特意學習了λ演算，函數式編程教程等許多文章，網絡上的資料仍是蠻多的，收穫頗深，特此作了一個小總結

---

λ 演算（英語：lambda calculus，λ-calculus）

lambda演算是由Alonzo Church設計的一個正式的數學系統，用於探討函數，函數應用和遞歸(recursion)

1.定義

形式化地，咱們從一個標識符（identifier）的可數無窮集合開始，好比{a, b, c, ..., x, y, z, x₁, x₂, ...}，則全部的lambda表達式能夠經過下述以BNF範式表達的上下文無關文法描述：

1. <表達式> ::= <標識符>       
2. <表達式> ::= (λ<標識符>.<表達式>)
3. <表達式> ::= (<表達式> <表達式>) 

前兩條規則用來生成函數，而第三條描述了函數是如何做用在參數上的在λ演算中，函數是經過λ表達式匿名定義的。例如：

f (x) = x + 2 在λ演算中表示爲λ x. x + 2

注意，若是一個λ表達式定義了一個函數，儘管這個函數的參數沒有被賦值，這個表達式也是有值的，這個值就是這個表達式自己,在λ演算中,值的概念並不只僅說一個數字是一個值，一個表達式也能夠是一個值.

λ演算只有三類表達式,而每條表達式就表明一個函數,而函數只有一個參數,也就是單參,而且返回一個值,函數是經過λ表達式匿名地定義的,好比函數f(x)=x+1,對應的λ表達式爲λx.(x + 1)

一般對於括號,若是不產生歧義的時候是能夠被省略的,由於函數的"做用"是左結合的

       好比 (λx.x)(λx.1-x),依次代 (λx.1-x)進函數(λx.x),就是λx.1-x

而且只要λ表達式操做符操做符被綁定到它後面的整個表達式

       例如:

1. 表達式λx.(x+1),能夠簡寫爲λx.x+1
2. 表達式 (λx.x x)(λy.y),能夠簡寫成λ(x.x x) λy.y 
3. 表達式 λx. (λy. ( x+y)),能夠簡寫爲λx. λy. ( x+y)

相似λx.(x y)這樣的lambda表達式,是未定義一個函數的,由於變量y的出現是自由的,即它並無被綁定到表達式中的任何一個λ上,因此一個lambda表達式的自由變量的集合是經過下述規則定義的：

1. 在表達式V中，V是變量，則這個表達式裏自由變量的集合只有V,好比表達式x,則自由變量的集合就是x
2. 在表達式λV.E中（V是變量，E是另外一個表達式），自由變量的集合是E中自由變量的集合減去變量V。於是，E中那些V被稱爲綁定在λ上。
3. 在表達式 (E E')中，自由變量的集合是E和E'中自由變量集合的並集。

例，對於表達式λx.x（咱們將第一個x視做變量，第二個x視做表達式），其中表達式x中，由1，它的自由變量集合是x，又由2，表達式λx.x的自由變量的集合是表達式x的自由變量集合減去變量x。因此對於表達式λx.x，它的自由變量集合是空。
例，對於表達式λx.x x由形式化描述的第3點，咱們把它看做((λx.x)(x))，(λx.x)和(x)分別爲表達式，由上一例知道(λx.x)的自由變量集合爲空，表達式(x)的變量集合爲變量x，因此對於λx.x x，它的自由變量集合爲x與空的並，即x,

自由變量的集合,以後會進行討論

λ演算有兩個最基本的概念"代入"和"置換","代入"就是α-變換,""置換"就是"Beta規約"

2.α-變換

Alpha-變換規則被綁定的變量名稱是不重要的,好比說λx.x和λy.y是同一個函數,修改了變量,不會改變表達式的含義,儘管如此,這條規則並不是像它看起來這麼簡單,關於被綁定的變量可否由另外一個替換有一系列的限制。而形式化的描述就是:若V與W均爲變量,E是一個λ表達式,則E[V:=W]是指把表達式E中全部的V的自由出現都替換爲W,好比λx.(λx.x) x這樣的表達式和λy.(λx.x) y是同樣的,

3.β-歸約

 

Beta規約是很是有趣的,它表達的是函數做用的概念,好比λx.(x+1) 1,即這個λ表達式x+1做用與1上,結果爲λx.(x+1)=1+1=2,其中表達式爲x+1,而標識符就是x

形式化陳述了若全部的E'的自由出如今E [V:=E']中仍然是自由的狀況下，有

((λV.E) E') == E [V:=E']

成立,對上述等價關係的一個更具操做性的定義能夠這樣得到：不容許任何beta歸約的lambda表達式被稱爲Beta範式。由於並不是全部的lambda表達式都存在與之等價的範式，若存在，則對於相同的形式參數命名而言是惟一隻容許從左至右來應用規則

4.η-變換

eta-變換,第三條規則,來造成一個等價關係,η-變換表達了「外延性」（extensionality）的概念,兩個函數被認爲是相等的「當且僅當」對於全部的參數，它們都給出一樣的結果,

λx.fx  f，只要 x 不是 f 中的自由出現。

5.λ演算中的運算

    在λ演算中有許多的方式能夠定義天然數,可是最多見仍是Church整數,如下是它們的定義   

• 0 = λ f. λ x. x
• 1 = λ f. λ x. f x
• 2 = λ f. λ x. f (f x)
• 3 = λ f. λ x. f (f (f x))

    以此類推。直觀地說，lambda 演算中的數字 n 就是一個把函數 f 做爲參數並以 f 的 n 次冪爲返回值的函數。換句話說，Church 整數是一個高階函數 -- 以單一參數函數 f 爲參數，返回另外一個單一參數的函數。

(注意在 Church 原來的 lambda 演算中，lambda 表達式的形式參數在函數體中至少出現一次，這使得咱們沒法像上面那樣定義 0) 在 Church 整數定義的基礎上，咱們能夠定義一個後繼函數，它以 n 爲參數，返回 n + 1：