Well-Founded Coalgebras Meet Kőnig’s Lemma
Urbat H, Wißmann T (2026)
Publication Type: Conference contribution
Publication year: 2026
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 363
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Paris
ISBN: 9783959774116
DOI: 10.4230/LIPIcs.CSL.2026.24
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 C, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on C 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.
Authors with CRIS profile
Henning Urbat
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Thorsten Wißmann
Lehrstuhl für Informatik 8 (Theoretische Informatik)
How to cite
APA:
Urbat, H., & Wißmann, T. (2026). Well-Founded Coalgebras Meet Kőnig’s Lemma. In Stefano Guerrini, Barbara Konig (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Paris, FR: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Urbat, Henning, and Thorsten Wißmann. "Well-Founded Coalgebras Meet Kőnig’s Lemma." Proceedings of the 34th EACSL Annual Conference on Computer Science Logic, CSL 2026, Paris Ed. Stefano Guerrini, Barbara Konig, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2026.
BibTeX: Download