utlc/nbe 设计

设计目标

小步范式化对每个 β 步都要从根重新搜索，并且每次都复制项。基于求值的范式化（NbE）则将项解释为宿主语言中的值，其中 β 归约就是函数应用，然后把该值读回为范式。本包为 De Bruijn 项上的无类型演算提供 NbE：速度快，但受燃料（fuel）限制，因为无类型项不一定可范式化。操作式归约器仍是参考语义；NbE 以它们为基准进行检验。

数学背景

语义域

值由下面的文法给出，其中 $\rho$ 是环境（值的列表，索引 $0$ 在前）， $t$ 是 De Bruijn 项， $x$ 是自由名字， $\ell$ 是层级（level）：

\begin{aligned} d \in D \;&::=\; \mathsf{atom}(v) \;\mid\; \mathsf{clo}(t, \rho) \;\mid\; \mathsf{delay}(t, \rho) \;\mid\; n, \\ n \in \mathrm{Ne} \;&::=\; \mathsf{free}(x) \;\mid\; \mathsf{lvl}(\ell) \;\mid\; \mathsf{app}(d, d). \end{aligned}

$\mathsf{clo}(t, \rho)$ 是 $\lambda.\,t$ 在 $\rho$ 中的值； $\mathsf{delay}(t, \rho)$ 是尚未求值的参数；中性值 $n$ 是卡在某个变量上的计算。在实现中，当 $d$ 是常量时也会出现 $\mathsf{app}(d, e)$ ，因为常量应用于参数同样会卡住。

求值

$\llbracket t \rrbracket\rho$ 求值到弱头形式：

\begin{aligned} \llbracket v \rrbracket\rho &= \mathsf{atom}(v), & \llbracket x \rrbracket\rho &= \mathsf{free}(x), & \llbracket i \rrbracket\rho &= \mathrm{force}(\rho_i), \\ \llbracket \lambda.\,t \rrbracket\rho &= \mathsf{clo}(t, \rho), & \llbracket t\,u_1 \cdots u_n \rrbracket\rho &= \mathrm{app}(\cdots\mathrm{app}(\llbracket t \rrbracket\rho, \mathsf{delay}(u_1, \rho))\cdots, \mathsf{delay}(u_n, \rho)), \end{aligned}

\mathrm{app}(\mathsf{clo}(t, \rho), e) = \llbracket t \rrbracket(e \cdot \rho), \qquad \mathrm{app}(d, e) = \mathsf{app}(d, e) \ \text{otherwise}, \qquad \mathrm{force}(\mathsf{delay}(t, \rho)) = \llbracket t \rrbracket\rho .

参数被延迟，因此求值是传名调用：从未使用的参数永远不会被求值。没有记忆化；被使用两次的延迟参数会被求值两次。

读回

$R_n(d)$ 在 $n$ 个绑定子之下读回 $d$ ：

\begin{aligned} R_n(\mathsf{atom}(v)) &= v, & R_n(\mathsf{free}(x)) &= x, & R_n(\mathsf{lvl}(\ell)) &= n - 1 - \ell, \\ R_n(\mathsf{clo}(t, \rho)) &= \lambda.\, R_{n+1}\big(\llbracket t \rrbracket(\mathsf{lvl}(n) \cdot \rho)\big), & R_n(\mathsf{app}(d, e)) &= R_n(d)\; R_n(e), & R_n(\mathsf{delay}(t,\rho)) &= R_n(\llbracket t \rrbracket\rho). \end{aligned}

闭包通过应用于一个新变量来读回。该变量由其层级 $n$ 表示，当值被携带到更多绑定子之下时层级不变，并在出现处转换为索引 $n - 1 - \ell$ （见 debruijn 设计中的层级）。对闭项 $t$ ，normalize(t) 即 $R_0(\llbracket t \rrbracket[\,])$ 。

设计决策

无类型 NbE 需要预算

问题。 对于 $\Omega = (\lambda.\,0\,0)(\lambda.\,0\,0)$ ，求值会无休止地展开 $\mathrm{app}(\mathsf{clo}(0\,0, [\,]), \cdot)$ 。在有类型的设定中终止性是一个定理（stlc 设计）；在这里它不成立。

选择。 每次对节点求值、每次 force 以及每个读回步骤都消耗一单位燃料，燃料耗尽时返回 FuelExhausted 及已消耗的量。预算贯穿所有阶段，因此在绑定子之下读回（可能会对闭包体求值）的开销也计算在内。

预算中的确定性。 计算除了用于停止之外不检查燃料，因此一次燃料为 $f$ 、在消耗 $c \le f$ 单位后以范式结束的运行，在任意燃料 $f' \ge c$ 下执行完全相同的计算。因此结果是可复现的，且 consumed 恰好是得到该结果所需的最小预算。

问题。 严格求值（传值调用）在 $(\lambda.\,7)\,\Omega$ 上发散，尽管该项有范式 $7$ 。

选择。 参数被延迟。读回先对每个中性项的头部求值，然后再处理其参数，并且只在头部确定之后才进入闭包；二者结合实现了正规序（最左最外）归约，即 eval 设计中的范式化策略。传需求调用会共享延迟的结果；未采用它是因为它需要可变的 thunk，而预算使重复计算的开销有界且可见。

不透明的语义值

Semantic[T] 是包裹一个私有枚举的结构体。调用者可以创建中性值（reflect_free、reflect_level）、求值和 quote，但无法构造环境作用域不良的闭包。这保持了“每个闭包环境都与其体的作用域相匹配”这一不变式，这也是 eval 只需验证一次输入、之后便可信任每次索引查找的原因。

范式中的一元应用

读回将 $R_n(\mathsf{app}(d, e)) = R_n(d)\,R_n(e)$ 生成为一元 Apply，因此脊 $f\,a\,b$ 被返回为 Apply(Apply(f, [a]), [b])。小步归约器则保留其输入中的 n 元 Apply(f, [a, b])。两者表示同一个柯里化应用；比较这两个范式化器时必须先展平脊。

正确性 / 不变量

定理（可靠性）。 若 normalize(t, fuel) 返回 NormalForm(u, _)，则 $u$ 是 β-范式，且 $t =_\beta u$ （在脊展平意义下）。

证明概要。 将值在 $n$ 个绑定子之下的指称 $\lfloor d \rfloor_n$ 定义为它所代表的项： $\lfloor \mathsf{clo}(t, \rho) \rfloor_n = \lambda.\,t[\rho]$ ， $\lfloor \mathsf{delay}(t, \rho) \rfloor_n = t[\rho]$ ， $\lfloor \mathsf{lvl}(\ell) \rfloor_n = n - 1 - \ell$ ，依此类推，其中 $t[\rho]$ 将 $\rho$ 的指称代换为 $t$ 的自由索引。对求值归纳可得 $t[\rho] \to_\beta^{*} \lfloor \llbracket t \rrbracket\rho \rfloor_n$ ：唯一非平凡的情形是 $\mathrm{app}(\mathsf{clo}(t, \rho), e)$ ，它就是 β 步 $(\lambda.\,t[\rho])\,\lfloor e \rfloor \to_\beta t[\lfloor e \rfloor \cdot \rho]$ （debruijn 附录中的代换引理）。读回只在绑定子之下插入 β 步，因此 $t \to_\beta^{*} u$ 。关于范式性： $R$ 只从闭包生成 $\lambda$ ，只从 $\mathsf{app}(d, e)$ 生成应用，而其头部 $d$ 是中性项或常量，绝不是闭包（闭包的应用会被求值，而不是被存储）。因此输出遵循文法

\mathit{nf} \;::=\; \lambda.\,\mathit{nf} \;\mid\; \mathit{ne}, \qquad \mathit{ne} \;::=\; x \;\mid\; i \;\mid\; v \;\mid\; \mathit{ne}\;\mathit{nf},

其中不含可约式 $(\lambda.\,t)\,u$ 。 $\square$

完备性（证明概要）。 若 $t$ 有 β 范式，则在燃料充足时 normalize 返回它。求值通过传名调用计算弱头范式，读回则递归地范式化闭包的体，以及中性项在其头部之后的参数：这正是分解为头部与参数的最左最外策略。由范式化定理（Barendregt 13.2.2），该策略在每个有范式的项上终止；由合流性，范式是唯一的。¹1 关于无类型 NbE，见 K. Aehlig 与 F. Joachimski，“Operational aspects of untyped normalisation by evaluation”，Mathematical Structures in Computer Science 14，2004；关于通过求值实现的强归约，见 B. Grégoire 与 X. Leroy，“A compiled implementation of strong reduction”，ICFP 2002。

与小步归约的一致性。 由可靠性与合流性，只要 @nbe.normalize 与 @debruijn.normalize 对同一个项都返回范式，这两个范式在脊展平后相等。src/utlc/nbe/nbe_test.mbt 中的测试检查了这一点，以及 $(\lambda.\,7)\,\Omega$ 上的惰性、 $\Omega$ 上的燃料耗尽，以及 quote 会把层级转换回索引。

其他不变式：

eval 和 normalize 在做任何工作之前就以 ScopeFailure 和 consumed=0 拒绝作用域不良的输入。
quote(value, n, _) 仅当某个层级变量不小于 $n$ 时才返回 ScopeFailure，而对于由 eval 产生并在层级 0 quote 的值，这不可能发生。
燃料：consumed 从不超过给定的燃料；上述确定性性质成立。

被否决的替代方案

有类型或 η-长形式的读回。 无类型读回无法知道在何处进行 η-展开；有类型项的 η-长形式范式由 stlc 提供。
宿主语言闭包（HOAS）。 将 $\mathsf{clo}$ 表示为 MoonBit 函数会更快，但会使燃料计量与值的检查变得不可能，而且若不在宿主侧使用新变量技巧，这些值也无法被 quote。一阶闭包使一切都保持可观察。
具名环境。 以 De Bruijn 索引对环境进行索引使查找按位置进行，并且求值期间不需要新名字。

边界

仅 β：没有 η，也没有常量的归约。
不是全函数：FuelExhausted 是发散项的预期结果，但它并不证明发散。
延迟参数不共享。
范式使用一元应用。
输入必须是 De Bruijn 语法；用 @debruijn.from_named 转换具名项，并用 @debruijn.to_named 把结果转换回来。

关于无类型 NbE，见 K. Aehlig 与 F. Joachimski，“Operational aspects of untyped normalisation by evaluation”，Mathematical Structures in Computer Science 14，2004；关于通过求值实现的强归约，见 B. Grégoire 与 X. Leroy，“A compiled implementation of strong reduction”，ICFP 2002。 ↩