Document Open Access Logo

Matrix Interpretations on Polyhedral Domains

Author Johannes Waldmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2015.318.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • termination of term rewriting
  • matrix interpretations
  • constraint programming
  • linear inequalities

Metrics

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

Abstract

We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities. Admissibility of such a restriction is shown by certificates whose validity can be expressed as a constraint program. This refinement is orthogonal to other features of matrix interpretations (complexity bounds, dependency pairs), but can be used to improve complexity bounds,  and we discuss its relation with the usable rules criterion. We present an implementation and experiments.

Cite As Get BibTex

Johannes Waldmann. Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 318-333, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.318

Author Details

Johannes Waldmann

References

  1. Sergei I. Adian. Upper bound on the derivational complexity in some word rewriting system. Doklady Mathematics, 80(2):679-683, 2009. Google Scholar
  2. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theor. Comput. Sci., 236(1-2):133-178, 2000. Google Scholar
  3. Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. CoRR, abs/cs/0612085, 2006. Google Scholar
  4. Clark Barrett, Aaron Stump, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). http://smt-lib.org/, 2010-.
  5. Alexander Bau, Markus Lohrey, Eric Nöth, and Johannes Waldmann. Compression of rewriting systems for termination analysis. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, volume 21 of LIPIcs, pages 97-112. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  6. Armin Biere and Robert Brummayer. Boolector. http://fmv.jku.at/boolector/, 2008-.
  7. Ahlem Ben Cherifa and Pierre Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program., 9(2):137-159, 1987. Google Scholar
  8. Michael Codish, Yoav Fekete, Carsten Fuhs, Jürgen Giesl, and Johannes Waldmann. Exotic semi-ring constraints. In Pascal Fontaine and Amit Goel, editors, 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012, volume 20 of EPiC Series, pages 88-97. EasyChair, 2012. Google Scholar
  9. Mike Develin and Josephine Yu. Tropical polytopes and cellular resolutions. Experimental Mathematics, 16(3):277-291, 2007. Google Scholar
  10. Niklas Een and Niklas Sörensson. Minisat. http://minisat.se/, 2003-. Google Scholar
  11. Jörg Endrullis, Johannes Waldmann, and Hans Zantema. Matrix interpretations for proving termination of term rewriting. J. Autom. Reasoning, 40(2-3):195-220, 2008. Google Scholar
  12. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Proving Termination of Programs Automatically with AProVE. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, volume 8562 of Lecture Notes in Computer Science, pages 184-191. Springer, 2014. Google Scholar
  13. Dieter Hofbauer and Johannes Waldmann. Termination of string rewriting with matrix interpretations. In Frank Pfenning, editor, Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, volume 4098 of Lecture Notes in Computer Science, pages 328-342. Springer, 2006. Google Scholar
  14. Adam Koprowski and Johannes Waldmann. Max/plus tree automata for termination of term rewriting. Acta Cybern., 19(2):357-392, 2009. Google Scholar
  15. Martin Korp and Harald Zankl. Cat (complexity and termination). http://cl-informatik.uibk.ac.at/software/cat/, 2008-.
  16. Salvador Lucas. mu-term: A tool for proving termination of context-sensitive rewriting. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 200-209. Springer, 2004. Google Scholar
  17. Salvador Lucas and José Meseguer. Models for logics and conditional constraints in automated proofs of termination. In Gonzalo A. Aranda-Corral, Jacques Calmet, and Francisco J. Martín-Mateos, editors, Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Seville, Spain, December 11-13, 2014. Proceedings, volume 8884 of Lecture Notes in Computer Science, pages 9-20. Springer, 2014. Google Scholar
  18. Georg Moser, Andreas Schnabl, and Johannes Waldmann. Complexity analysis of term rewriting based on matrix and context dependent interpretations. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India, volume 2 of LIPIcs, pages 304-315. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. Google Scholar
  19. Friedrich Neurauter and Aart Middeldorp. Revisiting matrix interpretations for proving termination of term rewriting. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 251-266. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  20. Friedrich Neurauter, Harald Zankl, and Aart Middeldorp. Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 550-564. Springer, 2010. Google Scholar
  21. Albert Rubio, Claude Marche, Hans Zantema, and René Thiemann. Termination problems data base (tpdb). http://termination-portal.org/wiki/TPDB, 2003-.
  22. Christian Sternagel and Aart Middeldorp. Root-labeling. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 336-350. Springer, 2008. Google Scholar
  23. Christian Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl. CeTA - A Tool for Certified Termination Analysis. CoRR, abs/1208.1591, 2012. Google Scholar
  24. Aaron Stump, Tyler Jensen, and Cesare Tinelli. Starexec. https://www.starexec.org/, 2013-.
  25. Sergej N. Tschernikow. Lineare Ungleichungen. Berlin, 1971. Google Scholar
  26. Aard Varks. Farkas' lemma. http://aardvarks.bandcamp.com/album/farkas-lemma, 1996.
  27. Stefan von der Krone. Stareexec-presenter. https://github.com/stefanvonderkrone/star-exec-presenter, 2014-.
  28. Johannes Waldmann. Polynomially bounded matrix interpretations. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK, volume 6 of LIPIcs, pages 357-372. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  29. Johannes Waldmann, Alexander Bau, and Eric Noeth. Matchbox termination prover. http://github.com/jwaldmann/matchbox/, 2014-. Google Scholar
  30. Hans Zantema. Termination of term rewriting by interpretation. In Michaël Rusinowitch and Jean-Luc Remy, editors, Conditional Term Rewriting Systems, Third International Workshop, CTRS-92, Pont-à-Mousson, France, July 8-10, 1992, Proceedings, volume 656 of Lecture Notes in Computer Science, pages 155-167. Springer, 1992. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact