λ 演算學習

最近為了學習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：