交互式定理证明器中的项重写策略 项重写的基本概念 项重写（Term Rewriting）是一种基于模式匹配的符号计算规则，形式为 $l \to r$，表示当项 $t$ 中存在子项匹配模式 $l$ 时，可将其替换为对应实例化的 $r$。例如规则 $\text{add}(0, x) \to x$ 可将 $\text{add}(0, 3)$ 重写为 $3$。在交互式定理证明器（如 Coq、Isabelle、Lean）中，项重写策略允许用户定向应用等式定理，自动化化简或变换目标。 重写规则的逻辑基础 项重写对应逻辑中的等式推理。若已有定理 $∀x. l(x) = r(x)$，重写策略可将其转化为从左到右的替换规则。关键要求是匹配过程需处理变量的绑定问题，尤其在依赖类型或高阶语境中。例如在 Coq 的 rewrite 策略中，用户需指定重写方向（ -> 或 <- ），并自动处理类型兼容性。 条件重写与多规则管理 实际定理常带前提条件，如 $∀x. P(x) → l(x) = r(x)$。此时重写策略需先证明当前上下文中条件 $P(t)$ 成立。证明器通过子目标生成处理该过程。系统通常维护重写规则库（如 Isabelle 的 simpset ），支持规则优先级、结合顺序控制，避免非终止循环。 高阶匹配与隐式参数 当项包含 λ-抽象或类型类约束时，重写需支持高阶匹配。例如规则 $∀f g. (∀x. f x = g x) → f = g$ 需在函数相等性上操作。证明器会通过合一算法处理隐式参数，用户可通过注解（如 Coq 的 subst 或 pattern ）指导匹配范围。 重写策略的扩展机制 现代证明器提供组合策略增强重写能力： 迭代重写 ：如 rewrite ![rule] 重复应用至无法匹配。 条件重写集 ：如 Isabelle 的 simp 自动选择规则序列。 语境限制 ：仅重写目标的特定子项（如 rewrite [...] at [...] ）。 等价关系泛化 ：支持任意等价关系（如 setoid_rewrite ），不限于相等性。 终止性与一致性保障 证明器不自动验证规则集的终止性，但提供工具辅助分析（如依赖顺序、测度函数）。用户可通过声明规则属性（如 [simp] ）将其加入简化器，系统会记录规则来源以防循环依赖。高级策略如 ac_rewrite 还能处理结合律/交换律的重写优化。 与自动化证明的集成 项重写常作为更大自动化策略的组件，例如： 在归纳证明中通过 simpa 化简归纳假设。 结合 unification 和 paramodulation 进行等式推理。 与 SMT 求解器协作，将重写结果编码为背景理论。 这种集成使重写成为连接人工指导与完全自动证明的关键桥梁。