归结原理之外：项重写系统（Term Rewriting System）

项重写系统是一种基于规则的计算模型，由一组重写规则组成，每条规则把符合左侧模式的项替换为右侧的项，通过反复应用规则来化简表达式或进行符号推理。

概述

项重写系统是抽象重写理论在项结构上的具体化，广泛用于形式化方程理论、函数式程序求值和自动定理证明。它把计算看作方向性的化简过程，与方程逻辑关系密切，但重写规则只能单向使用，这一方向性使得计算有明确的推进方向。

核心特点

• 终止性：又称强正规化，指不存在无限长的重写序列，保证化简过程一定会停下来。
• 合流性：又称丘奇-罗塞尔性质，指无论以何种顺序应用规则，最终都能汇合到相同结果。
• 正规形式：无法再被任何规则改写的项，代表化简的终点。
• 完备性：终止且合流的系统称为完备，此时每个项都有唯一正规形式，可作为判定方程相等的决策过程。
• 克努斯-本迪克斯补全：一种从方程集合自动构造完备重写系统的经典算法。

应用场景

项重写系统用于函数式语言的求值语义、自动定理证明中的方程推理、代数规范的可执行化、以及编译器优化中的表达式化简。克努斯-本迪克斯补全算法在群论等代数结构的判定问题中有实际应用。它也是抽象解释和符号执行的理论工具。

常见问题

问：终止性和合流性为什么都需要？答：终止性保证化简总会停止，合流性保证结果唯一，两者缺一不可。只有终止而不合流，可能得到多个不同正规形式；只有合流而不终止，则可能永远算不出结果。

问：如何判断一个重写系统会终止？答：终止性一般不可判定，但可以通过构造一个使每步重写都严格递减的良基序来证明，常用的方法包括递归路径序和多项式解释等技术。