Document Open Access Logo

Initial Algebras Without Iteration ((Co)algebraic pearls)

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

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Jiří Adámek
  • Czech Technical University in Prague, Czech Republic
  • Technische Universität Braunschweig, Germany
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lawrence S. Moss
  • Indiana University, Bloomington, IN, USA

Funding

  • Adámek, Jiří: Supported by the grant No. 19-0092S of the Czech Grant Agency.
  • Milius, Stefan: Supported by Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1 and as part of the Research and Training Group 2475 "Cybercrime and Forensic Computing" (393541319/GRK2475/1-2019).
  • Moss, Lawrence S.: Supported by grant #586136 from the Simons Foundation.

Cite AsGet BibTex

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
    PDF Downloads
    0
    Metadata Views

References

  1. Jiří Adámek. Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carolin., 15:589-602, 1974. Google Scholar
  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. Google Scholar
  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. Google Scholar
  5. Andrej Bauer and Peter Lefanu Lumsdane. On the Bourbaki-Witt principle in toposes. Math. Structures Comput. Sci., 155(1):87-99, 2013. Google Scholar
  6. Nicolas Bourbaki. Sur le théorème de Zorn. Arch. Math., 2:434-437, 1949. Google Scholar
  7. Georg Cantor. Über eine elementare frage der Mannigfaltigkeitslehre. Jahresbericht der Deutschen Mathematiker-Vereinigung, 1:75-78, 1891. Google Scholar
  8. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inform. and Comput., 204:437-468, 2006. Google Scholar
  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. Google Scholar
  11. Martín Escardó. Joins in the complete Heyting algebra of nuclei. Appl. Categ. Structures, 11:117-124, 2003. Google Scholar
  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. Google Scholar
  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. Google Scholar
  15. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Math. Structures Comput. Sci., 27:1111-1131, 2017. Google Scholar
  16. Bronislav Knaster. Un theéorème sur les fonctions d'ensembles. Ann. Soc. Pol. Math., 6:133-134, 1928. Google Scholar
  17. Joachim Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151-161, 1968. Google Scholar
  18. George Markowsky. Chain-complete posets and directed sets with applications. Algebra Universalis, 6(1):53-68, 1976. Google Scholar
  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. Google Scholar
  20. G. Osius. Categorical set theory: a characterization of the category of sets. J. Pure Appl. Algebra, 4(79-119), 1974. Google Scholar
  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. Google Scholar
  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. Google Scholar
  24. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5(2):285-309, 1955. Google Scholar
  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. Google Scholar
  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. Google Scholar
  29. Věra Trnková. On a descriptive classification of set functors I. Comment. Math. Univ. Carolin., 12:143-174, 1971. Google Scholar
  30. Ernst Witt. Beweisstudien zum Satz von M. Zorn. Math. Nachr., 4:434-438, 1951. Google Scholar
  31. Ernst Zermelo. Beweis, daß jede Menge wohlgeordnet werden kann. Math. Ann., 59:514-516, 1904. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact