论文标题
单型单子保存方程
Preservation of Equations by Monoidal Monads
论文作者
论文摘要
如果单调$ t $是单一的，则可以将$ x $的操作从典范上抬起到$ tx $的操作。在本文中，我们研究了$ t $在这些操作之间保持方程式的结构属性。已经证明，任何单型单元都可以保持线性方程。仿射单子保存下降方程（其中某些变量仅出现在一侧，例如$ x \ cdot y = y $）和相关的monads保留dup方程（其中某些变量是重复的，例如$ x \ cdot x = x $）。我们通过显示相反的纸张开始论文：如果手工的单个单元保留了一个滴剂方程，则必须是仿射。由此，我们表明是否保留给定（滴）方程是不可决定的问题。相关性的相反事实更加微妙：保留某些DUP方程式意味着我们称之为$ n $ relevance的较弱的概念。最后，我们确定方程的子类，使它们的保存等同于相关性。
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\cdot y = y$) and relevant monads preserve dup equations (where some variable is duplicated, such as $x \cdot 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.
