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

@inproceedings{AYCSRTKK2016-CSL,
  author    = "Akihisa Yamada and Christian Sternagel and Ren{\'e} Thiemann
               and Keiichirou Kusakari",
  title     = "{AC} Dependency Pairs Revisited",
  booktitle = "Proceedings of the 25th EACSL Annual Conference on Computer
               Science Logic (CSL 2016)",
  pages     = "8:1--8:16",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 62,
  year      = 2016,
  editor    = "Jean-Marc Talbot and Laurent Regnier",
  publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  doi       = "http://dx.doi.org/10.4230/LIPIcs.CSL.2016.8",
}