Document Open Access Logo

The Algebra of Iterative Constructions

Authors Kevin Batz , Benjamin Lucien Kaminski , Lucas Kehrer , Gerwin Klein , Todd Schmid , Henning Urbat

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.17.pdf
  • Filesize: 2.86 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
  • Mathematics of computing
Keywords
  • fixed point theorems
  • fixed point iteration
  • algebra
  • equational logic

Metrics

Abstract

Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. For example,
F ◇ F^* ⊥ = ◇ F^* ⊥ 
states in AIC that sup_n Fⁿ (⊥) - a construction known from the Kleene fixed point theorem - is a fixed point of F. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of k-induction - a technique used in software verification. 
We moreover present a novel fixed point theorem. It improves a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors through iterating an endomap on an arbitrary seed element: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle’s sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically.
Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no complete axiomatization of standard models given by finitely many finitary axioms.

Cite As Get BibTex

Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, and Henning Urbat. The Algebra of Iterative Constructions. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 17:1-17:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.17

Author Details

Kevin Batz
  • Cornell University, Ithaca, NY, USA
Benjamin Lucien Kaminski
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
  • University College London, UK
Lucas Kehrer
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Gerwin Klein
  • Proofcraft, Sydney, Australia
  • University of New South Wales, Sydney, Australia
Todd Schmid
  • Bucknell University, Lewisburg, PA, USA
Henning Urbat
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Batz, Kevin: ERC grant Autoprobe (no. 101002697).
  • Kehrer, Lucas: Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 563038229.
  • Urbat, Henning: Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 569130867.

Acknowledgements

This work was initiated during a 2023 workshop at the Bellairs Research Institute of McGill University in Holetown, Barbados. We thank Jan Reineke for his valuable comments.

Supplementary Materials

References

  1. Samson Abramsky and Achim Jung. Domain Theory. In Handbook of Logic In Computer Science, volume 3. Clarendon Press, 1994. Google Scholar
  2. Jirí Adámek, Stefan Milius, and Jirí Velebil. What are iteration theories? In MFCS, Lecture Notes in Computer Science, pages 240-252. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74456-6_23.
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  4. Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. Fixpoint Theory - Upside Down. Log. Methods Comput. Sci., 19(2), 2023. URL: https://doi.org/10.46298/LMCS-19(2:15)2023.
  5. Paolo Baldan, Sebastian Gurke, Barbara König, Tommaso Padoan, and Florian Wittbold. Approximating Fixpoints of Approximated Functions. In CAV (2), Lecture Notes in Computer Science, pages 193-215. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-98679-6_9.
  6. Paolo Baldan, Barbara König, and Tommaso Padoan. Systems of Fixpoint Equations: Abstraction, Games, Up-To Techniques and Local Algorithms. Inf. Comput., 301:105233, 2024. URL: https://doi.org/10.1016/J.IC.2024.105233.
  7. Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Latticed k-Induction with an Application to Probabilistic Programs. In CAV (2), volume 12760 of Lecture Notes in Computer Science, pages 524-549. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_25.
  8. Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. PrIC3: Property Directed Reachability for MDPs. In CAV (2), Lecture Notes in Computer Science, pages 512-538. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_27.
  9. Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, and Henning Urbat. The Algebra of Iterative Constructions. CoRR, 2026. URL: https://arxiv.org/abs/2605.03176.
  10. Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, and Todd Schmid. The Algebra of Iterative Constructions. Archive of Formal Proofs, April 2026. Formal proof development. URL: https://isa-afp.org/entries/Iteration_Algebra.html.
  11. Dirk Beyer, Matthias Dangl, and Philipp Wendler. Boosting k-Induction with Continuously-Refined Invariants. In CAV (1), volume 9206 of Lecture Notes in Computer Science, pages 622-640. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_42.
  12. Stephen L. Bloom and Zoltán Ésik. Iteration Theories - The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, 1993. URL: https://doi.org/10.1007/978-3-642-78034-9.
  13. Aaron R. Bradley. SAT-Based Model Checking without Unrolling. In VMCAI, Lecture Notes in Computer Science, pages 70-87. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-18275-4_7.
  14. Stanley N. Burris and H. P. Sankappanavar. A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics. Springer, New York, 1981. Google Scholar
  15. Edmund M. Clarke. Program Invariants as Fixed Points. In FOCS, pages 18-29. IEEE Computer Society, 1977. Google Scholar
  16. Patrick Cousot and Radhia Cousot. Constructive Versions of Tarski’s Fixed Point Theorems. Pacific journal of Mathematics, 82(1):43-57, 1979. Google Scholar
  17. Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer. Software Verification Using k-Induction. In SAS, volume 6887 of Lecture Notes in Computer Science, pages 351-368. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23702-7_26.
  18. Frank M. V. Feys and Helle Hvid Hansen. Arrow’s Theorem Through a Fixpoint Argument. In TARK, volume 297 of EPTCS, pages 175-188, 2019. URL: https://doi.org/10.4204/EPTCS.297.12.
  19. Carl A Gunter. Semantics of Programming Languages: Structures and Techniques. MIT press, 1992. Google Scholar
  20. Arie Gurfinkel and Alexander Ivrii. k-Induction without Unrolling. In FMCAD, pages 148-155. IEEE, 2017. URL: https://doi.org/10.23919/FMCAD.2017.8102253.
  21. Morris William Hirsch and Hal Smith. Monotone Maps: A Review. Journal of Difference Equations and Applications, 11(4-5):379-398, 2005. Google Scholar
  22. Jacek Jachymski, Leslaw Gajek, and Piotr Pokarowski. The Tarski-Kantorovitch Prinicple and the Theory of Iterated Function Systems. Bulletin of the Australian Mathematical Society, 61(2):247-261, 2000. Google Scholar
  23. Dejan Jovanovic and Bruno Dutertre. Property-directed k-Induction. In FMCAD, pages 85-92. IEEE, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886665.
  24. Tomasz Kiwerski and Jakub Tomaszewski. Arithmetic, Interpolation and Factorization of Amalgams, 2024. URL: https://arxiv.org/abs/2401.05526.
  25. Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, and Ichiro Hasuo. The Lattice-Theoretic Essence of Property Directed Reachability Analysis. In CAV (1), Lecture Notes in Computer Science, pages 235-256. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_12.
  26. Dexter Kozen. Results on the propositional μ-calculus. In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings, volume 140 of Lecture Notes in Computer Science, pages 348-359. Springer, 1982. URL: https://doi.org/10.1007/BFB0012782.
  27. Dexter Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/INCO.1994.1037.
  28. Jean-Louis Lassez, V. L. Nguyen, and Liz Sonenberg. Fixed Point Theorems and Semantics: A Folk Tale. Information Processing Letters, 14(3):112-116, 1982. URL: https://doi.org/10.1016/0020-0190(82)90065-5.
  29. Holbrook Mann MacNeille. Partially ordered Sets. Transactions of the American Mathematical Society, 1936. Google Scholar
  30. Jayadev Misra. A Walk over the Shortest Path: Dijkstra’s Algorithm viewed as Fixed-point Computation. Inf. Process. Lett., 77(2-4):197-200, 2001. URL: https://doi.org/10.1016/S0020-0190(00)00202-7.
  31. John Forbes Nash. Equilibrium Points in n-person Games. Proceedings of the National Academy of Sciences, 36(1):48-49, 1950. Google Scholar
  32. Wojciech Olszewski. On Convergence of Sequences in Complete Lattices. Order, 38:251-255, 2021. URL: https://doi.org/10.1007/S11083-020-09538-Z.
  33. Wojciech Olszewski. On Sequences of Iterations of Increasing and Continuous Mappings on Complete Lattices. Games and Economic Behavior, 126:453-459, 2021. URL: https://doi.org/10.1016/J.GEB.2021.01.011.
  34. David Park. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence, 5, 1969. Google Scholar
  35. Amir Pnueli. The Temporal Logic of Programs. In FOCS, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  36. Marcus Rossel, Rudi Schneider, Thomas Koehler, Michel Steuwer, and Andrés Goens. Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation. Proc. ACM Program. Lang., 10(POPL):718-747, 2026. URL: https://doi.org/10.1145/3776667.
  37. Alejandro Santacruz Hidalgo and Gord Sinnamon. Core Decreasing Functions. Journal of Functional Analysis, 287(4):110490, 2024. Google Scholar
  38. Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking Safety Properties using Induction and a SAT-Solver. In FMCAD, volume 1954 of Lecture Notes in Computer Science, pages 108-125. Springer, 2000. URL: https://doi.org/10.1007/3-540-40922-X_8.
  39. Gord Sinnamon. Monotonicity in Banach Function Spaces. Nonlinear Analysis, Function Spaces and Applications, pages 205-240, 2007. Google Scholar
  40. Mark Theunissen and Yde Venema. MacNeille Completions of Lattice Expansions. Algebra Universalis, 2007. Google Scholar
  41. Igor Walukiewicz. Completeness of Kozen’s Axiomatisation of the Propositional mu-Calculus. In LICS, pages 14-24. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/LICS.1995.523240.
  42. Tobias Winkler and Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration. In TACAS (2), volume 13994 of Lecture Notes in Computer Science, pages 391-409. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_24.
  43. Tengshun Yang, Hongfei Fu, Jingyu Ke, Naijun Zhan, and Shiyang Wu. Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. CoRR, 2024. URL: https://doi.org/10.48550/arXiv.2403.17567.
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