利用多向因果結構對字符串圖進行快速自動推理

利用多向因果結構對字符串圖進行快速自動推理

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] 所開發的方法之上。具體而言，我們使用一個基于相應多路演化路徑中出射因果邊數量的選擇函數 S S 來對等式項進行排序，并引入了用于選擇性歸結的演繹推理規則：

關于（因果）選擇函數 S S 是最大的。因此，在選擇將哪些引理添加到重寫系統時（無論是源自歸結/因子分解實例的替換引理，還是源自完備化/疊加/參數化實例的臨界對引理），我們不再像傳統的無失敗完備化方法那樣使用項上的標準約化排序，而是選擇那些在多路演化因果圖的關聯路徑中最大化出射因果邊數量的引理，因為直觀上，這構成了一個合理的啟發式方法，用于選擇那些對縮短后續證明產生最大影響的引理。該推理系統的完整證明演算在 [25] 中給出。

盡管上面給出的示例證明考慮的是沒有“懸空”超邊的閉超圖的情況，但值得注意的是，開超圖和閉超圖最終都是前一節中提出的完整類型化超圖形式體系的特例。具體而言，對于每個超圖 G G，都存在一個獨特的超圖 （類型超圖），帶有一個全超圖態射（類型化態射）：

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