Adámek, Jiří ;
Milius, Stefan ;
Moss, Lawrence S.
Initial Algebras Without Iteration ((Co)algebraic pearls)
Abstract
The Initial Algebra Theorem by Trnková et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a prefixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initialalgebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given prefixed 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 directedcomplete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initialalgebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.
BibTeX  Entry
@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.5,
author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.},
title = {{Initial Algebras Without Iteration}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {5:15:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772129},
ISSN = {18688969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15360},
URN = {urn:nbn:de:0030drops153606},
doi = {10.4230/LIPIcs.CALCO.2021.5},
annote = {Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initialalgebra chain}
}
08.11.2021
Keywords: 

Initial algebra, Pataraia’s theorem, recursive coalgebra, initialalgebra chain 
Seminar: 

9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Issue date: 

2021 
Date of publication: 

08.11.2021 