如何使用图表证明方程，第 1 部分

这篇文章交叉发布在 Topos Institute 博客上。 e-graph 是“等式图”的缩写，是一种在表达式树上维护同余关系的数据结构：在形成新表达式时稳定的等价关系。电子图首次由 Nelson 和 Oppen 于 1980 年设计（Nelson 1980；Nelson 和 Oppen 1980），当 Willsey 等人通过他们的软件包 Egg 证明电子图与等式饱和相结合可以成为快速、强大且适应性强的方程推理工具时，电子图受到了新的关注（Willsey 等人，2021）。在我自己的 CatColab 工作中，我开始使用 Egg 的后继者 Egglog (Zhang et al. 2023) 来推理有限呈现的类别。标准演示从 Nelson 的博士论文 (Nelson 1980) 开始，强调实现电子图所需的数据结构和算法，例如并查数据结构。计算机代数工作最终以这种方式落地是至关重要的。尽管如此，我还是忍不住想知道，从实现细节中抽象出来，电子图到底是怎么回事。电子图的图解和视觉本质，在交互式 Egglog 演示中如此明显，将向任何类别理论家表明，类别思想可能隐含在起作用。两个小组最近提出了电子图的分类语义（Biondo、Castelnovo 和 Gadducci 2025；Tiurin 等人 2025）。在不深入细节的情况下，两者都将“电子超图”定义为配备有直接或间接指定等价关系的额外结构的标记超图。他们的出发点是解释什么是电子图。虽然我最终会提出我自己的“电子图”定义，但我将首先考虑如何操作电子图，最终目标是为电子图计算提供分类和操作语义。关键概念是初始函子。在这篇文章中，我将介绍类别的主要思想，而无需任何额外的结构。与电子图相比，此设置将具有相当的限制性 - 它将对应于仅允许一元函数符号 - 但它的优点是使我们能够以最少的设置达到目的。在以后的文章中，我们将推广到具有有限产品的类别并恢复电子图的标准设置。使用图表表示方程如果您遇到过任何抽象代数，您可能已经了解范畴论学家如何通过绘制交换图来表示态射之间的方程。例如，说某个类别中态射的平方可交换意味着方程 \(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}\) 中的图像是相等的。请注意，图很可能既是自由的又是可交换的：自由性仅是图形状的属性，而交换性也与图在目标类别中的图像关系密切。在实践中，我们使用免费且有限呈现的图表。这意味着图的形状是由有限图自由生成的，有限图是一种易于在计算机上实现的数据结构。在进行计算机代数时，目标类别本身将由生成器和关系有限地表示。最初，我们“知道”的唯一方程是作为关系明确给出的方程。我们的目标是通过操纵目标类别中的图表来推导目标类别中的进一步方程。但是等等：如果可以仅使用任何计算机科学家都熟悉的图论概念来描述有限呈现类别中的图，那么引入类别和函子的意义何在？我们将看到范畴论对于简洁地描述图表的有效操作是必不可少的。这些操作采用图之间态射的形式，它们是满足额外属性的函子。初始函子图推理，或“图追逐”，是将给定图（例如 \(D: \mathsf{J} \to \mathsf{C}\) ）转换为另一个图 \(D': \mathsf{J}' \to \mathsf{C}\) 的艺术，遵循一定的推理规则。在普通的数学实践中，没有人费心去说明这些规则是什么。我们的目标是更加系统化。让我们考虑一下我们可以采取的明显行动。给定一个图 \(D: \mathsf{J} \to \mathsf{C}\) ，我们可以沿着函子 \(R: \ma