高效检查项排序约束的优化策略

### 高效检查项排序约束的优化策略 在算法执行过程中，对于固定值 A 的特定属性，我们可以设计专门的算法 `algA(B)` 来避免 `alg(A, B)` 中一些冗余的操作。通常，`algA(B)` 能利用 A 的已知特性，识别出某些对 A 恒为真或假的测试，展开循环和递归等。只要 `algA(B)` 能完成与 `alg(A, B)` 相同的任务，我们可以自由选择合适的算法。 与部分求值不同，这里 A 的值在运行时才确定，因此特化过程也在运行时进行。而且，我们不需要 `alg` 的具体表示，只需在编写特化程序时想象其功能。这意味着我们不能使用通用的算法特化方法，而需要为每个特定的算法 `alg` 编写特化程序。不过，这样做的好处是可以利用 `alg` 的特性进行强大的特定优化。 特化后的算法需要以可解释的形式表示。在很多情况下，当 `algA(B)` 要对多个 B 值依次计算时，我们可以将 `algA` 编译成特殊抽象机的代码。抽象机的指令可以用记录表示，其中一个字段存储标识指令类型的整数标签，其他字段存储指令参数。代码的所有指令可以存储在数组、列表或树中。解释过程是按一定顺序获取指令，识别其类型并执行相应操作。在 C 或 C++ 中，我们可以使用 `switch` 语句将不同的操作与指令标签关联起来。现代编译器通常能高效地编译具有窄范围整数标签的 `switch` 语句，通过将对应值 i 的语句地址存储在特殊数组的第 i 个单元中。我们可以利用这一点，从一个小的整数区间中选取指令标签的值。 当需要长期存储多个 A 的实例，并且 `alg(A, B)` 的调用中 B 的值以不可预测的顺序出现时，全面的编译特化可能会因内存使用过多而不合适。但我们有时可以为每个 A 找到一个紧凑的特化表示 A'，可以与 A 一起存储或替代 A。同时，我们定义一个变体 `alg'` 来处理这个表示，将所有对 `alg(A, B)` 的调用替换为 `alg'(A', B)`，以更快地完成相同的任务。 #### 通用框架 下面介绍一个用于特化 KBO 约束检查的通用框架，该框架将用于后续的前向检查和后向检查实现。 ##### 特化权重比较 在实现 KBO 约束检查时，引入一个比较权重表达式的函数 `compw` 会很方便： ```plaintext compw : P(V) × P(V) →{ = , > , < , ≤, ≥, ? } compw(p1, p2) =                    = if p1 = p2; > if p1 > p2; < if p2 > p1; ≤ if p2 ⋗p1 but neither p2 = p1 nor p2 > p1; ≥ if p1 ⋗p2 but neither p1 = p2 nor p1 > p2; ? otherwise. ``` 对于固定的项 s 和 t，`compw(|sθ|, |tθ|)` 的计算可以分为两个逻辑阶段进行特化： 1. **阶段 1**：为每个替换 θ 定义权重分配 σθ，即对于所有 x ∈ V，σθ(x) = |xθ|。这样，我们可以计算 `compw(σθ(|s|), σθ(|t|))` 作为 `compw(|sθ|, |tθ|)` 的值。当 s 和 t 固定时，权重表达式 |s| 和 |t| 可以预先计算，避免了对不同 θ 下的 sθ 和 tθ 中的 s 和 t 部分进行遍历。而且，在优化后的比较中，对于 s 和 t 中的每个变量，我们只计算一次 σθ(x) = |xθ|，而通用程序在计算 |sθ| 和 |tθ| 时会根据 x 在 s 和 t 中出现的次数多次遍历项 xθ。例如，对于 s = f(x0, f(x0, f(x1, f(x2, x3))))，我们可以计算 4 + 2|x0θ| + |x1θ| + |x2θ| + |x3θ|，而不是直接计算 |f(x0θ, f(x0θ, f(x1θ, f(x2θ, x3θ))))|，从而避免了对 f(., f(., f(., f(., .)))) 部分的遍历和对 x0θ 的重复检查。 2. **阶段 2**：我们可以计算 `compw(σθ(lft(|s|, |t|)), σθ(rht(|s|, |t|)))` 代替 `compw(σθ(|s|), σθ(|t|))`。函数 `lft` 和 `rht` 定义如下：`lft(p1, p2)` 是取 p1 - p2 中所有系数为正的项，`rht(p1, p2)` 是取 p2 - p1 中所有系数为正的项。多项式 `lft(|s|, |t|)` 和 `rht(|s|, |t|)` 可能比 |s| 和 |t| 包含更少的不同变量，这样我们需要检查的项 xθ 就会更少。例如，对于 s = f(x0, f(x0, f(x1, f(x2, x3)))) 和 t = f(x1, f(x2, f(x3, x3)))，比较 4 + 2|x0θ| + |x1θ| + |x2θ| + |x3θ| 与 3 + |x1θ| + |x2θ| + 2|x3θ| 可以简化为比较 1 + 2|x0θ| 与 |x3θ|，无需检查 x1θ 和 x2θ，也不需要对 |x3θ| 进行常数乘法。 对于固定的 p1, p2 ∈ P(V)，根据 p1 和 p2 的形式，σθ(p1) 与 σθ(p2) 的比较可以进一步特化： - 当 p1 = α1x1 + ... + αnxn（αi > 0），p2 = β0 > 0 时，σθ(p1) ⋗ σθ(p2) 等价于 α1 · mwgi(x1θ) + ... + αn · mwgi(xnθ) ≥ β0，其中 `mwgi(t)` 表示项 t 的基实例的最小权重，可以通过将 t 中的所有变量替换为最小权重的常数来计算。同样，σθ(p1) > σθ(p2) 等价于 α1 · mwgi(x1θ) + ... + αn · mwgi(xnθ) > β0，σθ(p1) = σθ(p2) 当且仅当 α1 · mwgi(x1θ) + ... + αn · mwgi(xnθ) = β0 且所有 xiθ 都是基项。这样做有两个优点：一是 `mwgi(xiθ)` 是数字而不是多项式，更容易计算、存储和操作；二是对于许多替换 θ，我们不需要完全计算 α1 · mwgi(x1θ) + ... + αn · mwgi(xnθ)，可以逐步计算，一旦发现 α1 · mwgi(x1θ) + ... + αi · mwgi(xiθ) + αi+1µ + ... + αnµ > β0，就可以立即停止并得出 σθ(p1) > σθ(p2) 的结论。 - 当 p1 = α0，p2 = β1x1 + ... + βnxn 时，σθ(p1) ⋗ σθ(p2) 当且仅当所有 xiθ 都是基项且 α0 ≥ β1 · mwgi(x1θ) + ... + βn · mwgi(xnθ)。同样，一旦发现某个 xiθ 是非基项或 β1 · mwgi(x1θ) + ... + βi · mwgi(xiθ) + βi+1µ + ... + βnµ > α0，就可以停止并得出 σθ(p1) ̸ ⋗ σθ(p2) 的结论。 - 对于一般情况 p1 = α0 + α1x1 + ... + αnxn 和 p2 = β0 + β1x1 + ... + βnxn，当发现 σθ(p1) 或 σθ(p2) 是常数时，就会退化为上述特殊情况。 ##### 展开递归和循环 下面是一个用于检查任意项 s 和 t 的 `s ≻ t` 的简单算法： ```plaintext fun greater(s, t : T (F, V)) if s is a variable x if x = t return = return × if t is a variable x if x occurs in s return > return × cw := compw(|s|, |t|) if cw = > return > /* s ≻ t */ if cw ∈{ = , ≥} return greater ′(s, t) return × /* failure */ fun greater ′(s, t) let s = f(s1, . . . , sm) and t = g(t1, . . . ```