Coinductive resumption monads: guarded iterative and guarded Elgot

Paul Blain Levy; Sergey  Goncharov

doi:10.4230/LIPIcs.CALCO.2019.13

Coinductive resumption monads: guarded iterative and guarded Elgot

Paul Blain Levy, Sergey Goncharov

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

104 Downloads (Pure)

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.

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	https://doi.org/10.4230/LIPIcs.CALCO.2019.13
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

Access to Document

10.4230/LIPIcs.CALCO.2019.13Licence: Creative Commons: Attribution (CC BY)

Levy_&_Goncharov_Coinductive_resumption_monads_CALCO_2019Final published version, 523 KBLicence: Creative Commons: Attribution (CC BY)

https://drops.dagstuhl.de/opus/volltexte/2019/11441/

Cite this

Levy, P. B., & Goncharov, S. (2019). Coinductive resumption monads: guarded iterative and guarded Elgot. In M. Roggenbach, & A. Sokolova (Eds.), 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) (Vol. 139, pp. 13:1--13:17). (Leibniz International Proceedings in Informatics (LIPIcs)). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.CALCO.2019.13

@inproceedings{2c49a3ba806f48f7bdcf755a2c315894,

title = "Coinductive resumption monads: guarded iterative and guarded Elgot",

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.",

keywords = "guarded iteration, guarded monads, coalgebraic resumptions",

author = "Levy, {Paul Blain} and Sergey Goncharov",

year = "2019",

month = dec,

day = "31",

doi = "10.4230/LIPIcs.CALCO.2019.13",

language = "English",

isbn = "978-3-95977-120-7",

volume = "139",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl",

pages = "13:1----13:17",

editor = "Markus Roggenbach and Ana Sokolova",

booktitle = "8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)",

address = "Germany",

note = "8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) ; Conference date: 03-06-2019 Through 06-06-2019",

}

Levy, PB & Goncharov, S 2019, Coinductive resumption monads: guarded iterative and guarded Elgot. in M Roggenbach & A Sokolova (eds), 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). vol. 139, Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl, pp. 13:1--13:17, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), London, United Kingdom, 3/06/19. https://doi.org/10.4230/LIPIcs.CALCO.2019.13

Coinductive resumption monads: guarded iterative and guarded Elgot. / Levy, Paul Blain; Goncharov, Sergey .
8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). ed. / Markus Roggenbach; Ana Sokolova. Vol. 139 Schloss Dagstuhl, 2019. p. 13:1--13:17 (Leibniz International Proceedings in Informatics (LIPIcs)).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Coinductive resumption monads

T2 - 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

AU - Levy, Paul Blain

AU - Goncharov, Sergey

PY - 2019/12/31

Y1 - 2019/12/31

N2 - 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.

AB - 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.

KW - guarded iteration

KW - guarded monads

KW - coalgebraic resumptions

U2 - 10.4230/LIPIcs.CALCO.2019.13

DO - 10.4230/LIPIcs.CALCO.2019.13

M3 - Conference contribution

SN - 978-3-95977-120-7

VL - 139

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 13:1--13:17

BT - 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

A2 - Roggenbach, Markus

A2 - Sokolova, Ana

PB - Schloss Dagstuhl

Y2 - 3 June 2019 through 6 June 2019

ER -

Coinductive resumption monads: guarded iterative and guarded Elgot

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this