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)
λx是一个x的抽象
y是自由变量因为它不在任何的λy的绑定范围内，也就是它的外面没有λy
x是绑定变量，因为它在λx的绑定范围内
(λx.(x · (λx.(x · x )))
第一个x是绑定在第一个λx上的
第二个x是绑定在第二个λx上的
第三个x也是绑定在第二个λx上的
((λx.(y · x )) · x )
第一个x是绑定在第一个λx上的
第二个x是自由变量
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的变量名。这就是α归约的原理。
可以将自由变量修改成不与其他变量冲突的变量名。
例子：
((λx.(y · x )) · x ) = ((λz.(y · z )) · x )
((λx.(x · (λx.x )) · x ) · x ) = ((λy.(y · (λz.z )) · y) · x )
β归约
β归约的表达形式： (λx.M ) · N = M [x := N ]
意思是将M中所有的自由变量x换成N，举几个例子：
((λx.(x · y)) · z ) = ((λx.(x · y)) · z ) = (z · y)
((λx.((λx.x ) · x ) · z ) = ((λx.x ) · z ) 【注意最里面的x是绑定变量】
η 归约
η归约的表达形式：如果M中没有x的自由变量，那么 λx.Mx = M
同时还有一个变形：如果M中没有x的自由变量，那么 (λx.Mx )N = Mx [x := N ] = MN
举个例子：
λf.(λx.(λy.f · x · y)) = λf.(λx.f · x) = λf.f