A dependency pair framework for AVC-termination

Beatriz Alarcón, Salvador Lucas, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
Pages35-51
Number of pages17
DOIs
StatePublished - 2010
Event8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010 - Paphos, Cyprus
Duration: Mar 20 2010Mar 21 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6381 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
CountryCyprus
CityPaphos
Period3/20/103/21/10

Keywords

  • dependency pairs
  • equational rewriting
  • termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A dependency pair framework for AVC-termination'. Together they form a unique fingerprint.

Cite this