Document Open Access Logo

Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot

Authors Paul Blain Levy , Sergey Goncharov

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2019.13.pdf
  • Filesize: 0.51 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Axiomatic semantics
Keywords
  • Guarded iteration
  • guarded monads
  • coalgebraic resumptions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Paul Blain Levy and Sergey Goncharov. Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CALCO.2019.13

Author Details

Paul Blain Levy
  • University of Birmingham, UK
Sergey Goncharov
  • FAU Erlangen-Nürnberg, Germany

Funding

  • Goncharov, Sergey: Support by Deutsche Forschungsgemeinschaft (DFG) under project GO 2161/1-2 is gratefully acknowledged.

References

  1. J. Adámek, R. Börger, S. Milius, and J. Velebil. Iterative algebras: How iterative are they? Theory Appl. Cat., 19:61-92, 2008. Google Scholar
  2. Stephen Bloom and Zoltán Ésik. Iteration theories: the equational logic of iterative processes. Springer, 1993. Google Scholar
  3. F. Borceux. Handbook of Categorical Algebra 1. Cambridge University Press, 1994. Google Scholar
  4. 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. Google Scholar
  5. Venanzio Capretta. General recursion via coinductive types. Log. Meth. Comput. Sci., 1(2), 2005. Google Scholar
  6. Pietro Cenciarelli and Eugenio Moggi. A syntactic approach to modularity in denotational semantics. In Category Theory and Computer Science, CTCS 1993, 1993. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob. Unguarded Recursion on Coinductive Resumptions. Logical Methods in Computer Science, 14(3), 2018. Google Scholar
  10. 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. Google Scholar
  11. Masahito Hasegawa. Models of Sharing Graphs: A Categorical Semantics of Let and Letrec. Springer, 1999. Google Scholar
  12. 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. Google Scholar
  13. Martin Hyland, Paul Levy, Gordon Plotkin, and John Power. Combining algebraic effects with continuations. Theoret. Comput. Sci., 375(1-3):20-40, 2007. Google Scholar
  14. Martin Hyland, Gordon Plotkin, and John Power. Combining Computational Effects: Commutativity & Sum. In TCS'02, volume 223, pages 474-484. Kluwer, 2002. Google Scholar
  15. Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoret. Comput. Sci., 357(1-3):70-99, 2006. Google Scholar
  16. Stefan Milius. Completely iterative algebras and completely iterative monads. Inf. Comput., 196(1):1-41, 2005. Google Scholar
  17. R. Milner. Communication and concurrency. Prentice-Hall, 1989. Google Scholar
  18. Eugenio Moggi. Notions of Computation and Monads. Inf. Comput., 93:55-92, 1991. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. 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.
  22. Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Logic in Computer Science, LICS 2000, pages 30-41, 2000. Google Scholar
  23. Tarmo Uustalu. Generalizing Substitution. ITA, 37(4):315-336, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact