Document Open Access Logo

Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)

Author Akihisa Yamada

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.4.pdf
  • Filesize: 0.55 MB
  • 5 pages

Document Identifiers

Author Details

Akihisa Yamada
  • National Institute of Advanced Industrial Science and Technology, Tokyo, Japan

Cite AsGet BibTex

Akihisa Yamada. Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.4

Abstract

Automated termination analysis is a central topic in the research of term rewriting. In this talk, I will first review the theoretical foundation of termination of term rewriting, leading to the recently established tuple interpretation method. Then I will present an Isabelle/HOL formalization of the theory. Although the formalization is based on the existing library IsaFoR (Isabelle Formalization of Rewriting), the present work takes another approach of representing relations (predicates rather than sets) so that the notation is more human friendly. Then I will present a unified implementation of the termination analysis techniques via SMT encoding, leading to the termination prover NaTT. Many tools have been developed for termination analysis and have been competing annually in termCOMP (Termination Competition) for two decades. At the end of the talk, I will share my experience in organizing termCOMP in the last five years.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Automated reasoning
Keywords
  • Term rewriting
  • Termination
  • Isabelle/HOL
  • Competition

Metrics

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

References

  1. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theor. Compt. Sci. , 236(1-2):133-178, 2000. URL: https://doi.org/0.1016/S0304-3975(99)00207-8.
  2. Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Sci. Comput. Program., 185, 2020. URL: https://doi.org/10.1016/j.scico.2019.102338.
  3. Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 305-343. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_11.
  4. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. Google Scholar
  5. 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.
  6. H. Zantema C. Marché, A. Rubio. Termination problem data base: format of input files, 2005. URL: https://www.lri.fr/~marche/tpdb/format.html.
  7. M. Codish, J. Giesl, P. Schneider-Kamp, and R. Thiemann. SAT solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reasoning, 49(1):53-93, 2012. Google Scholar
  8. Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated certified proofs with cime3. In Manfred Schmidt-Schauß, editor, RTA 2011, 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.
  9. Nachum Dershowitz. Orderings for term-rewriting systems. Theor. Compt. Sci. , 17(3):279-301, 1982. URL: https://doi.org/10.1016/0304-3975(82)90026-3.
  10. Nachum Dershowitz. Termination of rewriting. J. Symb. Comput. , 3(1-2):69-115, 1987. Google Scholar
  11. Jörg Endrullis, Johannes Waldmann, and Hans Zantema. Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. , 40(2-3):195-220, 2008. URL: https://doi.org/10.1007/s10817-007-9087-9.
  12. Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl. Maximal termination. In Andrei Voronkov, editor, RTA 2008, volume 5117 of LNCS, pages 110-125. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70590-1_8.
  13. 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, IJCAR 2014, volume 8562 of LNCS, pages 184-191. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_13.
  14. 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, TACAS 2019, Part III, volume 11429 of LNCS, pages 156-166. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17502-3_10.
  15. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. J. Autom. Reason. , 37(3):155-203, 2006. URL: https://doi.org/10.1007/s10817-006-9057-7.
  16. Raúl Gutiérrez and Salvador Lucas. mu-term: Verify termination properties automatically (system description). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020 (2), volume 12167 of LNCS, pages 436-447. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_28.
  17. Nao Hirokawa and Aart Middeldorp. Dependency pairs revisited. In Vincent van Oostrom, editor, RTA 2004, volume 3091 of LNCS, pages 249-268. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_18.
  18. Dieter Hofbauer and Johannes Waldmann. Termination of string rewriting with matrix interpretations. In Frank Pfenning, editor, RTA 2006, volume 4098 of LNCS, pages 328-342. Springer, 2006. URL: https://doi.org/10.1007/11805618_25.
  19. José Iborra, Naoki Nishida, Germán Vidal, and Akihisa Yamada. Relative termination via dependency pairs. J. Autom. Reason., 58(3):391-411, 2017. URL: https://doi.org/10.1007/s10817-016-9373-5.
  20. Programming languages: C++, ISO/IEC 14882:2020. Google Scholar
  21. Sam Kamin and Jean-Jacques Lévy. Two generalizations of the recursive path ordering, 1980. Unpublished note. Google Scholar
  22. 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.
  23. Cynthia Kop and Deivid Vale. Tuple interpretations for higher-order complexity. In Naoki Kobayashi, editor, FSCD 2021, volume 195 of LIPIcs, pages 31:1-31:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.31.
  24. Adam Koprowski and Johannes Waldmann. Max/plus tree automata for termination of term rewriting. Acta Cybern., 19(2):357-392, 2009. Google Scholar
  25. Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In Ralf Treinen, editor, RTA 2009, volume 5595 of LNCS, pages 295-304. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_21.
  26. J.B. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyia’s conjecture. Transactions of the American Mathematical Society, 95(2):210-225, 1960. Google Scholar
  27. D. Lankford. Canonical algebraic simplification in computational logic. Technical Report ATP-25, University of Texas, 1975. Google Scholar
  28. Salvador Lucas and Raúl Gutiérrez. Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. , 60(4):465-501, 2018. URL: https://doi.org/10.1007/s10817-017-9419-3.
  29. Z. Manna and S. Ness. On the termination of Markov algorithms. In the 3rd Hawaii International Conference on System Science, pages 789-792, 1970. Google Scholar
  30. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  31. Ocaml. URL: https://v2.ocaml.org/.
  32. 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, FroCoS 2007, volume 4720 of LNCS, pages 267-282. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74621-8_18.
  33. star-exec-presenter (software), 2014. URL: https://github.com/jwaldmann/star-exec-presenter/.
  34. starexec-master (software). URL: https://github.com/TermCOMP/starexec-master.
  35. Christian Sternagel and Akihisa Yamada. Reachability analysis for termination and confluence of rewriting. In Tomás Vojnar and Lijun Zhang, editors, TACAS (1) 2019, volume 11427 of LNCS, pages 262-278. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_15.
  36. 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, IJCAR 2014, volume 8562 of LNCS, pages 367-373. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_28.
  37. Termination competitions results (repository). URL: https://termcomp.github.io/.
  38. René Thiemann and Christian Sternagel. Certification of termination proofs using CeTA. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs 2009, volume 5674 of LNCS, pages 452-468. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_31.
  39. The termination problem data base. URL: http://termination-portal.org/wiki/TPDB.
  40. Johannes Waldmann. Matchbox: A tool for match-bounded string rewriting. In Vincent van Oostrom, editor, RTA 2004, volume 3091 of LNCS, pages 85-94. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_6.
  41. T.J. Watson, J.A. Goguen, J.W. Thatcher, and E.G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In Current Trends in Programming Methodology. Prentice Hall, 1976. Google Scholar
  42. Akihisa Yamada. Term orderings for non-reachability of (conditional) rewriting. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, IJCAR 2022, volume 13385 of LNCS, pages 248-267. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_15.
  43. Akihisa Yamada. Tuple interpretations for termination of term rewriting. J. Autom. Reason., 66(4):667-688, 2022. URL: https://doi.org/10.1007/s10817-022-09640-4.
  44. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Nagoya termination tool. In Gilles Dowek, editor, RTA-TLCA 2014, volume 8560 of LNCS, pages 466-475. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_32.
  45. 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.
  46. Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari. AC dependency pairs revisited. In Jean-Marc Talbot and Laurent Regnier, editors, CSL 2016, volume 62 of LIPIcs, pages 8:1-8:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.8.
  47. Harald Zankl. Lazy Termination Analysis. PhD thesis, University of Innsbruck, 2009. Google Scholar
  48. Harald Zankl, Nao Hirokawa, and Aart Middeldorp. KBO orientability. J. Autom. Reasoning, 43(2):173-201, 2009. 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