依赖对与依赖图在项重写系统终止性证明中的应用

### 依赖对与依赖图在项重写系统终止性证明中的应用 #### 1. 依赖对框架与AProVE工具的改进 在项重写系统（TRS）的终止性证明领域，依赖对框架是一种强大的技术。以一个具体例子来说，最终得到了DP问题\((\{(11)\}, R'_{sort})\)。为了从该DP问题中移除DP (11)，使用归纳定理证明器来证明\(R'_{sort} \gt_{Pol1} \models_{ind} del \gt_{Pol1}(max(co(x, xs)), co(x, xs)) = tt\)，即每个非空列表都包含其最大值。这里，定理12中的元组属性和非重叠性要求显然得到满足，并且所有规则相对于\(\geq_{Pol1}\)都是递减的。因此，归纳处理器得到了平凡问题\((\varnothing, R'_{sort})\)和问题\((DP(R'_{sort}), R'_{sort}) = (\{(2), ..., (10)\}, R'_{sort})\)。依赖图处理器将后一个问题转换为之前已经解决的问题\((P_i, R'_{sort})\)（\(1 \leq i \leq 4\)）。 AProVE工具引入了一种新的处理器，能够处理由于算法的归纳属性而终止的TRS。该处理器会自动提取这些属性并将其转化为猜想，然后传递给归纳定理证明器进行验证。为了获得强大的方法，证明这些猜想对于类型良好的项就足够了，即使所研究的原始TRS是无类型的。 AProVE工具的具体操作步骤如下： 1. 选择一个DP \(s \to t\)。 2. 搜索一个约简对\((\geq, \gt)\)，该约简对至少严格定向\(U(t)\)的一条规则（在强单调位置上）。 3. 测试\(t \gt = tt\)是否归纳有效。 与之前使用归纳定理证明器进行终止分析的方法相比，这种自动化方法可以搜索任意约简对，而不受限于固定的小集合顺序。搜索约简对的过程由强单调位置上必须有严格递减的可用规则这一事实引导。 为了展示该方法的强大之处，有一组19个典型的TRS，这些TRS的终止性证明需要归纳论证。该集合包含了几个计算经典算术算法的TRS，以及许多使用标准列表操作算法（如排序、反转等）的TRS。之前版本的AProVE在国际终止证明器竞赛中是最强大的项重写终止工具，但该版本以及竞赛中的所有其他工具在这些例子上都失败了。相比之下，新的AProVE版本在每个例子限时60秒的情况下，自动证明了其中16个的终止性。同时，新的AProVE版本在终止问题数据库的其余例子上与之前的版本一样成功。 #### 2. 依赖图处理器的改进 依赖对框架中的依赖图处理器是将终止问题分解为更小的子问题的重要处理器。它需要计算依赖图的过近似。在文献中，有几种这样的近似方法被提出，例如Arts和Giesl给出的基于抽象和统一的有效算法，Kusakari和Toyama使用的Huet和Lévy的ω - 归约概念来近似AC - 终止的依赖图，Middeldorp提倡使用树自动机技术并在后来通过考虑对称性改进了之前的近似方法，Giesl等人则紧密结合了抽象和统一，得到了一种特别适用于应用系统的改进方法。 本文通过结合前向闭包的右侧，对依赖图处理器进行了改进。与树自动机完成相结合，得到了一种高效的处理器，可用于替代终止证明器中常用的依赖图近似方法。 下面是依赖图处理器和SCC处理器的相关定义和示例： - **依赖图处理器**：将DP问题\((P, R, G)\)映射到\(\{(P, R, G \cap DG(P, R))\}\)。其中\(DG(P, R)\)是\(P\)和\(R\)的依赖图，其节点为\(P\)中的规则，从\(s \to t\)到\(u \to v\)存在一条弧当且仅当存在替换\(\sigma\)和\(\tau\)使得\(t\sigma \to^*_R u\tau\)。 - **示例**：考虑DP问题\((P, R, G)\)，其中\(R\)由重写规则\(f(g(x), y) \to g(h(x, y))\)和\(h(g(x), y) \to f(g(a), h(x, y))\)组成，\(P = DP(R)\)由以下规则组成： 1. \(F(g(x), y) \to H(x, y)\) 2. \(H(g(x), y) \to F(g(a), h(x, y))\) 3. \(H(g(x), y) \to H(x, y)\