Initial algebras without iteration

Adámek J, Milius S, Moss LS (2021)

Publication Type: Conference contribution

Publication year: 2021

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 211

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Virtual, Salzburg, AUT

ISBN: 9783959772129

DOI: 10.4230/LIPIcs.CALCO.2021.5

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.

Authors with CRIS profile

Stefan Milius Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

Czech Technical University in Prague / České vysoké učení technické v Praze CZ Czech Republic (CZ) Indiana University US United States (USA) (US)

How to cite

APA:

Adámek, J., Milius, S., & Moss, L.S. (2021). Initial algebras without iteration. In Fabio Gadducci, Alexandra Silva, Alexandra Silva (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Virtual, Salzburg, AUT: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Adámek, Jiří, Stefan Milius, and Lawrence S. Moss. "Initial algebras without iteration." Proceedings of the 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, Virtual, Salzburg, AUT Ed. Fabio Gadducci, Alexandra Silva, Alexandra Silva, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021.

BibTeX: Download