Equivalence Hypergraphs: E-Graphs for Monoidal Theories
<|reference_start|>Equivalence Hypergraphs: E-Graphs for Monoidal Theories: 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.<|reference_end|>
@article{ghica2024equivalence,
    title={Equivalence Hypergraphs: E-Graphs for Monoidal Theories},
    author={Dan R. Ghica, Chris Barrett, Aleksei Tiurin},
    journal={arXiv preprint arXiv:2406.15882},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.15882},
    primaryClass={cs.LO math.CT}
}