eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-11-08
5:1
5:20
10.4230/LIPIcs.CALCO.2021.5
article
Initial Algebras Without Iteration ((Co)algebraic pearls)
Adámek, Jiří
1
2
Milius, Stefan
3
https://orcid.org/0000-0002-2021-1644
Moss, Lawrence S.
4
Czech Technical University in Prague, Czech Republic
Technische Universität Braunschweig, Germany
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Indiana University, Bloomington, IN, USA
The Initial Algebra Theorem by Trnková et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point A of the functor, it uses Pataraia’s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of A. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.5/LIPIcs.CALCO.2021.5.pdf
Initial algebra
Pataraia’s theorem
recursive coalgebra
initial-algebra chain