eval 设计

设计目标

eval 为文献和下游包中谈到的归约策略命名，并通过 rewrite 的单步机制在任意规则上运行它们。选择策略应当是一个可以存储、比较和打印的值，而不是调用另一个函数。

数学背景

这些策略对任意规则 $r$ 都有定义；经典结果是针对 lambda 演算的 beta 规则 $(\lambda x.\,b)\,a \to_\beta b[x := a]$ 陈述的，其中 Apply 被读作柯里化的脊柱，Bind 被读作 $\lambda$。

归约上下文

一个策略由它可以收缩可约式的上下文以及这些上下文之间的顺序来描述。用 $\Box$ 表示洞：

$$\begin{aligned} \text{full:}\qquad C &::= \Box \;\mid\; \lambda x.\,C \;\mid\; C(\bar u) \;\mid\; t(u_0, \dots, C, \dots, u_n), \\ \text{weak head:}\qquad H &::= \Box \;\mid\; H(\bar u). \end{aligned}$$

• 正规序 在所有完整上下文 $C$ 中收缩最左最外的可约式。
• 应用序 在所有完整上下文 $C$ 中收缩最左最内的可约式。
• 弱头 归约若根处有可约式则收缩它，否则只在头部位置 $H$ 中查找；它从不进入绑定子或参数。

弱头归约找不到 beta 可约式的项处于弱头范式：即抽象 $\lambda x.\,t$，或头部 $h$ 为变量或值的脊柱 $h\,u_1 \cdots u_n$。

beta 的经典结果

标准化与正规化。 若一个项具有 beta 范式，则正规序归约能到达它。¹1 Curry 与 Feys，Combinatory Logic I，1958；另见 Barendregt，The Lambda Calculus，定理 13.2.2。 因此正规序是一个正规化策略，这也是它成为 lambda 演算各包默认策略的原因。

应用序不是正规化的。 令 $\Omega = (\lambda w.\,w\,w)(\lambda w.\,w\,w)$，它只归约到自身。对于 $t = (\lambda x.\,y)\,\Omega$：

$$\begin{aligned} \text{normal order:}\quad & (\lambda x.\,y)\,\Omega \;\to_\beta\; y && \text{root redex is outermost,}\\ \text{applicative order:}\quad & (\lambda x.\,y)\,\Omega \;\to_\beta\; (\lambda x.\,y)\,\Omega \;\to_\beta\; \cdots && \Omega \text{ is innermost.} \end{aligned}$$

一致性。 beta 归约是合流的（Church–Rosser），因此只要两个策略都到达 beta 范式，这些范式就是 alpha 等价的。²2 Church 与 Rosser，“Some properties of conversion”，Transactions of the AMS 39，1936。 一个策略可能不终止，但不可能产生不同的范式。

弱头归约 在弱头范式存在时计算出它；它是传名调用语言以及 utlc/nbe 中惰性求值器的求值顺序。

设计决策

以枚举表示策略

问题。 调用者需要选择、记录和比较策略，例如在一个将两个策略相互比对的测试中。

备选方案。 传入一个单步函数；传入一个 trait 对象；从枚举中选择。

选择。 Strategy 是一个带有 Eq 和 Debug 的普通枚举，由 reduce_once 解释。自定义策略仍然可行：任何单步函数都可以直接传给 @rewrite.normalize 和 @rewrite.trace。该枚举只涵盖有名称的策略。

每个策略都是 rewrite 的一种遍历

$$\begin{aligned} \texttt{NormalOrder},\ \texttt{FullNormal} &\;\mapsto\; \texttt{top\_down\_once} && \text{(pre-order: leftmost-outermost)},\\ \texttt{ApplicativeOrder} &\;\mapsto\; \texttt{bottom\_up\_once} && \text{(post-order: leftmost-innermost)},\\ \texttt{WeakHead} &\;\mapsto\; \text{root, then head of } \texttt{Apply}, \text{ recursively}. \end{aligned}$$

前序搜索返回第一个不被其他可约式包含的可约式，先扫描头部再扫描参数，参数从左到右；这就是最左最外的可约式，而 rewrite 设计 中的范式引理表明 NoStep 意味着”已是范式”。后序搜索返回一个不包含其他可约式的可约式，即最左最内的那个。弱头搜索只沿脊柱进行，因此它的 NoStep 仅意味着”已是弱头范式”，别无其他。

evaluate 与 trace 不添加任何自身的归约逻辑：它们把策略的单步函数传给 @rewrite.normalize 和 @rewrite.trace。因此每个策略都有轨迹，且步数契约对所有策略都相同。

FullNormal 作为单独的名称

目前 FullNormal 与 NormalOrder 映射到同一种遍历。区别在于意图：NormalOrder 承诺步骤的顺序（最左最外），FullNormal 只承诺得到完全范式。保留两个名称使得以后可以用更快的完全正规化器替换 FullNormal，而不改变 NormalOrder 的含义。

正确性 / 不变量

• 对每个策略，reduce_once 都满足 rewrite 的单可约式契约；WeakHead 步骤报告的路径仅由 ApplyHead 帧组成。
• 对于 NormalOrder、FullNormal 和 ApplicativeOrder，NoStep 意味着规则在任何位置都不适用；对于 WeakHead，意味着在头部脊柱上的任何位置都不适用。
• 使用 beta 规则时，对每个具有 beta 范式的 $t$，只要 $k$ 至少为正规序归约的长度，evaluate(t, _, beta, NormalOrder, k) 就返回 NormalForm（正规化定理）。
• 若对于一个合流的规则两个策略都返回 NormalForm，则这些项是 alpha 等价的（Church–Rosser）。

库的测试将具名与 De Bruijn 的 beta 步骤相互比对（src/utlc/lambda/lambda_test.mbt），并将正规序与 NbE 正规化器相互比对（src/utlc/nbe/nbe_test.mbt）。

被否决的替代方案

• 求值到值的传值调用求值。 通常的传值调用策略不在绑定子下归约，并把抽象视为值。它可以表达为自定义单步函数，但它不属于各包所需的完全策略或头部策略，因此不在枚举中。
• 绑定子下的头归约。 头归约（在外层绑定子下归约 $\lambda \bar x.\,(\lambda y.\,b)\,a\,\bar u$）可以写成自定义单步函数；枚举只保留实际使用的策略。
• 策略专属的结果类型。 所有策略共享 NormalizationResult，因此调用者无需修改代码即可切换策略。

边界

• 策略只选择位置；它们从不重命名、共享或记忆化。重复的子项会被分别归约。
• 没有以具名情形提供传值调用、传需求调用或头部策略。
• 终止性由 max_steps 加以限制，而不是被判定。
• eval 只作用于 Term[T]；下游 AST 使用自顶向下的 @rewrite.generic_normalize。

Footnotes

1. Curry 与 Feys，Combinatory Logic I，1958；另见 Barendregt，The Lambda Calculus，定理 13.2.2。 ↩

2. Church 与 Rosser，“Some properties of conversion”，Transactions of the AMS 39，1936。 ↩