一句话：为带交换（余）幺半群结构的 string diagrams 重写给出基于超图双推出重写的可靠完备刻画。
String diagrams 是 symmetric monoidal categories 中态射的图形表示，已应用于并发理论、量子计算、控制论、机器学习等领域。其重写理论通常把图解释为超图上的 double-pushout（DPO）重写；但已有工作表明，为保证 soundness 与 completeness，要么给 string diagrams 添加 Frobenius 代数结构，要么限制 DPO 重写（如 convex 重写）。本文研究更弱且应用上更自然的交换幺半群结构，刻画模交换幺半群等式的 string diagram 重写，并给出在适当超图 DPO 重写概念下的 sound and complete 解释。
String diagrams are pictorial representations for morphisms of symmetric monoidal categories. They constitute an intuitive and expressive graphical syntax, which has found application in a very diverse range of fields including concurrency theory, quantum computing, control theory, machine learning, linguistics, and digital circuits. Rewriting theory for string diagrams relies on a combinatorial interpretation as double-pushout rewriting of certain hypergraphs. As previously studied, there is a `tension' in this interpretation: in order to make it sound and complete, we either need to add structure on string diagrams (in particular, Frobenius algebra structure) or pose restrictions on double-pushout rewriting (resulting in 'convex' rewriting). From the string diagram viewpoint, imposing a full Frobenius structure may not always be natural or desirable in applications, which motivates our study of a weaker requirement: commutative monoid structure. In this work we characterise string diagram rewriting modulo commutative monoid equations, via a sound and complete interpretation in a suitable notion of double-pushout rewriting of hypergraphs.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MilosavljevicPZ25,
title = {Rewriting for Symmetric Monoidal Categories with Commutative (Co)Monoid Structure},
author = {Aleksandar Milosavljevic and Robin Piedeleu and Fabio Zanasi},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:12)2025}
}