Document Open Access Logo

Monads on Categories of Relational Structures

Authors Chase Ford , Stefan Milius , Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.14.pdf
  • Filesize: 0.84 MB
  • 17 pages

Document Identifiers

Author Details

Chase Ford
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Ford, Chase: Supported by the Deutsche Forschungsgemeinschaft (DFG) as part of the Research and Training Group 2475 "Cybercrime and Forensic Computing" (393541319/GRK2475/1-2019).
  • Milius, Stefan: Supported by the Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1.
  • Schröder, Lutz: Supported by Deutsche Forschungsgemeinschaft (DFG) under project SCHR 1118/15-1.

Cite AsGet BibTex

Chase Ford, Stefan Milius, and Lutz Schröder. Monads on Categories of Relational Structures. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.14

Abstract

We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity λ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders (λ = ω) or metric spaces (λ = ω₁). We establish a bijective correspondence between λ-accessible enriched monads on the given category of relational structures and a notion of λ-ary algebraic theories (i.e. with operations of arity < λ), with the syntax of algebraic theories induced by the relational signature (e.g. inequations or equations-up-to-ε). We provide a generic sound and complete derivation system for such relational algebraic theories, thus in particular recovering (extensions of) recent systems of this type for monads on partial orders and metric spaces by instantiation. In particular, we present an ω₁-ary algebraic theory of metric completion. The theory-to-monad direction of our correspondence remains true for the case of κ-ary algebraic theories and κ-accessible monads for κ < λ, e.g. for finitary theories over metric spaces.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Logic and verification
Keywords
  • monads
  • relational structures
  • Horn theories
  • relational logic

Metrics

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

Related Versions

References

  1. Jirí Adámek. Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carolin., 15(4):589-602, 1974. Google Scholar
  2. Jirí Adámek, Matěj Dostál, and Jirí Velebil. A categorical view of varieties of ordered algebras, 2021. URL: http://arxiv.org/abs/2011.13839.
  3. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories. Wiley-Interscience, New York, 1990. Google Scholar
  4. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. Google Scholar
  5. Jiří Adámek, Chase Ford, Stefan Milius, and Lutz Schröder. Finitary monads on the category of posets, 2020. URL: http://arxiv.org/abs/2011.14796.
  6. Stephen Bloom. Varieties of ordered algebras. J. Comput. System Sci., 2(13):200-212, 1976. Google Scholar
  7. Brian Day. A reflection theorem for closed categories. J. Pure Appl. Algebra, 2(1):1-11, 1972. Google Scholar
  8. Brian Day and Miguel Laplaza. On embedding closed categories. Bull. Austral. Math. Soc., 18(3):357-371, 1978. Google Scholar
  9. Chase Ford, Stefan Milius, and Lutz Schröder. Behavioural preorders via graded monads. In Logic in Computer Science, LICS 2021. IEEE, 2021. To appear. Preprint available as arXiv e-print https://arxiv.org/abs/2011.14339.
  10. Richard Garner and John Power. An enriched view on the extended finitary monad-Lawvere theory correspondence. Logical Methods Comput. Sci., 14(1):1-23, 2018. Google Scholar
  11. Thomas Jech. Set Theory. Springer, 2003. Google Scholar
  12. Max Kelly. Structures defined by finite limits in the enriched context, I. Cah. Topol. Géom. Différ. Catég., 23(1):3-42, 1982. Google Scholar
  13. Max Kelly and Steve Lack. Finite-product-preserving functors, Kan extensions, and strongly-finitary 2-monads. Appl. Categorical Struct., 1(1):85-94, 1993. Google Scholar
  14. Max Kelly and John Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. J. Pure Appl. Algebra, 15(3):163-179, 1993. Google Scholar
  15. Alexander Kurz and Jiří Velebil. Quasivarieties and varieties of ordered algebras: regularity and exactness. Math. Struct. Comput. Sci., 27(7):1153-1194, 2017. Google Scholar
  16. Fred Linton. Some aspects of equational theories. In Proc. Conf. on Categorical Algebra at La Jolla, pages 84-94. Springer, 1966. Google Scholar
  17. Fred Linton. An outline of functorial semantics. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, volume 80 of Lecture Notes Math., pages 7-52. Springer, 1969. Google Scholar
  18. Rory Lucyshyn-Wright. Enriched algebraic theories and monads for a system of arities. Theory Appl. Categ., 31(5):101-137, 2016. Google Scholar
  19. Ernest Manes. Algebraic Theories. Springer, 1976. Google Scholar
  20. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Logic in Computer Science, LICS 2016, pages 700-709. ACM, 2016. Google Scholar
  21. Eugenio Moggi. Notions of computations and monads. Inf. Comput., 93(1):55-92, 1991. Google Scholar
  22. Koki Nishizawa and John Power. Lawvere theories enriched over a general base. J. Pure Appl. Algebra, 213(3):377-386, 2009. Google Scholar
  23. Erik Palmgren and Steven Vickers. Partial horn logic and cartesian categories. Ann. Pure Appl. Log., 145(3):314-353, 2007. Google Scholar
  24. Gordon Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, FOSSACS 2001, volume 2030 of LNCS, pages 1-24. Springer, 2001. Google Scholar
  25. John Power. Enriched lawvere theories. Theory Appl. Categories, 6(7):83-93, 1999. Google Scholar
  26. Jiří Rosický. Metric monads, 2021. URL: http://arxiv.org/abs/2012.14641.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact