rewrite 设计

设计目标

rewrite 把一条局部规则（在项的根处重写的部分函数）变成全局的、可审计的归约：在选定位置执行一步，并记录位置和所用规则，以及对这样的步骤做有界的重复。库中的所有操作语义（eval 策略、lambda 演算、debruijn 中的 De Bruijn 归约器）都被定义为这种形式的单步函数，从而每个正规化器都可以逐步解释。

数学背景

抽象重写系统

抽象重写系统是一个集合 $A$ 连同一个关系 $\to\ \subseteq A \times A$ 。¹1 Terese，Term Rewriting Systems，Cambridge University Press 2003，第 1 章。记 $\to^{*}$ 为其自反传递闭包， $\leftrightarrow^{*}$ 为其等价闭包。

若不存在 $b$ 使得 $a \to b$ ，则 $a$ 是一个范式。
若不存在无穷链 $a_0 \to a_1 \to \cdots$ ，则 $\to$ 是终止的（强正规化）；若每个元素都能归约到某个范式，则它是弱正规化的。
若 $b \leftarrow^{*} a \to^{*} c$ 蕴涵对某个 $d$ 有 $b \to^{*} d \leftarrow^{*} c$ ，则 $\to$ 是合流的；若这对单步分叉 $b \leftarrow a \to c$ 成立，则它是局部合流的。

合流性使范式唯一：若 $a \to^{*} n_1$ 且 $a \to^{*} n_2$ ，且两者均为范式，则公共归约结果 $d$ 必须同时等于两者。Newman 引理指出，终止且局部合流的系统是合流的；项重写系统的局部合流性由其临界对的可汇合性得出（Knuth–Bendix）。²2 M. H. A. Newman，“On theories with a combinatorial definition of equivalence”，Annals of Mathematics 43，1942。

位置与上下文

位置是从根出发的帧路径 $p$ ：BinderBody 进入 $\beta x.\,\Box$ ，ApplyHead 进入 $\Box(\bar u)$ ，ApplyArgument(i) 进入第 $i$ 个参数。记 $t|_p$ 为位置 $p$ 处的子项， $t[s]_p$ 为将该子项替换为 $s$ 后的 $t$ ：

\begin{aligned} t|_{\varepsilon} &= t, & (\beta x.\,t)|_{\mathsf{B}\cdot p} &= t|_p, & t(\bar u)|_{\mathsf{H}\cdot p} &= t|_p, & t(u_0,\dots,u_n)|_{\mathsf{A}_i\cdot p} &= u_i|_p . \end{aligned}

规则的重写关系

规则是一个部分函数 $r : \mathrm{Term} \rightharpoonup \mathrm{Term}$ 。 $r$ 的可约式是其定义域中的项。 $r$ 的重写关系是它在上下文下的闭包：

\frac{t|_p \in \operatorname{dom} r}{t \;\to_r\; t[\,r(t|_p)\,]_p}

策略是一个部分函数 $S$ ，只要有定义就满足 $S(t) \in \{\, u \mid t \to_r u \,\}$ ；它在可能的步骤中选择一个。本包的遍历函数都是策略，而 StepResult 使这种选择可观察。

设计决策

单步是原语

问题。 一遍就重写”所有能重写之处”的正规化器速度快，但其行为无法与规范对照，中间状态也会丢失。

选择。 原语是在一个位置上的一步，返回为 Reduced(before, after, rule, path) 或 NoStep。其契约在实现中由构造保证，即

\texttt{Reduced}(t, u, r, p) \implies t|_p \in \operatorname{dom} r \;\wedge\; u = t[\,r(t|_p)\,]_p ,

因此每个报告的步骤都恰好是在所报告位置上的一步 $\to_r$ 。遍历仅重建路径上的节点来构造 after，并在返回途中每层前置一个帧来构造 path。正规化器和轨迹都是在这个原语上的循环，不添加任何语义。这一设计的代价是完全正规化每一步都要从根重新遍历；好处是每个正规化器都有轨迹，并且两个实现可以逐步比较。

策略即遍历顺序

top_down_once 先在节点上尝试规则，再尝试其子节点，子节点顺序为头部、参数 0、参数 1、… 它返回前序中的第一个可约式，即最左最外的可约式：没有可约式包含它，且在这样的可约式中它是最左的。bottom_up_once 先尝试子节点，返回后序中的第一个可约式，即最左最内的可约式：它不包含其他可约式。

引理（范式）。 对两种遍历， $t$ 上的 NoStep 当且仅当 $t$ 是 $\to_r$ 的范式。

两种遍历都访问 $t$ 的每个位置（进入绑定子体、头部和所有参数），并在那里尝试 $r$ 。只有在每次尝试都返回 None 后它们才返回 NoStep，因此没有位置是可约式；反之，若某个位置是可约式，遍历会到达它，除非更早以另一步返回。 $\square$

因此，使用任一遍历的 normalize 仅当 $t$ 是 $\to_r$ 范式时才返回 NormalForm(t, n)。其他策略，例如 eval 中的弱头归约，访问的位置更少；对它们而言 NoStep 仅意味着”在策略考虑的位置上没有可约式”。

带精确计数的有界重复

normalize(t, step, k) 计算序列 $t_0 = t$ 、 $t_{i+1} = \mathit{after}(\mathit{step}(t_i))$ ，并在第一个满足 $\mathit{step}(t_n) = \texttt{NoStep}$ 的 $n$ 处或在 $n = k$ 处停止：

\texttt{normalize}(t, \mathit{step}, k) = \begin{cases} \texttt{NormalForm}(t_n, n) & n \le k,\ \mathit{step}(t_n) = \texttt{NoStep},\\ \texttt{StepLimitReached}(t_k, k) & \mathit{step}(t_k) \ne \texttt{NoStep}. \end{cases}

在 $n = k$ 处的额外调用区分了”恰好 $k$ 步后为范式”与”达到上限”，因此结果从不声称一个未经检查的范式。步数上限是必要的，因为对任意规则而言终止性不可判定（且对无类型 lambda 演算不成立）；它是一个参数，而不是全局设置。

规则是命名的，而非注册的

问题。 重写系统通常有多条规则。

备选方案。 包内的规则注册表；每次调用一个规则列表；每次调用一个规则函数。

选择。 每次调用一个规则函数和一个 RuleName。具有多条规则的系统要么合并为一条规则（如 lambda 中的 beta_eta_rule，它在每个位置先尝试 beta 再尝试 eta），要么表达为依次尝试若干单规则遍历的单步函数。这两种选择给出不同的策略：前者选取任一规则适用的最外位置，后者在整个项中优先第一条规则。把这一选择留给调用者，避免了为每种语言固定同一种优先级方案。

通过视图的泛型遍历

generic_top_down_once 就是使用 project 做模式匹配、使用 trait 构造器做重建的 top_down_once。除了视图定律之外，它不需要了解下游 AST 的任何信息，因此多项式或数值表达式 AST 可以免费获得位置和轨迹。只有自顶向下策略提供了泛型版本，因为它是下游化简器使用的策略，并且它使范式引理可用。

正确性 / 不变量

一步至多在一个位置重写，且所报告的 path 在 before 中指向该位置（契约见上文）。由 “structured step records rule and root path” 以及 debruijn 的路径测试检验。
来自 top_down_once、bottom_up_once 或 generic_top_down_once 的 NoStep 意味着该项对该规则是范式（范式引理）。
normalize 与 trace 至多执行 max_steps 步，并至多调用 step max_steps + 1 次；NormalForm(t, n) 蕴涵 step(t) = NoStep。
在 ReductionTrace 中，steps[0].before = initial，steps[i].after = steps[i+1].before，且 result 的最终项是最后一个 after（若没有步骤则为 initial）。

不检查的内容。 本包不判定规则的终止性或合流性。当规则合流时，每个终止的策略都到达相同的范式；当规则不合流时，不同策略可以合理地返回不同的范式，而轨迹会显示原因。

代价：对大小为 $n$ 的项，一步需要 $O(n)$ 次规则尝试，外加重建路径；以 $k$ 步正规化需要 $O(k \cdot n)$ 次规则尝试。

被否决的替代方案

原地或记忆化的重写。 更快，但会丢失 before 和路径，并与不可变项相冲突。
固定的规则语言（带变量的模式）。 模式语言需要匹配和出现检查；以 MoonBit 函数表示的规则可以使用宿主语言的模式匹配以及任意附加条件。
感知捕获的遍历。 遍历可以在把开子项传给规则之前对绑定子重命名。需要感知绑定的规则使用代换，它已经会重命名；在遍历中重命名会在规则不知情的情况下改变绑定子名称。

边界

规则把绑定子下的子项视为开项；遍历既不重命名，也不报告哪些绑定子在作用域内。规则必须在开项上正确。
不支持模结合律、交换律或 alpha 等价的匹配；规则按项的原样用 MoonBit 模式进行匹配。
不做终止性、合流性或临界对分析。
泛型版本仅存在于自顶向下策略以及不带轨迹的正规化。
上限 max_steps 计数的是步数，而不是时间或内存。

Terese，Term Rewriting Systems，Cambridge University Press 2003，第 1 章。 ↩
M. H. A. Newman，“On theories with a combinatorial definition of equivalence”，Annals of Mathematics 43，1942。 ↩