Home Publications Research Data Research Grants Equipment Inventions & Patents Awards Additional Research Activities Faculties & Institutions Research Areas

The Algebra of Iterative Constructions

Batz K, Kaminski BL, Kehrer L, Klein G, Schmid T, Urbat H (2026)

---

Publication Type: Conference contribution

Publication year: 2026

Journal

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 380

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Lisbon

ISBN: 9783959774345

DOI: 10.4230/LIPIcs.LICS.2026.17

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 supn 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.

Authors with CRIS profile

Involved external institutions

How to cite

APA:

Batz, K., Kaminski, B.L., Kehrer, L., Klein, G., Schmid, T., & Urbat, H. (2026). The Algebra of Iterative Constructions. In Faggian Claudia, Katoen Joost-Pieter, Katoen Joost-Pieter (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Lisbon, PT: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Batz, Kevin, et al. "The Algebra of Iterative Constructions." Proceedings of the 41st Annual Symposium on Logic in Computer Science, LICS 2026, Lisbon Ed. Faggian Claudia, Katoen Joost-Pieter, Katoen Joost-Pieter, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2026.

BibTeX: Download