utlc/lambda 设计

设计目标

utlc/lambda 是尽可能直接地写在共享层之上的无类型 λ 演算：具名项来自 syntax，避免捕获的代换来自 substitution，策略来自 eval。它追求显然正确而非速度，以便更快的范式化器（debruijn、utlc/nbe）以及有类型演算 stlc 可以以它为基准进行检验。

数学背景

λ 项为 $t ::= v \mid x \mid t\,u \mid \lambda x.\,t$ ，分别编码为 Value、Variable、Apply(t, [u]) 和 Bind(x, t)；n 元的 Apply(f, [a_1, …, a_n]) 表示柯里化的脊 $f\,a_1 \cdots a_n$ 。项在 $=_\alpha$ 意义下取模。

β 与 η

\begin{aligned} (\beta)\quad & (\lambda x.\,b)\,a \;\to\; b[x := a], \\ (\eta)\quad & \lambda x.\,f\,x \;\to\; f \qquad \text{if } x \notin \mathrm{FV}(f). \end{aligned}

两者在所有上下文下都封闭，包括在 $\lambda$ 之下（ $\xi$ 规则）。η 的附加条件是必不可少的：没有它， $\lambda x.\,x\,x \to x$ 会把闭项变成开项，并把行为不同的函数等同起来。η 表达的是外延性：在 $\beta$ 存在时，它等价于规则“若对新变量 $x$ 有 $f\,x = g\,x$ ，则 $f = g$ ”，因为

f \;\leftarrow_\eta\; \lambda x.\,f\,x \;=\; \lambda x.\,g\,x \;\to_\eta\; g \qquad (x \notin \mathrm{FV}(f) \cup \mathrm{FV}(g)).

经典性质

合流性。 $\to_\beta$ 与 $\to_{\beta\eta}$ 具有 Church–Rosser 性质，因此一个项在 $=_\alpha$ 意义下至多有一个范式。¹1 Barendregt，The Lambda Calculus，定理 3.2.8 与 3.3.9。
范式化。 若一个项有 β 范式，则最左最外策略能到达它（范式化定理，见 eval 设计）。
η 后置。 每个 $\beta\eta$ 归约都可以重排，使所有 $\beta$ 步位于所有 $\eta$ 步之前；因此一个项有 $\beta\eta$ 范式当且仅当它有 $\beta$ 范式。²2 Barendregt，The Lambda Calculus，§15.1。
不可判定性。 一个项是否有范式是不可判定的，这正是范式化器需要步数上限的原因。

设计决策

通过共享代换实现 β

beta_rule 调用 Substitution::singleton(x, a).apply(b)。因此所有避免捕获的处理都集中在一处，并在 substitution 设计中一次性证明。对于可约式 $(\lambda x.\,\lambda y.\,x\,y)\,y$ ：

\begin{aligned} (\lambda x.\,\lambda y.\,x\,y)\,y &\to_\beta (\lambda y.\,x\,y)[x := y] \\ &= \lambda y_1.\,(x\,y_1)[x := y] && y \in \mathrm{FV}(\text{replacement}),\ \text{rename } y \\ &= \lambda y_1.\,y\,y_1 \\ &\to_\eta y . \end{aligned}

代换引理（Barendregt 2.1.16，在 substitution 设计中推导）使 β 在 α 等价类上良定义，并与上下文相容。

脊每次收缩一个参数

可约式形如 Apply(Bind(x, b), [a, ..rest])。它只与第一个参数收缩并保留其余参数： $(\lambda x.\,b)\,a\,\bar r \to b[x := a]\,\bar r$ 。这是在脊的柯里化解读上的 β，因此每一步都是单个 β 步，步数等于对应柯里化归约的长度。De Bruijn 归约器做出相同的选择，从而使两者可以逐步比较。

η 仅作用于一元应用

eta_rule 匹配 Bind(x, Apply(f, [Variable(x)]))。在柯里化解读下， $\lambda x.\,f\,a\,x$ （写作 Apply(f, [a, x])）也是 η 可约式，但识别它需要拆分脊并重建 Apply(f, [a])。该规则保持为纯语法的；构建 n 元脊且需要 η 的调用者可以先把脊范式化为一元形式。

使用单一组合规则的正规序

normalize 以 NormalOrder 策略运行 beta_eta_rule，因此每一步收缩两种之一的最左最外可约式。组合规则只有一个名字 "beta_eta"；轨迹显示位置，但不显示两条规则中哪一条被触发。由于 β 与 η 可约式的根构造器不同，beta_eta_rule 内部的优先级永远不会改变一步的结果。

正确性 / 不变量

beta_rule(t) = Some(u) 蕴含在根处 $t \to_\beta u$ ；eta_rule 对 $\eta$ 同理，其附加条件由 @syntax.free_variables 检查。
normalize 仅对在任何位置都没有（一元） $\beta$ 或 $\eta$ 可约式的 $u$ 返回 NormalForm(u, n)（rewrite 范式引理）。
由合流性，本包、debruijn（仅 β）或 utlc/nbe（仅 β）在同一个项上的任意两次终止运行所给出的 β 范式，在转换和脊展平之后是 α-等价的。测试 “named and debruijn beta reduction agree modulo alpha” 检查了一个需要重命名的步骤。
β 与 η 组合时使用正规序作为策略；它能到达每个可范式化项的 $\beta\eta$ 范式，这一点依赖于 β 的范式化定理与 η 后置，并通过测试检查而非在此证明。

被否决的替代方案

单独的 λ AST。 使用 Term[T] 让演算留在共享基底之内：相同的分析、代换和轨迹都适用，领域值也原样随行。
分开的 β 与 η 范式化器。 以间接方式提供：将 beta_rule 或 eta_rule 以任意策略传给 @eval.evaluate。
β 中的迭代代换。 β 只代换一次；按演算的要求，参数不会被再次代换。

边界

没有类型：诸如 $\Omega$ 这样行为不良的项会被接受，并以 StepLimitReached 结束。
没有共享：被复制的参数在每个副本中各归约一次。如需高效范式化，请使用 utlc/nbe。
η 只识别一元应用。
常量（Value）在这里没有归约规则；请用 rewrite 或 eval 添加领域规则。

Barendregt，The Lambda Calculus，定理 3.2.8 与 3.3.9。 ↩
Barendregt，The Lambda Calculus，§15.1。 ↩