License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2021.5
URN: urn:nbn:de:0030-drops-153606
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15360/
Go to the corresponding LIPIcs Volume Portal

Adámek, Jiří ; Milius, Stefan ; Moss, Lawrence S.

Initial Algebras Without Iteration ((Co)algebraic pearls)

pdf-format:
LIPIcs-CALCO-2021-5.pdf (0.7 MB)

Abstract

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.

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:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15360},
  URN =		{urn:nbn:de:0030-drops-153606},
  doi =		{10.4230/LIPIcs.CALCO.2021.5},
  annote =	{Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra chain}
}

Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra chain
Collection: 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Issue Date: 2021
Date of publication: 08.11.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI