lambda演算
定义
lambda演算的对象是lambda表达式。一个lambda表达式由以下几个部分组成：
变量v1,v2....vn
抽象符号“λ”和点号"."。
括号"()"
lambda表达式的集合Λ，可以递归地定义：
如果x是一个变量，那么x属于集合Λ。
抽象：如果x是一个变量，并且M属于集合Λ，那么λx.M**属于集合Λ。
应用：如果M和N属于集合Λ，那么(MN)属于集合Λ。
解读:
- λx.M中的x叫做绑定的变量。
- λx.M的M中出现的变量叫做自由变量。
- 举例：(λy.(yx))中的y就是绑定变量，而x就是自由变量。这里的y存在于两个地方。
- 对应关系：抽象对应函数的定义，应用对应函数的调用，绑定变量对应函数的参数。
记法
在lambda表达式含义不变的前提下，可以变成简化形式：
- 最外层括号可以省略：(MN)可以写作MN。
- 表达式的应用运算时左关联的，所以MNP相当于是(MN)P。
- 应用比抽象的优先级要高，所以λx.MN的含义为λx.(MN)，而不是(λx.M)N，其中的括号也可省略。可以这么理解，确定抽象的范围时，边界尽可能向右延伸。
- 连续抽象可以缩写，例如：λx.λy.λz.N可以简写成λxyz.N。
化约
α化约：更改表达式中的绑定变量。
β化约：更改表达式主体中的绑定变量为某一个表达式。β化约所依赖的变量替换，用符号记作
E[V := R]，定义为把表达式E中所有自由变量V替换成表达式R。
β化约的具体替换过程(x,y：变量，M,N：lambda表达式)：
- x[x := N] ≡ N 将单个变量替换成表达式。
- y[x := N] ≡ y 如果x≠y,要替换的变量（这里是x）和当前变量（这里是y）不同，当前变（y）保持不变。
- (M1M2)[x := N] ≡ (M1[x := N]) (M2[x := N]) 对应用表达式进行替换，结果是对表达式的两个组成项分别进行替换。
- (λx.M)[x := N] ≡ λx.M 对抽象表达式进行替换，假如要替换的变量与绑定变量相同，表达式不变。
- (λy.M)[x := N] ≡ λy.(M[x := N]) 如果x≠y并且y在N中不是自由变量（对抽象表达式进行替换，假如要替换的变量与绑定的变量不同，并且绑定变量在要被替换的表达式中不是自由变量，对抽象表达式的主体进行变量替换。）
举例：
- （1）α化约：λx.x变换成λy.y。这就相当于说函数的参数更名。
- （2）β化约：λx.yx中的x替换成M,变换成了λx.yM。相当于函数的实参传入函数。