TY - GEN
T1 - A dependency pair framework for AVC-termination
AU - Alarcón, Beatriz
AU - Lucas, Salvador
AU - Meseguer, José
N1 - Funding Information:
Partially supported by EU (FEDER) and MICINN grant TIN 2007-68093-C02-02. José Meseguer has been partially supported by NSF Grants CCF-0905584, CNS-07-16038, and CNS-08-34709. Beatriz Alarcón was partially supported by the Spanish MEC/MICINN under FPU grant AP2005-3399.
PY - 2010
Y1 - 2010
N2 - 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 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 infinite rewrite sequences for rewrite theories whose equational part is a (free) combination of associative and commutative 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. Then, we have developed a suitable dependency pair framework for proving termination of AVC-rewrite theories.
AB - 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 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 infinite rewrite sequences for rewrite theories whose equational part is a (free) combination of associative and commutative 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. Then, we have developed a suitable dependency pair framework for proving termination of AVC-rewrite theories.
KW - dependency pairs
KW - equational rewriting
KW - termination
UR - http://www.scopus.com/inward/record.url?scp=78349300173&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78349300173&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-16310-4_4
DO - 10.1007/978-3-642-16310-4_4
M3 - Conference contribution
AN - SCOPUS:78349300173
SN - 3642163092
SN - 9783642163098
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 35
EP - 51
BT - Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
T2 - 8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
Y2 - 20 March 2010 through 21 March 2010
ER -