交互式定理证明器中的项重写

项重写是交互式定理证明器中的一种核心策略，用于通过应用重写规则来简化或转换表达式。其基本思想是将项中的某个子项替换为另一个等价的项，从而逐步推进证明或化简目标。下面我们将从项重写的基本概念开始，逐步深入其规则、策略和应用。

1. 项与重写规则的基本定义
   在逻辑系统中，项是由变量、常量或函数符号组成的表达式，例如 \(f(x, g(y))\)。重写规则是一个形如 \(L \to R\) 的定向等式，表示当项中出现与左端 \(L\) 匹配的子项时，可将其替换为右端 \(R\)。例如，规则 \(\text{add}(0, n) \to n\) 表示将 \(0+n\) 简化为 \(n\)。匹配过程需考虑变量的替换（即合一），例如用项 \(\text{add}(0, \text{suc}(m))\) 匹配规则时，变量 \(n\) 被替换为 \(\text{suc}(m)\)，重写后得到 \(\text{suc}(m)\)。

2. 重写过程的严格描述
   项重写的每一步需满足以下条件：

   • 找到当前项 \(t\) 的一个子项 \(s\)，使得存在重写规则 \(L \to R\) 和替换 \(\sigma\)（将规则中的变量映射为具体项），满足 \(\sigma(L) = s\)。
   • 将 \(s\) 替换为 \(\sigma(R)\)，得到新项 \(t'\)。
     这一过程可递归进行，直到无法匹配任何规则。例如，对项 \(\text{add}(\text{add}(0, a), b)\)，先应用规则将内层 \(\text{add}(0, a)\) 重写为 \(a\)，得到 \(\text{add}(a, b)\)。

3. 终止性与合流性
   重写系统需关注两个关键性质：

   • 终止性：确保重写过程总会停止，避免无限循环。例如，规则 \(f(x) \to f(g(x))\) 会导致无限重写，而规则 \(\text{add}(0, n) \to n\) 是终止的。终止性常通过序（如简化序）证明。
   • 合流性：若项可通过不同路径重写为多个结果，则这些结果必能最终重写为同一项。合流性保证重写结果的唯一性，是完成化简的关键。

4. 条件重写与策略控制
   实际证明器中，重写规则可能附带条件。例如，规则 \(x - y \to 0\) 需条件 \(x = y\)，此时重写前需先验证条件成立。策略上，证明器允许用户指定重写方向（从左到右或反向）、重写位置（仅最外层或所有子项），或与其他策略（如化简、归纳）结合使用。

5. 在证明中的应用示例
   假设要证明 \(\forall n, \text{add}(n, 0) = n\)，可通过重写系统实现：

   • 定义规则集：\(\text{add}(0, n) \to n\) 和 \(\text{add}(\text{suc}(m), n) \to \text{suc}(\text{add}(m, n))\)。
   • 对项 \(\text{add}(n, 0)\) 进行重写：若 \(n\) 为 \(0\)，直接应用第一条规则；若 \(n\) 为 \(\text{suc}(m)\)，先应用第二条规则，再递归重写内层项，最终化简为 \(n\)。
     此过程展示了重写如何将等式证明转化为计算问题。

通过以上步骤，项重写将逻辑等价关系转化为计算步骤，成为自动化推理的基石。在高级应用中，它还可与类型论、依赖类型等结合，处理复杂定理的证明。