利用多向因果结构对字符串图进行快速自动推理

利用多向因果结构对字符串图进行快速自动推理

Fast Automated Reasoning over String Diagrams using

Multiway Causal Structure

https://arxiv.org/pdf/2105.04057

我们在一个通用的双推出（DPO）框架内，介绍了一种用于实施弦图自动重写的直观算法方法论，其中重写序列的选择是依据底层图解演算的因果结构进行的。重写结构与因果结构的结合可以优雅地表述为一个配备了全和部分幺半双函子的弱 2-范畴，从而为一个通用的 Wolfram 模型超图重写系统的完整多路演化因果图提供了范畴语义。作为一个说明性的例子，我们展示了该算法的一个特例如何实现 ZX-演算中所表示的量子电路的高效自动简化。

1 引言

弦图，正如 Joyal 和 Street[26] 首次形式化的那样，为表示任意幺半范畴提供了一种严谨且优雅的图形语言。因此，对弦图的有效推理是应用范畴论许多领域的支柱，包括 ZX-演算[10][11] 和范畴量子力学[1][2]、并发理论[9]、网络与控制理论[4][6][5]，甚至是计算语言学[13][8]；因此，此前已经开发了各种流行的弦图交互式证明助手（例如用于 ZX-演算的 PyZX[30] 和用于更通用图解演算的 Quantomatic[31]），这就不足为奇了。这种基于弦图的自动推理系统构成了 Wolfram 模型多路系统[34][35][21][22] 的一个重要特例，这些系统用偏粘合范畴上的双推出重写系统[24][25] 来描述任意（超）图上的抽象重写系统及其因果结构。本文的目的是引入一个新的算法框架，用于在弦图上实施快速自动推理，在该框架中，自动定理证明系统引入的引理是基于其因果结构进行选择的，从而最大化多路系统中相应路径关联的出射因果边的总数，并论证这是一种有效的启发式方法，用于选择那些最有可能对缩短后续证明产生最大影响的引理。

在第 2 节中，我们展示了如何将 Wolfram 模型表述为超图范畴弦图上的双推出（DPO）重写系统，并讨论了如何利用代数图变换理论的并发性和并行性定理，从这样的重写系统中提取出对称幺半范畴结构。我们还讨论了 Coecke 和 Lal[12] 提出的因果范畴形式体系如何也允许对此类重写系统的因果结构进行组合式描述，使得整个 Wolfram 模型多路演化因果图（结合了重写结构和因果结构）能够被表述为一个弱 2-范畴，该范畴在 1-胞腔上配备了全幺半双函子，在 2-胞腔上配备了部分幺半双函子。在第 3 节中，我们要展示这种弱 2-范畴结构如何允许我们扩展传统的（无失败的）Knuth-Bendix 完备化算法，以产生一个反驳完备的证明演算，该演算考虑了底层图解推理语言的因果结构。最后，在第 4 节中，我们通过展示一个关于 CNOT 门幺正性的自动生成证明的完整工作示例，说明了该通用算法在一个显著特例中的应用，即 ZX-演算中量子电路的图解简化问题。

复现本文所述计算所需的所有代码均为开源代码，并可在 Wolfram 函数库（Wolfram Function Repository）上免费获取（附带详尽文档）。例如，MakeZXDiagram 使人们能够构建量子电路的弦图；QuantumDiscreteStateToZXDiagram / ZXDiagramToQuantumDiscreteState 使人们能够在 Wolfram 语言开源量子计算框架中的纯符号量子对象与 ZX-图之间进行转换；MultiwayOperatorSystem 允许人们演化所得的多路系统并提取其因果结构；FindWolframModelProof 允许人们构建（超图）弦图之间等价性的自动证明；等等。

2 （超）图重写系统的组合结构

尽管普通幺半范畴的弦图对应于（有向）图，但超图范畴的弦图（按照 Kissinger[29] 和 Fong[17][18] 的术语）对应于超图。

定义 1 “超图范畴”是一个对称幺半范畴 (C, ⊗, I)，其中 ob(C) 中的每个对象 A 都配备了一个特殊的交换弗罗贝尼乌斯代数结构 (A, μ, η, δ, ε)，使得幺半积 A ⊗ B（对于 ob(C) 中的 A 和 B）的弗罗贝尼乌斯代数结构由 A 和 B 的弗罗贝尼乌斯代数结构典范地诱导而来。一个类型化超图产生式[16][15]现在是一个单态射的跨度 p：

这些产生式之间的因果关系因此在 MuGraph 范畴内形成了 2-胞腔，产生了一个弱 2-范畴[7]，我们今后称之为 MuCauGraph，它代表了多路演化因果图[25]的组合结构。在图 1 中，我们通过一个明确的多路演化图来说明 MuGraph 的对称幺半范畴结构，其中所有产生式都显示为有向边；此外，我们还通过一个明确的多路演化因果图来说明 MuCauGraph 的弱 2-范畴结构，其中所有产生式都显示为黄色顶点，2-胞腔（因果关系）显示为橙色边。在所有此类多路系统中，状态顶点是基于超图同构进行合并的，使用的是文献 [19] 中所述算法的推广。

3 利用多路因果结构进行图解定理证明

在图3中，我们展示了该路径对应的证明图，其中带尖角的浅绿色方框表示公理，深橙色三角形表示临界对引理，浅橙色圆形表示替换引理，深绿色菱形表示假设，实线表示替换，虚线表示推导出的推理规则。

在这个证明图中，我们实质上利用了 MuCauGraph 的因果

结构 ⊗C，以便为一阶图解逻辑（带等式）构建一个反驳完备的证明演算，该演算扩展了传统的（无失败的）Knuth-Bendix 完备化过程[32]，并建立在 Bachmair 和 Ganzinger[3] 所开发的方法之上。具体而言，我们使用一个基于相应多路演化路径中出射因果边数量的选择函数 SS 来对等式项进行排序，并引入了用于选择性归结的演绎推理规则：

关于（因果）选择函数 SS 是最大的。因此，在选择将哪些引理添加到重写系统时（无论是源自归结/因子分解实例的替换引理，还是源自完备化/叠加/参数化实例的临界对引理），我们不再像传统的无失败完备化方法那样使用项上的标准约化排序，而是选择那些在多路演化因果图的关联路径中最大化出射因果边数量的引理，因为直观上，这构成了一个合理的启发式方法，用于选择那些对缩短后续证明产生最大影响的引理。该推理系统的完整证明演算在 [25] 中给出。

尽管上面给出的示例证明考虑的是没有“悬空”超边的闭超图的情况，但值得注意的是，开超图和闭超图最终都是前一节中提出的完整类型化超图形式体系的特例。具体而言，对于每个超图 GG，都存在一个独特的超图

（类型超图），带有一个全超图态射

（类型化态射）：

4 ZX-演算中量子电路简化的一个应用

现在，我们必须使用推导出的推理规则 B'（也称为 Hopf 定律），它是通过结合 B1（复制）、B2（双代数简化）、D2（菱形）和 S（融合/恒等）规则推导出来的。当与双代数简化规则 B2 结合时，Hopf 定律对应于这样一个陈述：不同颜色的蜘蛛之间的相互作用通常会产生缩放双代数（即仅因存在归一化因子而与双代数不同的结构）。因此，从这里开始，我们继续应用 Hopf 定律 B'，以便“解缠”Z-蜘蛛和 X-蜘蛛，从而产生一对平行线，每条线上有一个 Z/X-蜘蛛，如图 7 所示。

最后，我们应用 Z-蜘蛛恒等规则 (S2)，接着应用 X-蜘蛛恒等规则 (S2)，以便从图中完全移除剩余的无相 Z-蜘蛛和 X-蜘蛛，并按需要用单根（平行）线替换它们。最后两个引理分别显示在图 8 和图 9 中。

文献 [25] 中给出了该自动重写框架的完整性能分析，针对将随机生成的 Clifford 电路简化为伪正规形式以及减少随机生成的非 Clifford 电路中的 T 门的情况，分别在有无因果结构优化的情况下进行了分析，并在证明复杂度和时间复杂度指标上进行了比较。结果发现，当应用因果结构优化时，所有性能指标都表现出大致平方级的加速效果。

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