Sciweavers

AAECC
2005
Springer

The size-change principle and dependency pairs for termination of term rewriting

13 years 3 months ago
The size-change principle and dependency pairs for termination of term rewriting
Abstract In [24], a new size-change principle was 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 NP-complete. To benefit from their respective advantages, we show how to combine the s...
René Thiemann, Jürgen Giesl
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where AAECC
Authors René Thiemann, Jürgen Giesl
Comments (0)