Document Open Access Logo

Preservation of Equations by Monoidal Monads

Authors Louis Parlant, Jurriaan Rot, Alexandra Silva, Bas Westerbaan

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.77.pdf
  • Filesize: 5.58 MB
  • 14 pages

Document Identifiers

Author Details

Louis Parlant
  • University College London, UK
Jurriaan Rot
  • Radboud University, Nijmegen, The Netherlands
Alexandra Silva
  • University College London, UK
Bas Westerbaan
  • University College London, UK

Funding

This work was partially supported by the ERC Starting Grant ProFoundNet (grant code 679127), the Marie Curie Fellowship CARBS (grant code 795119), and the EPSRC Standard Grant CLeVer (EP/S028641/1).

Acknowledgements

We are grateful to Dan Marsden, Robin Piedeleu, Edmund Robinson and Maaike Zwart for inspiring discussions and suggestions.

Cite AsGet BibTex

Louis Parlant, Jurriaan Rot, Alexandra Silva, and Bas Westerbaan. Preservation of Equations by Monoidal Monads. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 77:1-77:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.MFCS.2020.77

Abstract

If a monad T is monoidal, then operations on a set X can be lifted canonically to operations on TX. In this paper we study structural properties under which T preserves equations between those operations. It has already been shown that any monoidal monad preserves linear equations; affine monads preserve drop equations (where some variable appears only on one side, such as x⋅ y = y) and relevant monads preserve dup equations (where some variable is duplicated, such as x ⋅ x = x). We start the paper by showing a converse: if the monad at hand preserves a drop equation, then it must be affine. From this, we show that the problem whether a given (drop) equation is preserved is undecidable. A converse for relevance turns out to be more subtle: preservation of certain dup equations implies a weaker notion which we call n-relevance. Finally, we identify a subclass of equations such that their preservation is equivalent to relevance.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • monoidal monads
  • algebraic theories
  • preservation of equations

Metrics

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

Related Versions

References

  1. Ronald V. Book and Friedrich Otto. String-rewriting systems. In String-Rewriting Systems, pages 35-64. Springer, 1993. Google Scholar
  2. J.R.B. Cockett and R.A.G. Seely. Linearly distributive functors. Journal of Pure and Applied Algebra, 143(1-3):155-203, 1999. Google Scholar
  3. Fredrik Dahlqvist, Alexandra Silva, and Louis Parlant. Layer by layer: composing monads. In ICTAC, 2018. Google Scholar
  4. N.D. Gautam. The validity of equations of complex algebras. Archiv für Mathematische Logik und Grundlagenforschung, 3(3-4):117-124, 1957. Google Scholar
  5. Martin Hyland, Paul Blain Levy, Gordon Plotkin, and John Power. Combining continuations with other effects. In Proc. Continuations Workshop, 2004. Google Scholar
  6. Bart Jacobs. Semantics of weakening and contraction. Annals of pure and applied logic, 69(1):73-106, 1994. Google Scholar
  7. Ohad Kammar and Gordon D. Plotkin. Algebraic foundations for effect-dependent optimisations. In POPL, pages 349-360. ACM, 2012. Google Scholar
  8. David J. King and Philip Wadler. Combining monads. In Functional Programming, Glasgow 1992, pages 134-143. Springer, 1993. Google Scholar
  9. Bartek Klin and Julian Salamanca. Iterated covariant powerset is not a monad. MFPS XXXIV, 2018. Google Scholar
  10. Anders Kock. Monads on symmetric monoidal closed categories. Archiv der Mathematik, 21(1):1-10, 1970. Google Scholar
  11. Anders Kock. Bilinearity and cartesian closed monads. Mathematica Scandinavica, 29(2):161-174, 1972. Google Scholar
  12. Anders Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23(1):113-120, 1972. Google Scholar
  13. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer, 2013. Google Scholar
  14. Ernie Manes and Philip Mulry. Monad compositions i: general constructions and recursive distributive laws. Theory and Applications of Categories, 18(7):172-208, 2007. Google Scholar
  15. Ernie Manes and Philip Mulry. Monad compositions ii: Kleisli strength. Mathematical Structures in Computer Science, 18(3):613-643, 2008. Google Scholar
  16. Micah Blake McCurdy. Graphical methods for Tannaka duality of weak bialgebras and weak Hopf algebras in arbitrary braided monoidal categories. arXiv preprint arXiv:1110.5542, 2011. Google Scholar
  17. Paul-André Melliès. Functorial boxes in string diagrams. In International Workshop on Computer Science Logic, pages 1-30. Springer, 2006. Google Scholar
  18. Louis Parlant, Jurriaan Rot, Alexandra Silva, and Bas Westerbaan. Preservation of equations by monoidal monads, 2020. URL: http://arxiv.org/abs/2001.06348.
  19. Maciej Pirog and Sam Staton. Backtracking with cut via a distributive law and left-zero monoids. Journal of Functional Programming, 27, 2017. Google Scholar
  20. Ana Sokolova, Bart Jacobs, and Ichiro Hasuo. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3, 2007. Google Scholar
  21. Maaike Zwart and Dan Marsden. No-go theorems for distributive laws. In LICS, pages 1-13. IEEE, 2019. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact