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

项重写是交互式定理证明器的核心机制之一，它通过应用重写规则系统化地转换逻辑项，逐步简化或变形表达式以完成证明。下面将从基础概念到实际应用展开说明。

1. 项与项语言的基础
   项是由函数符号、变量和常量按语法规则构成的表达式。例如在算术中，"f(x, g(2))" 是一个项，其中 f 和 g 是函数符号，x 是变量，2 是常量。项语言定义了合法表达式的构成规则，通常通过上下文无关文法描述。这种形式化是重写操作的载体。

2. 重写规则与匹配机制
   重写规则形如 "l → r"，表示当项中存在与左端 l 匹配的子结构时，可替换为右端 r。匹配过程通过替换 σ 使得 lσ 与目标子项一致。例如规则 "add(0, x) → x" 应用到项 "add(0, succ(y))" 时，通过替换 σ = {x ↦ succ(y)} 得到结果 "succ(y)"。此过程需处理变量绑定和结构一致性。

3. 重写策略的控制流程
   实际证明中需要控制重写方向与范围：

   • 定向重写：仅当规则左端匹配时触发，避免循环
   • 条件重写：附加约束（如等式条件）需先验证再应用
   • 上下文限定：通过策略组合子指定重写位置（如仅化简假设部分）
     例如在Coq中，"rewrite H at 2" 表示在第二个匹配位置应用等式H。

4. 终止性与合流性分析
   为保证可靠性，需验证重写系统的元性质：

   • 终止性：通过良基序（如词典序、多项式解释）证明无限重写序列不存在
   • 合流性：若项 t 可重写到不同项 u1, u2，则存在共同后继 v
     这些性质通过临界对分析和简化序自动检测，构成重写可靠性的理论基础。

5. 高阶扩展与依赖类型处理
   在高级证明助理（如Lean、Agda）中，需处理：

   • 高阶匹配：允许规则中出现函数变量，需高阶合一算法
   • 依赖类型上下文：重写时维护类型一致性，如根据类型定义计算化简规则
     例如在类型化λ演算中，"(λx: A. t) s → t[s/x]" 的重写需同时验证项s的类型与x的注解类型匹配。

6. 策略集成与证明管理
   项重写作为原子操作被集成到复合策略中：

   • 重写序列：连续应用规则序列，自动处理依赖关系
   • 条件重写策略：在重写前自动调用决策过程验证前提条件
   • 失败恢复：当某规则应用失败时回滚状态或尝试替代规则
     这种机制使得重写既能作为独立自动化工具，也能参与交互式证明探索。

通过这六个层次的递进，项重写从基础符号操作发展为支持复杂推理的智能工具，其严谨性保障了证明的正确性，灵活性则适应了多样化的验证场景。