Document Open Access Logo

Certified Infinite Descent Criteria in Isabelle/HOL

Authors Jamie Wright , Liron Cohen , Reuben N. S. Rowe , Andrei Popescu

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.14.pdf
  • Filesize: 1.34 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Cyclic Proof
  • Infinite Descent
  • Size-Change termination
  • Büchi automata

Metrics

Abstract

Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. Although these criteria are well studied on paper and implemented in tools, a unified, machine-checked account that relates them to the (abstract) Infinite Descent property has been missing. We present an Isabelle/HOL mechanization of this landscape. We develop a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable Isabelle lemmas for ω-regular reasoning over streams and for Büchi-automata constructions needed by the inclusion proofs.

Cite As Get BibTex

Jamie Wright, Liron Cohen, Reuben N. S. Rowe, and Andrei Popescu. Certified Infinite Descent Criteria in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.14

Author Details

Jamie Wright
  • University of Sheffield, UK
Liron Cohen
  • Ben-Gurion University of the Negev, Be'er Sheva, Israel
Reuben N. S. Rowe
  • Royal Holloway University of London, Egham, UK
Andrei Popescu
  • University of Sheffield, UK

Funding

Jamie Wright, Liron Cohen, and Andrei Popescu were supported by the Royal Society travel grant "Cyclic Reasoning Mechanisms for Interactive Theorem Proving". Liron Cohen was additionally supported by ISF Grant No. 2876/25. Jamie Wright and Andrei Popescu were additionally supported by: EPSRC grant EP/X015114/1 "COVERT"; and "Copilots for Isabelle" under the AI for Math Fund, an initiative by Renaissance Philanthropy with funding support from XTX Markets.

Supplementary Materials

References

  1. Linear temporal logic on streams. part of the isabelle library. https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Linear_Temporal_Logic_on_Streams.html, 2022.
  2. Andreas Abel and Thorsten Altenkirch. A Predicative Analysis of Structural Recursion. Journal of Functional Programming, 12(1):1-41, 2002. URL: https://doi.org/10.1017/S0956796801004191.
  3. Clemens Ballarin. Locales: A Module System for Mathematical Theories. J. Autom. Reason., 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  4. James Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006. URL: https://era.ed.ac.uk/handle/1842/1458.
  5. James Brotherston and Alex Simpson. Sequent Calculi for Induction and Infinite Descent. J. Log. Comput., 21(6):1177-1216, 2011. URL: https://doi.org/10.1093/LOGCOM/EXQ052.
  6. Julian Brunner. Büchi Complementation. Archive of Formal Proofs, October 2017. Formal proof development. URL: https://isa-afp.org/entries/Buchi_Complementation.html.
  7. Julian Brunner. Transition Systems and Automata. Archive of Formal Proofs, October 2017. Formal proof development. URL: https://isa-afp.org/entries/Transition_Systems_and_Automata.html.
  8. Liron Cohen, Adham Jabarin, Andrei Popescu, and Reuben N. S. Rowe. The Complex(ity) Landscape of Checking Infinite Descent. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632888.
  9. Liron Cohen and Reuben N. S. Rowe. Non-Well-Founded Proof Theory of Transitive Closure Logic. ACM Trans. Comput. Logic, 21(4), August 2020. URL: https://doi.org/10.1145/3404889.
  10. Liron Cohen, Reuben N. S. Rowe, and Matan Shaked. Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 336-354, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-90643-5_18.
  11. Anupam Das. On The Logical Complexity of Cyclic Arithmetic. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:1)2020.
  12. Christian Dax, Martin Hofmann, and Martin Lange. A Proof System for the Linear Time μ-Calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  13. Agda Developers. Agda. URL: https://agda.readthedocs.io/.
  14. Amina Doumane. Constructive Completeness for the Linear-time μ-calculus. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005075.
  15. The Idris Community. The Idris Reference, January 2016. Release 0.9.19.1. URL: https://docs.idris-lang.org/_/downloads/en/v0.10/pdf/.
  16. Eddie Jones, C.-H. Luke Ong, and Steven Ramsay. Cycleq: An Efficient Basis for Cyclic Equational Reasoning. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pages 395-409, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3519939.3523731.
  17. Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. Locales - A Sectioning Concept for Isabelle. In Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, and Laurent Théry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, volume 1690 of Lecture Notes in Computer Science, pages 149-166. Springer, 1999. URL: https://doi.org/10.1007/3-540-48256-3_11.
  18. Alexander" Krauss. Certified Size-Change Termination. In Frank" Pfenning, editor, Automated Deduction - CADE-21", pages 460-475", Berlin, Heidelberg", 2007". Springer Berlin Heidelberg". URL: https://doi.org/10.1007/978-3-540-73595-3_34.
  19. Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl. Termination of Isabelle functions via Termination of Rewriting. In Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, "Interactive Theorem Proving, pages 152-167, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-22863-6_13.
  20. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The Size-change Principle for Program Termination. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 81-92. ACM, 2001. URL: https://doi.org/10.1145/360204.360210.
  21. Rodolphe Lepigre and Christophe Raffalli. Practical Subtyping for Curry-Style Languages. ACM Trans. Program. Lang. Syst., 41(1):5:1-5:58, 2019. URL: https://doi.org/10.1145/3285955.
  22. Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar da Silva, and Thiago M. Ferreira Ramos. Formal Verification of Termination Criteria for First-Order Recursive Functions. Journal of Automated Reasoning, 67(4):40, 2023. URL: https://doi.org/10.1007/s10817-023-09669-z.
  23. Lawrence C. Paulson and Jasmin Christian Blanchette. Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011, volume 2 of EPiC Series in Computing, pages 1-11. EasyChair, 2010. URL: https://doi.org/10.29007/36dt.
  24. Luigi Santocanale. A Calculus of Circular Proofs and Its Categorical Semantics. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 357-371. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_25.
  25. Alex Simpson. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  26. Christoph Sprenger and Mads Dam. A Note on Global Induction in a mu-calculus with Explicit Approximations. In Zoltán Ésik and Anna Ingólfsdóttir, editors, Fixed Points in Computer Science, FICS 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings, volume NS-02-2 of BRICS Notes Series, pages 22-24. University of Aarhus, 2002. URL: https://www.brics.dk/NS/02/2.
  27. Christoph Sprenger and Mads Dam. On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-calculus. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 425-440. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_27.
  28. René Thiemann and Jürgen Giesl. The Size-Change Principle and Dependency Pairs for Termination of Term Rewriting. Applicable Algebra in Engineering, Communication and Computing, 16(4):229-270, September 2005. URL: https://doi.org/10.1007/s00200-005-0179-7.
  29. Dominik Wehr. Cyclic Proof Theory. Doctoral thesis, University of Gothenburg, Gothenburg, Sweden, December 2025. URL: https://hdl.handle.net/2077/89733.
  30. Jamie Wright, Andrei Popescu, Reuben N. S. Rowe, and Liron Cohen. Certified Infinite Descent Criteria in Isabelle/HOL - ITP 2026 Software Artifact, 2026. URL: https://doi.org/10.5281/zenodo.20323854.
  31. Jamie Wright, Andrei Popescu, Reuben N. S. Rowe, and Liron Cohen. Certified Infinite Descent Criteria in Isabelle/HOL (Browseable HTML), 2026. URL: https://jamierwright.github.io/InfiniteDescent/.
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