自由超圖范疇中的重寫

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