Document Open Access Logo

Certifying Higher-Order Polynomial Interpretations

Authors Niels van der Weide , Deivid Vale , Cynthia Kop

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.30.pdf
  • Filesize: 1.01 MB
  • 20 pages

Document Identifiers

Author Details

Niels van der Weide
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
Deivid Vale
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
Cynthia Kop
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands

Funding

  • van der Weide, Niels: This research was supported by the NWO project "The Power of Equality" OCENW.M20.380, which is financed by the Dutch Research Council (NWO).
  • Vale, Deivid: Author supported by NWO Top project "Implicit Complexity through Higher-Order Rewriting", NWO 612.001.803/7571.
  • Kop, Cynthia: Author supported by NWO Top project "Implicit Complexity through Higher-Order Rewriting", NWO 612.001.803/7571 and the NWO VIDI project "Constrained Higher-Order Rewriting and Program Equivalence", NWO VI.Vidi.193.075.

Acknowledgements

The authors thank Dan Frumin for his help with understanding and using Ltac.

Cite AsGet BibTex

Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying Higher-Order Polynomial Interpretations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.30

Abstract

Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method that is used to prove termination, namely the polynomial interpretation method. In addition, we give a program that processes proof traces containing a high-level description of a termination proof into a formal Coq proof script that can be checked by Coq. We demonstrate the usability of this approach by certifying higher-order polynomial interpretation proofs produced by Wanda, a termination analysis tool for higher-order rewriting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
Keywords
  • higher-order rewriting
  • Coq
  • termination
  • formalization

Metrics

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

Related Versions

Supplementary Materials

References

  1. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program., 29:e19, 2019. URL: https://doi.org/10.1017/S0956796819000170.
  2. Ariane Alves Almeida and Mauricio Ayala-Rincón. Formalizing the dependency pair criterion for innermost termination. Sci. Comput. Program., 195:102474, 2020. URL: https://doi.org/10.1016/j.scico.2020.102474.
  3. 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.
  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. Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio. The computability path ordering. Log. Methods Comput. Sci., 11(4), 2015. URL: https://doi.org/10.2168/LMCS-11(4:3)2015.
  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. 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.
  8. Carsten Fuhs and Cynthia Kop. Polynomial Interpretations for Higher-Order Rewriting. 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 176-192. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.176.
  9. Carsten Fuhs and Cynthia Kop. A Static Higher-Order Dependency Pair Framework. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 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, volume 11423 of Lecture Notes in Computer Science, pages 752-782. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_27.
  10. 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.
  11. 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, pages 156-166, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-17502-3_10.
  12. Raúl Gutiérrez and Salvador Lucas. mu-term: Verify termination properties automatically (system description). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 436-447. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_28.
  13. Makoto Hamana. Theory and practice of second-order rewriting: Foundation, evolution, and SOL. In Keisuke Nakano and Konstantinos Sagonas, editors, Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings, volume 12073 of Lecture Notes in Computer Science, pages 3-9. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_1.
  14. Martin Hofmann and Thomas Streicher. The groupoid model refutes uniqueness of identity proofs. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994, pages 208-212. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/LICS.1994.316071.
  15. Cynthia Kop. Higher Order Termination: Automatable Techniques for Proving Termination of Higher-Order Term Rewriting Systems. PhD thesis, Vrije Universiteit Amsterdam, 2012. Google Scholar
  16. Cynthia Kop. WANDA - a higher order termination tool (system description). In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 36:1-36:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.36.
  17. Cynthia Kop. Wanda’s source code repository, 2023. URL: https://github.com/hezzel/wanda.
  18. Cynthia Kop and Deivid Vale. Tuple Interpretations for Higher-Order Complexity. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), 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.
  19. Cynthia Kop and Femke van Raamsdonk. Dynamic Dependency Pairs for Algebraic Functional Systems. Log. Methods Comput. Sci., 8(2), 2012. URL: https://doi.org/10.2168/LMCS-8(2:10)2012.
  20. Adam Koprowski. Coq formalization of the higher-order recursive path ordering. Appl. Algebra Eng. Commun. Comput., 20(5-6):379-425, 2009. URL: https://doi.org/10.1007/s00200-009-0105-5.
  21. 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.
  22. Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, and Frédéric Blanqui. Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE Trans. Inf. Syst., 92-D(10):2007-2015, 2009. URL: https://doi.org/10.1587/transinf.E92.D.2007.
  23. 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 für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.RTA.2011.251.
  24. J.C. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis, University of Utrecht, 1996. URL: https://www.cs.au.dk/~jaco/papers/thesis.pdf.
  25. José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, and Francisco-Jesús Martín-Mateos. Formalizing Rewriting in the ACL2 Theorem Prover. In John A. Campbell and Eugenio Roanes-Lozano, editors, Artificial Intelligence and Symbolic Computation, International Conference AISC 2000 Madrid, Spain, July 17-19, 2000, Revised Papers, volume 1930 of Lecture Notes in Computer Science, pages 92-106. Springer, 2000. URL: https://doi.org/10.1007/3-540-44990-6_7.
  26. Bas Spitters and Eelis van der Weegen. Type classes for mathematics in type theory. Math. Struct. Comput. Sci., 21(4):795-825, 2011. URL: https://doi.org/10.1017/S0960129511000119.
  27. William W. Tait. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  28. 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.
  29. Deivid Vale and Niels van der Weide. Onijn documentation, 2022. URL: https://deividrvale.github.io/nijn-coq-script-generation/onijn/index.html.
  30. Deivid Vale and Niels van der Weide. deividrvale/nijn-coq-script-generation: First Release of public API, May 2023. URL: https://doi.org/10.5281/zenodo.7915736.
  31. Niels van der Weide and Deivid Vale. nmvdw/nijn: 1.0.0, May 2023. URL: https://doi.org/10.5281/zenodo.7913023.
  32. Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying higher-order polynomial interpretations. CoRR, abs/2302.11892, 2023. URL: https://doi.org/10.48550/arXiv.2302.11892.
  33. 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.
  34. Akihisa Yamada. Multi-dimensional interpretations for termination of term rewriting. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 273-290. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_16.
  35. 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.
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