License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.8
URN: urn:nbn:de:0030-drops-65488
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6548/
Go to the corresponding LIPIcs Volume Portal

Yamada, Akihisa ; Sternagel, Christian ; Thiemann, René ; Kusakari, Keiichirou

AC Dependency Pairs Revisited

pdf-format:
LIPIcs-CSL-2016-8.pdf (0.5 MB)

Abstract

Rewriting modulo AC, i.e., associativity and/or commutativity of certain symbols, is among the most frequently used extensions of term rewriting by equational theories. In this paper we present a generalization of the dependency pair framework for termination analysis to rewriting modulo AC. It subsumes existing variants of AC dependency pairs, admits standard dependency graph analyses, and in particular enjoys the minimality property in the standard sense. As a direct benefit, important termination techniques are easily extended; we describe usable rules and the subterm criterion for AC termination, which properly generalize the non-AC versions.

We also perform these extensions within IsaFoR - the Isabelle formalization of rewriting - and thereby provide the first formalization of AC dependency pairs. Consequently, our certifier CeTA now supports checking proofs of AC termination.

BibTeX - Entry

@InProceedings{yamada_et_al:LIPIcs:2016:6548,
  author =	{Akihisa Yamada and Christian Sternagel and Ren{\'e} Thiemann and Keiichirou Kusakari},
  title =	{{AC Dependency Pairs Revisited}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Jean-Marc Talbot and Laurent Regnier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6548},
  URN =		{urn:nbn:de:0030-drops-65488},
  doi =		{10.4230/LIPIcs.CSL.2016.8},
  annote =	{Keywords: Equational Rewriting, Termination, Dependency Pairs, Certification}
}

Keywords: Equational Rewriting, Termination, Dependency Pairs, Certification
Collection: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Issue Date: 2016
Date of publication: 29.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI