Talk "The Algebra of Iterative Constructions"

by Benjamin Lucien Kaminski

Fri, 10 April 2026 at 10:27 am in Torino, Italy

Joint work with: Kevin Batz, Lucas Kehrer, Gerwin Klein, Henning Urbat, Todd Schmid

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. 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. We moreover improve upon 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 of suitably seeded fixed point iterations: 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 make notes on the completeness of our axiomatization of AIC. Our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and (b) a different finite set of infinitary axioms is complete. We also note that infinitary axioms are unavoidable: there exists no finite complete axiomatization of sequence models given by finitary axioms.