Document Open Access Logo

Well-Founded Coalgebras Meet Kőnig’s Lemma

Authors Henning Urbat , Thorsten Wißmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.24.pdf
  • Filesize: 1.05 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • Kőnig’s Lemma
  • Well-Foundedness
  • Coalgebra

Metrics

Abstract

Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.

Cite As Get BibTex

Henning Urbat and Thorsten Wißmann. Well-Founded Coalgebras Meet Kőnig’s Lemma. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.24

Author Details

Henning Urbat
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Thorsten Wißmann
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Urbat, Henning: Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project numbers 470467389 and 569130867.

Acknowledgements

The authors thank Stefan Milius for inspiring discussions on well-founded coalgebras, and Dominik Kirst for pointing out the relevance of Kőnig’s lemma and its relatives in reverse constructive mathematics.

References

  1. J. Adámek and H.-E. Porst. On tree coalgebras and coalgebra presentations. Theoretical Computer Science, 311(1):257-283, 2004. URL: https://doi.org/10.1016/S0304-3975(03)00378-5.
  2. Jirí Adámek, Stefan Milius, and Jirí Velebil. Free iterative theories: a coalgebraic view. Math. Struct. Comput. Sci., 13(2):259-320, 2003. URL: https://doi.org/10.1017/S0960129502003924.
  3. Jiří Adámek. Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carol., 15(4):589-602, 1974. Google Scholar
  4. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2025. URL: https://doi.org/10.1017/9781108884112.
  5. Jiří Adámek, Stefan Milius, Lurdes Sousa, and Thorsten Wißmann. On finitary functors. Theory Appl. Categ., 34(35):1134-1164, October 2019. Google Scholar
  6. Jiří Adámek, Stefan Milius, and Jiří Velebil. Iterative algebras at work. Math. Struct. Comput. Sci., 16(6):1085-1131, 2006. URL: https://doi.org/10.1017/S0960129506005706.
  7. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9780511600579.
  8. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  9. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  10. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism, probability, and termination. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/lmcs-18(2:21)2022.
  11. Luitzen E. J. Brouwer. Über Definitionsbereiche von Funktionen. Math. Ann., 97(1):60-75, 1927. URL: https://doi.org/10.1007/BF01447860.
  12. Doron Bustan, Sasha Rubin, and Moshe Y. Vardi. Verifying ω-regular properties of Markov chains. In 16th International on Computer Aided Verification (CAV 2004), volume 3114 of Lect. Notes Comput. Sci., pages 189-201. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_15.
  13. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inf. Comput., 204(4):437-468, 2006. URL: https://doi.org/10.1016/J.IC.2005.08.005.
  14. Aurelio Carboni, Stephen Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. J. Pure Appl. Algebra, 84(2):145-158, 1993. URL: https://doi.org/10.1016/0022-4049(93)90035-R.
  15. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88-98, 2011. URL: https://doi.org/10.1145/1941487.1941509.
  16. Hannes Diener and Hajime Ishihara. Bishop-style constructive reverse mathematics. In Vasco Brattka and Peter Hertling, editors, Handbook of Computability and Complexity in Analysis, pages 347-365. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-59234-9_10.
  17. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  18. Tomasz Gogacz, Henryk Michalewski, Matteo Mio, and Michał Skrzypczak. Measure properties of game tree languages. In 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014), volume 8635 of Lect. Notes Comput. Sci., pages 303-314. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_26.
  19. Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Bialgebraic reasoning on stateful languages, 2025. To appear in 30th ACM SIGPLAN International Conference on Functional Programming (IFCP 2025). URL: https://doi.org/10.48550/arXiv.2503.10955.
  20. Denis R. Hirschfeldt. Slicing the Truth: On the Computable and Reverse Mathematics of Combinatorial Principles. World Scientific, 2014. URL: https://doi.org/10.1142/9208.
  21. Paul Howard and Jean E. Rubin. Consequences of the Axiom of Choice. American Mathematical Society, 1998. URL: https://doi.org/10.1017/S1079898600003449.
  22. Tomasz Idziaszek, Michał Skrzypczak, and Mikołaj Bojańczyk. Regular languages of thin trees. Theory Comput. Syst., 58(4):614-663, 2016. URL: https://doi.org/10.1007/S00224-014-9595-Z.
  23. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  24. Thomas Jech. Set Theory: The Third Millennium Edition. Springer, 2002. URL: https://doi.org/10.1007/3-540-44761-X.
  25. Peter T Johnstone. Sketches of an elephant. Oxford logic guides. Oxford Univ. Press, New York, NY, 2002. URL: https://doi.org/10.1017/S1079898600003462.
  26. Peter T Johnstone. Topos Theory. Dover Publications, 2014. Google Scholar
  27. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  28. Dénes Kőnig. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged), 3(2-3):121-130, 1927. Google Scholar
  29. Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103:151-161, 1968. URL: https://doi.org/10.1007/BF01110627.
  30. Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, 2 edition, 1978. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  31. Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion - the locally finite fixpoint and its properties. In Bart Jacobs and Christof Löding, editors, Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016), volume 9634 of LNCS, pages 107-125. Springer, April 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_7.
  32. Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion and iterative algebras. Information and Computation, pages 1-28, 2020. Article 104456. URL: https://doi.org/10.1016/j.ic.2019.104456.
  33. Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Regular behaviours with names. Applied Categorical Structures, 24(5):663-701, August 2016. URL: https://doi.org/10.1007/s10485-016-9457-8.
  34. Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), pages 1-14, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470717.
  35. Matteo Mio and Valeria Vignudelli. Monads and Quantitative Equational Theories for Nondeterminism and Probability. In 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of LIPIcs, pages 28:1-28:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.28.
  36. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139084673.
  37. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  38. Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110-3148, 2015. URL: https://doi.org/10.1016/j.jpaa.2014.10.005.
  39. Marshall H. Stone. Postulates for the barycentric calculus. Ann. Mat. Pura Appl., 29(1):25-30, 1949. URL: https://doi.org/10.1007/BF02413910.
  40. László Székely. Ramsey theory (Lecture notes). https://people.math.sc.edu/laszlo/Ramsey2.pdf, 2023.
  41. Paul Taylor. Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999. URL: https://doi.org/10.2307/3621547.
  42. Paul Teller. A Modern Formal Logic Primer: Predicate Logic and Metatheory, Volume II. Prentice Hall, 1989. Google Scholar
  43. Věra Trnková. On descriptive classification of set-functors. I. Comment. Math. Univ. Carol., 12(1):143-174, 1971. Google Scholar
  44. Henning Urbat. Finite Behaviours and Finitary Corecursion. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.24.
  45. Thorsten Wißmann and Stefan Milius. Initial algebras unchained - A novel initial algebra construction formalized in Agda. In 9th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024). ACM, 2024. URL: https://doi.org/10.1145/3661814.3662105.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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