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.

翻译：固定点是计算机科学中的一个常见主题，通常被构造为适当初始化的不动点迭代的极限。我们提出迭代构造代数（AIC）——一种纯粹代数的框架，用于推理完全格上连续自映射的不动点迭代。AIC 通过等式逻辑推导构造性不动点定理，避免了显式的指标计算。例如，公式 $$F \,\Diamond\, F^{*} \bot = \Diamond\, F^{*} \bot$$ 在 AIC 中表明 $\sup_n F^n (\bot)$ ——该构造源自 Kleene 不动点定理——是 $F$ 的一个不动点。我们通过给出多个已知与较少知的不动点定理的代数证明，展示了 AIC 的适用性：其中我们证明了 Tarski-Kantorovich 原理——Kleene 不动点定理的推广——以及 $k$-归纳法的一种不动点理论推广——该方法常用于软件验证。此外，我们提出一个新的不动点定理：在适当的连续性条件下，该定理通过格论中的下极限和上极限，得到从任意种子元素迭代自映射的不动点。我们已在 Isabelle/HOL 中实现了该代数框架。Isabelle 的 sledgehammer 工具能够全自动地找到上述不动点定理的证明。最后，我们研究 AIC 公理系统的完备性。我们证明：（a）有限的有限性公理集对 AIC 的标准模型（完全格中的元素序列）是可靠但不完备的；（b）另一个不同的有限无限性公理集是完备的。我们还证明无限性公理不可避免：不存在由有限条有限性公理给出的标准模型的完备公理化。