最近在学习计算理论方面的内容，这一系列文章主要介绍λ演算，这需要一些基本的离散数学如集合的知识，写的过程难免有错误欢迎大家指出。

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;}

3. λ演算法则

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

  · 变量（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. α 、β、η 归约（）

• α归约

           α归约也叫重命名化简，一种转换变量名的方法。我们先看一个例子

//第一种
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

Lambda Calculus的基本计算方式就是这些，下面一章会写编码方式和计算也就是如何用我们刚刚讲的这些来实现编程