eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-08-18
77:1
77:14
10.4230/LIPIcs.MFCS.2020.77
article
Preservation of Equations by Monoidal Monads
Parlant, Louis
1
Rot, Jurriaan
2
Silva, Alexandra
1
Westerbaan, Bas
1
University College London, UK
Radboud University, Nijmegen, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol170-mfcs2020/LIPIcs.MFCS.2020.77/LIPIcs.MFCS.2020.77.pdf
monoidal monads
algebraic theories
preservation of equations