论文标题
使用弦图削弱和迭代定律
Weakening and Iterating Laws using String Diagrams
论文作者
论文摘要
分配定律是将两个单子结合起来的标准方法，它为语义中的计算效应推理提供了一种组成方法。有时可以通过削弱分配法律的概念，仍能恢复复合材料单元来处理这种法律的情况。 Eugenia Cheng的著名结果表明，如果它们满足称为Yang-Baxter方程的连贯条件，则可以通过迭代更多的分配法律来结合$ n $ monads。此外，组成的顺序并不重要，导致了一种联想的形式。本文的主要贡献是在$ n = 3 $ monad的情况下概括迭代组成对弱分配法律的关联。为此，我们使用字符串 - 格拉马式符号，这显着有助于使日益复杂的证据更加可读。我们还提供了由迭代产生的新的弱分布定律的例子。
Distributive laws are a standard way of combining two monads, providing a compositional approach for reasoning about computational effects in semantics. Situations where no such law exists can sometimes be handled by weakening the notion of distributive law, still recovering a composite monad. A celebrated result from Eugenia Cheng shows that combining $n$ monads is possible by iterating more distributive laws, provided they satisfy a coherence condition called the Yang-Baxter equation. Moreover, the order of composition does not matter, leading to a form of associativity. The main contribution of this paper is to generalise the associativity of iterated composition to weak distributive laws in the case of $n = 3$ monads. To this end, we use string-diagrammatic notation, which significantly helps make increasingly complex proofs more readable. We also provide examples of new weak distributive laws arising from iteration.
