通过泛代数实现术语的泛化 GENERALIZATION OF TERMS VIA UNIVERSAL ALGEBRA

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