Simplifying Termination Proofs for Rewrite Systems by Preprocessing
Bernhard Gramlich
To appear at the 2nd International Conference on Principles and Practice of
Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000
Abstract
We prove some new results that simplify termination proofs for
non-overlapping term rewriting systems. The first one is a
refined modularity result (for not necessarily disjoint systems).
The second, more important one, gives conditions under which the
simplification of right-hand sides (using rules of the original
system) is a sound preprocessing step, in the sense that termination
of the original system is equivalent to termination of the simplified
system, and that the equational theory is preserved. The proofs are
based on some powerful structural properties known for non-overlapping
systems. Finally, we show how to extend these results, in particular,
to the case of conditional rewrite systems where we additionally treat
simplification of conditions of rules. The presented results provide
the theoretical basis for sound (and automatic) preprocessing steps
when proving termination of (possibly conditional) non-overlapping
rewrite systems and equational programs defined by such systems.