Preservation of Equations by Monoidal Monads

01/17/2020
by   Louis Parlant, et al.
0

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 the subclass of equations such that their preservation is equivalent to relevance.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset