λ演算中的α-等价 基本概念 α-等价是λ演算中描述“变量重命名不影响表达式含义”的规则。例如，表达式 λx.x 和 λy.y 在行为上完全一致，仅形式参数名不同。这种等价关系避免了变量名冲突对语义的干扰，是λ演算严谨性的基础。 自由变量与绑定变量 绑定变量 ：形如 λx.M 中， x 是被λ绑定的变量，其作用域为子项 M 。 自由变量 ：在 M 中未被绑定的变量称为自由变量。例如， λx.x y 中 y 是自由的。 α-等价要求重命名时需保持自由变量与绑定变量的关系不变。 形式化定义 两个λ项 M 和 N 是α-等价的，当且仅当可通过一系列绑定变量的一致重命名相互转换。例如： λx.x →α λy.y （合法，因变量名变更不影响结构） λx.λy.x y →α λa.λb.a b （合法） 但 λx.x y 与 λy.y y 不是α-等价（后者将自由变量 y 错误绑定）。 避免变量捕获 重命名需遵循“避免捕获”原则：新名称不能与当前作用域内的自由变量冲突。例如，将 λx.y x 重命名为 λy.y y 非法（原自由变量 y 被意外绑定），但 λz.y z 是合法的α-转换。 在归约中的应用 β-归约（如 (λx.M) N → M[N/x] ）依赖α-等价提前重命名变量，避免替换时发生冲突。例如： (λx.λy.x y) y 需先通过α-等价转换为 (λx.λz.x z) y ，再归约为 λz.y z ，否则直接替换会混淆自由变量 y 与绑定变量 y 。 与等价关系的关联 α-等价是λ演算中“同义反复”的基石，它与β-等价（计算规则）、η-等价（函数外延性）共同构成λ理论的核心等价关系，确保推理的严谨性。