The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl and Rene Thiemann
Size-Change Termination for Term Rewriting
2003-02
Abstract:
In [Lee, Jones & Ben-Amram, 2001], 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 orderings 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.
In order to benefit from their respective advantages,
we show how to combine the size-change principle
with classical orderings 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.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/
