2026-07-21T20:03:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26804 2026-07-09T11:31:08Z ddc:004 open_access

The Algebra of Iterative Constructions Batz, Kevin Kaminski, Benjamin Lucien Kehrer, Lucas Klein, Gerwin Schmid, Todd Urbat, Henning fixed point theorems fixed point iteration algebra equational logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kevin Batz and Benjamin Lucien Kaminski and Lucas Kehrer and Gerwin Klein and Todd Schmid and Henning Urbat 2026 Is Part Of LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.LICS.2026.17 urn:nbn:de:0030-drops-268040 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.17 eng https://creativecommons.org/licenses/by/4.0/legalcode