超圖重寫與λ-演算的因果結構

超圖重寫與λ-演算的因果結構

Hypergraph rewriting and Causal structure of λ?calculus

https://arxiv.org/pdf/2409.01006

摘要

在本文中，我們首先用范疇論的術語研究超圖重寫，試圖定義事件的概念并發展圖重寫中因果性的基礎。我們在粘著范疇（adhesive categories）的雙推out（double-pushout）重寫框架內引入新穎的概念。其次，我們將研究λ-演算中事件的概念，在其中我們構造一個算法，以確定在滿足某些條件的λ-表達式求值過程中事件之間的因果關系。最后，我們嘗試將這一定義擴展到任意λ-表達式。

1 引言

在計算系統中，關于兩個事件之間的關系出現了一個基本問題：具體來說，一個事件如何影響或導致另一個事件。計算機科學中因果性的概念最初由 Glynn Winskel [12] 探索，他引入了一個抽象框架來刻畫事件及其之間的因果關系。從那時起，在理解因果性背后的結構方面取得了重大進展。因果性的重要性在動力系統中也很明顯，正如愛因斯坦的廣義相對論中所強調的那樣，其中洛倫茲流形（Lorentzian manifold）的因果結構唯一地決定了時空的幾何結構（模去一個縮放因子）。此外，理論物理學中的因果集理論（causal set theory）等領域為這一復雜主題提供了額外的見解。盡管有這些發展，但在特定計算系統中事件及其因果關系的明確描述尚未得到廣泛研究。在本文中，我們首先通過考察超圖重寫背景下連續事件之間產生的事件概念和因果關系開始，并用范疇論的術語進行框架化。對于那些尋求進一步探索超圖重寫的人，Wolfram 物理項目 [5] 是一個極好的資源。值得注意的是，Wolfram 語言中提供了幾個與超圖重寫相關的工具，如 [1] 中所演示。

我們將在下一節展示，上述所有內容都可以用范疇論的術語優雅地表述，這在文獻中被稱為雙推出重寫（double-pushout rewriting）。關于這一點的極好解釋可以在文獻 [7] 中找到。

2 超圖重寫的范疇論表述

我們稱 H H 為圖生成（graph production），或輸出圖。即使不滿足無懸空邊（no-dangling edge）條件，也是可以進行圖重寫的——我們可以構造切割圖，然后粘合圖 R R。然而，如果我們想在任意范疇中進行重寫，那么雙推出（double-pushout，簡稱 DPO）重寫是首選的形式體系 [7]。一般來說，DPO 重寫可以在粘著范疇（adhesive categories）中進行，這類范疇是指那些推出補（pushout complements）在同構意義下唯一的范疇。關于粘著范疇的簡明介紹見 [8]。

定義（粘著范疇）：如果一個范疇 C C 滿足以下條件，則稱為粘著的（adhesive）：

• 它擁有沿單態射（monomorphisms）的推出（pushouts）
• 它擁有拉回（pullbacks）
• 沿單態射的推出是 Van-Kampen 方塊

關于 Van-Kampen (VK) 方塊的定義見 [8]。推出補的唯一性直接源于 VK 方塊條件。我們可以證明我們的范疇 H H 是粘著的。我們首先證明我們的范疇是廣延的（extensive）。

定義（廣延范疇）：當一個范疇 C C 滿足以下條件時，稱為廣延的（extensive）：

• 它擁有有限余積（finite coproducts）
• 它擁有沿余積注入（coproduct injections）的拉回
• 給定一個底行是余積的圖，

3 因果性

兩個不同的事件有可能應用于圖 G G 的不同位置，然而導致同構的輸出圖。理想情況下，人們會希望區分這些圖，為此不應使用雙推出重寫方法（因為推出補和推出僅在同構意義下被描述）。為了做到這一點，可以使用一個標記函數，將關于該事件的信息編碼在輸出圖中。這將在下一節關于確定 λ λ-演算中因果關系的語境中看到。然而，對于因果性的初步討論，考慮 H H 的同構類就足夠了。此外，以下內容可以推廣到任何粘著范疇（adhesive category），而在這些范疇中，典范標記（canonical labelling）是未知的。

4 λ-演算中的因果性

4.1 先前工作概述

從上文可以看出，集合上的因果關系不能是自反的。第二個關系明確指出，如果 x x 導致 y y ，那么 y y 不能導致 x x ，這在大多數物理和計算機系統中似乎是成立的（我們將在稍后討論物理學中的因果性概念及其與我們在本文中使用的概念的關系）。Winskel 擴展了因果集的定義以區分并發事件和因果斷開的事件。即，兩個并發事件必須是因果斷開的，但反過來不一定成立。例如，可能存在事件 A A 和 B B ，它們可能使用某些共同的“資源”，即兩者不能同時發生，但誰也不 導致 誰。在超圖重寫的情況下，例如，2 個可以一起發生但具有非空接口圖重疊的事件是因果斷開的，但它們不能順序發生，因為一個刪除了另一個匹配中的一些頂點/邊。所以它們不是并發的。在 [6] 中，并發定義如下：

第二個條件指出，如果一個有限的事件集 X X 都能發生在同一個計算歷史中，那么這些事件的一個子集 Y Y 也能發生在同一個歷史中，這是一個顯而易見的陳述。Con 中所有元素均為有限子集這一要求源于有限原因公理。啟用關系（enabling relation）被視為因果依賴關系的替代。

我們現在定義多路系統（multiway system）的概念，它由從單個 λ λ -表達式開始的所有可能的求值路徑組成。多路系統在 Wolfram 物理項目 [5] 中無處不在。

5 未來工作

原文鏈接： https://arxiv.org/pdf/2409.01006