如何用图证明等式（第一部分）：从 e-graph 到初始函子

Topos Institute 博客文章探讨如何用范畴论中的图（diagram）来证明等式，提出以初始函子（initial functor）刻画 e-graph 计算的合法操作。文章先在不含额外结构的范畴中展开，对应只允许一元函数符号的受限情形，后续将推广到有限积范畴以还原标准 e-graph 设定。文中提及 egglog 及近期两篇为 e-graph 建立范畴语义的工作。