用图证明方程：e-graphs 的范畴论视角

How to prove equations using diagrams, part 1

e-graph（等式图）作为等式饱和推理的核心数据结构，近年来在 `egg` 和 `egglog` 等工具中展现出强大威力。本文跳出传统实现细节，从范畴论角度重新审视 e-graphs 的本质。作者提出利用“初始函子”（initial functor）来形式化图的变换规则，确保在操作过程中方程的解集保持不变。通过引入操作、同余归约和方程引入等模式，文章机械地证明了交换方块的粘合律，并展示了如何在有限呈现的范畴中推导新方程。这种将图论操作与范畴语义结合的方法，为计算机代数中的等式推理提供了更深层的理论基础。