| Summary: | We present techniques to prove termination of cycle rewriting, that is,
string rewriting on cycles, which are strings in which the start and end are
connected. Our main technique is to transform cycle rewriting into string
rewriting and then apply state of the art techniques to prove termination of
the string rewrite system. We present three such transformations, and prove for
all of them that they are sound and complete. In this way not only termination
of string rewriting of the transformed system implies termination of the
original cycle rewrite system, a similar conclusion can be drawn for
non-termination. Apart from this transformational approach, we present a
uniform framework of matrix interpretations, covering most of the earlier
approaches to automatically proving termination of cycle rewriting. All our
techniques serve both for proving termination and relative termination. We
present several experiments showing the power of our techniques.
|
|---|