GATlab：用廣義代數(shù)理論進行建模與編程

GATlab：用廣義代數(shù)理論進行建模與編程

GATlab: Modeling and Programming with Generalized

Algebraic Theories

https://arxiv.org/pdf/2404.04837v3

摘要

范疇和范疇結(jié)構(gòu)作為科學(xué)與工程建模中有用的抽象工具，正日益得到認可。為了在軟件中統(tǒng)一地實現(xiàn)范疇論數(shù)學(xué)模型，我們引入了 GATlab，這是一種嵌入在通用編程語言中的、用于代數(shù)規(guī)約的領(lǐng)域特定語言。GATlab 基于廣義代數(shù)理論（GATs），這是一種擴展了依賴類型的代數(shù)理論的邏輯系統(tǒng)，旨在涵蓋范疇論。使用 GATlab，程序員可以指定廣義代數(shù)理論及其模型，包括基于符號表達式的自由模型，以及由宿主語言中的任意代碼定義的計算模型。此外，程序員可以定義理論之間的映射，并利用它們以聲明式的方式將一個理論的模型遷移到另一個理論的模型。簡而言之，GATlab 旨在為計算機代數(shù)和軟件接口設(shè)計提供一個基于廣義代數(shù)理論的統(tǒng)一環(huán)境。在本文中，我們描述了 GATlab 的設(shè)計、實現(xiàn)及應(yīng)用。

關(guān)鍵詞： 廣義代數(shù)理論，GATs，代數(shù)規(guī)約，編程語言，應(yīng)用范疇論

1 引言

范疇論長期以來一直被認為是編程中一種有用的組織原則。范疇論與類型論之間廣泛的對應(yīng)關(guān)系——起源于笛卡爾閉范疇與帶積類型的 lambda 演算之間的等價性 [21]——促使語言設(shè)計者將各種各樣的范疇概念引入編程語言中。在這種用法中，范疇論充當(dāng)了編程語言的數(shù)學(xué)模型，通常為其提供指稱語義。但這并不是范疇論在編程中能扮演的唯一角色。應(yīng)用范疇論學(xué)者已經(jīng)展示了范疇論如何能夠形式化科學(xué)與工程中潛在的復(fù)合結(jié)構(gòu)，從關(guān)系數(shù)據(jù)庫到隨機和量子過程，再到微分方程和動力系統(tǒng) [37,15,13,24]。范疇論現(xiàn)在成為了主題領(lǐng)域的數(shù)學(xué)模型，而（像任何模型一樣）如果它能在軟件中實現(xiàn)，它將是最有用的。因此，我們需要一個能夠輕松表達并計算范疇結(jié)構(gòu)的軟件系統(tǒng)。

這一目標可以通過根據(jù)范疇論思想設(shè)計宿主語言來實現(xiàn)，但原則上并不依賴于它。事實上，目前這兩種角色之間存在張力，因為最自然地表達范疇概念的依賴類型語言往往缺乏科學(xué)與工程計算的功能，而科學(xué)家和工程師最常用的語言則通常只有極簡的類型系統(tǒng)。這個問題可以從兩個方向著手解決。在這項工作中，我們展示了如何增強現(xiàn)有的技術(shù)計算語言，為其添加高級類型系統(tǒng)，從而實現(xiàn)對范疇結(jié)構(gòu)的統(tǒng)一計算。

與其試圖將完整的依賴類型理論強行移植到弱類型編程語言上，我們采用廣義代數(shù)理論（Generalized Algebraic Theories），這是代數(shù)理論的擴展，足以公理化范疇結(jié)構(gòu)。廣義代數(shù)理論（GAT）[8,9]——更貼切地稱為依賴類型代數(shù)理論 [33]——與（有類型或排序的）代數(shù)理論類似，區(qū)別在于其類型可以依賴于項。GAT 的原型例子是范疇論，其中態(tài)射的類型依賴于一對對象，即定義域和陪域。盡管 GAT 是一種相對簡單的類型理論，但它足以公理化本質(zhì)上任何由配備了額外代數(shù)（方程）定義的結(jié)構(gòu)的范疇所組成的理論。可作為 GAT 公理化的范疇結(jié)構(gòu)示例包括：范疇；預(yù)層和余預(yù)層；幺半范疇（無論是嚴格的還是弱的，辮狀的還是對稱的）；配備了選定有限積或有限極限的范疇；以及 2-范疇、雙范疇和雙重范疇。

1.1 貢獻

在本文中，我們描述了 GATlab 的設(shè)計與實現(xiàn)，這是一個基于 Julia 編程語言構(gòu)建的嵌入式領(lǐng)域特定語言的廣義代數(shù)理論編程框架。GAT 長期以來一直是 Catlab 的基礎(chǔ)，Catlab 是一個專注于科學(xué)和工程應(yīng)用的應(yīng)用范疇論框架。我們最近從頭重寫了 GAT 系統(tǒng)，并顯著擴展了其功能。這是我們首次在印刷出版物中對其進行描述。

GATlab 的主要貢獻包括：

• 在技術(shù)編程語言中提供一種基于極簡依賴類型理論的代數(shù)規(guī)約語言；
• 支持包含超過 90 個可重用理論的標準庫，范圍從群和環(huán)等經(jīng)典代數(shù)結(jié)構(gòu)到幺半范疇和預(yù)層等范疇結(jié)構(gòu)；
• 實現(xiàn)對 GAT 模型的統(tǒng)一計算，包括基于符號表達式的自由模型，以及由宿主語言中的任意代碼定義的計算模型；
• 通過理論的態(tài)射，以聲明式和代數(shù)的方式將一個理論的模型遷移到另一個理論。

簡而言之，GATlab 旨在成為科學(xué)與工程中范疇結(jié)構(gòu)化建模工具的結(jié)構(gòu)化和符號化基礎(chǔ)。

1.2 相關(guān)工作

GATs 的數(shù)學(xué)理論及其在軟件中的應(yīng)用都有著悠久的歷史。本節(jié)我們將回顧其中部分歷史，并闡釋 GATlab 與之的關(guān)系。

最古老的相關(guān)研究脈絡(luò)是泛代數(shù)（universal algebra）理論。“泛代數(shù)”這一術(shù)語至少可追溯至懷特海 [39]，但該學(xué)科直到伯克霍夫 1946 年的論述 [3] 才奠定了形式化基礎(chǔ)。后來，勞維爾在其博士論文中展示了泛代數(shù)中的許多構(gòu)造如何自然地源于范疇論的基本概念 [23]。

泛代數(shù)的早期實現(xiàn)見于 OBJ 和 Clear 語言 [16,5]。Clear 語言的模塊系統(tǒng)影響了標準 ML 模塊系統(tǒng)的設(shè)計 [28,29] 以及后續(xù) OBJ 系列語言的迭代版本 [17]。這些泛代數(shù)概念的現(xiàn)代表現(xiàn)形式可見于 Maude 等系統(tǒng) [12]。我們最初為 GATlab 設(shè)定的目標之一，便是在 Julia 中構(gòu)建一個受 ML 啟發(fā)的模塊系統(tǒng)，使理論的實現(xiàn)成為可具體化的對象，正如簽名（signature）的實現(xiàn)在 ML 中那樣。直到后來我們才意識到，ML 模塊本身便是受泛代數(shù)啟發(fā)的，因此從某種意義上說，GATlab 繼承了一個久負盛名的傳統(tǒng)。

然而，GATlab 超越了這一傳統(tǒng)，它采用了廣義代數(shù)理論，將泛代數(shù)擴展至包含依賴類型，而這正是范疇論所必需的。用依賴類型擴展泛代數(shù)的挑戰(zhàn)已通過多種方式得到解決。一種途徑是通過邏輯框架（LF），該框架最早由 [20] 提出。邏輯框架是一種操縱依賴類型論語法的代數(shù)方法，即通過將依賴類型論嵌入到另一個依賴類型論中來實現(xiàn)。GATlab 扮演著與 LF 類似的“元”角色，但不支持對變量進行量化的類型構(gòu)造子。另一方面，GATlab 提供了 LF 所不具備的其他功能，例如向理論中添加任意方程的能力。此前人們認為這是一個壞主意，因為它會破壞類型檢查和相等性檢查的可判定性。但正如我們將展示的，即使在缺乏可判定類型檢查的情況下，利用 GATs 仍能完成有趣且有用的工作。

GATlab 強調(diào)以理論態(tài)射作為在不同理論間轉(zhuǎn)換及通過余極限組合理論的手段，這一思路也見于數(shù)學(xué)知識管理（MKM）系統(tǒng) MMT [34]；MMT 支持更廣泛的理論類別，但對計算語義的關(guān)注較少。同樣，這種 MKM 方法也見于 MathScheme [6] 以及關(guān)于理論展示組合子的相關(guān)工作 [7]。

最后，GATlab 是范疇及其他范疇結(jié)構(gòu)的計算實現(xiàn)。此方向上的相關(guān)項目包括 Rydeheard 和 Burstall 的計算范疇論 [36]，以及 CAP（Categories, Algorithms, and Programming）計算機代數(shù)系統(tǒng) [19,2]。

2 背景：廣義代數(shù)理論及其模型

我們回顧廣義代數(shù)理論（GATs）背后的主要思想，重點關(guān)注其語法（包括數(shù)學(xué)記號和 GATlab 編程記號）以及其標準的集合論語義。GATs 由 John Cartmell 在其博士論文 [8] 中引入，隨后在出版物 [9] 中發(fā)表，本文省略的許多細節(jié)可參閱該文獻。作為進一步的參考，Pitts [33, §6] 和 Taylor [38, Chapter VIII] 介紹了基于 Cartmell 的 GATs 的類型理論。

2.1 GATs 的語法

項構(gòu)造器（Term constructor） 帶類型的項由項構(gòu)造器引入。項本身及其類型均可依賴于上下文中的變量。

項相等性（Term equality） 斷言上下文中項之間等式的公理，通過項相等性來指定。

例如，范疇論包含兩個類型構(gòu)造器，分別對應(yīng)對象和態(tài)射；兩個項構(gòu)造器，分別對應(yīng)復(fù)合和單位態(tài)射；以及三個項相等性，分別對應(yīng)結(jié)合律、左單位律和右單位律公理。

作為技術(shù)補充說明，我們注意到，根據(jù) Cartmell 的觀點，GATs 還允許第四種判斷，即類型之間的相等性。我們遵循 Taylor [38] 的做法，在 GATlab 中排除了類型相等性。這一限制簡化了系統(tǒng)，即便它并未解決類型檢查問題（因為依賴類型仍可能因其所依賴的項之間的等式而產(chǎn)生非平凡的相等關(guān)系）。從范疇論的角度來看，禁止顯式的類型相等性并無損失，因為類型之間的等式無論如何都更適合用同構(gòu)來處理。

具體而言，這一限制使得種類檢查（sort-checking）和種類推斷（sort-inference）變得相當(dāng)簡單。種類推斷用于確定項的類型所使用的類型構(gòu)造器。例如，它將一個項歸類為對象或態(tài)射，而不必確切地找出該態(tài)射的定義域或陪域。這是一種實用且快速的檢查，我們在 GATlab 的大多數(shù)操作中都會執(zhí)行它，能夠捕獲表層的錯誤。

2.3 GATs 的替代方案

廣義代數(shù)理論屬于一族本質(zhì)上等價的邏輯，這些邏輯擴展了代數(shù)理論的邏輯，以涵蓋范疇論及其他類似理論。除了 GATs 之外，這些邏輯中最著名的是本質(zhì)代數(shù)理論（essentially algebraic theories）[1, §3.D]、有限極限草圖（finite limit sketches）和有限極限理論（finite limit theories）。Cartmell 勾勒了一個論證，大意是在其集合論語義下，廣義代數(shù)理論和本質(zhì)代數(shù)理論具有等價的模型范疇 [9, §6]。與此同時，本質(zhì)代數(shù)理論和有限極限草圖直接被意圖作為有限極限理論（一種理論的不變量概念）的語法呈現(xiàn)。

原則上，這些邏輯中的任何一種都可以扮演 GATs 在 GATlab 中所扮演的角色。我們選擇 GATs 是出于實用考慮：盡管它們的元理論很復(fù)雜，但 GATs 能產(chǎn)生迄今為止最易讀且最直觀的范疇結(jié)構(gòu)理論的呈現(xiàn)形式，往往與其教科書形式非常相似。

3 GATlab 中的 GAT 模型

在軟件工程的語境下，GATs 扮演著接口或形式規(guī)約的角色。因此，GAT 的模型就是實現(xiàn)該接口并滿足該形式規(guī)約的數(shù)據(jù)結(jié)構(gòu)。

3.1 代數(shù)理論的模型

3.2 將依賴類型納入模型

到目前為止，我們在 GATlab 中僅考慮了代數(shù)理論的模型。鑒于 Julia 并不完全具備依賴類型，我們?nèi)绾螖U展這些經(jīng)典的模型概念以支持依賴類型呢？[10] 我們曾考慮過兩種在非依賴語言中對依賴類型進行建模的方法。以范疇為例來考察這兩種方法具有啟發(fā)意義。

在這種風(fēng)格下，我們可以如下實現(xiàn)有限集范疇，或者更確切地說，是其骨架。首先，我們?yōu)檫@個范疇的對象和態(tài)射定義數(shù)據(jù)結(jié)構(gòu)。

在原始 Catlab 對 GATs 的實現(xiàn)中，采取的做法是將定義域和陪域與態(tài)射的數(shù)據(jù)一同存儲。事實上，定義域或陪域往往無法從態(tài)射的數(shù)據(jù)中推導(dǎo)出來。在上面的例子中，將函數(shù)的數(shù)據(jù)表示為一個值數(shù)組只能確定其值域（range），而不能確定其陪域（codomain），因此陪域必須單獨存儲。雖然這種方法很直觀，但其缺點是態(tài)射的數(shù)據(jù)結(jié)構(gòu)必須攜帶額外的數(shù)據(jù)。因此，一個由態(tài)射組成的圖表最終可能會存儲許多對象的冗余副本。

本節(jié)最后，我們將演示如何創(chuàng)建一個以基范疇為參數(shù)的切片范疇模型。首先，我們聲明一個模型結(jié)構(gòu)體。

3.3 GAT 的自由模型

• associate，針對結(jié)合律規(guī)范化二元運算
• associate_unit，針對結(jié)合律和單位律規(guī)范化二元運算
• associate_unit_inv，針對結(jié)合律、單位律和逆元規(guī)范化二元運算
• distribute_unary，將一元運算分配到二元運算上
• involute，規(guī)范化對合一元運算
• normalize_zero，當(dāng)表達式包含零時將其坍縮為零

然而，這些僅僅是我們發(fā)現(xiàn)有用的規(guī)范化策略；我們的方法并不排除實現(xiàn)其他策略的可能性。

4 GAT 的態(tài)射

雖然總是可以編寫任意函數(shù)將一個理論的模型轉(zhuǎn)換為另一個理論的模型，但必須編寫的代碼往往晦澀難懂且不易驗證。在許多情況下，解決這一問題的辦法在于不同的 GAT 之間通過態(tài)射（也稱為解釋）相互關(guān)聯(lián)。利用 GAT 的態(tài)射，我們實現(xiàn)了一種聲明式且可驗證的語法，用于將一個理論的模型遷移到另一個理論。

4.1 GAT 態(tài)射的語法

例如，考慮將幺半群語言中的語句翻譯為自然數(shù)算術(shù)語言：

上述例子可以與用戶聲明的、類型錯誤或給出無效解釋的態(tài)射進行對比：

4.2 GAT 態(tài)射子類的數(shù)據(jù)結(jié)構(gòu)

GAT 的態(tài)射具有高度的表現(xiàn)力，這也帶來了一定程度的復(fù)雜性。考慮那些限制性更強、但所需指定數(shù)據(jù)更少的 GAT 態(tài)射會是很有用的。這些限制更強的 GAT 態(tài)射也使得計算（例如推挽圖）變得更加容易。GATlab 定義了不少于四種數(shù)據(jù)結(jié)構(gòu)來實現(xiàn)不同表現(xiàn)力的 GAT 態(tài)射：

4.3 利用 GAT 態(tài)射進行計算

5 應(yīng)用與擴展

在創(chuàng)建 GATlab 包以替代 Catlab 中的 GAT 機制時，我們的首要目標是探索新的設(shè)計決策，例如： (i) ML 模塊風(fēng)格的 GAT 模型，以及 Haskell 類型類風(fēng)格（3.1 節(jié)）； (ii) 依賴類型的纖維化觀點與索引化觀點（3.2 節(jié)）； (iii) 通過作用域標簽進行的衛(wèi)生替換（附錄 A.1）； 但同時保留與 Catlab 足夠的向后兼容性，以便可以增量地采用這些新功能，而不是一次性全部采用。既然已經(jīng)完成了這項重大的工程工作，我們開始在整個用于應(yīng)用范疇論的 AlgebraicJulia 包生態(tài)系統(tǒng)中利用 GATlab 的新功能。

GATlab 背后的動機之一是為符號動力系統(tǒng)構(gòu)建功能。過去，我們在任意 Julia 函數(shù)之上構(gòu)建動力系統(tǒng) [24]。然而，使動力系統(tǒng)中的各種函數(shù)符號化解鎖了一系列新能力，例如：

• 系統(tǒng)可以被優(yōu)化/編譯以生成更高效的代碼
• 系統(tǒng)可以進行符號分析以證明其性質(zhì)，而無需對其進行模擬
• 系統(tǒng)可以在不同的編程語言之間轉(zhuǎn)移
• 定義系統(tǒng)的方程可以被美觀地打印并顯示給用戶

第一篇作者寫了一篇博客文章探討了這些方向 [25]，并且我們有一個作為操作代數(shù)（operad algebra）的符號資源共享器的初步實現(xiàn) [26]。值得注意的是，GATlab 允許我們實現(xiàn)這些符號資源共享器，使其不依賴于符號函數(shù)實現(xiàn)中可用的確切“原始函數(shù)”集合。例如，我們可以只允許多項式函數(shù)，或者只允許多項式和三角函數(shù)，等等。

為了支持這些系統(tǒng)理論能力，GATlab 的另一個主要方向是開發(fā)更豐富的計算機代數(shù)功能。我們有興趣探索類型如何有助于為超越經(jīng)典抽象代數(shù)的數(shù)學(xué)對象開發(fā)計算機代數(shù)。例如，我們已經(jīng)原型化了一個理論，其中主要的研究對象是“向量叢的截面”，其中向量叢本身和向量叢所在的空間都是類型構(gòu)造器的參數(shù)。這將使得微分幾何中的問題能夠進行 principled（有原則的）、無坐標的描述，并通過在 Decapodes [32,31] 中的應(yīng)用而應(yīng)用于偏微分方程。

我們正在考慮幾種方式為 GATlab 添加更復(fù)雜的重寫功能以用于計算機代數(shù)目的。基于對 egg 源代碼 [40] 的仔細閱讀，我們已經(jīng)原型化了針對 GATlab 語法樹的 e-graphs 實現(xiàn)。然而，Julia 已經(jīng)有了一個優(yōu)秀的 e-graphs 實現(xiàn)，即 Metatheory.jl [10]，我們希望與之集成。無論如何，e-graphs 的優(yōu)勢在于它們幾乎適用于任何重寫問題，這與 GATs 的通用性非常契合。然而，在環(huán)和模等專業(yè)領(lǐng)域中，涉及 Gr?bner 基的算法可能比樸素地使用 e-graphs 高效得多。我們可以通過 Symbolics.jl [18] 和 CAP 項目 [2] 在 Julia 中訪問此類計算機代數(shù)系統(tǒng)，因此另一個方向是將這些集成到 GATlab 中的特定理論中。

GATs 的一個局限性是，雖然我們可以為范疇指定一個 GAT，但 GATs 只有模型的 1-范疇而不是 2-范疇。因此，從范疇的 GAT 中，我們可以自動導(dǎo)出函子的概念，但不能導(dǎo)出自然變換的概念。Lambert 和 Patterson 有一個“笛卡爾雙重理論”的概念 [22]，其模型自然地形成一個 2-范疇，這可能是一個比廣義代數(shù)理論更自然的框架來用于“范疇的計算機代數(shù)”。

未來研究的另一個方向是隨機測試。這可以通過兩種方式完成。第一種是取理論中的一個任意方程（其有效性不確定），然后檢查它在 GAT 的隨機采樣有限模型中是否為真。當(dāng)然，這不能證明該方程為真，但它可以提供 Nitpick [4] 和 Alloy [30] 風(fēng)格的反例。第二種方法是取一個聲稱的 GAT 模型，然后在該模型中采樣類型的元素，以檢查 GAT 中的方程是否實際成立，采用 QuickCheck [11] 和 Hypothesis [27] 的風(fēng)格。這將提供一種廉價的方式來獲得對實現(xiàn)的信心，并提高任何使用 GATlab 的代碼的整體質(zhì)量。

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