EGGs Are Adhesive!

Biondo, Roberto; Castelnovo, Davide; Gadducci, Fabio

doi:10.4230/LIPIcs.CALCO.2025.10

EGGs Are Adhesive!

Roberto Biondo

Department of Computer Science, University of Pisa, Pisa, Italy Davide Castelnovo

Department of Computer Science, University of Pisa, Pisa, Italy Fabio Gadducci

Department of Computer Science, University of Pisa, Pisa, Italy

Abstract

The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way. E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders precise the properties of the data structure, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.

Keywords and phrases:

Hypergraphs, terms graphs, e-graphs, adhesive categories

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Models of computation ; Theory of computation

\rightarrow

Semantics and reasoning

Related Version:

Full Version: https://arxiv.org/abs/2503.13678 [6]

Funding:

The research has been partially supported by the Italian MUR - Call PRIN 2022 - Project 20228KXFN2 “Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic” (STENDHAL) and by the University of Pisa - Call PRA 2022 - Project 2022_99 “Formal Methods for the Healthcare Domain based on Spatial Information” (FM4HD).

DOI:

10.4230/LIPIcs.CALCO.2025.10

Event:

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The introduction of adhesive categories marked a watershed moment for the algebraic approaches to the rewriting of graph-like structures [25, 17]. Until then, key results of the approaches on e.g. parallelism and confluence had to be proven over and over again for each different formalism at hand, despite the obvious similarity of the procedure. Adhesive categories provides such a disparate set of formalisms with a common abstract framework where many of these general results can be recast and uniformly proved once and for all. In short, following the double-pushout (DPO) approach to graph transformation [13, 17], a rule is given by two arrows $l:K\to L$ and $r:K\rightarrow R$ and its application requires a match $m:L\to G$ : the rewriting step from $G$ to $H$ is then given by the diagram below, whose halves are pushouts.

Thus, $L$ and $R$ are the left- and right-hand side of the rule, respectively, while $K$ witnesses those parts that must be present for the rule to be executed, yet that are not affected by the rule itself. Should a category be adhesive, and the arrows of the rules monomorphisms, the presence of a match ensures that if the pushout complement $C\to G$ exists then it is unique, hence a rewriting step can be deterministically performed. The theory of $\mathcal{M}$ -adhesivity [2, 22] extends the core framework, ensuring that if the arrows of the rules are in a suitable class $\mathcal{M}$ of monomorphisms then the benefits of adhesivity can be recovered [15, 16]. If only the left-hand side belongs to $\mathcal{M}$ , the theory is still under development, as witnessed e.g. by [3]. However, despite the elegance and effectiveness, proving that a given category satisfies the conditions for being $\mathcal{M}$ -adhesive can be a daunting task. For this reason, sufficient criteria have been provided for the core framework, e.g. that every elementary topos is adhesive [24], as well as for the extended one of $\mathcal{M}$ -adhesivity [11]. For some structures such as hypergraphs with equivalence in [4], the question of their $\mathcal{M}$ -adhesivity has not yet been settled.

E-graphs (shortly, EGGs) are an up-and-coming formalism for program optimisation and synthesis via a compact representation and efficient implementation of equality saturation. Albeit a classical data structure [14], EGGs received new impulse after the seminal [31] and developed a thriving community, as witnessed by the official website [29]. The key idea of rewriting-based program optimisation is to perform the manipulation of a syntactical description of a program, replacing some of its components in such a way that the semantics is preserved while the computational costs of its actual execution are improved. Instead of directly removing sub-programs, EGGs just add the new components and link them to the older ones via the equivalence relation, until an optimal program is reached and extracted.

EGGs can be concisely defined as term graphs equipped with a notion of equivalence on nodes that is closed under the operators of a signature [14, Section 4.2]. In the presentation of term graphs via string diagrams [11], EGGs are (hyper)trees whose edges are labelled by operators and with the possibility of sharing subtrees, with an additional equivalence relation $\equiv$ on nodes that is closed under composition. In plain words and using a toy example: if $a$ and $b$ are two constants such that $a\equiv b$ , then $f(a)\equiv f(b)$ for any unary operator $f$ .

Building on the criterion developed in [11], this work proves that both hypergraphs with equivalence and EGGs form an $\mathcal{M}$ -adhesive category for a suitable choice of $\mathcal{M}$ . The advantages from this characterisation are two-fold. On the one side, we put the benefits per se of a formal presentation, making precise the properties of the data structure. On the other side, describing the optimisation steps via the DPO approach offers the tools for modelling their parallel and concurrent execution and for proving their confluence and termination.

Synopsis.

The paper has the following structure. In Section 2 we briefly recall the theory of $\mathcal{M}$ -adhesive categories and of kernel pairs. In Section 3 we present the graphical structures of our interest, (labelled) hypergraphs and term graphs, and we provide a functorial characterisation, which allows for proving their adhesivity properties. This is expanded in Section 4 for proving the $\mathcal{M}$ -adhesivity of hypergraphs and term graphs with equivalence and in Section 5 of their variants where equivalences are closed with respect to operator application, thus subsuming EGGs. In Section 6 we put the machinery at work, showing how the optimisation steps can be rephrased as the application of term graph rewriting rules. Finally, in Section 7 we draw our conclusions, hint at future endeavours and offer some brief remarks on related works. All the proofs can be found in the full version of the paper [6].

2 Facts about $\mathcal{M}$ -adhesive categories and kernel pairs

We open this background section by fixing some notation. Given a category X we do not distinguish notationally between X and its class of objects, so “ $X\in\textbf{{X}}$ ” means that $X$ is an object of X. We let $\mathsf{Mor}(\textbf{{X}})$ , $\mathsf{Mono}(\textbf{{X}})$ and $\mathsf{Reg}(\textbf{{X}})$ denote the class of all arrows, monos and regular monos of X, respectively. Given an object $X$ , we denote by $?_{X}$ the unique arrow from an initial object into $X$ and by $!_{X}$ that unique arrow from $X$ into a terminal one. We will also use the notation $e\colon X\twoheadrightarrow Y$ to denote that an arrow $e\colon X\to Y$ is a regular epi.

2.1 $\mathcal{M}$ -adhesivity

The key property of $\mathcal{M}$ -adhesive categories is the Van Kampen condition [8, 23, 25], and for defining it we need some notions. Let X be a category. A subclass $\mathcal{A}$ of $\mathsf{Mor}(\textbf{{X}})$ is said to be

$\blacksquare$

stable under pushouts (pullbacks) if for every pushout (pullback) square as the one below, if $m\in\mathcal{A}$ ( $n\in\mathcal{A}$ ) then $n\in\mathcal{A}$ ( $m\in\mathcal{A}$ );
$\blacksquare$

closed under composition if $h,k\in\mathcal{A}$ implies $h\circ k\in\mathcal{A}$ whenever $h$ and $k$ are composable;
$\blacksquare$

closed under decomposition, or left-cancellable, if whenever $g$ and $g\circ f$ belong to $\mathcal{A}$ , then $f\in\mathcal{A}$ .

Definition 2.1.

Let $\mathcal{A}\subseteq\mathsf{Mor}(\textbf{{X}})$ be a class of arrows in a category X and consider the cube below.

We say that the bottom square is an $\mathcal{A}$ -Van Kampen square if

1.

it is a pushout square;
2.

whenever the cube above has pullbacks as back and left faces and the vertical arrows belong to $\mathcal{A}$ , then its top face is a pushout if and only if the front and right faces are pullbacks.

Pushout squares that enjoy only the “if” half of item (2) above are called $\mathcal{A}$ -stable. A $\mathsf{Mor}(\textbf{{X}})$ -Van Kampen square is called Van Kampen and a $\mathsf{Mor}(\textbf{{X}})$ -stable square stable.

We can now define $\mathcal{M}$ -adhesive categories.

Definition 2.2 ([2, 15, 16, 25, 22]).

Let X be a category and $\mathcal{M}$ a subclass of $\mathsf{Mono}(\textbf{{X}})$ including all isos, closed under composition, decomposition, and stable under pullbacks and pushouts. The category X is said to be $\mathcal{M}$ -adhesive if

1.

it has $\mathcal{M}$ -pullbacks, i.e. pullbacks along arrows of $\mathcal{M}$ ;
2.

it has $\mathcal{M}$ -pushouts, i.e. pushouts along arrows of $\mathcal{M}$ ;
3.

$\mathcal{M}$ -pushouts are $\mathcal{M}$ -Van Kampen squares.

A category X is said to be strictly $\mathcal{M}$ -adhesive if $\mathcal{M}$ -pushouts are Van Kampen. We write $m\colon X\rightarrowtail Y$ to denote that an arrow $m\colon X\to Y$ belongs to $\mathcal{M}$ .

$\blacktriangleright$ Remark 2.3.

Our notion of $\mathcal{M}$ -adhesive category corresponds to what in [17] is called weak adhesive HLR category, while a strict $\mathcal{M}$ -adhesive categories corresponds to adhesive HLR ones. Finally, adhesivity and quasiadhesivity [25, 18] coincide with strict $\mathsf{Mono}(\textbf{{X}})$ -adhesivity and strict $\mathsf{Reg}(\textbf{{X}})$ -adhesivity, respectively.

$\mathcal{M}$ -adhesivity is well-behaved with respect to the construction of (co-)slice and functor categories [26], as well with respect to subcategories, as shown by the following properties, taken from [17, Thm. 4.15], [25, Prop. 3.5] and [11, Thm. 2.12].

Proposition 2.4.

Let X be an (strict) $\mathcal{M}$ -adhesive category. Then the following hold

1.

if Y is an (strict) $\mathcal{N}$ -adhesive category, $L\colon\textbf{{Y}}\to\textbf{{A}}$ a functor preserving $\mathcal{N}$ -pushouts and $R\colon\textbf{{X}}\to\textbf{{A}}$ one preserving $\mathcal{M}$ -pullbacks, then $L\hskip 1.0pt{\downarrow}R$ is (strictly) $\mathcal{N}\hskip 1.0pt{\downarrow}\mathcal{M}$ -adhesive, where

$\mathcal{N}\hskip 1.0pt{\downarrow}\mathcal{M}:=\{(h,k)\in\mathsf{Mor}(L\hskip 1% .0pt{\downarrow}R)\mid h\in\mathcal{N},k\in\mathcal{M}\}$
2.

for every object $X$ the categories $\textbf{{X}}/X$ and $X/\textbf{{X}}$ are, respectively, (strictly) $\mathcal{M}/X$ -adhesive and (strictly) $X/\mathcal{M}$ -adhesive, where

$\mathcal{M}/X:=\{m\in\mathsf{Mor}(\textbf{{X}}/X)\mid m\in\mathcal{M}\}\hskip 2% 5.0ptX/\mathcal{M}:=\{m\in\mathsf{Mor}(X/\textbf{{X}})\mid m\in\mathcal{M}\}$
3.

for every small category Y, the category $\textbf{{X}}^{\textbf{{Y}}}$ of functors $\textbf{{Y}}\to\textbf{{X}}$ is (strictly) $\mathcal{M}^{\textbf{{Y}}}$ -adhesive, where $\mathcal{M}^{\textbf{{Y}}}:=\{\eta\in\mathsf{Mor}(\textbf{{X}}^{\textbf{{Y}}})% \mid\eta_{Y}\in\mathcal{M}\text{ for every }Y\in\textbf{{Y}}\}$ ;
4.

if Y is a full subcategory of X closed under pullbacks and $\mathcal{M}$ -pushouts, then Y is (strictly) $\mathcal{N}$ -adhesive for every class of arrows $\mathcal{N}$ of Y contained in $\mathcal{M}$ that is stable under pullbacks and pushouts, contains all isos, and is closed under composition and decomposition.

We briefly list some examples of $\mathcal{M}$ -adhesive categories.

Example 2.5.

$\mathbf{Set}$ is adhesive, and, more generally, every topos is adhesive [24]. By the closure properties above, every presheaf $[\mathbf{X},\mathbf{Set}]$ is adhesive, thus the category $\mathbf{Graph}=[E\rightrightarrows V,\mathbf{Set}]$ is adhesive where $E\rightrightarrows{V}$ is the two objects category with two morphisms $s,t\colon{E}\to{V}$ . Similarly, various categories of hypergraphs can be shown to be adhesive, such as term graphs and hierarchical graphs [11]. Note that the category $\mathbf{sGraphs}$ of simple graphs, i.e. graphs without parallel edges, is $\mathsf{Reg}{(\mathbf{sGraphs})}$ -adhesive [5] but not quasiadhesive.

We can state some useful properties of $\mathcal{M}$ -adhesive category (see, for instance, [17, Thm. 4.26] or [2, Fact 2.6]).

Proposition 2.6.

Let X be an $\mathcal{M}$ -adhesive category. Then the following hold

1.

every $\mathcal{M}$ -pushout square is also a pullback;
2.

every arrow in $\mathcal{M}$ is a regular mono.

2.2 Some properties of kernel pairs and regular epimorphisms

In this section we recall the definition and some properties of kernel pairs.

Definition 2.7.

A kernel pair for an arrow $f\colon A\to B$ is an object $K_{f}$ together with two arrows $\pi^{1}_{f},\pi^{2}_{f}\colon K_{f}\rightrightarrows A$ , denoted as $(K_{f},\pi^{1}_{f},\pi^{2}_{f})$ , such that the square below is a pullback.

$\blacktriangleright$ Remark 2.8.

If $(K_{f},\pi^{1}_{f},\pi^{2}_{f})$ is a a kernel pair for $f\colon X\to Y$ and a product of $X$ with itself exists, then the canonical arrow $\langle\pi^{1}_{f},\pi^{2}_{f}\rangle\colon K_{f}\to X\times X$ is a mono.

$\blacktriangleright$ Remark 2.9.

An arrow $m\colon M\to X$ is a mono if and only if it admits $(M,\mathsf{id}_{M},\mathsf{id}_{M})$ as a kernel pair.

The previous remarks allow us to prove the following result.

Proposition 2.10.

Let $f\colon X\to Y$ be an arrow and $m\colon Y\to Z$ a mono. If $(K_{f},\pi_{f}^{1},\pi_{f}^{2})$ is a kernel pair for $f\colon X\to Y$ , then it is also a kernel pair for $m\circ f$ .

Regular epis are particular well-behaved with respect to their kernel pairs.

Proposition 2.11.

Let $e\colon X\twoheadrightarrow Y$ be a regular epi in a category X with a kernel pair $(K_{e},\pi^{1}_{e},\pi^{2}_{e})$ . Then, $e$ is the coequalizer of $\pi^{1}_{e}$ and $\pi^{2}_{e}$ .

We conclude this section exploring some properties of kernel pairs in an $\mathcal{M}$ -adhesive category. The results below are simple, yet they appear to be original.

Lemma 2.12.

Let $f\colon X\to Y$ and $g\colon Z\to W$ be arrows admitting kernel pairs and suppose that the solid part of the four squares below is given. If the leftmost square is commutative, then there is a unique arrow $k_{h}\colon K_{f}\to K_{g}$ making the other three commutative.

Moreover, the following hold

1.

if $h$ is a mono then $k_{h}$ is a mono;
2.

if the leftmost square is a pullback then the central two are pullbacks;
3.

if $h$ is mono and the leftmost square is a pullback then the rightmost is a pullback.

The previous result allows us to deduce the following lemma in an $\mathcal{M}$ -adhesive context.

Proposition 2.13.

Let X be a strict $\mathcal{M}$ -adhesive category with all pullbacks, and suppose that in the cube below the top face is an $\mathcal{M}$ -pushout and all the vertical faces are pullbacks. Then the right square is a pushout.

Focusing on $\mathbf{Set}$ , we can prove a sharper result.

Lemma 2.14.

Suppose that in $\mathbf{Set}$ the commuting cube in the diagram below on the left is given, whose top face is a pushout, the left and bottom faces are pullbacks, and $n\colon B\rightarrowtail D$ is an injection. Then the following hold

1.

the right face of the cube is a pullback;
2.

the right square, made by the kernel pairs of the vertical arrows, is a pushout.

3 Hypergraphical structures

In this section we briefly recall the notion of hypergraph. In order to do so, a pivotal role is played by the Kleene star monad $(-)^{\star}\colon\mathbf{Set}\to\mathbf{Set}$ , also known as list monad, sending a set to the free monoid on it [28, 30]. We recall some of its proprieties.

Proposition 3.1.

Let $X$ be a set and $n\in\mathbb{N}$ . Then the following facts hold

1.

there are arrows $v_{n}\colon X^{n}\to X^{\star}$ such that $(X^{\star},\{v_{n}\}_{n\in\mathbb{N}})$ is a coproduct;
2.

for every arrow $f\colon X\to Y$ , $f^{\star}\colon X^{\star}\to Y^{\star}$ is the coproduct of the family $\{f^{n}\}_{n\in\mathbb{N}}$ ;
3.

$(-)^{\star}$ preserves all connected limits [9], in particular it preserves pullbacks and equalizers.

$\blacktriangleright$ Remark 3.2.

Preservation of pullbacks implies that $(-)^{\star}$ sends monos to monos.

$\blacktriangleright$ Remark 3.3.

Notice that $1^{\star}$ can be canonically identified with $\mathbb{N}$ , thus for every set $X$ the arrow $!_{\textbf{{X}}}\colon X\to 1$ induces a length function $\mathsf{lg}_{X}\colon X^{\star}\to\mathbb{N}$ , which sends a word to its length.

3.1 The category of hypergraphs

We open this section with the definition of hypergraphs and we show how to label them with an algebraic signature.

Definition 3.4.

An hypergraph is a 4-uple $\mathcal{G}:=(E_{\mathcal{G}},V_{\mathcal{G}},s_{\mathcal{G}},t_{\mathcal{G}})$ made by two sets $E_{\mathcal{G}}$ and $V_{\mathcal{G}}$ , called respectively the sets of hyperedges and nodes, plus a pair of source and target arrows $s_{\mathcal{G}},t_{\mathcal{G}}\colon E_{\mathcal{G}}\rightrightarrows V_{% \mathcal{G}}^{\star}$ .

A hypergraph morphism $(E_{\mathcal{G}},V_{\mathcal{G}},s_{\mathcal{G}},t_{\mathcal{G}})\to(E_{% \mathcal{H}},V_{\mathcal{H}},s_{\mathcal{H}},t_{\mathcal{H}})$ is a pair $(h,k)$ of functions $h\colon E_{\mathcal{G}}\to E_{\mathcal{H}}$ , $k\colon V_{\mathcal{G}}\to V_{\mathcal{H}}$ such that the diagrams below are commutative.

We define Hyp to be the resulting category.

Let $\mathsf{prod}^{\star}$ be the functor $\mathbf{Set}\to\mathbf{Set}$ sending $X$ to the product $X^{\star}\times X^{\star}$ . We can use it to present Hyp as a comma category.

Proposition 3.5.

Hyp is isomorphic to $\mathsf{id}_{\mathbf{Set}}\hskip 1.0pt{\downarrow}\mathsf{prod}^{\star}$

Note that by hypothesis $(-)^{\star}$ preserves pullbacks, while $\mathsf{prod}$ is continuous by definition, hence by Proposition 3.5 and the characterisation of monos in comma categories we can deduce the following result.

Corollary 3.6.

A morphism $(h,k)$ is a mono in Hyp if and only if both its components are injective functions.

Applying Proposition 2.4 we also get the next corollary (cfr. [17, Fact 4.17]).

Corollary 3.7.

Hyp is an adhesive category.

Again Proposition 3.5 allows us to deduce immediately the following.

Proposition 3.8.

The forgetful functor $U_{\textbf{{Hyp}}}$ which sends a hypergraph $\mathcal{G}$ to its set of nodes has a left adjoint $\Delta_{\textbf{{Hyp}}}$ .

Example 3.9.

Since the initial object of Set is the empty set, $\Delta_{\textbf{{Hyp}}}(X)$ is the hypergraph which has $X$ as set of nodes, $\emptyset$ as set of hyperedges, and $?_{X}$ as source and target function.

Example 3.10.

We represent hypergraphs visually: dots denote nodes and boxes hyperedges. Should we be interested in their identity, we put a name near the corresponding dot or box. Sources and targets are represented by lines between dots and squares: the lines from the sources of a hyperedge comes from the left of the box, while the lines to the targets exit from the right of the box. Let us look at the picture below. It represent a hypergraph $\mathcal{G}$ with sets $V_{\mathcal{G}}=\{v_{1},v_{2},v_{3},v_{4}\}$ and $E_{\mathcal{G}}=\{h_{1},h_{2},h_{3},h_{4}\}$ of nodes and edges, respectively, such that $h_{1},h_{2}$ have no source and $h_{3},h_{4}$ a pair of nodes

$\blacktriangleright$ Remark 3.11.

It is worth to point out, as first noted in [7], that Hyp is equivalent to a category of presheaves. Indeed, consider the category H in which the set of objects is given by $(\mathbb{N}\times\mathbb{N})\cup\{\bullet\}$ and arrows are given by the identities $\mathsf{id}_{k,l}$ , $\mathsf{id}_{\bullet}$ and exactly $k+l$ arrows $f_{i}\colon(k,l)\rightarrow\bullet$ , where $i$ ranges from $0$ to $k+l-1$ . The functors $\textbf{{H}}\to\mathbf{Set}$ corresponds exactly to hypergraphs: nodes correspond to the image of $\bullet$ while the set of hyperedges with source of length $k$ and target of length $l$ corresponds to the image of $(k,l)$ (see [11]).

In particular, Remark 3.11 entails the following result.

Proposition 3.12.

Hyp has all limits and colimits.

3.1.1 Labelling hypergraph with an algebraic signature

Our interest for hypergraphs stems from their use as a graphical representation of algebraic terms. We thus need a way to label hyperedges with symbols taken from a signature.

Definition 3.13.

An algebraic signature $\Sigma$ is a pair $(O_{\Sigma},\mathsf{ar}_{\Sigma})$ given by a set of operations $O_{\Sigma}$ and an arity function $\mathsf{ar}_{\Sigma}\colon O_{\Sigma}\to\mathbb{N}$ . We define the hypergraph $\mathcal{G}_{\Sigma}$ associated with $\Sigma$ taking $O_{\Sigma}$ as set of hyperedges, $1$ as set of nodes, so that $1^{\star}$ is $\mathbb{N}$ , $\mathsf{ar}_{\Sigma}$ as the source function and $\gamma_{1}$ , which always picks the element $1$ , as target function. The category $\textbf{{Hyp}}_{\Sigma}$ of algebraically labelled hypergraphs is the slice category $\textbf{{Hyp}}/\mathcal{G}^{\Sigma}$ .

Example 3.14.

Let $\Sigma=(O_{\Sigma},\mathsf{ar}_{\Sigma})$ be the signature with $O_{\Sigma}=\mathbb{N}\uplus A\uplus\{*,/\}$ , where $n$ stands for any natural number and $a$ for any element in $A$ , both sets of constants, and $\mathsf{ar}_{\Sigma}(*)=\mathsf{ar}_{\Sigma}(/)=2$ . Then the hypergraph $\mathcal{G}^{\Sigma}$ is depicted as the picture below.

Proposition 2.4 gives us immediately an adhesivity result for $\textbf{{Hyp}}_{\Sigma}$ and a characterisation of monos in it.

Proposition 3.15.

Let $\Sigma$ be an algebraic signature. Then the following hold

1.

an arrow $(h,k)$ in $\textbf{{Hyp}}_{\Sigma}$ is a mono if and only if $h$ and $k$ are injective;
2.

$\textbf{{Hyp}}_{\Sigma}$ is an adhesive category.

$\blacktriangleright$ Remark 3.16.

Let $\mathcal{H}=(E,V,s,t)$ be a hypergraph, by definition we know that $U_{\textbf{{Hyp}}}(\mathcal{G}^{\Sigma})$ is the terminal object $1$ , so an arrow $\mathcal{H}\rightarrow\mathcal{G}^{\Sigma}$ , is determined by a function $h\colon E_{\mathcal{H}}\to O_{\Sigma}$ making the two squares below commutative (cfr. Remark 3.3).

Now, consider a coprojection $v_{n}\colon V^{n}_{\mathcal{H}}\to V^{\star}_{\mathcal{H}}$ . By the second diagram above entails that $t_{\mathcal{H}}$ factors via the inclusion $v_{1}\colon V_{\mathcal{H}}\to V_{\mathcal{H}}^{\star}$ of words of length $1$ , i.e. all hyperedges must have a single target vertex, that is $t_{\mathcal{H}}=v_{1}\circ\tau_{\mathcal{H}}$ for some $\tau_{\mathcal{H}}\colon E_{\mathcal{H}}\to V_{\mathcal{H}}$ .

$\textbf{{Hyp}}_{\Sigma}$ has a forgetful functor $U_{\Sigma}\colon\textbf{{Hyp}}_{\Sigma}\to\textbf{{X}}$ which sends $(h,k)\colon\mathcal{H}\to\mathcal{G}^{\Sigma}$ to $U_{\textbf{{Hyp}}}(\mathcal{H}$ ). Now, since $U_{\textbf{{Hyp}}}(\mathcal{G}^{\Sigma})=1$ for every set $X$ we can define $\Delta_{\Sigma}(X)\colon\Delta_{\textbf{{Hyp}}}(X)\to\mathcal{G}^{\Sigma}$ as $(?_{O_{\Sigma}},!_{X})$ . It is straightforward to see that in this way we get a left adjoint to $U_{\Sigma}$ .

Proposition 3.17.

$U_{\Sigma}$ has a left adjoint $\Delta_{\Sigma}$ .

We extend our graphical notation of hypergraphs to labeled ones putting the label of an hyperedge $h$ inside its corresponding square.

Example 3.18.

Consider again $\Sigma$ the signature of Example 3.14, then the hypergraph $\mathcal{G}$ of Example 3.10 can be labeled by a morphism $(l,!_{V_{\mathcal{G}}}):\mathcal{G}\to\mathcal{G}^{\Sigma}$ that is characterised by the image of the edges. If $l(h_{1})=a$ , $l(h_{2})=2$ , $l(h_{3})=*$ , and $l(h_{4})=/$ , we represent it visually by putting the labels of the edges in $\mathcal{G}^{\Sigma}$ inside the boxes representing the edges of $\mathcal{G}$ .

3.2 Term Graphs

Term graphs have been adopted as a convenient way to represent terms over a signature with an explicit sharing of sub-terms, and as such have been a convenient tool for an efficient implementation of term rewriting [27]. We elaborate here on the presentation given in [11].

Definition 3.19.

Given an algebraic signature $\Sigma$ , we say that a labelled hypergraph $(l,!_{V_{\mathcal{G}}})\colon\mathcal{G}\to\mathcal{G}^{\Sigma}$ is a term graph if $t_{\mathcal{G}}$ is a mono. We define $\textbf{{TG}}_{\Sigma}$ to be the full subcategory of $\textbf{{Hyp}}_{\Sigma}$ given by term graphs and denote by $I_{\Sigma}$ the inclusion. Restricting $U_{\Sigma}\colon\textbf{{Hyp}}_{\Sigma}\to\textbf{{Set}}$ we get a forgetful functor $U_{\textbf{{TG}}_{\Sigma}}\colon\textbf{{TG}}_{\Sigma}\to\textbf{{Set}}$ .

$\blacktriangleright$ Remark 3.20.

By Remark 3.16, we know that if $\mathcal{G}$ is a term graph then $t_{\mathcal{G}}=v_{1}\circ\tau_{\mathcal{G}}$ , where $v_{1}$ is the coprojection of $V_{\mathcal{G}}$ into $V^{\star}_{\mathcal{G}}$ . Notice that since $t_{\mathcal{G}}$ is a mono then $\tau_{\mathcal{G}}$ is a mono.

Example 3.21.

The labelled hypergraph of Example 3.18 is a term graph.

We now examine some properties of $\textbf{{TG}}_{\Sigma}$ , in order to study its adhesivity properties. We begin noticing that, for every set $X$ , $\Delta_{\Sigma}(X)$ has no hyperedges and so is a term graph. This yields at once the following.

Proposition 3.22.

The forgetful functor $U_{\textbf{{TG}}_{\Sigma}}$ has a left adjoint $\Delta_{\textbf{{TG}}_{\Sigma}}$ .

We can list some other categorical properties of $\textbf{{TG}}_{\Sigma}$ (see [11, Sec. 5]).

Proposition 3.23.

Let $\Sigma$ be an algebraic signature. Then the following hold

1.

if $(i,j)\colon\mathcal{H}\to\mathcal{G}$ is a mono from $(l,!_{V_{\mathcal{G}}})\colon\mathcal{G}\to\mathcal{G}^{\Sigma}$ to $(l^{\prime},!_{V_{\mathcal{H}}})\colon\mathcal{H}\to\mathcal{G}^{\Sigma}$ in $\textbf{{Hyp}}_{\Sigma}$ and the latter is in $\textbf{{TG}}_{\Sigma}$ , then also the former is in $\textbf{{TG}}_{\Sigma}$
2.

$\textbf{{TG}}_{\Sigma}$ has equalizers, binary products and pullbacks and they are created by $I_{\Sigma}$ .

$\blacktriangleright$ Remark 3.24.

$\textbf{{TG}}_{\Sigma}$ in general does not have terminal objects. Since $U_{\textbf{{TG}}_{\Sigma}}$ preserves limits, if a terminal object exists it must have the singleton as set of nodes, therefore the set of hyperedges must be empty or a singleton. Hence, for a counterexample, it suffices to take a signature with two operations $a$ and $b$ , both of arity $0$ . $\textbf{{TG}}_{\Sigma}$ is not an adhesive category, either. In particular, as noted in e.g. [11], it does not have pushouts along all monos.

Definition 3.25.

Let $(l,!_{V_{\mathcal{G}}})\colon\mathcal{G}\to\mathcal{G}^{\Sigma}$ be a term graph. A input node is an element of $V_{\mathcal{G}}$ not in the image of $\tau_{\mathcal{G}}$ . A morphism $(f,g)$ between $(l,!_{V_{\mathcal{G}}})\colon\mathcal{G}\to\mathcal{G}^{\Sigma}$ and $(l,!_{V_{\mathcal{H}}})\colon\mathcal{H}\to\mathcal{G}^{\Sigma}$ in $\textbf{{TG}}_{\Sigma}$ , is said to preserve input nodes if $g$ sends input nodes to input nodes.

Preservation of input nodes characterizes regular monos in $\textbf{{TG}}_{\Sigma}$ .

Proposition 3.26.

Let $(i,j)$ be a mono between two term graphs $(l,!_{V_{\mathcal{G}}})\colon\mathcal{G}\to\mathcal{G}^{\Sigma}$ and $(l^{\prime},!_{V_{\mathcal{H}}})\colon\mathcal{H}\to\mathcal{G}^{\Sigma}$ . Then it is a regular mono if and only if it preserves the input nodes.

This characterization, in turn, provides us with the following result [11, 10].

Lemma 3.27.

Consider three term graphs $(l_{0},!_{V_{\mathcal{G}}})\colon\mathcal{G}\to\mathcal{G}^{\Sigma}$ , $(l_{1},!_{V_{\mathcal{H}}})\colon\mathcal{H}\to\mathcal{G}^{\Sigma}$ and $(l_{2},!_{V_{\mathcal{K}}})\colon\mathcal{K}\to\mathcal{G}^{\Sigma}$ . Given $(f_{1},g_{1})\colon(l_{0},!_{V_{\mathcal{G}}})\to(l_{1},!_{V_{\mathcal{H}}})$ , $(f_{2},g_{2})\colon(l_{0},!_{V_{\mathcal{G}}})\to(l_{2},!_{V_{\mathcal{K}}})$ , if $(f_{1},g_{1})$ is a regular mono, then its pushout $(p,!_{V_{\mathcal{P}}})\colon\mathcal{P}\to\mathcal{G}^{\Sigma}$ in $\textbf{{Hyp}}_{\Sigma}$ along $(f_{2},g_{2})$ is a term graph.

Propositions 2.4 and 3.15, Proposition 3.26 and Lemma 3.27 allow us to recover the following result, previously proved by direct computation in [12, Thm. 4.2] (see also [11, Cor. 5.15] for the details of the argument presented here).

Corollary 3.28.

The category $\textbf{{TG}}_{\Sigma}$ is quasiadhesive.

4 Adding equivalences to hypergraphical structures

The use of hypergraphs equipped with an equivalence relation over their nodes has been argued as a convenient way to express concurrency in the DPO approach to rewriting [4]. This section presents the framework by means of adhesive categories, including also its version for term graphs, as a stepping stone towards an analogous characterisation for e-graphs.

4.1 Hypergraphs with equivalence

Let us start with the case of general hypergraphs. These were introduced in [4], even if no general consideration about their structure as a category was proved, and adhesivity, which is the main focus here, was yet to be presented to the world.

Definition 4.1.

A hypergraph with equivalence $\mathcal{G}=(E_{\mathcal{G}},V_{\mathcal{G}},Q_{\mathcal{G}},s_{\mathcal{G}},t% _{\mathcal{G}},q_{\mathcal{G}})$ is a 6-tuple such that $\mathcal{G}=(E_{\mathcal{G}},V_{\mathcal{G}},s_{\mathcal{G}},t_{\mathcal{G}})$ is a hypergraph, $Q_{\mathcal{G}}$ is a set and $q_{\mathcal{G}}:V_{\mathcal{G}}\twoheadrightarrow Q_{\mathcal{G}}$ is a surjection called quotient map. A morphism $h\colon\mathcal{G\to H}$ is a triple $(h_{E},h_{V},h_{Q})$ such that the following diagrams commute

The category of hypergraphs with equivalence and their morphisms is denoted EqHyp.

$\blacktriangleright$ Remark 4.2.

Notice that in $\mathbf{Set}$ the classes of surjections, epis and regular epis coincide.

$\blacktriangleright$ Remark 4.3.

Morphisms of hypergraphs with equivalences are uniquely determined by the first two components. That is, if $h_{1}=(h_{E},h_{V},f)$ and $h_{2}=(h_{E},h_{V},g)$ are two morphisms $\mathcal{G}\rightrightarrows\mathcal{H}$ , then we have $f\circ q_{\mathcal{G}}=q_{\mathcal{H}}\circ h_{V}=g\circ q_{\mathcal{G}}.$ Since $q_{\mathcal{G}}$ is epi, we obtain $f=g$ .

Forgetting the quotient part yields a functor $T\colon\textbf{{EqHyp}}\to\textbf{{Hyp}}$ sending a hypergraph with equivalence $(E_{\mathcal{G}},V_{\mathcal{G}},C_{\mathcal{G}},s_{\mathcal{G}},t_{\mathcal{G% }},q_{\mathcal{G}})$ to $(E_{\mathcal{G}},V_{\mathcal{G}},s_{\mathcal{G}},t_{\mathcal{G}})$ . We now explore some of its properties to deduce information on the structure of EqHyp.

Proposition 4.4.

Consider the forgetful functor $T\colon\textbf{{EqHyp}}\to\textbf{{Hyp}}$ . Then the following hold

1.

$T$ is faithful;
2.

$T$ has a left adjoint;
3.

$T$ has a right adjoint.

Corollary 4.5.

The functor $T$ preserves limits and colimits.

From the previous results we get the following characterization of monos in EqHyp.

Corollary 4.6.

An arrow $(h_{E},h_{V},h_{Q}):\mathcal{G\to H}$ in EqHyp is a mono if and only if $(h_{E},h_{V})$ is a mono in Hyp.

Now, we can consider the forgetful functor $U_{\mathsf{eq}}\colon\textbf{{EqHyp}}\to\mathbf{Set}$ obtained by composing $T$ and $U_{\textbf{{Hyp}}}$ . By Proposition 3.8 and the second point of Proposition 4.4 we get the following.

Corollary 4.7.

$U_{\mathsf{eq}}$ has a left adjoint $\Delta_{\mathsf{eq}}\colon\mathbf{Set}\to\textbf{{EqHyp}}$ .

Notice that there is another functor $K:\textbf{{EqHyp}}\to\mathbf{Set}$ sending $(E,V,Q,s,t,q)$ to $Q$ , and a morphism $(h_{E},h_{V},h_{Q})$ to $h_{Q}$ . We exploit it to compute limits and colimits in EqHyp.

Lemma 4.8.

Consider a diagram $F\colon\textbf{{D}}\to\textbf{{EqHyp}}$ and let $(E_{D},V_{D},Q_{D},s_{D},t_{D},q_{D})$ be the image of an object $D$ . Then the following hold

1.

$F$ has a colimit, which is preserved by $K$ ;
2.

consider a cone $(L,\{l_{D}\}_{D\in\textbf{{D}}})$ limiting for $K\circ F$ and let $((E,V),\{(\pi^{D}_{E},\pi^{D}_{V})\}_{D\in\textbf{{D}}})$ be one for $T\circ F$ , then $F$ has a limit $(E,V,Q,s,t,q)$ and there is a mono $m\colon Q\rightarrowtail L$ such that the diagram below commutes for every $D\in\textbf{{D}}$ .

Corollary 4.9.

An arrow $(h_{E},h_{V},h_{Q}):\mathcal{G\to H}$ in EqHyp is a regular mono if and only if all its components are injective functions.

We have now all the ingredients to study the adhesivity properties of EqHyp. As a first step we need to introduce a class of monos.

Definition 4.10.

We define $\mathsf{Pb}$ as the class of regular monos $(h_{E},h_{V},h_{Q})\colon\mathcal{G}\to\mathcal{H}$ in EqHyp such that the square below is a pullback

Now, we show that $\mathsf{Pb}$ is a suitable class for adhesivity.

Lemma 4.11.

The class $\mathsf{Pb}$ contains all isomorphisms, it is closed under composition, decomposition and it is stable under pullbacks and pushouts.

Finally, we show the key lemma for $\mathsf{Pb}$ -adhesivity of EqHyp.

Lemma 4.12.

In EqHyp, $\mathsf{Pb}$ -pushouts are stable.

Example 4.13.

It is noteworthy to show that pushouts along regular monos are not stable. Consider e.g. the cube below: the vertices are just graphs without edges, and in the graphs themselves the equivalence classes are denoted by encircling nodes with a dotted line. All the arrows are regular monos. It is immediate to see that the bottom face is a pushout and the side faces are pullbacks. Unfortunately, the top face fails to be a pushout.

Having proved stability of $\mathsf{Pb}$ -pushouts, we now turn to prove that they are Van Kampen with respect to regular monos.

Lemma 4.14.

In EqHyp, pushouts along arrows in $\mathsf{Pb}$ are $\mathsf{Reg}(\textbf{{EqHyp}})$ -Van Kampen.

Corollary 4.15.

EqHyp is $\mathsf{Pb}$ -adhesive.

4.2 Term graphs with equivalence

We are now going to generalize the work done in the previous section equipping term graphs with equivalence relation. First of all we need a notion of labelling for EqHyp.

Definition 4.16.

Let $\Sigma$ be an algebraic signature and $\mathcal{G}^{\Sigma}$ the hypergraph associated to it. A labelled hypergraph with equivalence is a pair $(\mathcal{H},l)$ where $\mathcal{H}$ is an object of EqHyp and $l$ a morphism $T(\mathcal{H})\to\mathcal{G}^{\Sigma}$ of Hyp. A morphism of labelled hypergraphs with equivalence between $(\mathcal{H},l)$ and $(\mathcal{H}^{\prime},l^{\prime})$ is an arrow $h\colon\mathcal{H}\to\mathcal{H}^{\prime}$ such that $l=l^{\prime}\circ T(h)$ .

We denote the resulting category by $\textbf{{EqHyp}}_{\Sigma}$ .

Let $(\mathcal{H},l)$ be an object of $\textbf{{EqHyp}}_{\Sigma}$ : since $T$ has a right adjoint $R$ by Proposition 4.4, $l\colon T(\mathcal{H})\to\mathcal{G}^{\Sigma}$ corresponds to the arrow $(l,!_{Q_{\mathcal{H}}})\colon\mathcal{H}\to R(\mathcal{G}^{\Sigma})$ . It is immediate to see that this correspondence extends to an equivalence with the slice over $R(\mathcal{G}^{\Sigma})$ .

Proposition 4.17.

$\textbf{{EqHyp}}_{\Sigma}$ is equivalent to $\textbf{{EqHyp}}/R(\mathcal{G}^{\Sigma})$ .

Let $V_{\Sigma}\colon\textbf{{EqHyp}}_{\Sigma}\to\textbf{{EqHyp}}$ be the functor forgetting the labelling and $\mathsf{Pb}_{\Sigma}$ the class of morphisms in $\textbf{{EqHyp}}_{\Sigma}$ whose image in EqHyp is in $\mathsf{Pb}$ . From Lemma 4.8, the second point of Propositions 2.4 and 4.15, we can deduce the following.

Proposition 4.18.

Consider the forgetful functor $V_{\Sigma}\colon\textbf{{EqHyp}}_{\Sigma}\to\textbf{{EqHyp}}$ . Then the following hold

1.

$\textbf{{EqHyp}}_{\Sigma}$ has all colimits and all connected limits, which are created by $V_{\Sigma}$ ;
2.

$\textbf{{EqHyp}}_{\Sigma}$ is $\mathsf{Pb}_{\Sigma}$ -adhesive.

Using Corollaries 4.6 and 4.9 we immediately get the following result.

Corollary 4.19.

Let $h=(h_{E},h_{V},h_{Q})$ be an arrow in $\textbf{{EqHyp}}_{\Sigma}$ . Then the following hold

1.

$h$ is mono if and only if $h_{E}$ and $h_{V}$ are injective;
2.

$h$ is a regular mono if and only if $h_{E}$ , $h_{V}$ and $h_{Q}$ are injective.

We can now easily define term graphs with equivalence.

Definition 4.20.

Let $\Sigma$ be an algebraic signature. An object $(\mathcal{H},l)$ of $\textbf{{EqHyp}}_{\Sigma}$ is a term graph with equivalence if $l\colon T(\mathcal{H})\to\mathcal{G}^{\Sigma}$ is a term graph. We denote by $\textbf{{EqTG}}_{\Sigma}$ the full subcategory of $\textbf{{EqHyp}}_{\Sigma}$ so defined and by $J_{\Sigma}$ the corresponding inclusion functor.

$\blacktriangleright$ Remark 4.21.

Let $T_{\Sigma}:\textbf{{EqHyp}}_{\Sigma}\to\textbf{{Hyp}}_{\Sigma}$ the forgetful functor lifting $T:\textbf{{EqHyp}}\to\textbf{{Hyp}}$ . Notice that, by definition, $(\mathcal{H},l)$ is in $\textbf{{EqTG}}_{\Sigma}$ amounts to say that $(T(\mathcal{H}),l)$ is in $\textbf{{TG}}_{\Sigma}$ . Thus there exists a functor $S_{\Sigma}$ as in the diagram below.

$\blacktriangleright$ Remark 4.22.

Notice that, by Corollary 4.5 and Proposition 4.18, the functor $T_{\Sigma}$ preserves all connected limits and all colimits.

The previous remark allows us to prove an analog of Proposition 3.23.

Proposition 4.23.

$\textbf{{EqTG}}_{\Sigma}$ has equalizers, binary products and pullbacks and they are created by $J_{\Sigma}$ .

Let now $\mathcal{T}$ be the class of morphism in $\textbf{{EqTG}}_{\Sigma}$ whose image through $J_{\Sigma}$ is in $\mathsf{Pb}_{\Sigma}$ and whose image through $S_{\Sigma}$ is a regular mono in $\textbf{{TG}}_{\Sigma}$ . By Propositions 3.26 and 4.19, we have that a morphism $(h_{E},h_{V},h_{Q})\colon(\mathcal{G},l)\to(\mathcal{H},l^{\prime})$ is in $\mathcal{T}$ if and only if all of its components are injections and the square below is a pullback.

In particular, by Corollary 3.28 and Lemma 4.12, $\mathcal{T}$ contains all isomorphisms, is closed under composition and decomposition and stable under pushout and pullbacks.

The following proposition is now an easy corollary of Lemma 3.27, Proposition 4.18, and Remark 4.21.

Proposition 4.24.

$\textbf{{EqTG}}_{\Sigma}$ has all $\mathcal{T}$ -pushouts, which are created by $J_{\Sigma}$ .

Corollary 4.25.

$\textbf{{EqTG}}_{\Sigma}$ is $\mathcal{T}$ -adhesive.

5 EGGs

The previous section proved some adhesivity property for the categories EqHyp and $\textbf{{EqTG}}_{\Sigma}$ . We extend these results to encompass equivalence classes which are closed under the target arrow, i.e. under operator composition for term graphs, thus precisely capturing EGGs.

5.1 E-hypergraphs

We start introducing the notion of e-hypergraphs, hypergraphs equipped with an equivalence relation that is closed under the target arrow: in other words, whenever the relation identifies the source of two hyperedges, it identifies their targets too.

Definition 5.1.

Let $\mathcal{G}=(E,V,Q,s,t,q)$ be a hypergraph with equivalence and $(S,\pi_{1},\pi_{2})$ a kernel pair for $q^{\star}\circ s$ . We will say that $\mathcal{G}$ is an e-hypergraph if $q^{\star}\circ t\circ\pi_{1}=q^{\star}\circ t\circ\pi_{2}$ .

We will denote by $\mathsf{e}\text{-}\textbf{{EqHyp}}$ the full subcategory of EqHyp whose objects are e-hypergraphs, and by $I\colon\mathsf{e}\text{-}\textbf{{EqHyp}}\to\textbf{{EqHyp}}$ the associated inclusion functor.

Example 5.2.

Consider the hypergraph $\mathcal{G}$ of Example 3.10 and consider as quotient the identity $\mathsf{id}_{V_{\mathcal{G}}}\colon V_{\mathcal{G}}\colon\to\mathcal{G}$ . Then the kernel pair of $\mathsf{id}_{V^{\star}_{\mathcal{G}}}\circ s$ concide with the kernel pair of $s$ , which is empty. Thus $\mathcal{G}$ is, trivially, an e-hypergraph

A first result that we need is that limits in $\mathsf{e}\text{-}\textbf{{EqHyp}}$ are computed as in EqHyp.

Lemma 5.3.

$\mathsf{e}\text{-}\textbf{{EqHyp}}$ has all limits and $I$ creates them.

Corollary 5.4.

If an arrow $h:\mathcal{G\to H}$ in $\mathsf{e}\text{-}\textbf{{EqHyp}}$ is a regular mono in $\mathsf{e}\text{-}\textbf{{EqHyp}}$ then $I(h)$ is a regular mono in Hyp.

We can now turn to pushouts.

Lemma 5.5.

Suppose that the square below is a pushout in EqHyp and that $m$ is a mono in $\mathsf{Pb}$ . If $\mathcal{G}_{1}$ , $\mathcal{G}_{2}$ and $\mathcal{G}_{3}$ are e-hypergraphs, then $\mathcal{P}$ is is an e-hypergraph.

Let now $\mathsf{ePb}$ be the class of arrows in $\mathsf{e}\text{-}\textbf{{EqHyp}}$ that are sent to $\mathsf{Pb}$ by $I$ . By definition and Lemma 4.11 we have that such class is closed under composition and decomposition, it contains all isomorphisms and it is stable under pullbacks. Using Lemmas 4.11 and 5.5 we can further deduce that it is stable under pushouts. Then Propositions 2.4 and 4.15 yield the following.

Corollary 5.6.

$\mathsf{e}\text{-}\textbf{{EqHyp}}$ is $\mathsf{ePb}$ -adhesive.

5.2 E-term graphs, a.k.a. EGGs

We now turn our attention to the labelled context.

Definition 5.7.

We say that an object $(\mathcal{H},l)$ of $\textbf{{EqHyp}}_{\Sigma}$ is a labelled e-hypergraph if $\mathcal{H}$ is an e-hypergraph. We define the category $\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}$ as the full subcategory of $\textbf{{EqHyp}}_{\Sigma}$ given by labelled e-hypergraphs. We denote by $Z_{\Sigma}$ the corresponding inclusion functor .

To prove some adhesivity property of $\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}$ , we begin with the following elementary, yet useful observation.

$\blacktriangleright$ Remark 5.8.

Given a signature $\Sigma=(O_{\Sigma},\mathsf{ar}_{\Sigma})$ , the hypergraph $R(\mathcal{G}^{\Sigma})=(O_{\Sigma},1,1,\mathsf{ar}_{\Sigma},\gamma_{1},% \mathsf{id}_{1})$ is an object of $\mathsf{e}\text{-}\textbf{{EqHyp}}$ . Indeed, under the identification of $1^{\star}$ with $\mathbb{N}$ , the kernel $(S,\pi_{1},\pi_{2})$ of $\mathsf{id}_{\mathbb{N}}\circ\mathsf{ar}_{\Sigma}$ , is given by $S:=\{(o_{1},o_{2})\in O_{\Sigma}\times O_{\Sigma}\mid\mathsf{ar}_{\Sigma}(o_{1% })=\mathsf{ar}_{\Sigma}(o_{2})\}$ equipped with the two projections. On the other hand, both $\mathsf{id}_{\mathbb{N}}\circ\gamma_{1}\circ\pi_{1}$ and $\mathsf{id}_{\mathbb{N}}\circ\gamma_{1}\circ\pi_{2}$ are the function $O_{\Sigma}\to\mathbb{N}$ constant in $1$ .

Remark 5.8 now implies at once the following result.

Proposition 5.9.

Let $\Sigma$ be an algebraic signature. Then the following hold

1.

$\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}$ is equivalent to $\mathsf{e}\text{-}\textbf{{EqHyp}}/R(\mathcal{G}^{\Sigma})$ ;
2.

there exists a functor $W_{\Sigma}\colon\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}\to\mathsf{e}\text{% -}\textbf{{EqHyp}}$ forgetting the labeling which creates all colimits, pullbacks and equalizers.

Let $\mathsf{ePb}_{\Sigma}$ be the class of morphisms in $\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}$ whose image in $\mathsf{e}\text{-}\textbf{{EqHyp}}$ lies in $\mathsf{ePb}$ . Notice that $\mathsf{ePb}_{\Sigma}$ is also the class of arrows whose image through $Z_{\Sigma}$ is in $\mathsf{Pb}_{\Sigma}$ . By Proposition 2.4 we get the following result.

Corollary 5.10.

$\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}$ is $\mathsf{ePb}_{\Sigma}$ -adhesive.

We turn now to term graphs with equivalence.

Definition 5.11.

Given a signature $\Sigma$ , we say that an object $(\mathcal{H},l)$ of $\textbf{{EqTG}}_{\Sigma}$ is an e-term graph if $\mathcal{H}$ is an e-hypergraph. We define the category $\mathbf{EGG}$ as the full subcategory of $\textbf{{EqTG}}_{\Sigma}$ given by e-term graphs and denote by $K_{\Sigma}$ the corresponding inclusion.

$\blacktriangleright$ Remark 5.12.

By definition we also have an inclusion functor $Y_{\Sigma}\colon\mathbf{EGG}\to\mathsf{e}\text{-}\textbf{{EqHyp}}_{\Sigma}$ .

$\blacktriangleright$ Remark 5.13.

Now that we have put all the structures of this work in place, it is worthwhile to give a visual map of all the categories that we have discussed/introduced and of the relationships between them. We will use the curved arrows to denote full and faithful inclusions.

We can now prove our last three results.

Proposition 5.14.

$\mathbf{EGG}$ has equalizers, binary products and pullbacks and they are created by $K_{\Sigma}$ .

Let now $\mathcal{T}_{\Sigma}$ be the class of morphisms of $\mathbf{EGG}$ which are sent by $K_{\Sigma}$ to the class $\mathcal{T}$ . Then Lemmas 5.5 and 4.24 allow us to deduce the following result.

Proposition 5.15.

$\mathbf{EGG}$ has $\mathcal{T}_{\Sigma}$ -pushouts, which are created by $K_{\Sigma}$ .

Reasoning as in the previous sections, Propositions 5.14 and 5.15 now give us the following.

Corollary 5.16.

$\mathbf{EGG}$ is $\mathcal{T}_{\Sigma}$ -adhesive.

6 Pros and cons of adhesive rewriting

The previous sections have shown how hypergraphs and term graphs with equivalence can be described as suitable $\mathcal{M}$ -adhesive categories. The same fact holds for their sub-categories where the equivalence is closed with respect to operator composition, and this allows to model EGGs, as originally presented in [31].

Sharing.

Terms are trees, thus different term graphs may represent the same term, up-to the sharing of sub-terms. Consider e.g. a constant $a$ and a binary operator $/$ : the term $a/a$ admits a few different representations as a term graph with equivalence, as shown below

The left-most and the right-most images represent just ordinary term graphs, the middle one is a term graph with equivalence. As such, they are all objects of $\textbf{{EqTG}}_{\Sigma}$ . However, note that the right-most image is not an object of $\mathbf{EGG}$ : constants have no input, and nodes that are targets of edges with the same label and whose source is the empty word must be equivalent and possibly coincide, as in the middle and in the left-most image, respectively.

In general, for (acyclic) term graphs, a maximally and a minimally shared representation exist, and for our toy example are the left-most and the right-most diagram above, respectively: it is a standard result for term graph rewriting, see e.g. [1]. These two representations can be interpreted as the final and the initial object of a suitable comma category. respectively. The same properties carry on for term graphs with equivalence and for EGGs. However, while in the former case the two representations are the same of those for ordinary term graphs, in the latter case the minimally shared representation is now the middle diagram.

Rewriting.

The theory of $\mathcal{M}$ -adhesivity ensures that if the rules are spans of arrows in $\mathcal{M}$ , then we can lift the standard properties of the DPO approach that hold in the category of graphs. However, as we recalled in the introduction, instead of removing sub-terms, the EGG approach chooses to just add new terms and link them to the older ones via the equivalence relation [14]. So, the corresponding DPO rules are spans $L\leftarrow L\rightarrow R$ , where the first component is the identity, thus in $\mathsf{Pb}_{\Sigma}$ , while the second component may not belong to $\mathsf{Pb}_{\Sigma}$ .

Consider e.g. an EGG rule such $x/x\to 1$ , from the introductory example in [31]. Variables in a term graph are represented as nodes that do not occur among the targets of an edge, thus the rule can be modelled as the DPO rule below, concisely given by the arrow $L\rightarrow R$

In this case $L$ is the minimally shared EGG corresponding to the term $x/x$ , thus the rule could be applied to the two EGGs depicted above with a match that is injective on equivalence classes. In general, if the term graph underlying the EGG to whom the DPO rule is applied is acyclic, the same property holds for the EGG obtained as the result of the rule application. The right-hand side is a regular mono, though, hence it is not an arrow in $\mathsf{Pb}_{\Sigma}$ . The asymmetry between left-hand and right-hand sides falls in the current research about left-linear rules for adhesive categories, as pursued e.g. in [3].

Application conditions.

As argued above, the DPO rules that are suitable for the EGG approach have identities as left-hand side, thus they belong to any choice of $\mathcal{M}$ . However, this would allow for the repeated application of the same rule, hence the possibility to keep on performing the same rewriting step. This is forbidden by using rules with negative application conditions, given as the usual span $L\leftarrow K\rightarrow R$ plus an additional arrow $n:L\rightarrow N$ , such that a match $m:L\to G$ is admissible if it cannot be factorised through $n$ [21]. For EGGs and rules $L\leftarrow L\rightarrow R$ , it suffices to choose $n$ as the right-hand side itself. The theory of $\mathcal{M}$ -adhesivity carries on for rules with negative application conditions, see [15, 16].

7 Conclusions and further and related works

The aim of our paper was to extend the theory of $\mathcal{M}$ -adhesive categories in order to include EGGs, a formalism for program optimisation. To do so, we revisited the notions of hyper-graphs and term graphs with equivalence, proving that they are $\mathcal{M}$ -adhesive categories, and we extended these results in order to prove the same property for EGGs as term graphs with equivalence satisfying a suitable closure constraint. Summing up, we proved that EGGs are objects of an $\mathcal{M}$ -adhesive category $\mathbf{EGG}$ and that optimisation steps are obtained via DPO rules (possibly with negative application conditions) whose left-hand side is in $\mathcal{M}$ , and that allows for exploiting the properties of the $\mathcal{M}$ -adhesive framework.

Future works.

Our result on $\mathbf{EGG}$ opens a few threads of research. The first is to check how the $\mathcal{M}$ -adhesivity of EGGs can be pushed to model their rewriting via the double-pushout (DPO) approach. We have seen that the rules adopted in the literature of EGGs appears to be spans whose left-hand side is an identity and right-hand side is a regular mono (possibly with negative application conditions), and as such they fit the mould of rewriting on left-linear rewriting in $\mathcal{M}$ -adhesive categories. However, it still needs to be shown how parallelism and causality, the key features for DPO rewriting on $\mathcal{M}$ -adhesive categories, can be exploited in the context of implementing the EGGs updates. Moreover, extensions of the EGGs formalism could be suggested by the adhesive machinery we developed. In fact, most of the results presented here for hypergraphs can be generalised to hierarchical hypergraphs, that is, hypergraphs with a hierarchy (a partial order) among edges [20, 11]. The additional structure is useful for modelling properties such as encapsulation and sandboxing, and it seems worthwhile to check the expressiveness and applications of hierarchical EGGS.

Related works.

Despite the interest they have ben raising as an efficient data structure, we are not aware of any attempt to provide an algebraic characterisation of EGGs, the only exception being [19]. We leave for future work an in-depth comparison among the two proposals, which appear to be related yet quite different. In fact, for both proposals the key intuition is to use string diagrams to represent term graphs. We adopted a more down-to-earth approach by equipping concretely the nodes of a term graph with an equivalence relation, thus directly corresponding to the original presentation [14], at the same time extending and generalising it [4] in the contemporary jargon of adhesive categories. The route chosen in [19] is to consider term graphs as arrows of a symmetric monoidal category, and equipping them with an enrichment over semi-lattices, the resulting formalism being reminiscent of hierarchical hypergraphs. Thus, the solution in [19] is more general than ours since it can be lifted to term graphs defined over categories other than $\mathbf{Set}$ . At the same time, we both consider the DPO approach for rewriting, even if only our solution guarantees that the resulting category is actually $\mathcal{M}$ -adhesive, thus allowing to exploit all the features of the framework as they hold for DPO graph transformation.

References

[1] Zena M. Ariola, Jan Willem Klop, and Detlef Plump. Bisimilarity in term graph rewriting. Information and Computation, 156(1-2):2–24, 2000. doi:10.1006/INCO.1999.2824.
[2] Guilherme Grochau Azzi, Andrea Corradini, and Leila Ribeiro. On the essence and initiality of conflicts in $\mathcal{M}$ -adhesive transformation systems. Journal of Logical and Algebraic Methods in Programming, 109:100482, 2019. doi:10.1016/J.JLAMP.2019.100482.
[3] Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci. Left-linear rewriting in adhesive categories. In Rupak Majumdar and Alexandra Silva, editors, CONCUR 2024, volume 311 of LIPIcs, pages 11:1–11:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CONCUR.2024.11.
[4] Paolo Baldan, Fabio Gadducci, and Ugo Montanari. Concurrent rewriting for graphs with equivalences. In Christel Baier and Holger Hermanns, editors, CONCUR 2006, volume 4137 of LNCS, pages 279–294. Springer, 2006. doi:10.1007/11817949_19.
[5] Nicolas Behr, Russ Harmer, and Jean Krivine. Fundamentals of compositional rewriting theory. Journal of Logical and Algebraic Methods in Programming, 135:100893, 2023. doi:10.1016/J.JLAMP.2023.100893.
[6] Roberto Biondo, Davide Castelnovo, and Fabio Gadducci. EGGs are adhesive! CoRR, abs/2503.13678, 2025. doi:10.48550/arXiv.2503.13678.
[7] F. Bonchi, F. Gadducci, A. Kissinger, P. Sobociński, and F. Zanasi. String diagram rewrite theory I: Rewriting with Frobenius structure. Journal of the ACM, 69(2):1–58, 2022. doi:10.1145/3502719.
[8] Ronald Brown and George Janelidze. Van Kampen theorems for categories of covering morphisms in lextensive categories. Journal of Pure and Applied Algebra, 119(3):255–263, 1997.
[9] Aurelio Carboni and Peter Johnstone. Connected limits, familial representability and Artin glueing. Mathematical Structures in Computer Science, 5(4):441–459, 1995. doi:10.1017/S0960129500001183.
[10] D. Castelnovo. Fuzzy algebraic theories and $\mathcal{M},\mathcal{N}$ -adhesive categories. PhD thesis, University of Udine, 2023.
[11] Davide Castelnovo, Fabio Gadducci, and Marino Miculan. A simple criterion for $\mathcal{M}$ , $\mathcal{N}$ -adhesivity. Theoretical Computer Science, 982:114280, 2024.
[12] Andrea Corradini and Fabio Gadducci. On term graphs as an adhesive category. In Maribel Fernández, editor, TERMGRAPH 2004, volume 127(5) of ENTCS, pages 43–56. Elsevier, 2004. doi:10.1016/J.ENTCS.2005.02.014.
[13] Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, and Michael Löwe. Algebraic approaches to graph transformation - part I: basic concepts and double pushout approach. In Grzegorz Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 163–246. World Scientific, 1997.
[14] David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. Journal of the ACM, 52(3):365–473, 2005. doi:10.1145/1066100.1066102.
[15] H. Ehrig, U. Golas, A. Habel, L. Lambers, and F. Orejas. $\mathcal{M}$ -adhesive transformation systems with nested application conditions. Part 2: Embedding, critical pairs and local confluence. Fundamenta Informaticae, 118(1-2):35–63, 2012. doi:10.3233/FI-2012-705.
[16] H. Ehrig, U. Golas, A. Habel, L. Lambers, and F. Orejas. $\mathcal{M}$ -adhesive transformation systems with nested application conditions. Part 1: Parallelism, concurrency and amalgamation. Mathematical Structures in Computer Science, 24(4):240406, 2014. doi:10.1017/S0960129512000357.
[17] Harmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic Graph Transformation. Springer, 2006. doi:10.1007/3-540-31188-2.
[18] R. Garner and S. Lack. On the axioms for adhesive and quasiadhesive categories. Theory and Applications of Categories, 27(3):27–46, 2012.
[19] Dan R. Ghica, Chris Barrett, and Aleksei Tiurin. Equivalence hypergraphs: E-graphs for monoidal theories. CoRR, abs/2406.15882, 2024. doi:10.48550/arXiv.2406.15882.
[20] Dan R. Ghica and Fabio Zanasi. Hierarchical string diagrams and applications. CoRR, abs/2305.18945, 2023. doi:10.48550/arXiv.2305.18945.
[21] Annegret Habel, Reiko Heckel, and Gabriele Taentzer. Graph grammars with negative application conditions. Fundamenta Informaticae, 26(3/4):287–313, 1996. doi:10.3233/FI-1996-263404.
[22] T. Heindel. A category theoretical approach to the concurrent semantics of rewriting. PhD thesis, Universität Duisburg–Essen, 2009.
[23] Peter T. Johnstone, Stephen Lack, and Pawel Sobocinski. Quasitoposes, quasiadhesive categories and Artin glueing. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, CALCO 2007, volume 4624 of LNCS, pages 312–326. Springer, 2007. doi:10.1007/978-3-540-73859-6_21.
[24] Stephen Lack and Pawel Sobocinski. Toposes are adhesive. In Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, and Grzegorz Rozenberg, editors, ICGT 2006, volume 4178 of LNCS, pages 184–198. Springer, 2006. doi:10.1007/11841883_14.
[25] Sthephen Lack and Pawel Sobociński. Adhesive and quasiadhesive categories. RAIRO-Theoretical Informatics and Applications, 39(3):511–545, 2005. doi:10.1051/ITA:2005028.
[26] Saunders Mac Lane. Categories for the working mathematician. Springer, 2013.
[27] D. Plump. Term graph rewriting. In H. Ehrig, G. Engels, H-J Kreowski, and G. Rozenberg, editors, Handbook of Graph Grammars and Computing by Graph Transformation, Volume 2: Applications, Languages and Tools, pages 3–61. World Scientific, 1999.
[28] J. Sakarovitch. Elements of automata theory. Cambridge University Press, 2009.
[29] VV.AA. egg: e-graphs good. https://egraphs-good.github.io/.
[30] Philip Wadler. Monads for functional programming. In Johan Jeuring and Erik Meijer, editors, Advanced Functional Programming, volume 925 of LNCS, pages 24–52. Springer, 1995. doi:10.1007/3-540-59451-5_2.
[31] Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. egg: Fast and extensible equality saturation. In POPL 2021, volume 5 of PACMPL, pages 1–29. ACM, 2021. doi:10.1145/3434304.

[bib.bib1] [1] Zena M. Ariola, Jan Willem Klop, and Detlef Plump. Bisimilarity in term graph rewriting. Information and Computation, 156(1-2):2–24, 2000. doi:10.1006/INCO.1999.2824.

[bib.bib2] [2] Guilherme Grochau Azzi, Andrea Corradini, and Leila Ribeiro. On the essence and initiality of conflicts in $\mathcal{M}$ -adhesive transformation systems. Journal of Logical and Algebraic Methods in Programming, 109:100482, 2019. doi:10.1016/J.JLAMP.2019.100482.

[bib.bib3] [3] Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci. Left-linear rewriting in adhesive categories. In Rupak Majumdar and Alexandra Silva, editors, CONCUR 2024, volume 311 of LIPIcs, pages 11:1–11:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CONCUR.2024.11.

[bib.bib4] [4] Paolo Baldan, Fabio Gadducci, and Ugo Montanari. Concurrent rewriting for graphs with equivalences. In Christel Baier and Holger Hermanns, editors, CONCUR 2006, volume 4137 of LNCS, pages 279–294. Springer, 2006. doi:10.1007/11817949_19.

[bib.bib5] [5] Nicolas Behr, Russ Harmer, and Jean Krivine. Fundamentals of compositional rewriting theory. Journal of Logical and Algebraic Methods in Programming, 135:100893, 2023. doi:10.1016/J.JLAMP.2023.100893.

[bib.bib6] [6] Roberto Biondo, Davide Castelnovo, and Fabio Gadducci. EGGs are adhesive! CoRR, abs/2503.13678, 2025. doi:10.48550/arXiv.2503.13678.

[bib.bib7] [7] F. Bonchi, F. Gadducci, A. Kissinger, P. Sobociński, and F. Zanasi. String diagram rewrite theory I: Rewriting with Frobenius structure. Journal of the ACM, 69(2):1–58, 2022. doi:10.1145/3502719.

[bib.bib8] [8] Ronald Brown and George Janelidze. Van Kampen theorems for categories of covering morphisms in lextensive categories. Journal of Pure and Applied Algebra, 119(3):255–263, 1997.

[bib.bib9] [9] Aurelio Carboni and Peter Johnstone. Connected limits, familial representability and Artin glueing. Mathematical Structures in Computer Science, 5(4):441–459, 1995. doi:10.1017/S0960129500001183.

[bib.bib10] [10] D. Castelnovo. Fuzzy algebraic theories and $\mathcal{M},\mathcal{N}$ -adhesive categories. PhD thesis, University of Udine, 2023.

[bib.bib11] [11] Davide Castelnovo, Fabio Gadducci, and Marino Miculan. A simple criterion for $\mathcal{M}$ , $\mathcal{N}$ -adhesivity. Theoretical Computer Science, 982:114280, 2024.

[bib.bib12] [12] Andrea Corradini and Fabio Gadducci. On term graphs as an adhesive category. In Maribel Fernández, editor, TERMGRAPH 2004, volume 127(5) of ENTCS, pages 43–56. Elsevier, 2004. doi:10.1016/J.ENTCS.2005.02.014.

[bib.bib13] [13] Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, and Michael Löwe. Algebraic approaches to graph transformation - part I: basic concepts and double pushout approach. In Grzegorz Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 163–246. World Scientific, 1997.

[bib.bib14] [14] David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. Journal of the ACM, 52(3):365–473, 2005. doi:10.1145/1066100.1066102.

[bib.bib15] [15] H. Ehrig, U. Golas, A. Habel, L. Lambers, and F. Orejas. $\mathcal{M}$ -adhesive transformation systems with nested application conditions. Part 2: Embedding, critical pairs and local confluence. Fundamenta Informaticae, 118(1-2):35–63, 2012. doi:10.3233/FI-2012-705.

[bib.bib16] [16] H. Ehrig, U. Golas, A. Habel, L. Lambers, and F. Orejas. $\mathcal{M}$ -adhesive transformation systems with nested application conditions. Part 1: Parallelism, concurrency and amalgamation. Mathematical Structures in Computer Science, 24(4):240406, 2014. doi:10.1017/S0960129512000357.

[bib.bib17] [17] Harmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic Graph Transformation. Springer, 2006. doi:10.1007/3-540-31188-2.

[bib.bib18] [18] R. Garner and S. Lack. On the axioms for adhesive and quasiadhesive categories. Theory and Applications of Categories, 27(3):27–46, 2012.

[bib.bib19] [19] Dan R. Ghica, Chris Barrett, and Aleksei Tiurin. Equivalence hypergraphs: E-graphs for monoidal theories. CoRR, abs/2406.15882, 2024. doi:10.48550/arXiv.2406.15882.

[bib.bib20] [20] Dan R. Ghica and Fabio Zanasi. Hierarchical string diagrams and applications. CoRR, abs/2305.18945, 2023. doi:10.48550/arXiv.2305.18945.

[bib.bib21] [21] Annegret Habel, Reiko Heckel, and Gabriele Taentzer. Graph grammars with negative application conditions. Fundamenta Informaticae, 26(3/4):287–313, 1996. doi:10.3233/FI-1996-263404.

[bib.bib22] [22] T. Heindel. A category theoretical approach to the concurrent semantics of rewriting. PhD thesis, Universität Duisburg–Essen, 2009.

[bib.bib23] [23] Peter T. Johnstone, Stephen Lack, and Pawel Sobocinski. Quasitoposes, quasiadhesive categories and Artin glueing. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, CALCO 2007, volume 4624 of LNCS, pages 312–326. Springer, 2007. doi:10.1007/978-3-540-73859-6_21.

[bib.bib24] [24] Stephen Lack and Pawel Sobocinski. Toposes are adhesive. In Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, and Grzegorz Rozenberg, editors, ICGT 2006, volume 4178 of LNCS, pages 184–198. Springer, 2006. doi:10.1007/11841883_14.

[bib.bib25] [25] Sthephen Lack and Pawel Sobociński. Adhesive and quasiadhesive categories. RAIRO-Theoretical Informatics and Applications, 39(3):511–545, 2005. doi:10.1051/ITA:2005028.

[bib.bib26] [26] Saunders Mac Lane. Categories for the working mathematician. Springer, 2013.

[bib.bib27] [27] D. Plump. Term graph rewriting. In H. Ehrig, G. Engels, H-J Kreowski, and G. Rozenberg, editors, Handbook of Graph Grammars and Computing by Graph Transformation, Volume 2: Applications, Languages and Tools, pages 3–61. World Scientific, 1999.

[bib.bib28] [28] J. Sakarovitch. Elements of automata theory. Cambridge University Press, 2009.

[bib.bib29] [29] VV.AA. egg: e-graphs good. https://egraphs-good.github.io/.

[bib.bib30] [30] Philip Wadler. Monads for functional programming. In Johan Jeuring and Erik Meijer, editors, Advanced Functional Programming, volume 925 of LNCS, pages 24–52. Springer, 1995. doi:10.1007/3-540-59451-5_2.

[bib.bib31] [31] Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. egg: Fast and extensible equality saturation. In POPL 2021, volume 5 of PACMPL, pages 1–29. ACM, 2021. doi:10.1145/3434304.

EGGs Are Adhesive!

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Synopsis.

2 Facts about 𝓜-adhesive categories and kernel pairs

2.1 𝓜-adhesivity

Definition 2.1.

Definition 2.2 ([2, 15, 16, 25, 22]).

▶ Remark 2.3.

Proposition 2.4.

Example 2.5.

Proposition 2.6.

2.2 Some properties of kernel pairs and regular epimorphisms

Definition 2.7.

▶ Remark 2.8.

▶ Remark 2.9.

Proposition 2.10.

Proposition 2.11.

Lemma 2.12.

Proposition 2.13.

Lemma 2.14.

3 Hypergraphical structures

Proposition 3.1.

▶ Remark 3.2.

▶ Remark 3.3.

3.1 The category of hypergraphs

Definition 3.4.

Proposition 3.5.

Corollary 3.6.

Corollary 3.7.

Proposition 3.8.

Example 3.9.

Example 3.10.

▶ Remark 3.11.

Proposition 3.12.

3.1.1 Labelling hypergraph with an algebraic signature

Definition 3.13.

Example 3.14.

Proposition 3.15.

▶ Remark 3.16.

Proposition 3.17.

Example 3.18.

3.2 Term Graphs

Definition 3.19.

▶ Remark 3.20.

Example 3.21.

Proposition 3.22.

Proposition 3.23.

▶ Remark 3.24.

Definition 3.25.

Proposition 3.26.

Lemma 3.27.

Corollary 3.28.

4 Adding equivalences to hypergraphical structures

4.1 Hypergraphs with equivalence

Definition 4.1.

▶ Remark 4.2.

▶ Remark 4.3.

Proposition 4.4.

Corollary 4.5.

Corollary 4.6.

Corollary 4.7.

Lemma 4.8.

Corollary 4.9.

Definition 4.10.

Lemma 4.11.

Lemma 4.12.

Example 4.13.

Lemma 4.14.

Corollary 4.15.

4.2 Term graphs with equivalence

2 Facts about $\mathcal{M}$ -adhesive categories and kernel pairs

2.1 $\mathcal{M}$ -adhesivity

$\blacktriangleright$ Remark 2.3.

$\blacktriangleright$ Remark 2.8.

$\blacktriangleright$ Remark 2.9.

$\blacktriangleright$ Remark 3.2.

$\blacktriangleright$ Remark 3.3.

$\blacktriangleright$ Remark 3.11.

$\blacktriangleright$ Remark 3.16.

$\blacktriangleright$ Remark 3.20.

$\blacktriangleright$ Remark 3.24.

$\blacktriangleright$ Remark 4.2.

$\blacktriangleright$ Remark 4.3.

$\blacktriangleright$ Remark 4.21.

$\blacktriangleright$ Remark 4.22.

$\blacktriangleright$ Remark 5.8.

$\blacktriangleright$ Remark 5.12.

$\blacktriangleright$ Remark 5.13.