GENERALIZATION OF TERMS VIA UNIVERSAL ALGEBRA
通過泛代數實現術語的泛化
https://arxiv.org/pdf/2502.18259
摘要
我們為“基于等式理論”的項的泛化問題 提供了一種新的基礎性方法。我們將泛化問題解釋為一個泛代數 (universal algebra)的框架,并在與所考慮的等式理論相關的簇(variety)中,關鍵性地使用了投射代數 (projective algebras)和精確代數 (exact algebras)。我們證明,一個泛化問題的“一般性偏序集”(generality poset)及其類型(即最小一般解的完全集合的基數)可以在這種代數設定下進行研究。
此外,我們識別出一類簇,在這些簇中對“一般性偏序集”的研究可以完全歸約為對“單生成自由代數”(1-generated free algebra)的同余格(congruence lattice)的研究。我們將這些結果應用于代數簇和(可代數化的)邏輯中。特別地,我們得到了若干具有單位型 (unitary type)的例子:阿貝爾群、交換幺半群和交換半群;所有其“單生成自由代數”是平凡的簇,例如格、半格、不含常量且運算滿足冪等性的簇;布爾代數、Kleene 代數、G?del 代數——它們分別是經典邏輯、三值 Kleene 邏輯和 G?del-Dummett 邏輯的等價代數語義。
1. 引言
如果一個項 t 可以通過對另一個項 s 進行變量替換得到,則稱 s 是 t 的一個泛化 (generalization)。識別兩個或多個項的共同泛化問題是大量研究的重點,這一研究最早由 Plotkin [44]、Popplestone [45] 和 Reynolds [49] 在一系列論文中展開,并于 1970 年收錄在同一本論文集中。
這些初始論文的目標是對歸納推理過程的形式化抽象。術語上,文獻 [44] 中將這種抽象稱為“歸納泛化”(inductive generalization),而近期文獻則簡單稱之為“泛化過程”(generalization processes)(參見例如 [16])。在這里我們遵循后一種用法。
在此背景下,主要目標是尋找“最佳”解,即那些盡可能接近定義問題的原始項的泛化項。這個最優解集合的基數 被稱為該問題的“泛化類型”(generalization type)。
本文提出了一種新的關于等式泛化 (equational generalization)的基礎性方法,即在某個等式理論下理解項之間的等價關系。我們的方法基于泛代數 ,這是處理等式理論最自然的環境,因為從模型類(即簇)的角度來看,泛代數正是研究等式理論的理想框架。
已有若干作者在理論計算機科學領域研究了基于等式理論的泛化問題 [5, 11, 46, 8]。迄今為止,大多數相關結果都是通過特定技術獲得的(參見如半環上的結果 [15],以及冪等操作的結果 [16]),而人們對建立一種通用的、基礎性的方法的興趣日益增長(參見最近的綜述 [17])。
在文獻中,用于求解泛化問題的各種方法和技術通常統稱為反合一 (anti-unification)。這一術語暗示了泛化與更為人熟知的合一問題 (unification problems)之間的聯系,后者旨在尋找給定項對的共同實例化。
我們的方法確實受到了 Ghilardi 關于等式合一問題的代數框架 [30] 的啟發。由于它允許使用(泛)代數技術 [1, 2, 26, 33, 52] 以及利用 Priestley 類 [10, 13, 12, 32] 和幾何對偶性 [29, 40, 53] 等對偶理論方法,這種方法已在文獻中被廣泛采用。
正如我們在本文中也將展示的那樣,泛代數視角的一個優勢在于它可以揭示問題與解的本質不變量:將問題轉化為代數設定有助于識別哪些問題共享相同的解,以及哪些解在所考慮的等式理論下本質上是等價的。
在本文中,我們將等式泛化問題 (以下簡稱 e-泛化問題)及其解翻譯為特殊類代數之間的同態映射 ,特別是所考慮等式理論對應簇中的投射代數 和精確代數 。我們的第一個主要結果表明,“泛化類型”可以在完全代數的設定下進行研究(定理 3.6,推論 3.7)。
在我們的分析中起關鍵作用的是所考慮簇中的“單生成代數”。雖然“單生成”不是一個范疇論意義上的概念,但我們證明,只要保持自由代數的范疇等價(在 [41] 中簡稱為等價),我們的結果仍然成立(定理 3.8);此外,范疇方法也可以并將在研究 e-泛化問題中發揮作用,這在最后一節中以 Kleene 代數簇為例進行了說明。
在發展一般理論之后,我們利用一些基本的泛代數工具,提出了一種基于所考慮簇中“單生成自由代數的同余格”的研究方法;特別地,我們識別出一類簇,使得對泛化類型的分析可以完全歸約到對此同余格的研究(定理 4.19)。最后,我們給出了一個充分條件,確保某個簇中的任何泛化問題都存在“最優解”,即具有單位型(推論 4.25)。
借助我們的方法,我們能夠處理來自代數和可代數化邏輯 [9, 28] 的多種例子。特別地,我們展示了以下簇中的泛化問題具有單位型:
阿貝爾群、交換半群和交換幺半群(例 4.26);
所有其“單生成自由代數”是平凡的簇,例如格、半格、不含常量且運算滿足冪等性的簇(例 4.22);
布爾代數、Kleene 代數、G?del 代數,它們分別是經典邏輯、三值 Kleene 邏輯和 G?del-Dummett 邏輯的等價代數語義(第 5 節)。
第 2 節為預備知識;
第 3 節發展代數 e-泛化問題的一般理論;
第 4 節通過所考慮簇中“單生成自由代數”的同余格研究 e-泛化類型;
第 5 節將我們的結果應用于可代數化邏輯中。
2. 預備知識 2.1 泛代數預備知識:投射性與精確性
對于所有未解釋的泛代數概念,我們參考文獻 [42]。
若 ρ 是一個代數類型,則一個 ρ-等式 (ρ-equation)是兩個 ρ-項 組成的一對,我們記作
(p, q) ,并形象地寫作 p ≈ q 。
一組相同類型下的等式集合 Σ 被稱為一個等式理論 (equational theory)。
在下文中,我們通常省略類型,僅考慮等式,并假設有一個固定的類型;當我們考慮一個代數類 K 時,也假設其中的所有代數具有相同的類型。
我們用 Tρ(X) 表示由變量集 X 生成的、關于類型 ρ 的絕對自由代數 (absolutely free algebra),
用 FK(X) 表示類 K 關于 X 的自由代數 (free algebra)。
如果 X = {x} ,我們常將 FK({x}) 簡寫為 FK(x) 。
給定任意一個變量集 X ,我們將從 X 到某個同類型代數 A 的一個函數 h 稱為對 X 的一個賦值 (assignment),它唯一地擴展為從 Tρ(X) 到 A 的一個同態映射(我們也稱之為 h )。
如果 h(p) = h(q) 在代數 A 中成立,我們就說代數 A 在賦值 h 下滿足等式 p ≈ q ,記作
A, h ? p ≈ q ;
如果對所有賦值 h ,都有 A, h ? p ≈ q ,則稱 A 是等式 p ≈ q 的模型,記作
A ? p ≈ q 。
如果 Σ 是一個等式理論,則稱 A 是 Σ 的模型,記作
A ? Σ ,當且僅當對所有的 σ ∈ Σ 都有 A ? σ 。
最后,如果一個代數類 K 中的每個代數都是 Σ 的模型,則稱 K 是 Σ 的模型類,記作
K ? Σ 。
一個代數類是一個簇 (variety),當且僅當它是某個等式理論的所有模型構成的類。
等價地說,簇是那些在如下代數操作下封閉的代數類:取同態像、子代數和直積。
因此,簇包含其所有自由代數。
固定一個簇 V ,所謂一個替換 (substitution)是指 FV(ω) 上的一個自同態,即在可數無窮個變量上生成的 V 中的自由代數。
注意,替換完全由它對每個生成變量所賦予的值決定。
通常我們考慮的替換只在一個變量子集 X 上不同于恒等映射,并將其映射到由另一變量集 Y 上寫出的項中;
我們通過將這樣的替換視為從 FV(X) 到 FV(Y) 的一個同態來強調這一點。
我們現在引入投射代數 (projective algebras),它在我們的研究中起著關鍵作用。
定義 2.1 . 給定一個代數類 K ,若對任意 A, B ∈ K 、任意同態映射 h : P → B 和滿射同態映射 g : A → B ,都存在一個同態映射 f : P → A ,使得 h = g ? f ,則稱代數 P ∈ K 是 K 中的投射代數 (projective in K)。
一般來說,要確定一個類 K 中哪些代數是投射的是困難的;
但只要 K 包含其所有自由代數(尤其當 K 是一個簇時),那么投射性就有一個更直觀的刻畫。
我們稱代數 A 是代數 F 的一個回縮 (retract),如果存在同態映射 i : A → F 和 j : F → A ,使得j ? i = idA (從而 i 必然是單射的,而 j 必然是滿射的)。
下面這個定理最初由 Whitman 對格結構證明 [54],但它在一般情況下也是廣為人知的:
(注:接下來的內容應為 Whitman 定理的具體陳述,但在原始文本中被截斷。根據上下文,該定理應指出:一個代數是投射的當且僅當它是某個自由代數的回縮。)
定理 2.2 . 如果一個代數類 K 包含其所有的自由代數,那么一個代數 P 在 K 中是投射的當且僅當它是 K 中某個自由代數的回縮 (retract)。
因此,一個類 K 中的自由代數在 K 中顯然是投射的。
由于上述對簇中投射代數的刻畫將在本文中被廣泛使用,我們方便地用如下圖示來圖形化表示它:
鑒于上述表示,并為了突出確定回縮的兩個映射 i 和 j 的作用,我們今后將稱該投射代數 P 是 FV(Y) 的一個 (i, j)-回縮 ((i, j)-retract)。
2.2 e-泛化問題
對于一個泛化問題 t,人們通常感興趣的是確定其 泛化序 (generality poset)中的極小解集合是否存在、以及它的基數(即元素個數)。這些信息被編碼在 e-泛化類型 (e-generalization type)中。直觀上,它給出了“最優”(即最不一般)解的類的基數。讓我們更精確地定義。
請注意,如果簇 V具有例如有限型的 e-泛化 2-類型 ,我們不能用同樣的推理來得出它具有有限型的 e-泛化類型 ,因為上述證明中描述的過程可能不會終止。我們暫時將“每個簇的 e-泛化類型是否與其 2-類型相同”這一問題留作開放問題。
在結束預備章節之前,我們再做一個最后的觀察。
注記 2.8 :對于更熟悉合一問題(unification problems)的讀者來說,值得強調的是:e-泛化問題的解及其泛化序的行為與合一理論中的行為是不同的。
3. e-泛化問題的一個代數表述
在本節中,我們提出一個關于 e-泛化問題的新穎的通用代數方法 (universal-algebraic approach)。我們的出發點是這樣的直覺:給定一個符號泛化問題 t1,…,tm,每一個項都定義了某個自由代數中的一個由單個元素生成的子代數,即一個單生成的正合代數 E(tk)。
正如我們在注記 2.8 中所暗示的那樣,在研究泛化序時,為每個 k=1,…,m,我們需要固定具體的項 tk,而不僅僅是它所生成的那個正合代數(因為該正合代數可能有不同的生成元)。
因此,一個符號問題的所有解所構成的偏序集,以及特別是最不一般解的存在性,都可以通過代數方法來研究。我們由此可以推得,對于一個簇 V 的 e-泛化類型也是如此,它是該簇所有 e-泛化問題中出現的最差類型。
熟悉 Ghilardi 在文獻 [30] 中對合一問題所進行的代數研究的讀者會注意到,我們的結果具有類似的風格,但也存在一些顯著差異。重要的是,合一問題及其類型的研究所涉及的只是簇中有限展示代數 與投射代數 之間的同態;由于這些概念都是范疇論意義上的,因此可以直接得出:合一類型在范疇等價下是保持不變的。
而根據上述方法,我們并不能得到同樣的結論,因為我們關鍵性地使用了單生成的 (1-generated)(自由)代數,而“單生成”這一性質通常在范疇等價下并不保持。盡管如此,我們將證明:e-泛化類型在一個更強的范疇等價概念——即文獻 [41] 中所稱的等價 (equivalence)——之下仍然是保持的,這種等價在代數范疇中是相當常見的。讓我們更精確地說明這一點。
對于未加解釋的范疇論概念,我們建議讀者參考文獻 [39]。
給定任意一個代數類 K,我們可以考慮其對應的代數范疇,仍用相同的符號表示,其中對象是 K中的代數,態射是同態。兩個代數范疇 K與 L是等價的 (equivalent),如果它們通過某個保持自由代數的函子 Γ在范疇意義上等價,即對所有 X,都有 。
特別地,對于兩個簇 V與 W,它們是等價的當且僅當從范疇論角度看它們的代數理論是同構的,或者從通用代數角度看它們的克隆 (clones)是同構的;參見文獻 [41] 中的相關討論。
一個代數 e-泛化問題的定義中所涉及的所有概念——包括其解以及泛化序——都在這種等價下保持不變;因此我們可以用以下結論結束本節。
4. 基于同余的解偏序集研究
在本節中,我們利用 e-泛化問題的代數表示所提供的洞察力,開展對解的泛化偏序集的研究,其指導思想是所考慮簇中單生成自由代數 的同余格。
我們首先刻畫 e-泛化問題及其解的核(kernel),并利用它們來研究解的偏序結構。接著,我們識別出一類特殊的簇,后文將其稱為 1ESP 簇 ,在這類簇中,解的泛化偏序結構的研究完全歸約為對單生成自由代數的投射同余 (projective congruences)的研究。最后,我們對泛化類型進行代數分析,得出一些一般性結果,并給出一個簇具有單一型 (unitary type)的充分條件,即:有限個單生成正合代數的直積是投射的。
特別地,我們將證明以下簇具有單一型的 e-泛化類型 :阿貝爾群、交換半群和幺半群,以及所有其單生成自由代數為平凡代數的簇(例如:格、半格、沒有常元且運算均為冪等運算的簇)。
4.1. 通過同余研究 e-泛化問題
我們現在將刻畫在由一個同態 h 給出的 e-泛化問題中,哪些 單生成自由代數 的同余可以作為 ker(h) 出現;但在開始之前,我們首先需要一個技術性引理。
換句話說,一個單生成自由代數的同余 θ是某個代數 e-泛化問題的核,當且僅當它是有限個正合同余 的交。
4.2. 通過同余表示的代
現在我們轉向刻畫那些作為代數問題解之核的同余。
讓我們首先考慮群 與阿貝爾群 的簇。在兩種情況下,單生成自由代數都同構于整數加法群 Z=(Z,+,?,0)。
它的商代數包括:
自身 Z ;
平凡群 0 ;
對每個正整數 n ,有限循環群 Zn 。
顯然,Z和 0都是單生成自由代數 Z的子代數,因此它們是正合的 。然而,任何有限非平凡群都不能作為自由群的子代數出現。因此,Z的正合商代數只有它自身和平凡群 0,而這兩者都是投射的 (因為它們是自由的;其中 0是由零個生成元生成的自由(阿貝爾)群)。
因此,群簇和阿貝爾群簇 都是 1EP 簇 。
此外,許多來自邏輯的簇也是 1EP 簇 ;例如,Heyting 代數 (因為所有正合 Heyting 代數都是投射的,見 [31, Remark pp. 867–868]),以及我們將在最后一節看到的:布爾代數 、G?del 代數 和 Kleene 代數 。
然而,也可以構造一些不具有 1EP 性質 的簇的例子;下面的例子歸功于 Tommaso Moraschini(私人通信)。
5. 應用于(可代數化的)邏輯
在本節中,我們將迄今為止所獲得的結果應用于邏輯系統 的研究。考慮一個定義在語言 ρ上的邏輯 L,它由某個對替換封閉的后承關系 (consequence relation)來刻畫:
在可代數化邏輯 (algebraizable logics)的背景下(詳見 [9, 28]),由邏輯等價給出的等式理論正好對應于該邏輯的等價代數語義 (equivalent algebraic semantics)KL所生成的等式理論。相關的簇(variety)是包含 KL的最小簇,換句話說,就是由 KL生成的簇3。當 KL本身就是一個簇時,我們說該邏輯是強可代數化的 (strongly algebraizable),此時情況更為簡化。
因此,為了研究可代數化邏輯的 e-泛化問題,我們只需研究其對應的代數簇的 e-泛化類型。
在這一總體視角下,我們現在研究一些最著名的(可代數化)邏輯,并給出布爾代數、G?del 代數和 Kleene 代數簇具有單一型 (unitary type)的例子。
5.1 經典邏輯
我們首先考慮的是經典邏輯及其等價代數語義——布爾代數簇 BA。
根據例 4.15 中的推理,我們可以得出布爾代數簇是 1ESP 的。由推論 4.20 可知,對于 BA中的一個問題 h,其類型恰好等于 G(h)的類型;而根據推論 4.7,這又由位于 E-同余 ker(h)之下的所有投射同余所決定。
現在,由定理 4.4 可得,E-同余正是 Con(FBA(z))中所有有限個正合同余的交 (這些正合同余本身也是投射的)。
圖 2 展示了自由布爾代數 FBA(z)及其同余格;其中除了全同余 ?外,其余所有同余都是投射的。顯然,E-同余正是所有這些投射同余;并且對于每一個這樣的投射同余而言,其下方的所有投射同余集合都有最大元(即它自己)。
因此,應用推論 4.20,我們得到如下結果,這與句法情形 [44] 類似:
定理 5.1 :經典邏輯與布爾代數的 e-泛化類型是單一型 (unitary)。
請注意,我們也可以通過推論 4.25 得到上述結論,因為所有有限生成的布爾代數,特別是有限個單生成的正合布爾代數的直積,都是投射的。
5.2 G?del-Dummett 邏輯
G?del-Dummett 邏輯是研究最多的中間邏輯 之一,位于直覺邏輯與經典邏輯之間 [25]。它的語言包括連接詞 (∧,∨,→,0,1),從代數角度看,其等價代數語義是G?del 代數簇 GA,它是由所有鏈(即全序代數)生成的 Heyting 代數的子簇,參見 [36]。
由于所有非平凡的有限 G?del 代數都是投射的(見 [24, Proposition 2.5] 利用類似于 Priestley 對偶性的方法證明,或 [1, Theorem 5.17] 中的代數證明),因此 GA具有 1EP 性質 。
然而,不難看出 1ESP 性質并不成立 ,正如下面的例子所示。
5.3 三值 Kleene 邏輯
最后,我們考慮三值 Kleene 邏輯 ,也稱為 Kleene 的“強不確定性邏輯”(strong logic of indeterminacy);這是經典邏輯的一個推廣,在其標準模型中為真值常元引入了一個額外的不確定值 [38]。它的代數語義是Kleene 代數簇 KA,它是帶有對合運算 ?的有界分配格的一個子簇 [37]。
具體來說,KA由以下公理刻畫:
6. 結論
我們所提出的代數方法為研究 e-泛化問題 提供了一個全新的視角和新的技術工具,不僅適用于一般的等式理論,也特別適用于(可代數化的)邏輯系統。
我們強調了 e-泛化問題及其解在泛化性下的不變量,并利用單生成自由代數的同余 對其進行了刻畫。這些同余總是能夠揭示一個問題的解偏序集的一些結構特征,在某些情況下甚至可以完全刻畫它。
正如最后一節所暗示的那樣,我們的方法可以有效地應用于大量不同的例子研究。除了已討論的案例之外,還有一些非常值得關注的簇也適用于我們的方法,其中最有趣的例子之一是Heyting 代數 ,從邏輯角度看,對應的就是直覺主義邏輯 。事實上,Heyting 代數是一個 1EP 簇 。
另一個來自邏輯的重要 1EP 簇 是 MV-代數簇 ,它是無限值 Lukasiewicz 邏輯的等價代數語義。要處理這些例子,需要進行更深入的研究,這已經超出了本文的范圍;但我們計劃在未來的工作中繼續探索。
另一個值得進一步研究的重要方向是 e-泛化在反駁系統 (refutation systems)中的作用。所謂反駁系統,是指用于推導非有效公式 的公理系統 [50, 51, 18];在這樣的系統中,“反向替換規則”會從一個非有效的公式推出其所有泛化項的不可證性。這種系統與我們當前的理論之間可能存在聯系,值得進一步探討。
最后,泛化問題已經在多個領域中得到了廣泛應用,例如:
- 歸納邏輯程序設計
(inductive logic programming)[43, 20, 35],
- 并行編程
(parallel programming)[7],
- 概念融合
(conceptual blending)[27],
- 基于案例的推理
(case-based reasoning)[4]。
將這些應用與我們在本文中建立的理論框架相連接,也將是一個有價值的研究方向。
原文鏈接: https://arxiv.org/pdf/2502.18259
特別聲明:以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布,本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.