一句话：为非严格幺半范畴给出弦图生成元与关系表示，并由此给出 Mac Lane 严格性与相干性定理的图形化证明。
严格幺半范畴的弦图已有成熟理论并广泛用于计算机科学，但非严格幺半范畴的图形形式化研究较少。本文给出非严格幺半范畴弦图的生成元与关系表示，说明该构造可处理数字电路与编程语言等应用。作者证明该构造的正确性，由此得到 Mac Lane 严格性定理的新证明，并进一步给出其相干性定理的初等图形证明。该框架还能归纳地构造幺半范畴中的典范同构，为相干性提供可操作的计算视角。
Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string diagrams for non-strict monoidal categories, and show how this construction can handle applications in domains such as digital circuits and programming languages. We prove the correctness of our construction, which yields a novel proof of Mac Lane's strictness theorem. This in turn leads to an elementary graphical proof of Mac Lane's coherence theorem, and in particular allows for the inductive construction of the canonical isomorphisms in a monoidal category.
@article{paperbot2714,
title = {String diagrams for Strictification and Coherence},
author = {Paul Wilson and Dan Ghica and Fabio Zanasi},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:8)2024}
}