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...

• Type: Journal
• Year: 2005
• Where: AAECC
• Authors: René Thiemann, Jürgen Giesl
• Keywords: AAECC 2005, Algorithms, Dependency Pair Approach, Dependency Pairs, Size-change Principle