Critical Pair

设 和 是项重写系统的两个规则，并假设这些规则没有共同的变量。如果它们有，则重命名变量。如果 是 的子项（或项 本身），使得它不是变量，并且对 是可合一的，具有最通用的合一器 ，则 和通过用 替换 中的 而得到的结果被称为临界对。

一个项重写系统的所有临界对都是可连接的（即可简化为相同的表达式）这一事实，意味着该系统是局部合流的。

例如，如果 和 ，则 和 将形成一个临界对，因为它们都可以从 导出。

请注意，临界对有可能由一个规则产生，以两种不同的方式使用。例如，在字符串重写中"AA" -> "B"，临界对 ("BA", "AB") 是将一个规则应用于"AAA"以两种不同方式的结果。