Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs

TL;DR

This paper introduces a categorical semantics for e-graphs in monoidal categories, generalizes hypergraph representations to e-hypergraphs, and enables DPO rewriting for these structures, advancing program optimization techniques.

Contribution

It provides a new categorical framework for e-graphs in monoidal categories and develops a DPO rewriting method for e-hypergraphs, expanding their applicability.

Findings

Categorical semantics for e-graphs in monoidal categories.

A combinatorial representation of morphisms via e-hypergraphs.

A sound and complete DPO rewriting approach for e-hypergraphs.

Abstract

The technique of \emph{equality saturation}, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called \emph{e-graphs}, in terms of Cartesian categories enriched over the category of semilattices. This approach generalises 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 \emph{e-hypergraphs}. They have the usual advantage that many of their structural equations are absorbed into a general notion of isomorphism. This new principled approach to e-graphs enables double-pushout (DPO) rewriting for these structures, which constitutes the main contribution of this paper.