把 (λx. λy. x) y 化成 λy. y，看起来只做了一次文本替换，却已经改变了程序含义。传入的 y 原本由外部环境提供，替换后却变成了函数自己的参数。规约器必须区分名字相同与绑定关系相同，否则后面的函数组合、求值顺序乃至编译优化都没有可靠基础。

本篇承接λ 演算入门与写一个 λ 规约器。实验复用旧规约器的三类 AST、自由变量计算、绑定变量改名和避免捕获替换，增加 α 等价判定、两种完整规约策略、燃料计数和效果下的 η 反例。旧文保留原位置，新实验不覆盖旧实现。系列入口是导读与能力自测。

替换操作处理的是绑定关系

无类型 λ 项只有变量、函数抽象与应用三种形状：x、λx.M、M N。应用向左结合，f a b 表示 (f a) b；抽象的函数体尽量向右延伸。括号影响语法树，名字是否自由则由到根节点路径上的绑定决定。

自由变量集合满足 FV(x)={x}、FV(M N)=FV(M)∪FV(N)、FV(λx.M)=FV(M)-{x}。在 λx. x y 中，只有 y 自由。嵌套成 λy. λx. x y 后，整个项闭合，但不能据此认为任意子项都没有自由变量：单独取出内层函数，y 仍相对于这个子项自由。

实验沿用不可变数据类，而不是在字符串上查找替换：

1
2
3
4
5
6
7
8
9
10
11
12
13
@dataclass(frozen=True)
class Variable:
    name: str

@dataclass(frozen=True)
class Function:
    parameter: str
    body: "Expression"

@dataclass(frozen=True)
class Call:
    function: "Expression"
    argument: "Expression"

这里的不可变性使一次规约返回新树；它本身不保证替换正确。正确性来自递归分支：遇到目标变量才替换；遇到应用分别处理两边；遇到同名绑定器就停止，因为绑定器遮蔽了外部目标；遇到可能捕获替换项自由变量的绑定器，先改名再递归。

对 M[x:=N]，若 M=λy.B 且 y≠x，也不能立即进入 B。当 y∈FV(N) 时，需要选择没有出现在相关语法树中的新名字 z，把当前绑定器及其支配的使用位置改成 z。改名函数遇到另一个同名绑定器时必须停下，那一层属于不同作用域。选择名字时检查全部名字而非只有自由名字，可以避免新名字碰上已有内层绑定器。

手算上述错误样例：(λx. λy. x) y 先把内层绑定器改成 y_1，得到 (λx. λy_1. x) y，再做 β 规约，结果是 λy_1. y。结果自由变量集合仍为 {y}。如果错误结果是 λy.y，集合变成空集，这就是可直接检查的反例。Cornell 的避免捕获替换说明给出了同类冲突及新鲜变量处理规则；实验的多层名字冲突另外由本地断言覆盖。

α、β、η 分别允许改变什么

α 转换只改变绑定名字。λx.x 与 λz.z 相等价，但 λx.y 与 λz.z 不等价。仅仅把所有变量名排序或统一成一个名字，会丢失绑定层次。本实验将绑定变量编码成它距离最近对应绑定器的索引，自由变量仍保留原名。对两个项分别计算这个键，即可判定实验语法中的 α 等价。

β 规约把函数应用变成避免捕获的替换：(λx.M) N → M[x:=N]。它不是“先算出 N”的同义词；何时选择这个 redex，即可规约子式，由策略决定。一个大项可以同时含多个 redex，单步函数需要明确报告实际选择了哪一个。

η 收缩的规则是 λx. f x → f，前提为 x∉FV(f)。若 f=x，左侧 λx.x x 是闭合项，右侧 x 却是自由变量，收缩显然不成立。实验的 eta 只在 AST 恰好匹配且满足侧条件时返回函数部分；否则保留原项。

这些规则讨论的是选定语言中的等价。引入异常、状态、对象身份或者求值次数之后，直接把工程语言表达式代入公式，需要重新核对可观察行为。实验的 JavaScript 文件让 make() 每次创建函数时增加计数：

1
2
const expanded = x => make()(x);
const contracted = make();

分别调用两次，扩展式创建两次，收缩式只在定义时创建一次；两边返回值都可以是 3,3。即便返回值相同，创建次数和创建时机也不同。如果创建过程抛异常，异常发生位置也会改变。这个反例针对含效果的 make()，不否认纯 λ 演算中带侧条件的 η 等价，也不声称普通变量 f 的所有 η 转换都不安全。

同一项为什么会有不同终止结果

定义 I=λz.z、D=λx.x x、Ω=D D。Ω 一步 β 规约后仍是 Ω，因为把 x 替成 D，就再次得到 D D。这是不断规约的循环，不是正规形。

实验中 normal 策略优先规约最左外层 redex，applicative 策略先递归处理函数和参数的内部再应用。两者都是进入 λ 函数体的完整规约策略，因此不能不加限定地称为 JavaScript 的 call-by-value 或 Haskell 的 call-by-need。常见语言求值通常只求到某种值或弱头正规形，并不递归规范化每个未调用函数的函数体。

对 (λx.I) Ω，normal 第一步直接替换。由于 x 不在 I 中，参数被丢弃，结果立即是 I。applicative 则先尝试把 Ω 规约完，永远无法到达外层调用。这说明参数在返回值中未被使用，不代表所有策略都能绕过它。不能根据某个顺序失败，就断言项不存在正规形。

反方向也不能推导成“normal 能让任何程序终止”。直接规约 Ω 时，normal 一样循环。实验在每次真实 β 步骤后扣减燃料，达到四十步返回 fuel，而非继续阻塞测试。燃料用尽只说明在给定预算和策略下没有结束；对任意输入，它不是一般的非终止证明。Ω 的非终止性另由每步回到自身这个结构论证给出。

旧规约器以“下一棵树是否等于当前树”决定是否结束。在 Ω 上，这个判断把发生过的自规约误认为没有可规约位置。本实验保留其替换算法，但将单步结果改为 (新项, 是否发生规约)。changed=True 即使新旧树相等也要扣除燃料；只有找不到 redex 才报告正常结束。终止条件与结果比较必须分离，这是解释器之外的状态机也会遇到的问题。

从数学规则到测试边界

输入覆盖不能只放闭合项。闭合项往往不会暴露自由变量捕获，因此实验特别构造开放参数 y，并用已有 y_1 的嵌套结构迫使 fresh-name 继续选择 y_2。另外检查内部同名绑定器遮蔽、α 等价以及 η 侧条件，避免一个简短正常例子掩盖作用域错误。

运行完整入口：

1
node examples/functional-programming/run.mjs E01

本次 Python 3.9.6 与 Node 22.22.2 的实际输出包含：

1
2
3
capture=y_1; nested=y_2; alpha=true; eta-side-condition=true
normal=identity/1; applicative=fuel/40; omega=self-step/fuel/40
eta-effects: expanded builds=2; contracted builds=1; values=3,3

全部输入是Main.py与eta.mjs，命令、源文件哈希与退出状态见result.json。断言通过证明这些具体例子和边界得到处理，不构成实现对所有项正确的机器证明。

这个规约器也没有解析器、闭包环境、共享图或垃圾回收模型。替换可能复制参数树，节点数量与运行步数都可能迅速增长；四十步预算不等于四十单位内存。需要解释真实语言时，环境与闭包往往比直接复制语法树合适。call-by-need 还要共享同一计算的结果，不能只把 applicative 的遍历顺序换成 normal 就宣布实现了惰性共享。

简单类型 λ 演算讨论的是另一层约束。没有通用递归扩展的简单类型 λ 演算排除了 Ω 这样的自应用，并具有强规范化性质；Scala 或 Haskell 即使静态类型检查通过，仍允许递归、异常或底值，不能沿用该结论作为工程程序的终止担保。

替换与规约的两个不变量

替换函数可以先用一个集合关系检查：替换后的自由变量只可能来自原项中除去目标变量后的自由变量，或者替换项的自由变量。它不会凭空引入一个原先不存在的自由名字。新鲜名字虽然被创造出来，却应作为绑定变量出现；如果它落进结果的自由变量集合，通常说明绑定器和使用位置没有同步改名。

还可以检查目标变量不自由时的行为。对 M[x:=N]，如果 x 不在 M 的自由变量集合里，替换不应改变 M 的意义。实现可以提前返回 M，也可以做额外但正确的 α 改名；后者会使结构相等测试失败，却仍可能 α 等价。因此测试要区分“保留原对象的优化契约”和“保持绑定含义的语义契约”，不能把两者混为一条规则。

规约层则依赖单步报告：如果报告没有发生规约，遍历范围中就不应残留符合当前策略的 redex。完整 normal 会检查函数体内部，弱求值器却可以把函数体里的 redex 留着。新加的 λz.Ω 断言让两种强规约策略都耗尽四十步预算，明确证明本实现不是遇到函数就停止的弱 CBV 求值器。测试结果额外输出 under-lambda=both-fuel/40; strategies=strong-not-weak-CBV。

对开放项的应用也要谨慎。例如 f ((λx.x) y) 的最外层函数是自由变量 f，不能直接 β 规约，但完整策略仍会进入参数，得到 f y。这不等于真实语言已经找到 f 的值；无类型语法规约与带环境的程序执行在这里分道而行。把自由变量当作未定义异常，是增加了环境语义，不是替换算法的必然要求。

燃料计数的单位同样需要记录。本实验每个单步只完成一个 β 规约，但寻找这一步可能遍历很多节点，替换也可能复制大量子树。对巨大而接近正规形的输入，燃料很少并不保证运行很快。若将它作为公开服务，还要额外限制输入大小、遍历深度和整体时间；当前局部教学实验只使用手工构造的小树。

最后，α 等价键为绑定变量选择相对位置，对自由变量保留名字。这种设计也解释了为什么序列化时不能仅删除名字：闭合项可以只依赖绑定索引，开放项仍需要一种外部变量身份。如果不同模块都把自由变量叫 x，却代表不同来源，组合模块前还需要命名空间策略，而不是继续扩大 fresh-name 的数字后缀范围。

编译器优化还应声明使用哪种等价：只改绑定名字时可用 α 等价，执行替换时涉及 β 关系，消除一层调用则可能涉及 η。把所有变化都归为“结果一样”，会掩盖各自不同的侧条件。实验将三类断言分开，便于定位究竟是名字管理、求值策略还是效果观察出了问题。

自测与修改

先手算 ((λx.λy.x y) y) z。必须先避免捕获，第一步是 λy_1.y y_1，第二次应用后得到 y z；若算成 z z，说明第一次替换已经错了。再解释为什么 λx.x 与 λy.y 的自由变量集合相同仍不足以单独证明 α 等价：例如 λx.λy.x 与 λx.λy.y 都闭合，却选择不同的绑定位置。

修改题是在现有 step 之外增加弱头规约：遇到最外层函数就停止，不进入其函数体。使用 λz.Ω 比较弱头结束与完整 normal 燃料耗尽，并断言两种状态不能混用。再把燃料设为零，约定零预算下是允许检查正规形，还是立即拒绝执行，写出边界测试。这个选择属于接口契约，不能依靠循环中偶然的判断顺序决定。