λ演算中的η-等价 基础概念回顾 λ演算是一种形式系统，用于描述函数定义与应用。其核心语法包括： 变量 （如 \(x, y\)） 抽象 （如 \(\lambda x. M\)，表示函数） 应用 （如 \(M N\)，表示将函数 \(M\) 作用于参数 \(N\)）。 此前已介绍过 β-归约 （\((\lambda x. M) N \rightarrow M[ N/x]\)），它处理函数的应用。而 η-等价 是另一关键概念，关注函数的"外延行为"。 η-等价的形式定义 η-等价规则表示为： \[ \lambda x. M x \equiv M \quad \text{（若 \(x\) 不是 \(M\) 的自由变量）} \] 其含义是：若函数 \(\lambda x. M x\) 对任意输入 \(x\) 的行为与 \(M\) 完全相同（即应用结果一致），则两者等价。约束条件"\(x\) 不是 \(M\) 的自由变量"避免变量捕获（例如若 \(M = y\)，则 \(\lambda x. y x \equiv y\) 成立；但若 \(M = x\)，则 \(\lambda x. x x \not\equiv x\)）。 直观理解与示例 例1：设 \(M = \lambda y. y\)（恒等函数），则 \(\lambda x. M x = \lambda x. (\lambda y. y) x\)。通过 β-归约得 \(\lambda x. x\)，即 \(M\) 本身。 例2：若 \(M\) 本身不是抽象（如 \(M = f\)），则 \(\lambda x. f x\) 表示"将 \(f\) 作用于输入 \(x\)"，其行为与 \(f\) 一致。 η-等价体现了 函数外延性 ：两个函数若对所有输入结果相同，则视为同一函数。 η-等价与 β-归约的关系 在 λ演算中，η-等价常与 β-归约结合形成 βη-归约 。例如： β-归约规约函数内部（应用时替换参数），η-归约消除"冗余抽象"。 重要性：η-等价能简化项。如项 \(\lambda x. (\lambda y. y) x\) 先通过 β-归约得 \(\lambda x. x\)，再通过 η-等价（若需）可进一步简化，但此例中已是最简。 在编程语言中的体现 η-等价解释编程中的"函数柯里化"与"部分应用"。例如： 在 Haskell 中， f 与 \x -> f x 等价，编译器可能利用 η-等价优化代码。 它支持 函数外延性原理 的证明：若 ∀x, f x = g x ，则 f = g 。 理论意义与扩展 规范化定理 ：在简单类型 λ演算中，βη-归约满足强规范化性（任何归约序列终止）。 范畴论连接 ：η-等价对应范畴中 自然变换的单位律 （如幺半群单位元性质）。 类型系统 ：在依赖类型论中，η-规则用于定义类型的"唯一性"（如积类型的 η-扩张规则）。 通过以上步骤，η-等价从基本定义逐步关联到计算行为、类型理论及范畴结构，成为 λ演算中深化函数概念的核心工具。