Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 23 min ago
PreprintCC BY 4.0arXiv

Coinductive reasoning for parametrized functors and monads

  • Ugo Dal Lago
  • Zeinab Galal
Open at sourcePDFDOICite

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.

Related

  1. About the contractibility of the walking coinductive equivalence
    Viktoriya Ozornova, Martina Rovelli, Tashi Walde
    arXivPreprintarXiv licenceFull textAlgebra & number theoryGeometry & topologyarXiv
  2. Metrization of Quasi-Uniformities, Powerset Monads, and Qualitative Robustness Analysis
    Francesco Dagnino, Amin Farjudian, Eugenio Moggi
    arXivPreprintCC BY-NC-ND 4.0Full textGeometry & topologyarXiv
  3. Lax-idempotent monads in homotopy theory
    Fernando Abellán, Thomas Blom
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv
  4. Parametrized Power-Iteration Clustering for Directed Graphs
    Gwendal Debaussart-Joniec, Harry Sevi, Matthieu Jonckheere +1
    Proceedings of the 41st International Conference on Machine Learning (ICML), PMLRPeer-reviewedLicence not statedGeneral mathematicsHAL
  5. On deformations of foliated complex analytic structures II: Functors of Artin rings
    Chunghoon Kim
    arXivPreprintarXiv licenceFull textAlgebra & number theoryGeometry & topologyarXiv

Cite

BibTeXRIS
BibTeX
@misc{lago2026coinductive,
  title = {{Coinductive reasoning for parametrized functors and monads}},
  author = {Ugo Dal Lago and Zeinab Galal},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.35691},
  eprint = {2609.35691},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.35691},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Coinductive reasoning for parametrized functors and monads
AU  - Ugo Dal Lago
AU  - Zeinab Galal
PY  - 2026
DA  - 2026/09/28
PB  - arXiv
DO  - 10.48550/arxiv.2609.35691
UR  - https://arxiv.org/abs/2609.35691
AB  - 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.
ER  -