10.4230/LIPICS.CSL.2011.5
Adamek, Jiri
Jiri
Adamek
Milius, Stefan
Stefan
Milius
Moss, Lawrence S.
Lawrence S.
Moss
Sousa, Lurdes
Lurdes
Sousa
Power-Set Functors and Saturated Trees
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
saturated tree
extensional tree
final coalgebra
power-set functor
modal logic
Bezem, Marc
Marc
Bezem
2011
2011-08-31
2011-08-31
2011-08-31
en
urn:nbn:de:0030-drops-32194
10.4230/LIPIcs.CSL.2011
978-3-939897-32-3
1868-8969
10.4230/LIPIcs.CSL.2011
LIPIcs, Volume 12, CSL 2011
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
2013
12
5
5
19
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Bezem, Marc
Marc
Bezem
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
12
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
15 pages
446591 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
We combine ideas coming from several fields, including modal logic, coalgebra, and set theory. Modally saturated trees were introduced by K. Fine in 1975. We give a new purely combinatorial formulation of modally saturated trees, and we prove that they form the limit of the final omega-op-chain of the finite power-set functor Pf. From that, we derive an alternative proof of J. Worrell's description of the final coalgebra as the coalgebra of all strongly extensional, finitely branching trees. In the other direction, we represent the final coalgebra for Pf in terms of certain maximal consistent sets in the modal logic K. We also generalize Worrell's result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor Mf studied by H. P. Gumm and T. Schröder. We introduce the concept of an i-saturated tree for all ordinals i, and then prove that the i-th step in the final chain of the power set functor consists of all i-saturated trees. This leads to a new description of the final coalgebra for the restricted power-set functors Plambda (of subsets of cardinality smaller than lambda).
LIPIcs, Vol. 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, pages 5-19