博客文章：如何用图示证明等式（第一部分）

本文同步发布于 Topos Institute 博客。

e-graph（“等式图”的缩写）是一种数据结构，用于维护表达式树上的同余关系：即在构造新表达式时保持稳定的等价关系。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})（图的索引范畴或形状）是一个小范畴。进一步的术语：

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

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

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

用图进行推理，或称“图追踪”，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 字，完整内容请点「打开原文」。）