最近正好用到，就稍微做一下学习笔记。全部经过自己理解的归纳总结，坚持更新。
Lambda表达式强大到和图灵机等价，而且极其简洁、优美，太好玩了！
====
Formal Defination
Lambda表达式的语法非常简单。Lambda表达式包含3类字符，标示符i，抽象记号λ，以及左右括号()，其中i∈I，I为标示符集合：I={a,b,c,...,x,y,z,...,etc}。Lambda表达式集合L定义如下：
1. i∈L。
2. 若e∈L，则(λi.e)∈L。
3. 若x, y∈L，则(x y)∈L。
BNF下表示为：
1. <expr> ::= <identifier>
2. <expr> ::= (λ<identifier> .<expr>)
3. <expr> ::= (<expr> <expr>)
规则2被称为lambda抽象，规则3被称为函数作用。（为什么这么叫请看下文）
当然，形式化定义很难看懂，那么看看非形式化的定义。
Informal Defination
我的理解是这样的。Lambda表达式是这样一种函数：
1. 它接受一个单独的参数（输入）。这个单独的参数（输入）是一个lambda表达式。
2. 它的表达式说明了它对这个唯一的输入进行了某种操作。
3. 它的值（输出）是一个lambda表达式。
请看以下例子。
Examples
比如自增函数 f(x) = x+1 用lambda表达式可以写成(λx.x + 1)（注意，+号和加法在lambda演算中也是被事先定义的，具体可以参见wikipedia，若未被事先定义则该表达式不合法，这里为了方便就略去+号定义）。当然也可以写成(λy.y + 1)（虽然在这里变量名无关紧要，但是lambda演算的变量代换规则是很严格的，具体可以参见wikipedia）。这就相当于用lambda表达式定义了一个匿名函数（当然也可以显式写作INC = (λx.x + 1)），这就是规则2 lambda抽象。
f(2)的值可以写作((λx.x + 1) 2)，读作“将 +1操作 作用于 2 上”。这就是规则3 lambda函数作用。注意lambda函数作用是左结合的，即f x y = （f x) y。
这就是lambda表达式最基本的形式。下面来看一些复杂的例子。
1. (λf.f 2)是这样一个函数，它接受一个lambda表达式作为参数，并将该表达式作用于2上。那么以下几个表达式等价：
(λf.f 2)(λx.x + 1) 等价于 ((λx.x + 1) 2) 等价于 1 + 2
2. 有两个或更多参数的函数可以通过lambda表达式可以通过Currying（也称partial evaluation）这么表达，比如f(x, y) = x + y，写作(λx.λy.x + y)（byvoid的讲稿中写作(λx y.x + y)，我不知道这种表达方式是否正规，还是在不引起歧义的情况下可以这么写）。那么以下几个表达式等价：
(λx.λy.x + y) 1 2 等价于 (λy.1 + y) 2 等价于 1 + 2
有意思的是，Alonzo Church（lambda表达式发明者之一）证明了不存在一个通用算法来判定任意两个lambda表达式是否等价（lambda表达式这种语言是不可判定的）。这是第一个不可判定性问题，甚至还在图灵机和那个著名的停机问题之前。当然，后来lambda表达式被证明和图灵机等价。