Document Open Access Logo

New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations

Authors René Thiemann , Dieter Hofbauer , Ulysse Le Huitouze, Johannes Waldmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.32.pdf
  • Filesize: 0.87 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
Keywords
  • Isabelle/HOL
  • Matrix Interpretations
  • Narrowing
  • Right-Forward Closures
  • Term Rewriting

Metrics

Abstract

We provide new proofs of two important theorems for proving termination of term rewrite systems (TRSs), including a full formalization in Isabelle/HOL.
We first consider Dershowitz' theorem that termination starting from arbitrary terms is equivalent to termination starting from terms in the right-forward closures of right-hand sides, provided that the TRS is right-linear or orthogonal. Our new proof deviates from the original one in that no reorderings of steps in infinite derivations are required, making it more precise in its argumentation. It also subsumes a later result that one can weaken orthogonality to locally confluent overlay TRSs.
The second theorem is about matrix interpretations. These were introduced by Hofbauer and Waldmann for proving termination of string rewrite systems (SRSs), internally using the concept of a core. Subsequently, Endrullis, Waldmann and Zantema developed matrix interpretations for TRSs without using the idea of a core. Whereas matrix interpretations for TRSs have already been formalized several times, so far this was not the case for core SRS matrix interpretations. We not only provide such a formalization, but also extend core SRS matrix interpretations to TRSs. These new core matrix interpretations for TRSs generalize previous approaches.

Cite As Get BibTex

René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, and Johannes Waldmann. New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.32

Author Details

René Thiemann
  • University of Innsbruck, Austria
Dieter Hofbauer
  • ASW Saarland, Germany
Ulysse Le Huitouze
  • University of Rennes, France
Johannes Waldmann
  • HTWK Leipzig, Germany

Acknowledgements

We are grateful to the reviewers of both the Workshop on Termination (WST 2025) and FSCD 2026 for their detailed and helpful comments.

Supplementary Materials

References

  1. Beatriz Alarcón, Salvador Lucas, and Rafael Navarro-Marset. Proving termination with matrix interpretations over the reals. In Alfons Geser and Johannes Waldmann, editors, 10th International Workshop on Termination, WST 2009, Leipzig, Germany, June 3-5, 2009. Proceedings, pages 12-15, 2009. URL: https://termination-portal.org/wiki/WST.
  2. 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.
  3. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  4. 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.
  5. Evelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. J. Autom. Reason., 34(4):325-363, 2005. URL: https://doi.org/10.1007/S10817-005-9022-X.
  6. Pierre Courtieu, Gladys Gbedo, and Olivier Pons. Improved matrix interpretation. In Jan van Leeuwen, Anca Muscholl, David Peleg, Jaroslav Pokorný, and Bernhard Rumpe, editors, Current Trends in Theory and Practice of Computer Science, 36th Conference, SOFSEM 2010, Špindlerův Mlýn, Czech Republic, January 23-29, 2010. Proceedings, volume 5901 of Lecture Notes in Computer Science, pages 283-295. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-11266-9_24.
  7. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction, 28th International Conference, CADE 28, Virtual Event, July 12-15, 2021. Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  8. Nachum Dershowitz. Termination of linear rewriting systems (preliminary version). In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, July 13-17, 1981. Proceedings, volume 115 of Lecture Notes in Computer Science, pages 448-458. Springer, 1981. URL: https://doi.org/10.1007/3-540-10843-2_36.
  9. 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.
  10. Nachum Dershowitz and Charles Hoot. Natural termination. Theor. Comput. Sci., 142(2):179-207, 1995. URL: https://doi.org/10.1016/0304-3975(94)00275-4.
  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. Andreas Gebhardt, Dieter Hofbauer, and Johannes Waldmann. Matrix evolutions. In Dieter Hofbauer and Alexander Serebrenik, editors, 9th International Workshop on Termination, WST 2007, Paris, France, June 29, 2007. Proceedings, pages 5-8, 2007. URL: https://termination-portal.org/wiki/WST.
  13. Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Match-bounded string rewriting systems. Appl. Algebra Eng. Commun. Comput., 15(3-4):149-171, 2004. URL: https://doi.org/10.1007/S00200-004-0162-8.
  14. Alfons Geser, Dieter Hofbauer, Johannes Waldmann, and Hans Zantema. Finding finite automata that certify termination of string rewriting. In Michael Domaratzki, Alexander Okhotin, Kai Salomaa, and Sheng Yu, editors, Implementation and Application of Automata, 9th International Conference, CIAA 2004, Kingston, Canada, July 22-24, 2004. Revised Selected Papers, volume 3317 of Lecture Notes in Computer Science, pages 134-145. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30500-2_13.
  15. Alfons Geser, Dieter Hofbauer, Johannes Waldmann, and Hans Zantema. On tree automata that certify termination of left-linear term rewriting systems. Inf. Comput., 205(4):512-534, 2007. URL: https://doi.org/10.1016/J.IC.2006.08.007.
  16. Oliver Geupel. Overlap closures and termination of term rewriting systems. Technical Report MIP-8922, Universität Passau, Passau, 1989. Google Scholar
  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. Reason., 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. Bernhard Gramlich. Relating innermost, weak, uniform and modular termination of term rewriting systems. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, International Conference, LPAR '92, St. Petersburg, Russia, July 15-20, 1992. Proceedings, volume 624 of Lecture Notes in Computer Science, pages 285-296. Springer, 1992. URL: https://doi.org/10.1007/BFB0013069.
  20. Dieter Hofbauer. Termination proofs by context-dependent interpretations. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001. Proceedings, volume 2051 of Lecture Notes in Computer Science, pages 108-121. Springer, 2001. URL: https://doi.org/10.1007/3-540-45127-7_10.
  21. Dieter Hofbauer. MultumNonMulta at TermComp 2018. In Salvador Lucas, editor, 16th International Workshop on Termination, WST 2018, Oxford, U. K., July 18-19, 2018. Proceedings, page 80, 2018. URL: https://termination-portal.org/wiki/WST.
  22. 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. URL: https://doi.org/10.1007/11805618_25.
  23. Adam Koprowski and Johannes Waldmann. Arctic termination ... below zero. 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 202-216. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70590-1_14.
  24. Adam Koprowski and Johannes Waldmann. Max/plus tree automata for termination of term rewriting. Acta Cybern., 19(2):357-392, 2009. URL: https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772.
  25. Martin Korp and Aart Middeldorp. Match-bounds revisited. Inf. Comput., 207(11):1259-1283, 2009. URL: https://doi.org/10.1016/J.IC.2009.02.010.
  26. Salvador Lucas. Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Informatics Appl., 39(3):547-586, 2005. URL: https://doi.org/10.1051/ITA:2005029.
  27. Salvador Lucas. On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. Appl. Algebra Eng. Commun. Comput., 17(1):49-73, 2006. URL: https://doi.org/10.1007/S00200-005-0189-5.
  28. Salvador Lucas. From matrix interpretations over the rationals to matrix interpretations over the naturals. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings, volume 6167 of Lecture Notes in Computer Science, pages 116-131. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14128-7_11.
  29. Friedrich Neurauter and Aart Middeldorp. On the domain and dimension hierarchy of matrix interpretations. In Nikolaj S. Bjørner and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of Lecture Notes in Computer Science, pages 320-334. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28717-6_25.
  30. Friedrich Neurauter and Aart Middeldorp. Polynomial interpretations over the natural, rational and real numbers revisited. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:22)2014.
  31. 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.
  32. René Thiemann and Christian Sternagel. Certification of termination proofs using CeTA. 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.
  33. Yoshihito Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett., 25(3):141-143, 1987. URL: https://doi.org/10.1016/0020-0190(87)90122-0.
  34. 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.
  35. Johannes Waldmann. Matrix interpretations on polyhedral domains. In Maribel Fernández, editor, Rewriting Techniques and Applications, 26th International Conference, RTA 2015, Warsaw, Poland, June 29 - July 1, 2015. Proceedings, volume 36 of LIPIcs, pages 318-333. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.318.
  36. Hans Zantema. Termination of string rewriting proved automatically. J. Autom. Reason., 34(2):105-139, 2005. URL: https://doi.org/10.1007/S10817-005-6545-0.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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