LIPIcs.CALCO.2017.5.pdf
- Filesize: 0.58 MB
- 16 pages
Document
Monoidal Company for Accessible Functors
Authors
-
Part of:
Volume:
7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-11-17
Cite As Get BibTex
Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal Company for Accessible Functors. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CALCO.2017.5
Abstract
Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties. Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.
Subject Classification
Keywords
- coalgebras
- distributive laws
- accessible functors
- monoidal categories
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- J. Adamek, S. Milius, and L Moss. Initial algebras and terminal coalgebras: a survey. Preliminary version, 2010. URL: https://www.tu-braunschweig.de/Medien-DB/iti/survey_full.pdf.
- J. Adamek and J. Rosicky. Locally Presentable and Accessible Categories. Cambridge Tracts in Mathematics. Cambridge University Press, 1994. URL: https://books.google.nl/books?id=iXh6rOd7of0C.
-
F. Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004.
- Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal company for accessible functors (full version, with proofs). URL: https://hal.archives-ouvertes.fr/hal-01529340/.
-
Filippo Bonchi, Matias Lee, and Jurriaan Rot. Bisimilarity of open terms in stream GSOS. In FSEN, 2017. To appear.
- Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In CSL-LICS, pages 20:1-20:9. ACM, 2014. URL: http://arxiv.org/abs/1401.6675, URL: http://dx.doi.org/10.1145/2603088.2603149.
- Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in T.C.S. Cambridge University Press, 2016. URL: http://dx.doi.org/10.1017/CBO9781316823187.
- B. Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.03.023.
- Bartek Klin and Beata Nachyla. Presenting morphisms of distributive laws. In CALCO, volume 35 of LIPIcs, pages 190-204. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CALCO.2015.190.
-
B. Knaster. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématiques, 6:133-134, 1928.
- Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electronic Notes in Theoretical Computer Science, 33:230-260, 2000. URL: http://dx.doi.org/10.1016/S1571-0661(05)80350-0.
-
S. MacLane. Categories for the working mathematician. Springer, 1998.
-
M. Makkai and R. Paré. Accessible Categories: The Foundations of Categorical Model Theory, volume 104 of Contemporary mathematics - American Mathematical Society. American Mathematical Society, 1989.
- Joachim Parrow and Tjark Weber. The largest respectful function. Logical Methods in Computer Science, 12(2), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(2:11)2016.
- Damien Pous. Complete lattices and up-to techniques. In APLAS, volume 4807 of LNCS, pages 351-366. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-76637-7_24.
- Damien Pous. Coinduction all the way up. In LICS, pages 307-316. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2934564.
- Damien Pous and Jurriaan Rot. Companions, codensity and causality. In FoSSaCS, volume 10203 of LNCS, pages 106-123, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_7.
- John Power and Hiroshi Watanabe. Combining a monad and a comonad. Theoretical Computer Science, 280(1-2):137-162, 2002. URL: http://dx.doi.org/10.1016/S0304-3975(01)00024-X.
- Jan J. M. M. Rutten. A coinductive calculus of streams. Mathematical Structures in Computer Science, 15(1):93-147, 2005. URL: http://dx.doi.org/10.1017/S0960129504004517.
- Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(1:9)2013.
- Ross Street. The formal theory of monads. J. of Pure and Applied Algebra, 2(2):149-168, 1972. URL: http://dx.doi.org/10.1016/0022-4049(72)90019-9.
-
A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5(2):285-309, June 1955.
- D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In LICS, pages 280-291. IEEE, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614955.
- Hiroshi Watanabe. Well-behaved translations between structural operational semantics. Electronic Notes in Theoretical Computer Science, 65(1):337-357, 2002. URL: http://dx.doi.org/10.1016/S1571-0661(04)80372-4.