Document Open Access Logo

Coinductive Reasoning for Parametrized Functors and Monads

Authors Ugo Dal Lago , Zeinab Galal

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.29.pdf
  • Filesize: 2.17 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Operational semantics
Keywords
  • categorical semantics
  • parametrized monads
  • effects
  • relations
  • lax extensions
  • behavioral equivalence
  • coalgebra
  • global state

Metrics

Abstract

Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs.
In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.

Cite As Get BibTex

Ugo Dal Lago and Zeinab Galal. Coinductive Reasoning for Parametrized Functors and Monads. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 29:1-29:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.29

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
Zeinab Galal
  • RIMS, Kyoto University, Japan

Funding

The first author was partly supported by the ANR Project HOPR (ANR-24-CE48-5521-01) and the second author was supported by the Research Institute for Mathematical Sciences (RIMS) and by the JSPS KAKENHI Grant 26K21167.

References

  1. Peter Aczel and Nax Mendler. A final coalgebra theorem. In Category Theory and Computer Science: Manchester, UK, September 5-8, 1989 Proceedings, pages 357-365. Springer, 2005. Google Scholar
  2. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, and Tetsuya Sato. Higher-order probabilistic adversarial computations: categorical semantics and program logics. Proc. ACM Program. Lang., 5(ICFP):1-30, 2021. URL: https://doi.org/10.1145/3473598.
  3. Robert Atkey. Substructural Simple Type Theories for Separation and In-place Update. PhD thesis, University of Edinburgh, College of Science and Engineering., 2006. Google Scholar
  4. Robert Atkey. Algebras for parameterised monads. In International Conference on Algebra and Coalgebra in Computer Science, pages 3-17. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_2.
  5. Robert Atkey. Parameterised notions of computation. Journal of functional programming, 19(3-4):335-376, 2009. URL: https://doi.org/10.1017/S095679680900728X.
  6. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral metrics via functor lifting. arXiv preprint arXiv:1410.3385, 2014. URL: https://arxiv.org/abs/1410.3385.
  7. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14, 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  8. Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, pages 39-55. Springer, 1969. Google Scholar
  9. Marta Bílková, Alexander Kurz, Daniela Petrişan, and Jiří Velebil. Relation liftings on preorders and posets. In Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011. Proceedings 4, pages 115-129. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22944-2_9.
  10. Marta Bilkova, Alexander Kurz, Daniela Petrisan, and Jiri Velebil. Relation lifting, with an application to the many-valued cover modality. Logical Methods in Computer Science, 9, 2013. Google Scholar
  11. Aurelio Carboni, G Max Kelly, and Richard J Wood. A 2-categorical approach to change of base and geometric morphisms i. Cahiers de topologie et géométrie différentielle catégoriques, 32(1):47-95, 1991. Google Scholar
  12. Eugenia Cheng, Nick Gurski, and Emily Riehl. Cyclic multicategories, multivariable adjunctions and mates. Journal of K-Theory, 13(2):337-396, 2014. URL: https://doi.org/10.1017/is013012007jkt250.
  13. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proceedings of the ACM on Programming Languages, 6(POPL):1-28, January 2022. URL: https://doi.org/10.1145/3498692.
  14. Soichiro Fujii. A 2-categorical study of graded and indexed monads. arXiv preprint arXiv:1904.08083, 2019. URL: https://arxiv.org/abs/1904.08083.
  15. Francesco Gavazzo, Riccardo Treglia, and Gabriele Vanoni. Monadic intersection types, relationally. In European Symposium on Programming, pages 22-51. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_2.
  16. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantalic behavioural distances. Google Scholar
  17. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Identity-Preserving Lax Extensions and Where to Find Them. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025), volume 327, pages 40:1-40:20, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2025.40.
  18. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Relators and notions of simulation revisited. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 776-789. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00064.
  19. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich Functors and Characteristic Logics for Behavioural Distances. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, volume 13992, pages 46-67. Springer Nature Switzerland, Cham, 2023. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-031-30829-1_3.
  20. John W Gray. Formal category theory: adjointness for 2-categories, volume 391. Springer, 2006. Google Scholar
  21. H Peter Gumm and Mehdi Zarrad. Coalgebraic simulations and congruences. In International Workshop on Coalgebraic Methods in Computer Science, pages 118-134. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44124-4_7.
  22. Dirk Hofmann, Gavin J Seal, and Walter Tholen. Monoidal Topology: A Categorical Approach to Order, Metric, and Topology, volume 153. Cambridge University Press, 2014. Google Scholar
  23. Bart Jacobs. Introduction to coalgebra, volume 59. Cambridge University Press, 2017. Google Scholar
  24. Niles Johnson and Donald Yau. 2-dimensional categories. Oxford University Press (UK), 2021. Google Scholar
  25. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 633-645, 2014. URL: https://doi.org/10.1145/2535838.2535846.
  26. Barbara König and Christina Mika-Michalski. (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In 29th International Conference on Concurrency Theory (CONCUR 2018), volume 118 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.37.
  27. Michael Lambert. Characterizing double categories of relations. Applied Category Theory, 2021. Google Scholar
  28. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science & Business Media, 1998. Google Scholar
  29. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, and Éric Tanter. Dijkstra monads for all. Proceedings of the ACM on Programming Languages, 3(ICFP):1-29, 2019. URL: https://doi.org/10.1145/3341708.
  30. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 81(5):880-900, 2015. URL: https://doi.org/10.1016/J.JCSS.2014.12.006.
  31. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  32. Susan Niefield. Cartesian closed double categories. Theory and Applications of Categories, 40(3):63-79, 2024. Google Scholar
  33. Pedro Nora, Jurriaan Rot, Lutz Schröder, and Paul Wild. Relational connectors and heterogeneous simulations. In International Conference on Foundations of Software Science and Computation Structures, pages 111-132. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90897-2_6.
  34. Dirk Pattinson. An introduction to the theory of coalgebras. Course notes for NASSLLI, 2003. Google Scholar
  35. Jacques Riguet. Relations binaires, fermetures, correspondances de galois. Bulletin de la société mathématique de France, 76:114-155, 1948. Google Scholar
  36. Jan JMM Rutten. Relators and metric bisimulations. Electronic Notes in Theoretical Computer Science, 11:252-258, 1998. URL: https://doi.org/10.1016/S1571-0661(04)00063-5.
  37. Jan JMM Rutten. Universal coalgebra: a theory of systems. Theoretical computer science, 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  38. Davide Sangiorgi. Introduction to bisimulation and coinduction. Cambridge University Press, 2011. Google Scholar
  39. Christoph Schubert and Gavin J Seal. Extensions in the theory of lax algebras. Theory and Applications of Categories [electronic only], 21:118-151, 2008. Google Scholar
  40. Gavin J Seal. Canonical and op-canonical lax algebras. Theory Appl. Categ, 14(10):221-243, 2005. Google Scholar
  41. Mike Shulman. 2-dinatural transformation. URL: https://ncatlab.org/nlab/show/2-dinatural%20transformation.
  42. AL Smirnov. Graded monads and rings of polynomials. Journal of Mathematical Sciences, 151(3):3032-3051, 2008. Google Scholar
  43. Věra Trnková. Relational automata in a category and their languages. In International Conference on Fundamentals of Computation Theory, pages 340-355. Springer, 1977. Google Scholar
  44. Franck Van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115-142, 2005. URL: https://doi.org/10.1016/J.TCS.2004.09.035.
  45. Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Logical Methods in Computer Science, 18, 2022. URL: https://doi.org/10.46298/LMCS-18(2:19)2022.
  46. James Worrell. On coalgebras and final semantics. PhD thesis, University of Oxford, 2000. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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