Document Open Access Logo

AC Dependency Pairs Revisited

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

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.8.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Akihisa Yamada
Christian Sternagel
René Thiemann
Keiichirou Kusakari

Cite AsGet BibTex

Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari. AC Dependency Pairs Revisited. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.8

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.
Keywords
  • Equational Rewriting
  • Termination
  • Dependency Pairs
  • Certification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. B. Alarcón, S. Lucas, and J. Meseguer. A dependency pair framework for A∨C-termination. In WRLA 2010, volume 6381 of LNCS, pages 36-52, 2010. Google Scholar
  2. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theor. Compt. Sci. , 236(1-2):133-178, 2000. Google Scholar
  3. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  4. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979. Google Scholar
  5. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plucker, P. Schneider-Kamp, T. Stroder, S. Swiderski, and R. Thiemann. Proving termination of programs automatically with AProVE. In IJCAR 2014, LNAI 8562, pages 184-191, 2014. Google Scholar
  6. J. Giesl and D. Kapur. Dependency pairs for equational rewriting. In RTA 2001, volume 2051 of LNCS, pages 93-107, 2001. Google Scholar
  7. J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In LPAR 2004, volume 3452 of LNAI, pages 75-90, 2004. Google Scholar
  8. N. Hirokawa and A. Middeldorp. Automating the dependency pair method. Inf. Comput. , 199(1,2):172-199, 2005. Google Scholar
  9. N. Hirokawa and A. Middeldorp. Tyrolean Termination Tool: Techniques and features. Inf. Comput. , 205(4):474-511, 2007. Google Scholar
  10. J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155-1194, 1986. Google Scholar
  11. K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. Appl. Algebr. Eng. Comm. Compt. , 18(5):407-431, 2007. Google Scholar
  12. K. Kusakari and Y. Toyama. On proving AC-termination by AC-dependency pairs. IEICE T. Inf. Syst. , E84-D(5):439-447, 2001. Google Scholar
  13. C. Marché and X. Urbain. Termination of associative-commutative rewriting by dependency pairs. In RTA 1998, volume 1379 of LNCS, pages 241-255, 1998. Google Scholar
  14. C. Marché and X. Urbain. Modular and incremental proofs of AC-termination. J. Symb. Comput. , 38(1):873-897, 2004. Google Scholar
  15. T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  16. G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233-264, 1981. Google Scholar
  17. A. Rubio. A fully syntactic AC-RPO. Inf. Comput. , 178(2):515-533, 2002. Google Scholar
  18. C. Sternagel and R. Thiemann. Certified subterm criterion and certified usable rules. In RTA 2010, volume 6 of LIPIcs, pages 325-340, 2010. Google Scholar
  19. C. Sternagel and R. Thiemann. A relative dependency pair framework. In WST 2012, pages 79-83, 2012. Google Scholar
  20. Christian Sternagel and Rene Thiemann. The certification problem format. In UITP 2014, volume 167 of EPTCS, pages 61-72, 2014. Google Scholar
  21. TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  22. R. Thiemann, G. Allais, and J. Nagele. On the formalization of termination techniques based on multiset orderings. In RTA 2012, volume 15 of LIPIcs, pages 339-354, 2012. Google Scholar
  23. R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In TPHOLs 2009, volume 5674 of LNCS, pages 452-468, 2009. Google Scholar
  24. A. Yamada, K. Kusakari, and T. Sakabe. Nagoya Termination Tool. In RTA-TLCA 2014, volume 8560 of LNCS, pages 466-475, 2014. Google Scholar
  25. A. Yamada, S. Winkler, N. Hirokawa, and A. Middeldorp. AC-KBO revisited. Theor. Pract. Log. Prog. , 16(2):163-188, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact