Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot
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.
Guarded iteration
guarded monads
coalgebraic resumptions
Theory of computation~Categorical semantics
Theory of computation~Axiomatic semantics
13:1-13:17
Regular Paper
Paul Blain
Levy
Paul Blain Levy
University of Birmingham, UK
https://orcid.org/0000-0003-0864-1876
Sergey
Goncharov
Sergey Goncharov
FAU Erlangen-Nürnberg, Germany
https://orcid.org/0000-0001-6924-8766
Support by Deutsche Forschungsgemeinschaft (DFG) under project GO 2161/1-2 is gratefully acknowledged.
10.4230/LIPIcs.CALCO.2019.13
J. Adámek, R. Börger, S. Milius, and J. Velebil. Iterative algebras: How iterative are they? Theory Appl. Cat., 19:61-92, 2008.
Stephen Bloom and Zoltán Ésik. Iteration theories: the equational logic of iterative processes. Springer, 1993.
F. Borceux. Handbook of Categorical Algebra 1. Cambridge University Press, 1994.
N. Bowler, P.B. Levy, and G.D. Plotkin. Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies. In Proceedings, 34th Conference on the Mathematical Foundations of Programming Semantics, volume 341 of ENTCS, pages 23-44, 2018.
Venanzio Capretta. General recursion via coinductive types. Log. Meth. Comput. Sci., 1(2), 2005.
Pietro Cenciarelli and Eugenio Moggi. A syntactic approach to modularity in denotational semantics. In Category Theory and Computer Science, CTCS 1993, 1993.
Sergey Goncharov, Stefan Milius, and Christoph Rauch. Complete Elgot Monads and Coalgebraic Resumptions. In Mathematical Foundations of Programming Semantics, MFPS 2016, volume 325 of ENTCS, pages 147-168. Elsevier, 2016.
Sergey Goncharov and Lutz Schröder. Guarded Traced Categories. In Christel Baier and Ugo Dal Lago, editors, Proc. 21th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018), volume 10803 of LNCS, pages 313-330. Springer, 2018.
Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob. Unguarded Recursion on Coinductive Resumptions. Logical Methods in Computer Science, 14(3), 2018.
Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg. Unifying Guarded and Unguarded Iteration. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2017, volume 10203 of LNCS, pages 517-533. Springer, 2017.
Masahito Hasegawa. Models of Sharing Graphs: A Categorical Semantics of Let and Letrec. Springer, 1999.
Masihito Hasegawa. Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi. In Typed Lambda Calculi and Applications, TLCA 1997, volume 1210 of LNCS, pages 196-213. Springer, 1997.
Martin Hyland, Paul Levy, Gordon Plotkin, and John Power. Combining algebraic effects with continuations. Theoret. Comput. Sci., 375(1-3):20-40, 2007.
Martin Hyland, Gordon Plotkin, and John Power. Combining Computational Effects: Commutativity & Sum. In TCS'02, volume 223, pages 474-484. Kluwer, 2002.
Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoret. Comput. Sci., 357(1-3):70-99, 2006.
Stefan Milius. Completely iterative algebras and completely iterative monads. Inf. Comput., 196(1):1-41, 2005.
R. Milner. Communication and concurrency. Prentice-Hall, 1989.
Eugenio Moggi. Notions of Computation and Monads. Inf. Comput., 93:55-92, 1991.
Maciej Piróg and Jeremy Gibbons. The Coinductive Resumption Monad. In Mathematical Foundations of Programming Semantics, MFPS 2014, volume 308 of ENTCS, pages 273-288, 2014.
Maciej Piróg and Jeremy Gibbons. Monads for Behaviour. In Mathematical Foundations of Programming Semantics, MFPS 2013, volume 298 of ENTCS, pages 309-324, 2015.
A. W. Roscoe. Unbounded nondeterminism in CSP. Technical Report PRG-67, Oxford University Computing Laboratory, July 1988. in Two papers on CSP, Also appeared in Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993). URL: http://www.cs.ox.ac.uk/people/bill.roscoe/publications/28.ps.
http://www.cs.ox.ac.uk/people/bill.roscoe/publications/28.ps
Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Logic in Computer Science, LICS 2000, pages 30-41, 2000.
Tarmo Uustalu. Generalizing Substitution. ITA, 37(4):315-336, 2003.
Paul Blain Levy and Sergey Goncharov
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode