Coinductive resumption monads: guarded iterative and guarded Elgot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • FAU Erlangen-Nürnberg

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.

Details

Original languageEnglish
Title of host publication8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
EditorsMarkus Roggenbach, Ana Sokolova
Publication statusAccepted/In press - 27 May 2019
Event8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) - UCL Bloomsbury Campus, London, United Kingdom
Duration: 3 Jun 20196 Jun 2019

Publication series

NameLIPIcs–Leibniz International Proceedings in Informatics
PublisherSchloss-Dagstuhl
ISSN (Electronic)1868-8969

Conference

Conference8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
CountryUnited Kingdom
CityLondon
Period3/06/196/06/19

Keywords

  • Guarded iteration, guarded monads, coalgebraic resumptions