教程：如何用图表证明等式（第一部分）

这篇文章同时在 Topos Institute 博客上发布。

e-graph，全称“equality graph”（等式图），是一种维护表达式树上的同余关系的数据结构：所谓同余关系，就是在构造新表达式时保持稳定的等价关系。e-graph 最早由 Nelson 和 Oppen 于 1980 年提出（Nelson 1980; Nelson and Oppen 1980）。Willsey 等人通过他们的软件包 egg 证明，e-graph 结合等式饱和（equality saturation）可以成为快速、强大且适应性强的等式推理工具，此后 e-graph 重新获得了大量关注（Willsey et al. 2021）。在我自己关于 CatColab 的工作中，我开始使用 egg 的后继者 egglog（Zhang et al. 2023）来对有限呈现范畴进行推理。

从 Nelson 的博士论文（Nelson 1980）开始，标准的介绍都强调实现 e-graph 所需的数据结构和算法，比如并查集（union-find）数据结构。计算机代数领域的工作最终必须这样落到实处，这一点至关重要。不过，我还是不禁要想：如果把实现细节抽象掉，e-graph 本质上究竟在做什么？e-graph 的图解性和可视化特性——在 egglog 的交互式 demo 中表现得如此明显——会让任何范畴论学者想到，范畴论的思想可能在其中隐式地起作用。

最近有两个团队分别为 e-graph 提出了范畴语义（Biondo, Castelnovo, and Gadducci 2025; Tiurin et al. 2025）。具体细节暂且不谈，两者都把“e-hypergraph”定义为一个带标签的超图，并配备额外的结构，这些结构直接或间接地指定了一个等价关系。他们的出发点是说明 e-graph 是什么。尽管我最终会提出自己关于“e-diagram”的定义，但我会先从考察 e-graph 如何被操作入手，最终目标是为 e-graph 计算给出范畴语义和操作语义。关键概念将是初始函子（initial functor）。

在这篇文章中，我将针对不带任何额外结构的范畴介绍主要思想。与 e-graph 相比，这个设定限制相当大——它对应于只允许一元函数符号——但它的优点是能让我们以最少的准备工作直达要点。在后续文章中，我们会推广到具有有限积的范畴，并恢复 e-graph 的标准设定。

如果你接触过任何抽象代数，你很可能见过范畴论学者如何通过画交换图来表示态射之间的等式。例如，说某个范畴中的态射方块

交换，意思就是等式 (g \circ f = k \circ h) 成立。

让我们回顾一下形式定义，这些定义是标准的，尽管并非没有细微差别。

定义 1 范畴 (\mathsf{C}) 中的一个图（diagram）是一个函子 (D: \mathsf{J} \to \mathsf{C})，其定义域 (\mathsf{J})——图的索引范畴或形状——是一个小范畴。进一步的术语：

注意，一个图完全可以既是自由的又是交换的：自由性仅仅是图形状的属性，而交换性还关键地涉及图在目标范畴中的像。

在实践中，我们处理的是自由且有限呈现的图。这意味着图的形状由一个有限图自由生成，而有限图是一种很容易在计算机上实现的数据结构。在做计算机代数时，目标范畴本身将由生成元和关系有限呈现。最初，我们“知道”的等式只有那些作为关系明确给出的等式。我们的目标是通过操作目标范畴中的图，推导出目标范畴中更多的等式。

但等等：如果一个有限呈现范畴中的图可以只用任何计算机科学家都熟悉的图论概念来描述，那么引入范畴和函子又有什么意义呢？我们将看到，范畴论对于简洁地描述图的合法操作是不可或缺的。这些操作采取图之间的态射的形式，而图之间的态射就是满足额外性质的函子。

用图进行推理，或者说“图追逐”（diagram chasing），1 是将给定的图，比如 (D: \mathsf{J} \to \mathsf{C})，按照某些推理规则变换为另一个图 (D': \mathsf{J}' \to \mathsf{C}) 的艺术。在通常的数学实践中，没人会费心说明这些规则是什么。我们力求更加系统化。

让我们考虑一下可以做出的显而易见操作。给定一个图 (D: \mathsf{J} \to \mathsf{C})，我们可以沿函子 (R: \mathsf{J}' \to \mathsf{J}) 将它拉回，得到另一个图 (D' \mathrel{\vcenter{:}}=D \circ R: \mathsf{J}' \to \mathsf{C})。反过来，我们可以通过找到一个函子 (R: \mathsf{J} \to \mathsf{J}') 以及一个图 (D': \mathsf{J}' \to \mathsf{C}) 使得 (D = D' \circ R)，来扩展图 (D)：

如果不做更多假设，上述两条设想的推理规则没有一条在精确保持图所呈现的等式的解的意义上是有效的（这一点后面会精确说明）。为此，我们需要 (R) 是一种特殊的函子，即初始函子，它由下面的定义/定理刻画。

定理 1（初始函子） 一个函子 (R: \mathsf{J} \to \mathsf{K}) 是初始的，这里记作 (R: \mathsf{J} \twoheadrightarrow \mathsf{K})，如果以下等价条件中的任何一个成立：

关于这个等价性（的对偶）的证明，见（Riehl 2014, Lemma 8.3.4）。

如果对极限有良好的直觉，初始性的极限刻画是很有用的，因为你通常只要想象一下集合的极限会发生什么，就能一眼看出给定的函子是否是初始的。另一方面，切片刻画则很有用，因为它具体且是语法的。回忆一下，给定函子 (R: \mathsf{J} \to \mathsf{K}) 和对象 (k \in \mathsf{K})，逗号范畴 (R/k) 具有

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）