Document Open Access Logo

Certifying the Weighted Path Order (Invited Talk)

Authors René Thiemann , Jonas Schöpf , Christian Sternagel , Akihisa Yamada

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.4.pdf
  • Filesize: 0.54 MB
  • 20 pages

Document Identifiers

Author Details

René Thiemann
  • University of Innsbruck, Austria
Jonas Schöpf
  • University of Innsbruck, Austria
Christian Sternagel
  • DVT, Innsbruck, Austria
Akihisa Yamada
  • National Institute of Advanced Industrial Science and Technology, Tokyo, Japan

Funding

René Thiemann was supported by the Austrian Science Fund (FWF) project Y757. Jonas Schöpf and Christian Sternagel were supported by FWF project P27502. A part of Akihisa Yamada’s contribution was made while he was working in University of Innsbruck under support by FWF projects Y757 and P27502.

Acknowledgements

We thank Sarah Winkler for her assistance and discussions on IsaFoR, TTT2 and WPO.

Cite AsGet BibTex

René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada. Certifying the Weighted Path Order (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.4

Abstract

The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
Keywords
  • certification
  • Isabelle/HOL
  • reduction order
  • termination analysis

Metrics

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

Supplementary Materials

References

  1. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theor. Comput. Sci., 236(1-2):133-178, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  2. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  3. Clemens Ballarin. Locales: A module system for mathematical theories. J. Autom. Reasoning, 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  4. Amir M. Ben-Amram and Michael Codish. A SAT-based approach to size change termination with global ranking functions. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 218-232. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_16.
  5. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.
  6. Frédéric Blanqui and Adam Koprowski. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci., 21(4):827-859, 2011. URL: https://doi.org/10.1017/S0960129511000120.
  7. Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, and René Thiemann. Verifying a solver for linear mixed integer arithmetic in Isabelle/HOL. In NASA Formal Methods Symposium, 12th International Conference, Proceedings, 2020. To appear. Google Scholar
  8. Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, and Akihisa Yamada. Certifying safety and termination proofs for integer transition systems. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 454-471. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_28.
  9. Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, and René Thiemann. SAT solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reasoning, 49(1):53-93, 2012. URL: https://doi.org/10.1007/s10817-010-9211-0.
  10. Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007, Proceedings, volume 4720 of Lecture Notes in Computer Science, pages 148-162. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74621-8_10.
  11. Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated certified proofs with CiME3. 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 21-30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.RTA.2011.21.
  12. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  13. Nachum Dershowitz. Orderings for term-rewriting systems. Theor. Comput. Sci., 17:279-301, 1982. URL: https://doi.org/10.1016/0304-3975(82)90026-3.
  14. Nachum Dershowitz. Termination of rewriting. J. Symb. Comput., 3(1/2):69-116, 1987. URL: https://doi.org/10.1016/S0747-7171(87)80022-6.
  15. 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. URL: https://doi.org/10.1007/s10817-007-9087-9.
  16. Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl. Maximal termination. 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 110-125. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70590-1_8.
  17. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Analyzing program termination and complexity automatically with aprove. J. Autom. Reasoning, 58(1):3-31, 2017. URL: https://doi.org/10.1007/s10817-016-9388-y.
  18. Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. The Termination and Complexity Competition. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science, pages 156-166. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17502-3_10.
  19. Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, volume 3452 of Lecture Notes in Computer Science, pages 301-331. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-32275-7_21.
  20. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. J. Autom. Reasoning, 37(3):155-203, 2006. URL: https://doi.org/10.1007/s10817-006-9057-7.
  21. Nao Hirokawa and Aart Middeldorp. Tsukuba Termination Tool. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, volume 2706 of Lecture Notes in Computer Science, pages 311-320. Springer, 2003. URL: https://doi.org/10.1007/3-540-44881-0_22.
  22. Nao Hirokawa and Aart Middeldorp. Polynomial interpretations with negative coefficients. In Bruno Buchberger and John A. Campbell, editors, Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004, Proceedings, volume 3249 of Lecture Notes in Computer Science, pages 185-198. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30210-0_16.
  23. Nao Hirokawa, Aart Middeldorp, and Harald Zankl. Uncurrying for termination and complexity. J. Autom. Reasoning, 50(3):279-315, 2013. URL: https://doi.org/10.1007/s10817-012-9248-3.
  24. Jan Jakubuv and Cezary Kaliszyk. Towards a unified ordering for superposition-based automated reasoning. In James H. Davenport, Manuel Kauers, George Labahn, and Josef Urban, editors, Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings, volume 10931 of Lecture Notes in Computer Science, pages 245-254. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96418-8_29.
  25. Sam Kamin and Jean-Jacques Lévy. Two generalizations of the recursive path ordering, 1980. Unpublished note. Google Scholar
  26. Donald E. Knuth and Peter Bendix. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, New York, 1970. URL: https://doi.org/10.1016/B978-0-08-012975-4.50028-X.
  27. Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In Ralf Treinen, editor, Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, volume 5595 of Lecture Notes in Computer Science, pages 295-304. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_21.
  28. Alexander Krauss. Recursive definitions of monadic functions. In Ekaterina Komendantskaya, Ana Bove, and Milad Niqui, editors, Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010, volume 5 of EPiC Series, pages 1-13. EasyChair, 2010. URL: http://www.easychair.org/publications/paper/52847.
  29. Keiichirou Kusakari, Masaki Nakamura, and Yoshihito Toyama. Argument filtering transformation. In Gopalan Nadathur, editor, Principles and Practice of Declarative Programming, International Conference PPDP'99, Paris, France, September 29 - October 1, 1999, Proceedings, volume 1702 of Lecture Notes in Computer Science, pages 47-61. Springer, 1999. URL: https://doi.org/10.1007/10704567_3.
  30. Dallas Lankford. Canonical algebraic simplification in computational logic. Technical Report ATP-25, University of Texas, 1975. Google Scholar
  31. Dallas Lankford. On proving term rewrite systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA, 1979. Google Scholar
  32. 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. URL: https://doi.org/10.1007/978-3-540-25979-4_14.
  33. Zohar Manna and Stephen Ness. On the termination of Markov algorithms. In 3rd Hawaii International Conference on System Science, pages 789-792, 1970. Google Scholar
  34. Aart Middeldorp. Approximating dependency graphs using tree automata techniques. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of Lecture Notes in Computer Science, pages 593-610. Springer, 2001. URL: https://doi.org/10.1007/3-540-45744-5_49.
  35. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  36. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified prover based on ordered resolution. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 152-165. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294100.
  37. Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish, and Jürgen Giesl. Proving termination using recursive path orders and SAT solving. In Boris Konev and Frank Wolter, editors, Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007, Proceedings, volume 4720 of Lecture Notes in Computer Science, pages 267-282. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74621-8_18.
  38. Jonas Schöpf and Christian Sternagel. Tęrn-0.15emåisebox-0.55exTęrn-0.15emTęrn-0.15emåisebox-0.55ex2 with termination templates for teaching. In Proc. of the 16th International Workshop on Termination, 2018. URL: http://arxiv.org/abs/1806.05040.
  39. Christian Sternagel and René Thiemann. Generalized and formalized uncurrying. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 243-258. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24364-6_17.
  40. Christian Sternagel and René Thiemann. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. 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 287-302. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.RTA.2013.287.
  41. Christian Sternagel and René Thiemann. The certification problem format. In Christoph Benzmüller and Bruno Woltzenlogel Paleo, editors, Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014, volume 167 of EPTCS, pages 61-72, 2014. URL: https://doi.org/10.4204/EPTCS.167.8.
  42. Christian Sternagel and René Thiemann. Formalizing monotone algebras for certification of termination and complexity proofs. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science, pages 441-455. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_30.
  43. Christian Sternagel and René Thiemann. XML. Archive of Formal Proofs, October 2014. , Formal proof development. URL: http://isa-afp.org/entries/XML.html.
  44. Christian Sternagel and Akihisa Yamada. Reachability analysis for termination and confluence of rewriting. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 262-278. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_15.
  45. Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. StarExec: A cross-community infrastructure for logic solving. 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 367-373. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_28.
  46. René Thiemann, Guillaume Allais, and Julian Nagele. On the Formalization of Termination Techniques based on Multiset Orderings. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 339-354. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.339.
  47. René Thiemann and Christian Sternagel. Certification of termination proofs using Cęrn-0.15exeęrn-0.45exTęrn-0.45exA. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 452-468. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_31.
  48. Xavier Urbain. Modular and incremental automated termination proofs. J. Autom. Reasoning, 32(4):315-355, 2004. URL: https://doi.org/10.1007/BF03177743.
  49. Johannes Waldmann. Matchbox: A tool for match-bounded string 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 85-94. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_6.
  50. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Partial status for KBO. In Johannes Waldmann, editor, 13th International Workshop on Termination (WST 2013), pages 74-78, 2013. Google Scholar
  51. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Unifying the Knuth-Bendix, recursive path and polynomial orders. In Ricardo Pe~na and Tom Schrijvers, editors, 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013, pages 181-192. ACM, 2013. URL: https://doi.org/10.1145/2505879.2505885.
  52. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Nagoya Termination Tool. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science, pages 466-475. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_32.
  53. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. A unified ordering for termination proving. Sci. Comput. Program., 111:110-134, 2015. URL: https://doi.org/10.1016/j.scico.2014.07.009.
  54. Harald Zankl, Nao Hirokawa, and Aart Middeldorp. Constraints for argument filterings. In Jan van Leeuwen, Giuseppe F. Italiano, Wiebe van der Hoek, Christoph Meinel, Harald Sack, and Frantisek Plasil, editors, SOFSEM 2007: Theory and Practice of Computer Science, 33rd Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 20-26, 2007, Proceedings, volume 4362 of Lecture Notes in Computer Science, pages 579-590. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-69507-3_50.
  55. Harald Zankl, Nao Hirokawa, and Aart Middeldorp. KBO orientability. J. Autom. Reasoning, 43(2):173-201, 2009. URL: https://doi.org/10.1007/s10817-009-9131-z.
  56. Harald Zankl and Aart Middeldorp. Satisfiability of non-linear (ir)rational arithmetic. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 481-500. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_27.
  57. Hans Zantema. Termination of string rewriting proved automatically. J. Autom. Reasoning, 34(2):105-139, 2005. URL: https://doi.org/10.1007/s10817-005-6545-0.
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