使用初始函子来形式化图示等式推理

在计算机代数领域，e-graphs（等式图）已成为用于等式推理的强大数据结构，它们通过维护表达式树上的一致关系来实现这一功能。虽然这些结构通常使用 union-find 等标准算法来实现，但一个新的范畴论视角表明，e-graphs 的视觉特性可以通过范畴论的视角进行形式化，从而提供一种更系统的方法来操作和证明方程。

E-Graphs 在等式推理中的作用

e-graph 是一种旨在维护表达式树上一致关系的数据结构——这是一种即使在形成新表达式时仍保持稳定的等价关系。这些结构最早于 1980 年设计，由于它们能够执行等式饱和（equality saturation）技术（一种用于推导给定系统中所有可能等式的技术），近年来引起了广泛关注。

虽然传统的计算机代数侧重于底层数据结构（如 union-find），但 e-graphs 的图示性质暗示了一种潜在的范畴结构。通过将方程视为交换图，研究人员可以朝着更正式的操作语义迈进，以描述这些图是如何被操作的。

使用初始函子形式化图示追踪

在范畴论中，图是从索引范畴（形状）到目标范畴的函子。如果相同域和余域之间的所有路径都导致相等的态射，则该图“交换”。为了推导新方程，必须使用特定的推理规则来转换这些图。

这些有效转换的核心机制是“初始函子”。如果一个函子的拉回（pullback）保留极限，则该函子被认为是初始的。直观地说，这意味着如果一个图代表一个方程组，那么沿着初始函子拉回该图将保留这些方程的所有可能解集。

这可以通过组合方式进行检查：为了使一个函子成为初始函子，“逗号范畴”（代表函子与对象之间关系的结构）必须是非空的且连通的。这提供了一种系统、机械的方法来验证哪些图示移动在数学上是有效的。

机械证明与实际应用

该框架允许对标准代数属性进行机械证明，例如“粘贴律”。该定律指出，共享公共边的两个交换方可以连接成一个更大的交换矩形。通过从单例图开始并应用一系列初始函子（如操作引入和一致关系简化），通过证明极限保持不变来证明矩形的交换性。

目前，这种特定方法仅限于具有仅含一元函数符号的范畴，以减少设置复杂度。未来的迭代将扩展到具有有限积的范畴，以恢复 e-graphs 的完整标准设置，从而允许进行更复杂的等式推理。