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


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.