Document Open Access Logo

Certification of Complexity Proofs using CeTA

Authors Martin Avanzini, Christian Sternagel, René Thiemann

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.23.pdf
  • Filesize: 0.59 MB
  • 17 pages

Document Identifiers

Author Details

Martin Avanzini
Christian Sternagel
René Thiemann

Cite AsGet BibTex

Martin Avanzini, Christian Sternagel, and René Thiemann. Certification of Complexity Proofs using CeTA. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 23-39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.23

Abstract

Nowadays certification is widely employed by automated termination tools for term rewriting, where certifiers support most available techniques. In complexity analysis, the situation is quite different. Although tools support certification in principle, current certifiers implement only the most basic technique, namely, suitably tamed versions of reduction orders. As a consequence, only a small fraction of the proofs generated by state-of-the-art complexity tools can be certified. To improve upon this situation, we formalized a framework for the certification of modular complexity proofs and incorporated it into CeTA. We report on this extension and present the newly supported techniques (match-bounds, weak dependency pairs, dependency tuples, usable rules, and usable replacement maps), resulting in a significant increase in the number of certifiable complexity proofs. During our work we detected conflicts in theoretical results as well as bugs in existing complexity tools.
Keywords
  • complexity analysis
  • certification
  • match-bounds
  • weak dependency pairs
  • dependency tuples
  • usable rules
  • usable replacement maps

Metrics

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

References

  1. Martin Avanzini. Verifying Polytime Computability Automatically. PhD thesis, University of Innsbruck, 2013. URL: http://cl-informatik.uibk.ac.at/~zini/publications/diss.pdf.
  2. Martin Avanzini and Georg Moser. A combination framework for complexity. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of Leibniz International Proceedings in Informatics, pages 55-70, 2013. \doi10.4230/LIPIcs.RTA.2013.55. Google Scholar
  3. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  4. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979. \doi10.1145/359138.359142. Google Scholar
  5. Bertram Felgenhauer and René Thiemann. Reachability analysis with state-compatible automata. In Proc. 8th International Conference on Language and Automata Theory and Applications, volume 8370 of Lecture Notes in Computer Science, pages 347-359, 2014. \doi10.1007/978-3-319-04921-2_28. Google Scholar
  6. Guillaume Feuillade, Thomas Genet, and Valérie Viet Triem Tong. Reachability analysis over term rewriting systems. Journal of Automated Reasoning, 33:341-383, 2004. \doi10.1007/s10817-004-6246-0. Google Scholar
  7. Alfons Geser, Dieter Hofbauer, Johannes Waldmann, and Hans Zantema. On tree automata that certify termination of left-linear term rewriting systems. Information and Computation, 205(4):512-534, 2007. \doi10.1016/j.ic.2006.08.007. Google Scholar
  8. 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 Proc. 7th International Joint Conference on Automated Reasoning, volume 8562 of Lecture Notes in Computer Science, pages 184-191, 2014. \doi10.1007/978-3-319-08587-6_13. Google Scholar
  9. Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Proc. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 301-331, 2005. \doi10.1007/978-3-540-32275-7_21. Google Scholar
  10. Nao Hirokawa and Georg Moser. Automated complexity analysis based on the dependency pair method. In Proc. 4th International Joint Conference on Automated Reasoning, volume 5195 of Lecture Notes in Computer Science, pages 364-379, 2008. \doi10.1007/978-3-540-71070-7_32. Google Scholar
  11. Nao Hirokawa and Georg Moser. Automated complexity analysis based on context-sensitive rewriting. In Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science, pages 257-271, 2014. \doi10.1007/978-3-319-08918-8_18. Google Scholar
  12. Martin Korp and Aart Middeldorp. Match-bounds revisited. Information and Computation, 207(11):1259-1283, 2009. \doi10.1016/j.ic.2009.02.010. Google Scholar
  13. Georg Moser and Andreas Schnabl. The derivational complexity induced by the dependency pair method. Logical Methods in Computer Science, 7(3:1):1-38, 2011. \doi10.2168/LMCS-7(3:1)2011. Google Scholar
  14. Tobias Nipkow, Lawrence C. Paulson, and Makarius Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. \doi10.1007/3-540-45949-9. Google Scholar
  15. Lars Noschinski, Fabian Emmes, and Jürgen Giesl. Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning, 51(1):27-56, 2013. \doi10.1007/s10817-013-9277-6. Google Scholar
  16. Christian Sternagel and René Thiemann. Certified subterm criterion and certified usable rules. In Proc. 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics, pages 325-340, 2010. \doi10.4230/LIPIcs.RTA.2010.325. Google Scholar
  17. Christian Sternagel and René Thiemann. Formalizing monotone algebras for certification of termination and complexity proofs. In Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science, pages 441-455, 2014. \doi10.1007/978-3-319-08918-8_30. Google Scholar
  18. René Thiemann and Christian Sternagel. Certification of termination proofs using Cęrn-0.2exeęrn-0.5exTęrn-0.5exA. In Proc. 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 452-468, 2009. \doi10.1007/978-3-642-03359-9_31. Google Scholar
  19. Harald Zankl and Martin Korp. Modular complexity analysis via relative complexity. In Proc. 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics, pages 385-400, 2010. \doi10.4230/LIPIcs.RTA.2010.385. Google Scholar
  20. Harald Zankl and Martin Korp. Modular complexity analysis for term rewriting. Logical Methods in Computer Science, 10(1:19):1-34, 2014. \doi10.2168/LMCS-10(1:19)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