Abstract
We introduce a new notion of “guarded Elgot monad”, that is a monad equipped with a form ofiteration. 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.
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.
Original language | English |
---|---|
Title of host publication | 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) |
Editors | Markus Roggenbach, Ana Sokolova |
Publisher | Schloss Dagstuhl |
Pages | 13:1--13:17 |
Number of pages | 18 |
Volume | 139 |
ISBN (Print) | 978-3-95977-120-7 |
DOIs | |
Publication status | Published - 31 Dec 2019 |
Event | 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) - UCL Bloomsbury Campus, London, United Kingdom Duration: 3 Jun 2019 → 6 Jun 2019 |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Publisher | Schloss-Dagstuhl |
ISSN (Electronic) | 1868-8969 |
Conference
Conference | 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) |
---|---|
Country/Territory | United Kingdom |
City | London |
Period | 3/06/19 → 6/06/19 |
Keywords
- guarded iteration
- guarded monads
- coalgebraic resumptions