| Autor: |
Adámek, Jiří, Milius, Stefan, Moss, Lawrence S. |
| Rok vydání: |
2021 |
| Předmět: |
|
| Zdroj: |
Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), volume 211 of LIPIcs, pages 5:1-5:20 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.4230/LIPIcs.CALCO.2021.5 |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
