Coinductive resumption monads: Guarded iterative and guarded Elgot
Levy PB, Goncharov S (2019)
Publication Type: Conference contribution
Publication year: 2019
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 139
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: London
ISBN: 9783959771207
DOI: 10.4230/LIPIcs.CALCO.2019.13
Abstract
We introduce a new notion of “guarded Elgot monad”, that is a monad equipped with a form of iteration. It requires every guarded morphism to have a specified fixpoint, and classical equational laws of iteration to be satisfied. This notion includes Elgot monads, but also further examples of partial non-unique iteration, emerging in the semantics of processes under infinite trace equivalence. We recall the construction of the “coinductive resumption monad” from a monad and endofunctor, that is used for modelling programs up to bisimilarity. We characterize this construction via a universal property: if the given monad is guarded Elgot, then the coinductive resumption monad is the guarded Elgot monad that freely extends it by the given endofunctor.
Authors with CRIS profile
Involved external institutions
How to cite
APA:
Levy, P.B., & Goncharov, S. (2019). Coinductive resumption monads: Guarded iterative and guarded Elgot. In Markus Roggenbach, Ana Sokolova (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. London, GB: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Levy, Paul Blain, and Sergey Goncharov. "Coinductive resumption monads: Guarded iterative and guarded Elgot." Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019, London Ed. Markus Roggenbach, Ana Sokolova, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019.
BibTeX: Download