The size-change principle and dependency pairs for termination of term rewriting
The size-change principle and dependency pairs for termination of term rewriting
复制标题
终止术语重写的大小变化原理和依赖对
DOI：
10.1007/s00200-005-0179-7
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Giesl
中科院分区：
文献类型：
--
作者：
René Thiemann;J. Giesl
在b[24]中，提出了一种新闻大小变化原理来自动验证功能程序的终止。为了证明任意项重写系统的终止和最内层终止，我们扩展了这一原理。此外，我们将这种方法与现有的trs终止分析技术（如递归路径顺序或依赖对）进行了比较。事实证明，对于许多可以通过标准重写技术处理的示例，大小更改原则本身是失败的，但是也有一些trs，它成功了，而现有的重写技术失败了。此外，我们还比较了各自方法的复杂性。为此，我们为依赖对方法开发了第一个复杂性分析。虽然大小变化原则是pspace完全的，但我们证明依赖对方法（与经典路径顺序结合使用）只是-完全的。为了从它们各自的优势中获益，我们将展示如何将大小变化原则与经典顺序和依赖对结合起来。通过这种方法，我们获得了一种比以前的方法更强大的自动终止证明的新方法。我们还表明，与依赖对的组合不会增加大小变化原则的复杂性，也就是说，组合的方法仍然是pspace完备的。
In [24], a newsize-change principlewas proposed to verify termination of functional programs automatically. We extend this principle in order to prove termination and innermost termination of arbitrary term rewrite systems (TRSs). Moreover, we compare this approach with existing techniques for termination analysis of TRSs (such as recursive path orders or dependency pairs). It turns out that the size-change principle on its own fails for many examples that can be handled by standard techniques for rewriting, but there are also TRSs where it succeeds whereas existing rewriting techniques fail. Moreover, we also compare the complexity of the respective methods. To this end, we develop the first complexity analysis for the dependency pair approach. While the size-change principle is PSPACE-complete, we prove that the dependency pair approach (in combination with classical path orders) is only -complete. To benefit from their respective advantages, we show how to combine the size-change principle with classical orders and with dependency pairs. In this way, we obtain a new approach for automated termination proofs of TRSs which is more powerful than previous approaches. We also show that the combination with dependency pairs does not increase the complexity of the size-change principle, i.e., the combined approach is still PSPACE-complete.