Lambda 演算归约练习
Lambda 演算是函数式编程和形式语义学的基础。在进行归约时，理解自由变量捕获、$\alpha$-变换以及归约顺序至关重要。以下是 8 道典型的 Lambda 演算练习题及其详细推导过程。
1. 自由变量捕获与换名 (Alpha-conversion)
题目：计算 $(\lambda x. \lambda y. xy)(yz)$
推导：
由于输入项中含有自由变量 $y$，而函数抽象内部也使用了绑定变量 $y$，为了避免捕获，需要先进行 $\alpha$-变换。
- $(\lambda x. \lambda y. xy)(yz)$
- $\to_\alpha (\lambda x. \lambda w. xw)(yz)$ （将内部的 $y$ 换名为 $w$）
- $\to_\beta \lambda w. (yz)w$ （将 $x$ 替换为 $yz$）
- $\equiv \lambda w. yzw$
2. 多重嵌套应用
题目：计算 $((\lambda x. \lambda y. yx)(\lambda z. y))w$
推导：
注意此处的自由变量 $y$ 与 $\lambda y$ 的区别。
- $((\lambda x. \lambda y. yx)(\lambda z. y))w$
- $\to_\beta (\lambda y. y(\lambda z. y))w$ （将 $x$ 替换为 $\lambda z. y$）
- $\to_\beta w(\lambda z. y)$ （将 $y$ 替换为 $w$）
3. 组合子逻辑归约 (S K I)
题目：计算 $(\lambda f. \lambda g. \lambda x. fx(gx))(\lambda y. \lambda z. y)(\lambda w. w)$
推导：这实际上是组合子 $S K I$ 的过程。
- $(\lambda f. \lambda g. \lambda x. fx(gx))(\lambda y. \lambda z. y)(\lambda w. w)$
- $\to_\beta (\lambda g. \lambda x. (\lambda y. \lambda z. y)x(gx))(\lambda w. w)$
- $\to_\beta \lambda x. (\lambda y. \lambda z. y)x((\lambda w. w)x)$
- $\to_\beta \lambda x. (\lambda z. x)((\lambda w. w)x)$
- $\to_\beta \lambda x. x$ （即恒等函数 $I$）
4. 深度 $\alpha$-变换（双重冲突）
题目：计算 $(\lambda x. \lambda y. x(\lambda z. xz))(yz)$
推导：
- $(\lambda x. \lambda y. x(\lambda z. xz))(yz)$
- $\to_\alpha (\lambda x. \lambda w. x(\lambda u. xu))(yz)$ （对 $y$ 和 $z$ 进行换名以防冲突）
- $\to_\beta \lambda w. (yz)(\lambda u. (yz)u)$
- $\equiv \lambda w. yz(\lambda u. yzu)$
5. 高阶函数归约
题目：计算 $(\lambda f. (f \lambda x. x))(\lambda g. \lambda y. gy)$
推导：
- $(\lambda f. (f \lambda x. x))(\lambda g. \lambda y. gy)$
- $\to_\beta (\lambda g. \lambda y. gy)(\lambda x. x)$
- $\to_\beta \lambda y. (\lambda x. x)y$
- $\to_\beta \lambda y. y$
6. Church 数运算 (Succ 1)
题目：计算 $(\lambda n. \lambda f. \lambda x. f(nfx))(\lambda f. \lambda x. fx)$
(注：前者为后继函数 Succ，后者为 Church 数 1)
推导：
- $(\lambda n. \lambda f. \lambda x. f(nfx))(\lambda f. \lambda x. fx)$
- $\to_\beta \lambda f. \lambda x. f((\lambda f. \lambda x. fx)fx)$
- $\to_\beta \lambda f. \lambda x. f((\lambda x. fx)x)$
- $\to_\beta \lambda f. \lambda x. f(fx)$
(结果为 Church 数 2)
7. 复杂的 $\beta$-归约链
题目：计算 $(\lambda x. xx)(\lambda y. y)(\lambda z. z)w$
推导：
- $(\lambda x. xx)(\lambda y. y)(\lambda z. z)w$
- $\to_\beta ((\lambda y. y)(\lambda y. y))(\lambda z. z)w$
- $\to_\beta (\lambda y. y)(\lambda z. z)w$
- $\to_\beta (\lambda z. z)w$
- $\to_\beta w$
8. 涉及自由变量的布尔逻辑 (AND true x)
题目：计算 $(\lambda a. \lambda b. ab(\lambda x. \lambda y. y))(\lambda x. \lambda y. x)z$
(注：AND True z)
推导：
- $(\lambda a. \lambda b. ab(\lambda x. \lambda y. y))(\lambda x. \lambda y. x)z$
- $\to_\beta (\lambda b. (\lambda x. \lambda y. x)b(\lambda x. \lambda y. y))z$
- $\to_\beta (\lambda x. \lambda y. x)z(\lambda x. \lambda y. y)$
- $\to_\beta (\lambda y. z)(\lambda x. \lambda y. y)$
- $\to_\beta z$
总结：在做 Lambda 归约题时，建议遵循“先检查变量冲突、再由外向内归约”的原则。对于复杂的项，可以先标注出对应的函数和参数，避免混淆。
