Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda
Thorsten Wißmann, Stefan Milius
TL;DR
The paper tackles constructing initial algebras for endofunctors $F$ without relying on ordinal-indexed chains, instead defining the initial algebra as the colimit of all finitary recursive coalgebras in a Fil-accessible locally presentable category. It proves that this colimit $(A,\alpha)$ is locally finrec, that $\alpha: A\to FA$ is an isomorphism via Lambek's lemma, and thus $\alpha^{-1}$ yields the initial $F$-algebra; the results are given with a fully constructive Agda formalization. This approach avoids transfinite recursion and aligns with rational fixed-point ideas, while ensuring constructivity and mechanized verification, with detailed treatment of colimit creation and universality. The work advances mechanized category theory by providing a general, constructive construction of initial algebras and sheds light on how finite-describeable coalgebras build up the canonical data types modulo behavioural equivalence, with potential implications for well-founded coalgebras and quotient-rich formalizations.
Abstract
The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra construction by Adámek (1974) starts with the initial object (e.g. the empty set) and successively applies the functor until a fixed point is reached, an idea inspired by Kleene's fixed point theorem. Depending on the functor of interest, this may require transfinitely many steps indexed by ordinal numbers until termination. We provide a new initial algebra construction which is not based on an ordinal-indexed chain. Instead, our construction is loosely inspired by Pataraia's fixed point theorem and forms the colimit of all finite recursive coalgebras. This is reminiscent of the construction of the rational fixed point of an endofunctor that forms the colimit of all finite coalgebras. For our main correctness theorem, we assume the given endofunctor is accessible on a (weak form of) locally presentable category. Our proofs are constructive and fully formalized in Agda.