##### λ-演算 - λ-演算 - **λ-演算**是对[[映射|函数]]抽象的[[形式系统]], 也是一种可以用来模拟任何[[图灵机]]的[[计算模型]]. λ-演算只有三种基本构造和两个计算规则 - 变量, 如 $x, y, z$, 表示计算中的基本符号 - 函数抽象, 形如 $\lambda x.M$, 表示一个函数, 其中 $x$ 是参数, $M$ 是函数体, 例如 $\lambda x.x$ 表示恒等映射 - 函数应用, 形如 $(M N)$, 表示将函数 $M$ 应用于参数 $N$ - β-规约, 将函数应用于参数时, 将参数代入函数体, 例如 $(\lambda x.x) y \to y$, 即将恒等映射 $\lambda x.x$ 应用于 $y$，结果为 $y$ - α-转换, 重命名绑定变量以避免命名冲突, 例如 $\lambda x.x \equiv \lambda y.y$