A path ordering for proving termination of AC rewrite systems

We describe a method that extends the lexicographic recursive path ordering of Dershowitz and Kamin and Levy for proving termination of associative-commutative (AC) rewrite systems. Instead of comparing the arguments of an AC-operator using the multiset extension, wepartition them into disjoint subsets and use each subset only once for comparison. To preserve transitivity, we introduce two techniques —pseudocopying andelevating of arguments of an AC operator. This method imposesno restrictions at all on the underlying precedence relation on function symbols. It can therefore prove termination of a much more extensive class of AC rewrite systems than can previous methods, such as associative path ordering, that restrict AC operators to be minimal or subminimal in precedence. A number of examples illustrating the power of the approach are discussed. The method has been implemented inRRL, Rewrite Rule Laboratory, a theorem-proving environment based on rewrite techniques and completion.A preliminary version appears in Proc. of10th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India (1990).Partially supported by the National Science Foundation Grant no. CCR-8906678.Partially supported by the National Science Foundation Grant no. CCR-9009755Partially supported by the National Science Foundation under Grants CCR-9202838 and CCR-9357851.