λ演算 (Lambda Calculus) 一 ： 定義與函數式編程

 

 

1. 什么是λ演算 (Lambda Calculus)？

  λ演算是數學家邱奇（Alonzo Church）在20世紀30年代發表的一種計算模型，以變量綁定和替換的規則，每個輸入參數用一個字母 λ (lambda)來表示，研究函數如何抽象化定義，函數如何被應用以及遞歸，最終形成的一套函數化計算規則，被廣泛的運用於函數式編程的理論基礎。

2. 什么是函數式編程 （Functional Programming）?

  函數式編程是實現λ演算的一次實踐，比如： Lisp, Scheme, Haskell...

  其核心思想就是所有的計算都是基於函數

 

近些年來，許多過程式編程語言（非函數式編程語言Lisp等）都內置了λ演算或是函數式編程方法。Java 8 中就引入了λ演算

// 代表接受一個值，並返回其2倍的值 

//通常寫法
public int mult_Two(int x){
    return 2*x;
}

//Lambda Calculus寫法
(int x) -> { return 2 * x;}

 

Python也引入了λ演算並且寫法更加直接：

( lambda x : x + 1)(1)  #結果為2

( lambda x , y , z : ( y - x ) ∗ z ) ) ( 1 , 2 , 3)  #結果為3

 

3. λ演算表達式（Expression）

λ演算中只有以下三種合法的表示方式：

  · 變量（Variable）

  就是所熟知的變量，沒有類型限制，可以代表一個字符，可以是字符串，甚至是一個列表

  例如：x、y、a、b、c

  · 應用（Application）

  第一種演算方式

  例如：(F · A)

  代表將一個輸入A應用到一些算法F中。比如A是3，F是函數 x → x + 1，(F · A)的最簡式就是4。通常我們可以省略點和括號寫成FA。

  應用是從左到右的關聯方式例如：

  × (+ 1 2) 3 = × 3 3 = 9

  · 抽象（Abstraction）

  第二種演算方式

  例如：λx.M[x]

  代表函數 x → M[x]。 具體的來說M中所有的自由變量x將被替換成一個輸入值。比如 λx.x 代表 x → x。

  多個抽象可以合並只用一個λ，比如λx.λy(xy) = λxy.(xy)

  抽象是從右到左的關聯方式例如：

  (λxyz. + (+ x z ) y ) 1 2 3 = ((((λx.(λy.(λz.((+ · ((+ · x ) · z )) · y)))) · 1) · 2) · 3) = ((+ · ((+ · 1) · 3)) · 2) = 6

 

4. 自由變量（Free）和綁定變量（Binding）

自由變量就是不受輸入約束的變量，相反綁定變量就是由輸入的值決定的，下面舉幾個例子來看一下：

• λx.(y · x)

1. λx是一個x的抽象
2. y是自由變量因為它不在任何的λy的綁定范圍內，也就是它的外面沒有λy
3. x是綁定變量，因為它在λx的綁定范圍內

• (λx.(x · (λx.(x · x )))

1. 第一個x是綁定在第一個λx上的
2. 第二個x是綁定在第二個λx上的
3. 第三個x也是綁定在第二個λx上的

• ((λx.(y · x )) · x )

1. 第一個x是綁定在第一個λx上的
2. 第二個x是自由變量
3. y也是自由變量

 

5. α 、β、η 歸約（Reduction）

• α歸約

           α歸約也叫重命名化簡(Rename)，一種轉換變量名的方法。

例子：

//第一種
int x = 0;
{int x = 9; System.out.println(x);}
System.out.println(x);
//第二種
int x = 0;
{int y = 9; System.out.println(y);}
System.out.println(x);
//第三種
int x = 0;
{int z = 9; System.out.println(z);}
System.out.println(x);

 

第一種代碼肯定是會報錯的，因為我們發現x在程序一開始就被定義了。所以把大括號內的x改成y就行了。那么一定要修改成y嗎？不一定，還可以修改成其他任何不是x的變量名。這就是α歸約的原理。

 

可以將自由變量修改成不與其他變量沖突的變量名。

例子：

1.  ((λx.(y · x )) · x ) = ((λz.(y · z )) · x )
2.  ((λx.(x · (λx.x )) · x ) · x ) = ((λy.(y · (λz.z )) · y) · x )

 

• β歸約

          β歸約的表達形式： (λx.M ) · N = M [x := N ]

          意思是將M中所有的自由變量x換成N，舉幾個例子：

1. ((λx.(x · y)) · z ) = ((λx.(x · y)) · z ) = (z · y)
2. ((λx.((λx.x ) · x ) · z ) = ((λx.x ) · z )   【注意最里面的x是綁定變量】

 

• η 歸約

          η歸約的表達形式：如果M中沒有x的自由變量，那么 λx.Mx = M

          同時還有一個變形：如果M中沒有x的自由變量，那么 (λx.Mx )N = Mx [x := N ] = MN

          舉個例子：

1. λf.(λx.(λy.f · x · y)) = λf.(λx.f · x) = λf.f