如何用图表证明等式，第一部分
How to prove equations using diagrams, part 1
Topos Institute 博客文章探讨用图表证明等式的方法，从 e-graph（等式图）出发，介绍 egglog 在 CatColab 中推理有限呈现范畴的实践。文章提出以初始函子（initial functor）为核心概念，先在不含额外结构的范畴中展开，后续将推广到有限积范畴以还原标准 e-graph 设定。
本文同步发布于 Topos Institute 博客。
e-graph（“等式图”的简称）是一种数据结构，用于在表达式树上维护同余关系：即在构造新表达式时保持稳定的等价关系。它最早由 Nelson 和 Oppen 于 1980 年提出（Nelson 1980；Nelson and Oppen 1980）。后来，Willsey 等人通过他们的软件包 egg 证明，e-graph 与等式饱和相结合，可以成为快速、强大且适应性强的等式推理工具，这使 e-graph 重新获得了大量关注（Willsey et al. 2021）。在我自己关于 CatColab 的工作中，我开始使用 egg 的后继者 egglog（Zhang et al. 2023）来对有限呈现范畴进行推理。
从 Nelson 的博士论文（Nelson 1980）开始，标准的论述都强调实现 e-graph 所需的数据结构和算法，例如并查集数据结构。计算机代数领域的工作最终必须以这种方式落到实处，这一点至关重要。不过，我还是忍不住想：如果从实现细节中抽象出来，e-graph 究竟真正在做什么？e-graph 的图解和可视化特性在交互式 egglog 演示中表现得如此明显，这会让任何范畴论学者想到，范畴论的思想可能在其中隐式地发挥作用。
最近有两个团队为 e-graph 提出了范畴语义（Biondo, Castelnovo, and Gadducci 2025；Tiurin et al. 2025）。在不深入细节的情况下，两者都将“e-超图”定义为一个带标签的超图，并配备额外的结构，这些结构直接或间接地指定了一个等价关系。他们的出发点是说明 e-graph 是什么。尽管我最终会提出自己关于“e-图”的定义，但我将首先考虑 e-graph 是如何被操作的，最终目标是为 e-graph 计算给出范畴语义和操作语义。关键概念将是初始函子。
在这篇文章中，我将介绍不带任何额外结构的范畴的主要思想。与 e-graph 相比，这一设定会相当受限——它对应于只允许一元函数符号——但它的优点是能以最少的准备工作把我们带到要点上。在未来的文章中，我们将推广到具有有限积的范畴，并恢复 e-graph 的标准设定。
用图表示方程
如果你接触过任何抽象代数，你很可能见过范畴论学者如何通过画交换图来表示态射之间的方程。例如，说态射的方块
在某个范畴中交换，意思是方程 \(g \circ f = k \circ h\) 成立。
让我们回顾一下形式定义，这些定义是标准的，尽管并非没有细微差别。
定义 1 范畴 \(\mathsf{C}\) 中的图是一个函子 \(D: \mathsf{J} \to \mathsf{C}\)，其定义域 \(\mathsf{J}\)（图的索引范畴或形状）是一个小范畴。进一步的术语：
- 如果图表的形状是自由范畴，即 \(\mathsf{J} =\mathrm{Path}(G)\) 由（可能无限的）图 \(G\) 自由生成，则该图表是自由的；
- 如果图表的形状是有限呈现范畴，则该图表是有限呈现的；
- 如果对于 \(\mathsf{J}\) 中每一对具有相同定义域和陪域态射，它们在 \(\mathsf{C}\) 中的像都相等，则该图表交换，或称交换的。
注意，一个图表完全可以既是自由的又是交换的：自由性仅仅是图表形状的性质，而交换性还关键地涉及图表在目标范畴中的像。
在实践中，我们处理的是自由且有限呈现的图表。这意味着图表的形状由一个有限图自由生成，这是一种易于在计算机上实现的数据结构。在进行计算机代数时，目标范畴本身将由生成元和关系有限呈现。最初，我们“已知”的唯一方程是那些作为关系明确给出的方程。我们的目标是通过操作目标范畴中的图表来推导出更多方程。
但是等等：如果有限呈现范畴中的图表可以仅用任何计算机科学家都熟悉的图论概念来描述，那么引入范畴和函子的意义何在？我们将看到，范畴论对于简洁地描述图表的有效操作是不可或缺的。这些操作采取图表之间的态射形式，即满足额外性质的函子。
初始函子
用图表推理，或称“图表追逐”，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}\)，如果以下任一等价条件成立：
- 沿 \(R\) 的拉回保持极限：若 \(\mathsf{C}\) 是一个范畴，且 \(D:\n\mathsf{K} \to \mathsf{C}\) 是 \(\mathsf{C}\) 中的一个图，则极限之间的典范态射 \[\lim_{\mathsf{K}} D \to \lim_{\mathsf{J}} (D \circ R)\] 是同构，只要所涉及的极限存在。
- 沿 \(R\) 的拉回保持集合的极限：若 \(D: \mathsf{K} \to \mathsf{Set}\) 是一个集合图，则极限之间的典范函数 \[\lim_{\mathsf{K}} D\n\to \lim_{\mathsf{J}} (D \circ R)\] 是双射。
- 相对于 \(R\) 的切片是连通的：对任意对象 \(k \in \mathsf{K}\)，逗号范畴 \(R/k\) 非空且连通。2
关于（该等价的对偶的）证明，见 (Riehl 2014, Lemma 8.3.4)。
若对极限有良好的直觉，初始性的极限刻画很有用，因为通常只需想象集合的极限会发生什么，就能一眼看出给定的函子是否是初始的。另一方面，切片刻画则具体且语法化，因而也有用。回忆一下，给定函子 \(R: \mathsf{J} \to \mathsf{K}\) 和对象 \(k \in \mathsf{K}\)，逗号范畴 \(R/k\) 具有
- 作为对象：一个对象 \(j \in \mathsf{J}\) 连同 \(\mathsf{K}\) 中的一个态射 \(f: R(j) \to\nk\)；
- 作为态射 \((j, f) \to (j', f')\)：\(\mathsf{J}\) 中的态射 \(h: j \to j'\)，使得三角形交换：
在典型情形下，所涉及的范畴是自由且有限生成的，因此证明初始性——即检查每个逗号范畴 \(R/k\) 非空且连通——就归结为一个组合问题。
解释
为什么初始函子与等式推理相关？一般来说，一个图的极限可以看作一个对象，它表示该图所假定的方程的所有可能解。这一解释在原范畴 \(\mathsf{Set}\) 中很清楚：在那里，一个一般公式将集合图的极限给出为满足由形状的态射所索引的方程的所有元素元组的子集。也就是说，图 \(D: \mathsf{J} \to \mathsf{Set}\) 的极限是所有元组 \((x_j)_{j \in \mathsf{J}}\) 的集合，其中 \(x_j \in D(j)\)，使得所有方程
\[ D(f)(x_i) = x_j, \qquad \forall f: i \to j\ \text{in}\ \mathsf{J}, \]
成立 (Leinster 2014, Example 5.1.22)。因此，由于沿初始函子的拉回保持极限，直观上初始函子就是那些保持由图所呈现的方程组的“解集”的函子。
然而，我们的兴趣在于目标为有限呈现范畴 \(\mathsf{C}\) 的图 \(D: \mathsf{J} \to \mathsf{C}\)。这类范畴很少有许多非平凡积或等化子。我们可以通过两种方式绕过这个问题。
首先，我们总是可以考虑该呈现的集合论解释，即函子 \(F: \mathsf{C} \to \mathsf{Set}\)。那么复合 \(F \circ D: \mathsf{J} \to \mathsf{Set}\) 就是一个集合的图，我们便回到了所有极限都存在的标准情形。e-graph 社区在谈论“未解释函数”或“函数符号”时（对我们而言，即 \(\mathsf{C}\) 的生成态射）采取的就是这一视角。对未解释函数推导出的任何等式，在将它们解释为集合间实际函数的任何解释下仍然成立。因此，如果你有一个对于函数等式推理完备的形式证明系统，那么在该系统中就存在对使用初始函子推导出的等式的证明。3
稍加留意，我们可以更进一步，推导出在任意范畴 \(\mathsf{C}\) 中成立的等式。假设我们从 \(\mathsf{C}\) 中的一个单元素图开始，它索引单个对象 \(X \in \mathsf{C}\)。该图的极限显然存在，就是 \(X\) 本身。因此，任何通过沿初始函子拉回或延拓该图而得到的图，都将继续以 \(X\) 为其极限。特别地，在这样的图中，任何起始于 \(X\) 的两条平行路径都必须交换。我们将在后续的计算中使用这一技巧。当我们推广到具有有限乘积的范畴时，它会变得更加强大，因为那时我们可以从任意有限离散图开始，其索引对象充当“自由变量”。
示例与计算
本文的剩余部分将通过常见示例和显式计算来说明初始函子的概念。目的是提示如何将初始函子用于图的机械推理，进一步的理论发展留待下次。
初始函子中的母题
让我们从几个初始函子的最小示例开始，它们充当母题或模式。每个这样的示例都将产生一条用于图解推理的推理规则。
图的靶范畴 \(\mathsf{C}\) 自始至终固定。也就是说，任何初始函子也应当是 \(\mathsf{C}\) 中图的范畴，即切片范畴 \(\mathsf{Cat}/\mathsf{C}\) 中的态射。
操作引入：对于 \(\mathsf{C}\) 中的任意态射 \(f: X \to Y\)，图映射
是初始的。
更一般地，对于 \(\mathsf{C}\) 中的任意路径 \(X_0 \xrightarrow{f_1} X_1 \xrightarrow{f_2} \cdots \xrightarrow{f_n} X_n\)，图映射
是初始的。
同余约简：对于 \(\mathsf{C}\) 中的任意态射 \(f: X \to Y\)，图映射，4
将定义域形状中的 \(y\) 和 \(y'\) 都送到余定义域形状中的 \(y\)，是初始的。
将操作引入和同余约简都包含在内，对于 \(\mathsf{C}\) 中的任意态射 \(f: X \to Y\) 和数 \(n \geq 0\)，图映射，
将 \(y_1,\dots,y_n\) 全部送到 \(y\)，是初始的。
方程引入：假设方程 \(g \circ f = k \circ h\) 在 \(\mathsf{C}\) 中成立，如前所示。那么自由图表张成中的两个映射
都是初始的。更一般地，这对 \(\mathsf{C}\) 中的任何路径方程都成立。作为另一个例子，我们可以引入一个零元路径方程，比如 \(\operatorname{id}_X = g \circ f\)，如下所示：
稍后，我们将不仅形式化这些规则，还将形式化如何应用它们，使用来自范畴论重写的思想。目前，我们暂且认为在更大的上下文中应用规则时，所得函子仍然是初始的。或者，你可以在每次应用时通过检查来验证初始性。
粘贴交换方块
我们准备进行第一次计算，证明交换方块的粘贴律：两个有公共边的交换方块可以并置产生一个交换矩形。记号使这看起来显然为真——这正是好记号的特点！——但它仍然需要证明。我们将以高度机械化的风格呈现证明，其中序列中的每个图表都通过一个初始函子或（在引入方程时）通过初始函子的张成与前一个图表相关联。
假设：给定两个交换方块
我们的意思是，目标范畴 \(\mathsf{C}\) 由六个对象生成，称为 \(X,X',Y,Y',Z,Z'\)，以及七个态射，称为 \(f,f',g,g',h,k,\ell\)，并满足这两个方程。
构造：从 \(X\) 上的单点图表开始，其极限显然是 \(X\)。引入我们要证明的路径方程的左侧和右侧：
将路径 \(X \xrightarrow{h} X' \xrightarrow{f'} Y'\) 识别为第一个方块的左侧，然后引入该方程：
对 \(f\) 的出现应用同余归约：
现在将路径 \(Y \xrightarrow{k} Y' \xrightarrow{g'} Z'\) 识别为第二个方块的左侧，然后引入该方程：
我们已经完成了，但不妨整理一下，对 \(g\) 的出现进行同余归约，然后对 \(\ell\) 进行同余归约：
结论：外矩形交换，因为图表的极限仍然是 \(X\)。
一个幺半群表示
考虑一个幺半群，其中元素 \(f\) 满足方程
\[ f^3 = \operatorname{id}= f^5. \]
也就是说，目标范畴 \(\mathsf{C}\) 由单个对象（比如 \(\bullet\)）和一个自同态 \(f: \bullet \to \bullet\) 生成，并满足这两个方程。
从单点图表 \(\{\bullet\}\) 开始，引入两个定义方程，注意由于每个方程的一侧是恒等，它们表现为循环：
我们将箭头留作未标记，因为每个箭头都位于生成态射 \(f\) 之上。我们现在将计算同余闭包，迭代应用同余归约直到不再可能。受同余归约影响的箭头在归约的两侧颜色相同，从上面的两个蓝色箭头开始。第一次归约是：
接下来：
再进行三次同余归约得到序列：
我们可以到此为止，但也不妨再归约两次，得到以 \(f\) 为自环的图。我们已经证明了等式
\[ f = \operatorname{id}, \]
因为该图的极限正是我们出发时的那个，即唯一的对象 \(\bullet\)。换言之，所呈现的幺半群实际上就是平凡幺半群。你可能还记得，这是群论中一个事实的特例：若群元素 \(g\) 对互素的数 \(m\) 和 \(n\) 满足 \(g^m = \operatorname{id}= g^n\)，则 \(g = \operatorname{id}\)。
讨论
范畴论常被说成是抽象的，甚至被称为“抽象废话”，但正是抽象与具体之间的相互作用赋予了范畴论力量。初始函子及其互补的内在描述与语法描述，正是这种相互作用的例证。
我们已经开始探索初始函子如何成为 e-graph 操作语义的基础。我们不是像通常的“小步”操作语义那样先定义各个步骤再将它们串联起来，而是通过初始函子以不变的方式定义有效变换，然后寻找有用的特化。除了其概念内容之外，这种灵活性之所以重要，是因为实际系统往往将归约批量处理以提高效率。对我们来说，这通常就相当于复合初始函子。
不过我们还没有直接联系到 e-graph，尽管已有许多暗示。另一个暗示是，我们的最后一个例子直接取自 Nelson 和 Oppen 的早期工作 (Nelson 1980; Nelson and Oppen 1980)，在其中它是一个贯穿始终的例子。在后续文章中，我们将加强与 e-graph 的联系。我们还将解释这一形式化如何推广到具有有限积的范畴，即代数理论的范畴对应物。
参考文献
Biondo, Roberto, Davide Castelnovo, and Fabio Gadducci. 2025. “EGGs Are Adhesive!” arXiv:2503.13678.
Leinster, Tom. 2014. Basic Category Theory. Cambridge University Press. DOI:10.1017/CBO9781107360068. arXiv:1612.09375.
Nelson, Greg. 1980. “Techniques for Program Verification.” PhD thesis, Stanford University.
Nelson, Greg, and Derek C. Oppen. 1980. “Fast Decision Procedures Based on Congruence Closure.” Journal of the ACM 27 (2): 356–64. DOI:10.1145/322186.322198.
Riehl, Emily. 2014. Categorical Homotopy Theory. Cambridge University Press. DOI:10.1017/CBO9781107261457. https://math.jhu.edu/~eriehl/cathtpy.pdf.
Tiurin, Aleksei, Barrett Chris, Dan R. Ghica, and Nick Hu. 2025. “Equivalence Hypergraphs: DPO Rewriting for Monoidal e-Graphs.” arXiv:2406.15882.
Willsey, Max, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. “Egg: Fast and Extensible Equality Saturation.” Proceedings of the ACM on Programming Languages 5 (POPL): 1–29. DOI:10.1145/3434304. arXiv:2004.03082.
Zhang, Yihong, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. “Better Together: Unifying Datalog and Equality Saturation.” Proceedings of the ACM on Programming Languages 7 (PLDI): 468–92. DOI:10.1145/3591239. arXiv:2304.04332.
脚注
在本系列中，我们首先使用裸范畴，之后再推广到笛卡尔范畴。最传统形式的图追踪发生在加法范畴与阿贝尔范畴中，这是推广的另一个方向。尝试将我们的方法扩展到加法设定会很有趣，先从以交换幺半群或阿贝尔群富化的范畴开始。↩︎
这并不是说，给出由完备性所蕴含的证明是容易或方便的。据我所知，证明提取是 e-graph 社区中一个活跃的研究课题。↩︎
在绘制图表 \(D: \mathsf{J} \to \mathsf{C}\) 时，“类型论式”记号 \(x: X\) 命名索引范畴 \(\mathsf{J}\) 中的一个对象 \(x\)，该对象被映射到目标范畴 \(\mathsf{C}\) 中的对象 \(X\)。将图表视为一个项图，对象 \(x\) 确实是一个“类型为 \(X\) 的项”。↩︎
来源：Hacker News · epatters.org