最近在看虎书的时候见到了函数式语言，随即想到了Lisp，和它的语言写法——即(write (+ 1 2))这类东西。Lisp语言受到过λ演算的启发，为了更好的理解下函数式，便去查找了下λ演算的资料——但是网上资料比较少，折腾了几日，把它们总结如下。
λ演算是阿隆佐邱奇（Alonzo Church）所发明的，那个时代还活跃着另一位科学家——阿兰图灵，就是发明图灵机的那位。λ演算和图灵机都做着相同的任务——计算，它是一个非常简单而且小巧的形式系统，简单理解，就像几何原本里面的几条公理，通过那几条公理，就像符号游戏一般，推导出整本书的所有定理、假设等等。这种有公理和能够进行推导的就是形式系统，自然地，描述它的就是形式语言。
在λ演算看来，一切都是表达式，包括函数——函数是抽象的表达式。它有三种合法的表达式，或者叫做项：
λ-term: 变量 Variable
首先是变量，是一个标识符，比如x、xy、var这些。注意，不要把变量理解为一个值，它可以代表任何东西，比如你认为平行线段永不相交，那么它就可以当作一个变量，并通过一系列操作推导出其它定理，当然，我们也可以用它表示一个值。
变量有着和一般程序语言类似的规则。当一个变量是在当前作用域下定义的，那么称它是绑定的（类比于局部变量），当一个变量是外层作用域定义的，但是本层作用域访问了，那么该变量是自由变量（类比逃逸变量）。注意，自由变量还是绑定变量是相对于作用域而言的——对于内层作用域，一个外层作用域的变量是自由的，而外层作用域则认为它是绑定的。
一个不含自由变量的项被称作封闭的，或者称为组合子。
λ-term: 抽象体 Abstraction
抽象体类似于函数一样，表达着拥有一个参数（只能是一个参数）的函数，以及它的返回值。例如λx.M，就表示参数为x，返回值为M。再来几个例子：λx.x 表示输入x就返回x，也就是输入什么就返回什么。λx.y，表示输入什么都返回y。可以对比一下这个图来理解，第二行是一些函数式语言的写法，第三行是JavaScript的样貌。
类似于高阶函数的概念，一个抽象体的输入x当然也可以是一个抽象体，自然的，表达式M的结果也可以是抽象体。
抽象体其实就是函数的一种抽象。下面我更多的使用我们熟悉的"函数"一词来替代它。
λ-term: 应用 Application
其实想像成调用会更加的形象。M N表示传入参数N，调用M。例如(λx.x) p，应该得到的结果是p——函数的输入参数是x，表达式的结果也是x，也就是一个输入什么就返回什么的函数，现在我们送入变量p，自然得到的也是p。同样的，我们可以类比下图，第二段是很多程序语言的函数调用写法：
我们再来一个例子：(λx.y)((λx.y) p)得到的结果是y，第一个应用是内层的，它得到y，第二个应用返回自身，得到的还是y。
消除歧义
为了避免歧义，有两条约定规则：
1. 函数会尽可能的往右拓展，例如λx.y z表达的是(λx.(yz))，而不是(λx.y) z
2. 从左往右查看它们
其余情况我们就使用小括号阐明优先级了，就像平时那样。
多参数函数: 柯里化 Currying
一个函数需要好几个参数非常正常的。但是我们之前约束了只能有一个参数——怎么办？
为了方便起见，我使用类似JavaScript的语法解释。例如这个函数：
function F(x, y)
{
return Express;
}这里有个多参数函数，它有两个参数。那么我们要把它变成一个参数的怎么处理呢，可以想到的方案之一就是：
function F(x)
{
return function(y)
{
return Express;
}
}套层娃。翻译成λ演算的表达：λx.(λy.xy)，xy是我们的表达式，而y是我们的内层函数的变量，x是自由的，即外层函数作用域下的变量。如此一来，我们第一步返回的是一个函数，它只有一个参数y，内层是我们的表达式，接着，我们再调用一次这个返回的函数，得到最终结果：
Result = F(x) (y);能够返回函数的函数也是函数式语言的关键点：高阶函数。
函数内联: α转换
为了方便理解，这里我选用C/C++语言作为例子。考虑下面的一个片段，我们手工完成一次函数内联。
inline int f(int x)
{
int y = x;
return y + 1;
}
int y;
void Apply()
{
x = f(5);
y = 8;
}
如果我们傻傻的直接拷贝过来，名字也不改，程序就变成了这样子：
int y;
void Apply()
{
int y;
y = 5;
x = y + 1;
y = 8;
}
很显然这是不可以的（该情况被称作变量捕获，即外层变量名被内层变量名覆盖，y=8不再是全局的y）。注意到，一个程序的运行情况并不会和变量名、函数名有什么关系，x = y * 2和x_pos = y_pos * 2在做的都是同样的任务——取得一个变量值，乘以2，储存到另一个变量中。当然，有例外情况，当一个变量a是自由的，那么它的名字不能随意更改，不然就无法对应到正确的位置了。因此，总结一下——一个被绑定的变量名字，并不会影响函数本身，更换另一个名字之后是等价的。
上面这条就是所谓的α转换。如果我们用λ演算式写一下，可以这样表达：
λx.x = λy.y
函数调用: β归约
计算λ式子就是归约（reduce，刻意强调下这个词）过程。例如(λx.E) p，我们将p代入，得到E。将它表述出来就是：
(λx.E) p = E [p / x] = E [x := p]
上面就是β归约——将E自由变量x（相对于E，x是自由变量）替换为p。一些地方会使用中间的表达，一些地方使用后面的表达。个人觉得后面的比较清晰，所以用后面的来表达。
我们来理解一下它，用一个类似JavaScript的例子：
function funA(a)
{
return (a + 2);
}用并不严格的λ式写法，它相当于λa.(a + 2)。现在我们调用funA(5)，即：
(λa.(a + 2)) 5
很显然，相对于a + 2，变量a是自由变量，因此将a替换为5：
5 + 2
可以看出，我们得到了想要的结果：7。接下来我们看一个特殊的例子：
(λx.(λy.xy)) y
我们进行代换，针对于(λy.xy)，x是自由变量：
(λy.xy) [ x:= y]
针对于xy，x依然是自由变量，我们简单的把它放进去，得到：λy.yy。完蛋。变量名错了。这就是之前提到的内联问题，外层变量被内层的覆盖掉了。所以我们要适当的时候α转换变换一下。我们可以把它换成y'，得到：λy.y'y，这样就是正确的了。
冗余消除: η归约
这个其实很简单，考虑下面这个JavaScript片段
function(x)
{
return y;
}我们无论送入任何样貌的参数x，都没法改变返回值。所以说，(λx.y) x是可以直接被替换为y的。概念化一些——对于λx.E，如果E不含绑定变量x，那么该式子恒等于E。这就是η归约。
参考资料
除了网络上各个大佬的专栏、博客外，还有：http://users.monash.edu/~lloyd/tildeFP/Lambda/Ch/01.Calc.html