定理证明器构建与项重写系统终止分析

# 定理证明器构建与项重写系统终止分析 ## 1. 结合律 - 交换律（AC）统一的挑战与应对 在理论研究中，结合律 - 交换律（AC）函数频繁出现，但普通的定理证明器若不进行特殊处理，很难对其进行有效处理。即便用 AC 统一替代普通统一这一概念上简单的想法，也会给定理证明器带来诸多影响，需要大量的理论和实现工作。 ### 1.1 AC 统一算法的发展 AC 统一算法于 1975 年首次被开发出来，但直到 1984 年才被证明是完备的。该算法十分有用，例如在证明所有罗宾斯代数都是布尔代数的过程中发挥了重要作用。 ### 1.2 充分利用 AC 统一算法的条件 仅仅开发和实现特殊的统一算法并不足以充分利用它。定理证明器的架构必须支持统一算法产生多个统一器，同时能够高效地对 AC 项进行索引。例如，存在一种复杂且尚未实现的 AC 区分树方法，对于 Snark 而言，拥有与 AC 兼容的路径索引扩展也会有所帮助。 ### 1.3 AC 函数的重写和调解 使用 AC 函数进行重写和调解时，需要扩展重写规则。例如，对于重写规则 \(f(s_1, \ldots, s_n) \to t\)（其中 \(f\) 是 AC 函数），通常还需要一个扩展重写规则 \(f(s_1, \ldots, s_n, x) \to f(t, x)\)。以 \(f(g(x), x) \to e\) 为例，它不适用于 \(f(g(a), a, b, c)\)，但扩展后的重写规则则适用。 ### 1.4 项排序与 AC 函数的兼容性 项排序对于有效的等式推理至关重要，但常用的项排序与 AC 函数不兼容。目前已经开发出了与 AC 兼容的项排序，但实现起来比基于其的排序要困难得多。例如，Snark 实现了递归路径排序的 AC 兼容扩展，但在实际应用中，其指数级的行为有时会成为严重问题。而 Knuth - Bendix 排序的 AC 兼容扩展据称可以克服这一缺陷。由于递归路径排序和 Knuth - Bendix 排序各有优势，因此为用户提供选择很重要，但这也增加了对 AC 函数进行特殊处理的成本。 ### 1.5 支持包和集合数据类型 在应用中，支持包（无序列表）或集合数据类型可能比 AC 本身更重要。有人可能会尝试使用 AC 统一处理包，使用 AC1 统一处理集合，但这种方法存在问题。例如，对于包 \(bag(x, y, z)\)，它是 \(bag(x, bag(y, z))\) 的扁平化形式，不能很好地表示包含元素 \(x\)、\(y\) 和 \(z\) 的三元包，因为它不允许包的正确嵌套。将包或集合的理论建立在并集操作上更为合理，例如以下等式： \[ \begin{align*} bagunion(x, bagunion(y, z)) &= bagunion(bagunion(x, y), z)\\ bagunion(x, y) &= bagunion(y, x) \end{align*} \] 但 AC 包并集函数的参数应该是包，而不是元素。可以通过将元素包装在单元素包构造函数中来解决这个问题，但如果主要关注包及其元素而非它们的并集，这种方法会显得繁琐。 另一种更有吸引力的方法是使用 \(bagcons\) 和 \(emptybag\) 来表示包，例如 \(bagcons(x, bagcons(y, bagcons(z, emptybag)))\) 表示包含元素 \(x\)、\(y\) 和 \(z\) 的三元包。\(bagcons\) 函数具有 \(bagcons(x, bagcons(y, z)) = bagcons(y, bagcons(x, z))\) 的性质，并且和 \(cons\) 一样，\(bagcons\) 可以将变量作为其第二个参数来表示包含未指定额外元素的包。这种表示方法为包提供了有用的操作，并且在索引和排序方面比 AC 函数更容易处理。集合的处理方式与包类似，但除非能假设或确定元素的不等性，否则会带来额外的问题。例如，如果 \(x = y\)，则 \(setcons(x, setcons(y, emptyset)) = setcons(y, emptyset)\)。目前，Snark 仅实现了包的统一。 ## 2. 定理证明器的现状与挑战 ### 2.1 现有定理证明器的特点 一些定理证明器，如 Snark 的浓缩分离问题编码器和 Pttp 的模型消除过程实现，具有完备性、速度快、易于实现等优点，有时还能取得惊人的成功，但也存在很大的局限性。归结和调解提供了广泛的选项和扩展机会，以支持诸如演绎问答等应用所需的推理。然而，一些基本困难，如调解和支持集的不兼容性，以及需要根据项和公式的匹配方式调整索引，使得保持完备性和性能极具挑战性。简单的添加，如 AC 统一，可能需要对定理证明器的索引、重写和项排序进行大规模的更改。 ### 2.2 定理证明器实现的困难 定理证明器的实现比预期的要困难。文献中的算法通常以简洁的数学方式描述，以便于证明正确性，而不是为高效实现提供指导。例如，标准的词法递归路径排序的呈现方式会导致低效的指数级实现。此外，一些算法在教学上追求简单，而忽视了实现的现实情况，例如将有序归结和调解呈现为好像等式是唯一的关系。 ### 2.3 代码实现与组件复用 使用高级语言（如 Lisp、ML 或 Python）编写的可执行代码可以像伪代码一样有效地传达算法，并且更不容易产生歧义或误解，还能为测试新实现的正确性和性能提供参考。尽管有定理证明器的代码可用，但组件的复用情况却很少。定理证明器有许多组件，需要大量的理论和实现工作，而且其中许多组件相互依赖、紧密耦合，必须协同开发。当任务更容易分离时，如 CNF 转换、相关性测试、提取排序理论和决定使用哪些推理规则，在许多定理证明器中独立实现这些任务往往不是最优的。 ## 3. 项重写系统（TRS）终止分析的挑战 ### 3.1 现有技术的局限性 目前有许多强大的技术和工具可以自动证明项重写系统（TRS）的终止性，并且这些工具在分析实际编程语言（如 Haskell 和 Prolog）的终止性方面也非常成功。每年都会举办国际终止证明器竞赛，让这些工具在大量的 TRS 数据集上进行竞争。然而，仍然存在一些自然算法，现有工具无法证明其终止性。 ### 3.2 示例：排序算法的 TRS 考虑以下 TRS \(R_{sort}\)： ```plaintext ge(x, 0) → true eq(0, 0) → true ge(0, s(y)) → false eq(s(x), 0) → false ge(s(x), s(y)) → ge(x, y) eq(0, s(y)) → false eq(s(x), s(y)) → eq(x, y) max(nil) → 0 max(co(x, nil)) → x if1(true, x, y, xs) → max(co(x, xs)) max(co(x, co ```