严格化与相干性的弦图
String diagrams for Strictification and Coherence
AI总结：
本文提出非严格幺半范畴弦图的生成元与关系表示，证明其正确性，并由此给出Mac Lane严格性定理与相干性定理的新图形证明，支持数字电路与编程语言等应用。
摘要：
虽然严格幺半范畴的弦图已被充分理解，并在计算机科学的多个领域得到应用，但非严格幺半范畴的图形形式化研究却远为不足。本文中，我们给出了非严格幺半范畴弦图的生成元与关系表示，并展示了该构造如何处理数字电路和编程语言等领域的应用。我们证明了该构造的正确性，由此得到了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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
