Todd Schmid

Todd Schmid

Axiomatizing covarieties of coalgebras for an endofunctor is less intuitive than axiomatizing varieties of algebras via equations (Dahlqvist and Schmid, 2022). Existing techniques come from coalgebraic modal logic, pattern avoidance specifications, and hidden algebra. We introduce equational path constraints, a well-behaved and relatively easy to describe class of finitary behavioural properties that provide an algebra-flavoured alternative to coequations. The basic idea is to assign a pair of values to each path through a coalgebra and posit that the two values coincide. We show that equational path constraints define covarieties and construct final coalgebras relative to equational path constraints in some concrete cases. We connect equational path constraints to coequations when values computed from paths live in a monad, and we compute an upper bound on the number of colours needed to express the coequation. One of our constructions is reminiscent of the initial/terminal sequences of (Adámek, 1974) and (Barr, 1993). Motivating examples include commutativity conditions in automata theory, differential equations, bi-infinite streams, and frame conditions.

Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer et al.

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.