A Dependency Pair Framework for AvC-Termination

Abstract

The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. One of the most important techniques for proving termination over a wide range of variants of rewriting (strategies) is the dependency pair approach. Several works have tried to adapt it to rewriting modulo associative and commutative (AC) equational theories, and even to more general theories. However, as we discuss in this paper, no appropriate notion of minimality (and minimal chain of dependency pairs) which is well-suited to develop a dependency pair framework has been proposed to date. In this paper we carefully analyze the structure of in nite rewrite sequences for rewrite theories whose equational part is any combination of associativity and/or commutativity axioms, which we call AvC-rewrite theories. Our analysis leads to a more accurate and optimized notion of dependency pairs through the new notion of stably minimal term. We then develop a suitable dependency pair framework for proving termination of AvC-rewrite theories.