重写

在数学、计算机科学和逻辑学中，重写涵盖了用其他术语替换公式中的子项的广泛方法。这些方法可以通过重写系统（也被称为重写系统、重写引擎或还原系统）来实现。

在其最基本的形式中，它们由一组对象，加上关于如何转换这些对象的关系组成。重写可以是非确定性的。一个重写术语的规则可以以许多不同的方式应用于该术语，或者有多个规则可以适用。

因此，重写系统并不提供将一个术语改为另一个术语的算法，而是提供一组可能的规则应用。然而，当与适当的算法相结合时，重写系统可以被看作是计算机程序，一些定理证明程序和声明性编程语言是基于术语重写的。

在逻辑学中，获得一个公式的共轭正常形式（CNF）的程序可以作为一个重写系统来实现。这样一个系统的例子的规则是。)表示与规则左侧相匹配的表达式可以改写成由右侧形成的表达式，而符号则分别表示一个子表达式。

在这样的系统中，每条规则的选择都是为了使左侧与右侧等价，因此当左侧匹配一个子表达式时，对该子表达式进行从左到右的重写可以保持逻辑上的一致性和整个表达式的价值。算术术语重写系统可以用来计算自然数的算术运算。

为此，每个自然数必须被编码为一个术语。最简单的编码是Peano公理中使用的编码，基于常数0（零）和继任函数S。例如，数字0，1，2和3分别由术语0，S(0)，S(S(0))和S(S(0))表示。

然后，以下术语重写系统可以用来计算给定自然数的和与积。

在语言学中，短语结构规则，也称为重写规则，在一些生成语法系统中使用，作为生成语言的语法正确句子的手段。

这种规则通常采用以下形式A→X{displaystyle{rm{ArightarrowX}}，其中A是一个句法的例子。｝其中，A是一个句法类别标签，如名词短语或句子，X是这种标签或语素的序列，表示在生成句子的成分结构时，A可以被X所取代。