An Initial Algebra Theorem Without Iteration

DOI10.4230/LIPICS.CALCO.2021.5arXiv2104.09837MaRDI QIDQ6365711

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

Publication date: 20 April 2021

Abstract: The Initial Algebra Theorem by Trnkov'a 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.

This page was built for publication: An Initial Algebra Theorem Without Iteration

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6365711)