Document

# Initial Algebras Without Iteration ((Co)algebraic pearls)

## File

LIPIcs.CALCO.2021.5.pdf
• Filesize: 0.72 MB
• 20 pages

## Cite As

Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras Without Iteration ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/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.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Models of computation
• Theory of computation → Logic and verification
##### Keywords
• Initial algebra
• Pataraia’s theorem
• recursive coalgebra
• initial-algebra chain

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Jiří Adámek. Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carolin., 15:589-602, 1974.
2. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. On well-founded and recursive coalgebras. In Barbara König and Jean Goubault-Larrecq, editors, Proc. Foundations of Software Science and Computation Structures (FoSSaCS), volume 12077 of Lecture Notes Comput. Sci. (ARCoSS), pages 17-36. Springer, 2020.
3. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial algebras, terminal coalgebras, and the theory of fixed points of functors. draft book, available at https://www8.cs.fau.de/ext/milius/publications/files/CoalgebraBook.pdf, 2021.
4. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. Cambridge University Press, 1994.
5. Andrej Bauer and Peter Lefanu Lumsdane. On the Bourbaki-Witt principle in toposes. Math. Structures Comput. Sci., 155(1):87-99, 2013.
6. Nicolas Bourbaki. Sur le théorème de Zorn. Arch. Math., 2:434-437, 1949.
7. Georg Cantor. Über eine elementare frage der Mannigfaltigkeitslehre. Jahresbericht der Deutschen Mathematiker-Vereinigung, 1:75-78, 1891.
8. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inform. and Comput., 204:437-468, 2006.
9. France Dacar. The join-induction principle for closure operators on dcpos. Available from http://dis.ijs.si/France/, January 2009.
10. Adam Eppendahl. Coalgebra-to-algebra morphisms. In Proc. Category Theory and Computer Science (CTCS), volume 29 of Electron. Notes Theor. Comput. Sci., pages 42-49, 1999.
11. Martín Escardó. Joins in the complete Heyting algebra of nuclei. Appl. Categ. Structures, 11:117-124, 2003.
12. Peter Freyd. Remarks on algebraically compact categories. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of category theory in computer science: Proceedings of the London Mathematical Society Symposium, Durham 1991, volume 177 of London Mathematical Society Lecture Note Series, pages 95-106. Cambridge University Press, 1992.
13. Jean Goubault-Larrecq. Bourbaki, Witt, and Dito Pataraia. available at https://projects.lsv.ens-cachan.fr/topology/?page_id=176, June 2021.
14. Friedrich Hartogs. Über das Problem der Wohlordnung. Math. Ann., 76(4):438-443, 1915.
15. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Math. Structures Comput. Sci., 27:1111-1131, 2017.
16. Bronislav Knaster. Un theéorème sur les fonctions d'ensembles. Ann. Soc. Pol. Math., 6:133-134, 1928.
17. Joachim Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151-161, 1968.
18. George Markowsky. Chain-complete posets and directed sets with applications. Algebra Universalis, 6(1):53-68, 1976.
19. Keye Martin. Nothing can be fixed. In Computation, logic, games, and quantum foundations, volume 7860 of Lecture Notes in Comput. Sci., pages 195-196. Springer, Heidelberg, 2013.
20. G. Osius. Categorical set theory: a characterization of the category of sets. J. Pure Appl. Algebra, 4(79-119), 1974.
21. Dito Pataraia. A constructive proof of Tarski’s fixed-point theorem for dcpo’s. Presented at the 65th Peripatetic Seminar on Sheaves and Logic, Aarhus, November 1997.
22. Andrew M. Pitts and S. C. Steenkamp. Constructing initial algebras using inflationary iteration, 2021. URL: http://arxiv.org/abs/2105.03252.
23. M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM J. Comput., 11(4):761-783, 1982.
24. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5(2):285-309, 1955.
25. Paul Taylor. Towards a unified treatment of induction I: the general recursion theorem. preprint, available at https://www.paultaylor.eu/ordinals/#towuti, 1995-6.
26. Paul Taylor. Practical Foundations of Mathematics. Cambridge University Press, 1999.
27. Paul Taylor. Well founded coalgebras and recursion. available at https://www.paultaylor.eu/ordinals/welfcr.pdf, April 2021.
28. V. Trnková, J. Adámek, V. Koubek, and J. Reiterman. Free algebras, input processes and free monads. Comment. Math. Univ. Carolin., 16:339-351, 1975.
29. Věra Trnková. On a descriptive classification of set functors I. Comment. Math. Univ. Carolin., 12:143-174, 1971.
30. Ernst Witt. Beweisstudien zum Satz von M. Zorn. Math. Nachr., 4:434-438, 1951.
31. Ernst Zermelo. Beweis, daß jede Menge wohlgeordnet werden kann. Math. Ann., 59:514-516, 1904.
X

Feedback for Dagstuhl Publishing