The technique of equipping graphs with an equivalence relation, called equality saturation, has recently proved both powerful and practical in program optimisation, particularly for satisfiability modulo theory solvers. We give a categorical semantics to these structures, called e-graphs, in terms of Cartesian categories enriched over a semilattice. We show how this semantics can be generalised to monoidal categories, which opens the door to new applications of e-graph techniques, from algebraic to monoidal theories. Finally, we present a sound and complete combinatorial representation of morphisms in such a category, based on a generalisation of hypergraphs which we call e-hypergraphs. They have the usual advantage that many of their structural equations are absorbed into a general notion of isomorphism.

翻译：为图配备等价关系的技术（称为等式饱和）近期在程序优化领域被证明兼具强大性与实用性，尤其在可满足性模理论求解器中。我们为这类称为e-图的结构建立了范畴语义学解释，其基础是半格上丰富的笛卡尔范畴。我们展示了该语义如何推广至幺半范畴，这为e-图技术从代数理论到幺半群理论的新应用开辟了道路。最后，基于超图的推广形式——我们称之为e-超图——我们提出了此类范畴中态射的一个可靠且完备的组合表示。该表示具有常规优势：其众多结构等式可被吸收到广义的同构概念中。