[来自 Lambda Calculus]

基本概念

λ 表达式 (λ-term) 的字母表中有: 符号 `λ`, 左右括号与无限个变量 (用小写字母 `x, y, z` 表示). 它的形式定义如下:
1. 每个字母都是一个 λ 表达式.
2. (application terms) 如果 `M` 和 `N` 是 λ 表达式, 则 `M N` 是 λ 表达式.

   `M N` 表示将函数 `M` 作用于参数 `N`. 多个 λ 表达式连写的时候, 按从左到右的次序进行运算: 如 `P Q R = (P Q) R`.

3. (abstraction terms) 如果 `M` 是 λ 表达式, 则 `lambda x.M` 是 λ 表达式.

   `lambda x.M` 表示一个函数 `f`, 且 `f x` 的结果是 `M`.

自由变量的代入 (substitution) 用记号 `M|_(x=N)` 表示将 `M` 中出现的所有自由变量 `x` 替换为 `N`. 形式定义如下 (`y` 是不同于 `x` 的变量):
1. `x|_(x=M) = M`;
2. `y|_(x=M) = y`;
3. `(AB)|_(x=M)` `= A|_(x=M)` `B|_(x=M)`;
4. `(lambda x.A)|_(x=M) = lambda x.A`;
5. `(lambda y.A)|_(x=M) = lambda y.(A|_(x=M))`.
注意 4. 中 `x` 不是自由变量, 所以代入 `x=M` 对它不会有任何影响.

α, β 和 η 代换

约束变量的替换, α 代换 (α-convertion) 是指将 `M` 中所有形如 `lambda x.A` 的子表达式替换为 `lambda y.(A|_(x=y))`. 可以类比微积分中的换元 `int f(x) dx = int f(y) dy`.

函数的应用, β 代换 (β-convertion) 是指在保持 `N` 中自由变量的前提下, 将表达式 `(lambda x.M)N` 变为 `M|_(x=N)`. 记作 `(lambda x.M)N |>_beta M|_(x=N)`. 记号 `|>_beta` 表示左边的表达式经过有限次 (含 0 次) β 代换可以得到右边的表达式. 在上下文明确时, 下标 `beta` 可以省略.

β 代换可以进行的前提是, `N` 中原有的自由变量在代换后仍保持自由. 如, 表达式 `lambda x.lambda y.(x y)` 不能直接作用于参数 `2y`, 因为将 `x` 替换为 `2y` 会使得 `y` 成为约束变量. 但是, 我们可以先进行 α 代换, 将 `y` 换为 `z`, 再进行 β 代换: `lambda x.lambda y.(x y)(2y)` `|>_alpha lambda x.lambda z.(x z)(2y)` `|>_beta lambda z.(2y z)`.

若一个表达式无法进行任何 β 代换, 则说它是一个 β 标准形. 事实上, 如果 `M, M'` 是同一个表达式的两个 β 标准形, 则 `M` 可以通过 α 代换变为 `M'`.

η 代换