A Dependency Pair Framework for A∨C-Termination

Authors

Beatriz Alarcón, Salvador Lucas, and José Meseguer.

Abstract

The development of powerful techniques for proving termination of rewriting modulo a set of equations is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, OBJ, etc. One of the most important techniques for proving termination over a wide range of variants of rewriting (strategies) is the dependency pairs 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 pairs framework has been proposed to date. The dependency pairs framework is a recent formulation of the dependency pairs approach which is specially well-suited for mechanizing proofs of termination and which, in the last years, has heavily increased the power of automatic termination provers. In this paper we carefully analyze the structure of infinite rewrite sequences for rewrite theories whose equational part is a (free) combination of associative and commutative axioms which we call A∨C-rewrite theories. Our analysis leads to a more accurate and optimized notion of dependency pairs through the new notion of stable minimal term. Then, we have developed a suitable dependency pairs framework for proving termination of A∨C-rewrite theories.

Publication

In Peter Ölveczky, editor,
Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA 2010,
LNCS 6381:36-52, Springer-Verlag, Berlin, 2010.