交互式定理证明器中的项重写 项重写是交互式定理证明器和形式化方法中的一个基础且强大的工具。它提供了一种通过应用一组预定义的规则来系统地化简或转换表达式（即“项”）的方法。其核心思想非常简单：找到一个匹配某个“模式”的子项，然后用另一个指定的“替换”来替换它。然而，在这种简单性之下，蕴含着表达复杂计算和逻辑推理的巨大能力。 项、变量和规则 首先，我们需要明确几个基本概念。 项 ：一个项是一个形式表达式，它可以是一个常量（如 0 , true ）、一个变量（如 x , n ），或者一个函数符号应用于若干个子项（如 suc(n) , x + y , f(a, b) ）。项用来表示数据结构、程序表达式或逻辑公式。 变量 ：变量是占位符，可以代表任何项。 重写规则 ：一条重写规则是一个形如 左端 → 右端 的有序对。其中左端和右端都是项。例如，一条表示加法消去的规则可以写成 x + 0 → x 。关键限制是：规则的左端不能仅仅是一个变量（否则规则 x → 0 会把任何项都变成 0 ，这通常不是我们想要的），并且右端中出现的变量必须在左端中也出现。 匹配与重写步骤 一个重写步骤是重写过程的核心。给定一个项 t 和一条规则 l → r ，其过程如下： 匹配 ：在项 t 中寻找一个子项 s ，使得存在一个“替换” σ （将规则中的变量映射到具体的项），使得 σ(l) （将替换应用到左端的结果）等于 s 。例如，对于项 (a + 0) + b 和规则 x + 0 → x ，我们可以匹配子项 a + 0 ，此时替换 σ 将变量 x 映射为 a 。 替换 ：应用相同的替换 σ 到规则的右端 r 上，得到 σ(r) 。在上例中， σ(r) = σ(x) = a 。 归约 ：用新得到的项 σ(r) 替换掉项 t 中匹配到的子项 s 。于是， (a + 0) + b 被重写为 a + b 。 这个过程就是一次基本的重写步骤。 重写策略与终止性 一个复杂的项中可能同时有多个地方可以应用规则。 重写策略 ：这决定了规则应用的顺序。例如，是从最内层的子项开始重写（惰性求值），还是从最外层开始（急切求值）？不同的策略可能导致不同的中间结果，但如果系统具有良好的性质，最终结果应该是一致的。 终止性 ：一个重写系统被称为是终止的（或强规范化的），如果不存在无限的重写序列 t1 → t2 → t3 → ... 。也就是说，无论应用规则的顺序如何，重写过程最终都会停止在一个无法再被重写的项上（称为正规形式）。证明终止性是一个重要课题，常用方法是构造一个“良基序”，使得每次重写后项在该序下都严格减小。 合流性与唯一正规形式 终止性保证了过程会结束，但我们需要保证结束点是唯一的。 合流性 ：一个重写系统被称为是合流的（或具有Church-Rosser性质），如果对于任意一个项 t ，如果它能通过不同的路径重写到 t1 和 t2 ，那么必然存在某个项 t3 ，使得 t1 和 t2 都能继续重写到 t3 。 意义 ：如果一个系统既是终止的又是合流的，那么每个项都有且只有一个唯一的正规形式。这意味着计算的结果是确定无疑的，与化简的顺序无关。这为等价性判断提供了强大工具：两个项是等价的当且仅当它们有相同的正规形式。 条件重写与在定理证明中的应用 基本的重写规则是无条件的。但很多情况下的转换是有前提的。 条件重写规则 ：规则形式扩展为 l → r if Condition 。例如，一条关于除法的规则： x / y → z if y * z = x 。应用这条规则时，不仅需要匹配左端，还需要证明条件 y * z = x 成立。这极大地增强了重写系统的表达能力。 在定理证明中的应用 ：在交互式定理证明器（如Coq, Isabelle, Lean）中，项重写是自动化策略（如 simpl , rewrite , unfold ）的基石。用户可以将已知的等式定理（如结合律、交换律）声明为重写规则。证明器会自动匹配当前证明目标中的模式，并应用规则进行化简，从而大大减轻了用户的证明负担。重写系统本身也可以作为研究对象，用于定义编程语言的语义（操作语义）和实现符号计算。 总结来说，项重写从一个简单的“查找-替换”概念出发，通过研究其终止性、合流性等元性质，并引入条件规则，发展成为在逻辑、程序验证和符号计算中处理等价性和化简问题的核心形式化工具。