The Algebra of Iterative Constructions

TL;DR

The paper introduces the algebra of iterative constructions (AIC), an algebraic framework for reasoning about fixed point iterations on complete lattices, with applications in fixed point theorems and software verification.

Contribution

It develops a purely algebraic approach to fixed point iterations, proving several classical and new fixed point theorems, and mechanizes the theory in Isabelle/HOL.

Findings

AIC allows derivation of fixed point theorems via equational logic.

Mechanized proofs in Isabelle/HOL are fully automatic.

Finite axioms are sound but incomplete; infinitary axioms are complete.

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 \,\Diamond\, F^{*} \bot = \Diamond\, F^{*} \bot$$ states in AIC that $\sup_n F^n (\bot)$ -- 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. Under suitable continuity conditions, it obtains fixed points as lattice-theoretic limit inferiors and limit superiors of iterating an endomap on an arbitrary seed element. 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.