自由超图范畴中的重写

Rewriting in Free Hypergraph Categories

自由超图范畴中的重写

https://arxiv.org/abs/1712.09495

我们研究在对称幺半范畴（symmetric monoidal categories）背景下等式理论的重写，其中每个对象上都有一个可分 Frobenius 幺半群（separable Frobenius monoid）。这些范畴也被称为超图范畴（hypergraph categories），其相关性日益增加：Frobenius 结构最近出现在跨学科应用中，包括对量子过程、动力系统和自然语言处理的研究。在这项工作中，我们将自由超图范畴的态射（arrows）组合刻画为标记超图的余跨（cospans），并建立了模 Frobenius 结构的重写与超图的双推出（double-pushout）重写之间的精确对应关系。这种解释允许利用关于超图的结果来确保自由超图范畴中重写的汇合性（confluence）的可判定性。我们的结果推广了之前的方法，那些方法仅考虑了由单个对象生成的范畴（props）。

1 引言

核心直觉是，这种额外的结构允许弦图的悬垂线（dangling wires）进行分叉、被丢弃、被移动到左/右侧，从而使得对所表示系统的接口（变量、存储单元）的操作更加灵活。将超图范畴用作计算的代数方法是由 Walters 及其合作者 [9, 20] 开创的，当时使用的名称是“良支撑紧致闭范畴”（well-supported compact closed categories）。从那时起，可分 Frobenius 幺半群普遍出现在不同研究线索的图示演算中。它们显著地出现在 ZX 演算 [10]（量子理论）中，其中每个 Frobenius 结构在量子可观测量方面都有精确的物理意义。Frobenius 幺半群也构成了无状态连接器演算 [7]、信号流图演算 [4, 5]、Baez 的网络理论 [1] 以及 Pavlovic 的幺半计算机 [28] 的骨干。最近，人们特别关注通过跨（span）、关系（relation）及其对偶的抽象概念来通用地构造超图范畴 [35, 15, 26, 16]。

虽然可分 Frobenius 幺半群构成了上述方法的共同核心，但在每个应用中，弦图还会被特定领域的方程进一步商（quotiented），这对于定义系统的适当行为等价性概念至关重要。本文的观点是承认一方面对称幺半结构和 Frobenius 结构（这是任何超图范畴的内置部分）与另一方面特定领域方程之间的概念差异。我们将把后者作为重写规则来研究：如果这样一个方程的左端可以在一个更大的弦图中找到，它就可以被删除并替换为其右端。

这与图示演算用户的日常实践是一致的，也是在证明辅助工具中实现图形推理的起点。存在一个关于幺半范畴重写的详尽数学理论，它将重写规则视为生成 2-胞腔（也被称为计算复合体（computads）[21] 或多图（polygraphs）[8]），并将可能的重写轨迹视为复合 2-胞腔。然而，这种抽象视角在涉及实现重写时并不能提供直接的帮助。主要的挑战是对匹配（matching）的具体理解：为了检测一个弦图是否包含重写规则的左端，人们需要根据结构方程考虑其所有可能的分解。在超图范畴中，这等同于说重写是模（modulo）可分 Frobenius 幺半群的方程发生的。例如，重写规则

关于弗罗贝尼乌斯结构的重写，[2, 3] 已沿着相同的思路进行了研究。这些由作者及其合作者近期完成的工作，为本文提供了路线图：本文旨在验证此类结果可推广至多类代数理论，其中自由生成的范畴在每个类上都具有一个弗罗贝尼乌斯结构。根据[2, 3]的启示，这一推广的展开方式并不特别令人惊讶，因为我们基本上能够将相同的证明技术从单类情形提升至多类情形。然而，我们认为，为这些结果撰写一篇参考性论文的时机已经成熟。首先，这得益于人们对超图范畴重新燃起的兴趣，这一点从近期若干应用中得到印证，特别是在电路理论[15]和自然语言语义学[26, 19]方面：使用[2, 3]中发展的理论将需要多类情形下的完全一般性。其次，另一个理由来自于对各种系统族（并发系统[7]、量子系统[10]、动力系统[4, 1]）的公理化方法，其中公理化系统行为的等式理论包含两个或更多弗罗贝尼乌斯代数。在重写方面，[2]中引入的方法仅允许在组合模型中吸收一个弗罗贝尼乌斯结构。在本文中，我们展示了如何以相同方式吸收额外的弗罗贝尼乌斯结构1，从而降低上述公理化方法的复杂性，并简化研究范式、合流性和终止性的任务。

2 Props 与超图范畴

我们将研究由操作签名（signature of operations）自由生成的超图范畴。以下是适用于幺半语境的概念。

这个例子表明，定理 3.2 不仅为代数结构提供了组合表示，而且反过来，它也有助于推导出众所周知的图论模型的代数表述。 我们现在给出刻画定理的证明。

4 模 Frobenius 重写的 DPOI 实现

5 合流性的可判定性

本节验证由定理 4.1 确立的重写形式具有 Knuth-Bendix 性质。呼应项重写的情况，我们使用这一术语意指合流问题可归约为关键对分析，且对于终止重写系统而言，两者均是可判定的。

为此，我们将文献 [3] 的结果实例化到我们的设定中。在那里，作者及其合作者证明了 DPOI 重写具有前述的 Knuth-Bendix 性质。接口在此处起着至关重要的作用，因为 Plump 证明了对于 DPO 重写（无接口），合流性是不可判定的 [29]。

命题 5.2 ([3]). 假设 C C 满足以下假设：(1) 它有一个满-单分解系统（epi-mono factorisation system）；(2) 它有二元余积、推出和拉回；(3) 它是粘合的（adhesive）；(4) 所有推出在拉回下稳定。那么 C C 中的 DPOI 重写对于可计算重写系统具有 Knuth-Bendix 性质。

6 结论

我们描述了超图范畴中字符串图重写的一种可靠且完备的解释，将其作为超图的双推出重写，并展示了对于终止重写系统，它享有合流性的可判定性。这种方法的一个主要优势是，在组合模型中，由执行模 Frobenius 方程匹配所带来的挑战消失了。这在研究具有多个 Frobenius 单子的公理化时变得重要：这些现在都可以被视为结构方程并融入组合模型中，从而将合流性和终止性的问题局限于非 Frobenius 公理。我们理论的这一应用（我们计划在未来工作中探索）是推广 [2, 3] 框架的主要原因，后者仅能够吸收单个 Frobenius 结构。另一个有希望的方向是二分图的代数研究（例 3.5），这可能与分析基于这些结构的图形语言有关，例如生物代谢网络 [33]。

原文链接： https://arxiv.org/pdf/1712.09495