Symmetric monoidal theories (SMTs) generalise algebraic theories in a way that make them suitable to express resource-sensitive systems, in which variables cannot be copied or discarded at will. In SMTs, traditional tree-like terms are replaced by string diagrams, topological entities that can be intuitively thoughts as diagrams of wires and boxes. Recently, string diagrams have become increasingly popular as a graphical syntax to reason about computational models across diverse fields, including programming language semantics, circuit theory, quantum mechanics, linguistics, and control theory. In applications, it is often convenient to implement the equations appearing in SMTs as rewriting rules. This poses the challenge of extending the traditional theory of term rewriting, which has been developed for algebraic theories, to string diagrams. In this paper, we develop a mathematical theory of string diagram rewriting for SMTs. Our approach exploits the correspondence between string diagram rewriting and double pushout (DPO) rewriting of certain graphs, introduced in the first paper of this series. Such a correspondence is only sound when the SMT includes a Frobenius algebra structure. In the present work, we show how an analogous correspondence may be established for arbitrary SMTs, once an appropriate notion of DPO rewriting (which we call convex) is identified. As proof of concept, we use our approach to show termination of two SMTs of interest: Frobenius semi-algebras and bialgebras.
翻译:平面单线理论( SMTs) 一般性的代数理论( SMTs ), 使其适合于表达资源敏感系统, 其变量不能被复制或随意丢弃。 在 SMTs 中, 传统的树类术语被字符串图取代。 在 SMTs 中, 传统词组重写理论被树类实体替换为直观思考作为线条和框图的图表。 最近, 字符串图越来越受欢迎, 作为一种图形合成词组, 以解释不同领域的计算模型, 包括编程语言语义、 电路理论、 量力、 语言学和控制理论。 在应用程序中, 通常可以方便地将 SMTs 中出现的等方公式作为重写规则。 这构成了扩大传统的术语重写理论的挑战, 传统的词组重写理论可以作为线条和框图的图。 在本文中, 我们的方法利用字符串图重写和双推( DPO) 重写某些图表之间的对应, 。 在本文的首页中, 只有当SMTBebbribelbel 概念包括了我们确定的SBenbribribora 格式概念时, 。