### The data structure

←Return to chapter

## 5.3. The data structure

We now present a data structure that is closely related to equality saturation but supports arbitrary graph rewriting. It is modelled on the graph unfolding construction as presented in Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. Unfolding Graph Transformation Systems: Theory and Applications to Verification.

Rather than maintaining equivalence relations between terms, as done in term graphs, we maintain equivalence relations between graph vertices. Our data structure stores the set of all applied rewrites – the main subject of this section is to show how all operations of interest on this data structure can be implemented efficiently.

The persistent graph rewriting data structure is given by a set D\mathcal{D}D of events δ=(G R, V−,μ)∈D\delta = (G_R, V^-, \mu) \in \mathcal{D}δ=(G R​,V−,μ)∈D, with

- vertex deletion set V−⊆V(D∖δ)V^- \subseteq V(\mathcal{D} \smallsetminus \delta)V−⊆V(D∖δ) and
- glueing relation μ: V−⇀V(G R)\mu: V^- \rightharpoonup V(G_R)μ: V−⇀V(G R​).

We have extended the V(⋅)V(\cdot)V(⋅) notation to D\mathcal{D}D by defining it as the union of all vertex sets of replacement graphs in D\mathcal{D}D. We will similarly use V(δ)V(\delta)V(δ) to denote the set of vertices in the replacement graph of a rewrite δ\delta δ.

Events resemble rewrites as defined in Definition . but differ in that they do not apply to a single graph G GG, i.e. there is no graph such that V−⊆V(G)V^- \subseteq V(G)V−⊆V(G). Instead,

V− ⊆ ⨆δ∈D V(δ)=V(D).V^-\ \subseteq\ \bigsqcup_{\delta \in \mathcal{D}} V(\delta) = V(\mathcal{D}).V− ⊆ δ∈D⨆​V(δ)=V(D).

We will see below how a graph G GG can be constructed such that an event δ∈D\delta \in \mathcal{D}δ∈D is indeed a valid rewrite on G GG.

Using the disjointness of the union in (1), for all v∈V(D)v \in V(\mathcal{D})v∈V(D), there is a unique δ∈D\delta \in \mathcal{D}δ∈D such that v∈V(δ)v \in V(\delta)v∈V(δ) that we call the owner of v v v. The parents (or directed causes) P(δ)P(\delta)P(δ) of an event δ\delta δ are then the owners of the vertices in the deletion set V−V^-V− of δ\delta δ:

P(δ)={δ p∈D∣V−∩V(δ p)≠∅}.P(\delta) = \left\{ \delta_p \in \mathcal{D} \mid V^- \cap V(\delta_p) \neq \varnothing \right\}.P(δ)={δ p​∈D∣V−∩V(δ p​)=∅}.

Inversely, we define the children of δ\delta δ as the set of event whose parents include δ\delta δ

P−1(δ)={δ c∈D∣δ∈P(δ c)}.P^{-1}(\delta) = \left\{\delta_c \in \mathcal{D} \mid \delta \in P(\delta_c)\right\}.P−1(δ)={δ c​∈D∣δ∈P(δ c​)}.

The following figure shows an example of a data structure D\mathcal{D}D on undirected graphs.

Events on an undirected graph with their history. Coloured directed edges represent the parent-child relationship. The area that they rewrite in the parent event is represented by dashed regions of the same colour. The map between graphs is given by the vertex IDs.

#### Merges, confluent persistence and event creation #

A rewrite r=(G R, V−,μ)r = (G_R, V^-, \mu)r=(G R​,V−,μ) that applies to a replacement graph of an event δ p\delta_p δ p​, i.e. V−⊆V(δ p)V^- \subseteq V(\delta_p)V−⊆V(δ p​) immediately defines a valid event δ r:=r\delta_r := r δ r​:=r. In that case, δ r\delta_r δ r​ has a unique parent

P(δ r)={ δ p }.P(\delta_r) = \{ \,\delta_p\, \}.P(δ r​)={δ p​}.

Creating an event δ r\delta_r δ r​ from a rewrite r r r is the simplest type of data mutation that can be recorded in D\mathcal{D}D. For D\mathcal{D}D to be a confluently persistent data structure, it must also be allowed to merge mulitple data mutations together. Rather than handling merges of versions of the data structure explicitly, an event δ∈D\delta \in \mathcal{D}δ∈D can define graph mutation operations that apply on collections of events P⊆D P \subseteq \mathcal{D}P⊆D – the resulting mutation is equivalent to explicitly creating a merged version of the versions in P P P, followed by the desired rewrite. In this case, the parents of δ\delta δ are precisely the set P=P(δ)P = P(\delta)P=P(δ).

In other words, the parent-child relationships of D\mathcal{D}D is precisely the event history of D\mathcal{D}D: a directed graph with vertex set D\mathcal{D}D and edges δ 1→δ 2\delta_1 \to \delta_2 δ 1​→δ 2​ if δ 1∈P(δ 2)\delta_1 \in P(\delta_2)δ 1​∈P(δ 2​). For D\mathcal{D}D to define a valid confluently persistent data structure, we need to

1. Ensure that the event history is acyclic, and
2. Define conditions that guarantee that events correspond to valid data mutations.

We hit both birds with one stone by restricting how D\mathcal{D}D can be constructed and modified in such a way that acyclicity is guaranteed. Specifically, we introduce two procedures:

- `CreateEmpty` constructs an empty D=∅\mathcal{D} = \varnothing D=∅, and
- `AddEvent`, adds an event δ\delta δ to D\mathcal{D}D.

The first is straightforward – and importantly, the only way to construct an instance D\mathcal{D}D. `AddEvent`, on the other hand, enforces two conditions that δ\delta δ must satisfy to be added to a set D\mathcal{D}D:

- P(δ)⊆D P(\delta) \subseteq \mathcal{D}P(δ)⊆D, and
- all parents of δ\delta δ must be compatible.

We defer the discussion on the second condition, enforced by the `AreCompatible` procedure, to its dedicated section below. The restriction P(δ)⊆D P(\delta) \subseteq \mathcal{D}P(δ)⊆D defines a partial order on events by guaranteeing that an event δ\delta δ can only be defined and added to D\mathcal{D}D after all its parents P(δ)P(\delta)P(δ) have been added.

We say that D\mathcal{D}D is valid if it can be constructed from a single call to `CreateEmpty`, followed by a sequence of calls to `AddEvent`. This is equivalent to requiring that

1. the parent-child relationship is acylic and
2. the parents of every event satisfy `AreCompatible`.

For the remainder of this chapter, we will always assume that D\mathcal{D}D is valid, and thus the event history of D\mathcal{D}D is always well-defined and acyclic.

    def CreateEmpty() -> Set[Event]:
        return set()

    def AddEvent(
        events: Set[Event],
        replacement_graph: Graph
        deletion_set: Set[V],
        glueing_relation: EquivalenceRelation[V]
    ) -> Set[Event]:
        new_event = (
            replacement_graph,
            deletion_set,
            glueing_relation
        )
        parents = parents(new_event)
        assert(issubset(parents, events))
        assert(AreCompatible(parents))

        events = union(events, {new_event})

#### Compatible events #

Assuming the parent-child relationship is acylic, we can define the ancestors (or causes) ⌊δ⌋\lfloor\delta\rfloor⌊δ⌋ of an event δ\delta δ recursively

⌊δ⌋={ δ } ∪ ⋃δ p∈P(δ)⌊δ p⌋.\lfloor\delta\rfloor = \{\,\delta\,\}\ \cup\ \bigcup_{\delta_p \in P(\delta)} \lfloor\delta_p\rfloor.⌊δ⌋={δ} ∪ δ p​∈P(δ)⋃​⌊δ p​⌋.

Events D⊆D D \subseteq \mathcal{D}D⊆D are compatible (or a configuration) if all vertex deletion sets V−V^-V− for all ancestors of δ∈D\delta \in D δ∈D are disjoint. That is, writing

⌊D⌋=⋃δ∈D⌊δ⌋,\lfloor D\rfloor = \bigcup_{\delta \in D} \lfloor \delta\rfloor,⌊D⌋=δ∈D⋃​⌊δ⌋,

we require that all sets {V−∣(G R, V−,μ)∈⌊D⌋}\{V^- \mid (G_R, V^-, \mu) \in \lfloor D \rfloor \}{V−∣(G R​,V−,μ)∈⌊D⌋} are disjoint. In the example above, events δ 5\delta_5 δ 5​ and δ 6\delta_6 δ 6​ are compatible, wheresa δ 5\delta_5 δ 5​ and δ 4\delta_4 δ 4​ are not. As pseudocode, this is implemented by the following procedure.

    def AreCompatible(events: Set[Event]) -> bool:
        all_ancestors = union([ancestors(d) for d in events])
        deleted_vertices = set()
        for d in all_ancestors:
            for v in deletion_set(d):
                if v in deleted_vertices:
                    return False
                deleted_vertices.add(v)
        return True

> Note that this definition of event compatibility is a strictly stronger version of parallel independence as is typically defined in DPO rewriting Corrad., 2018Andrea Corradini, Dominique Duval, Michael Löwe, Leila Ribeiro, Rodrigo Machado, Andrei Costa, Guilherme Grochau Azzi, Jonas Santos Bezerra and Leonardo Marques Rodrigues. 2018. On the Essence of Parallel Independence for the Double-Pushout and Sesqui-Pushout Approaches. In Graph Transformation, Specifications, and Nets, Cham. Springer International Publishing, 1--18. doi: 10.1007/978-3-319-75396-6_1. It does not allow for events δ 1\delta_1 δ 1​ and δ 2\delta_2 δ 2​ such that a vertex v v v is both

> - in the read only context of δ 1\delta_1 δ 1​, i.e. v∈V 1−∩d o m(μ 1)v \in V_1^- \cap dom(\mu_1)v∈V 1−​∩dom(μ 1​), and thus present both before and after the application of δ 1\delta_1 δ 1​,
> - in the deletion set of δ 2\delta_2 δ 2​, i.e. v∈V 2−v \in V^-_2 v∈V 2−​.

> This excludes asymmetric conflicts as discussed in e.g. Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. Unfolding Graph Transformation Systems: Theory and Applications to Verification, which arise in the more generali definition. This restriction simplifies our considerations as makes the event history of any event unique.

The runtime is O(D A log⁡D A)O(D_A \log D_A)O(D A​log D A​), where D A D_A D A​ is the sum of the sizes of all vertex deletion sets of events in ⌊D⌋\lfloor D \rfloor⌊D⌋

∑δ∈⌊D⌋∣V δ−∣.\sum_{\delta \in \lfloor D \rfloor} |V^-_\delta|.δ∈⌊D⌋∑​∣V δ−​∣.

The log⁡\loglog factor can typically be removed if the vertices v v v span a contiguous integer range or by using a hash function. Alternatively, the log⁡\loglog factor can also be reduced by using separate sets to track deleted vertices of each event.

When talking about compatible sets of events D⊆D D \subseteq \mathcal{D}D⊆D, it simplifies considerations to always choose D D D such that the ancestors of δ∈D\delta \in D δ∈D are also in D D D, i.e. D=⌊D⌋.D = \lfloor D \rfloor. D=⌊D⌋. We introduce the notation

Γ(D)={⌊D⌋∣D⊆D and D is compatible}⊆P(D)\Gamma(\mathcal{D}) = \{ \lfloor D \rfloor \mid D \subseteq \mathcal{D} \text{ and } D \text{ is compatible}\} \subseteq \mathcal{P}(\mathcal{D})Γ(D)={⌊D⌋∣D⊆D and D is compatible}⊆P(D)

for the set of all compatible sets of rewrites of the form ⌊D⌋\lfloor D \rfloor⌊D⌋.

#### Events are rewrites on the flattened history #

We have so far explored how events can be added to D\mathcal{D}D, as well as when they are compatible. However, until we have established that adding events to D\mathcal{D}D is in some sense equivalent to applying rewrites on a graph, it is hard to see how the data structure D\mathcal{D}D would be useable for graph rewriting. This is precisely our next point.

> In a valid non-empty D\mathcal{D}D, events δ∈D\delta \in \mathcal{D}δ∈D form a directed acyclic graph and therefore there must always be (at least) one “root” event δ 1∈D\delta_1 \in \mathcal{D}δ 1​∈D with no parents P(δ 1)=∅P(\delta_1) = \varnothing P(δ 1​)=∅. δ 1\delta_1 δ 1​ is thus a valid rewrite that can be applied to any graph.

> For the applications of D\mathcal{D}D that we consider, it will always be sufficient to have a unique root event δ 1\delta_1 δ 1​. Viewing δ 1\delta_1 δ 1​ as a rewrite that applies to the empty graph G 0=∅→G 1 G_0 = \varnothing \to G_1G 0​=∅→G 1​, we can understand it as injecting the input graph G 1 G_1G 1​ into D\mathcal{D}D.

> Non-root events in D\mathcal{D}D on the other hand typically correspond to valid (semantics preserving) rewrites in the GTS under consideration.

Consider a set of compatible events D∈Γ(D)D \in \Gamma(\mathcal{D})D∈Γ(D). Define a topological ordering δ 1,…,δ k\delta_1, \ldots, \delta_k δ 1​,…,δ k​ of the events in D D D, i.e. if δ j∈P(δ i)\delta_j \in P(\delta_i)δ j​∈P(δ i​) then i<j i < ji<j.

Proposition 5.1Events as valid rewrites

There are graphs G 0,…,G k G_0, \ldots, G_kG 0​,…,G k​ such that for all 1⩽i⩽k 1 \leqslant i \leqslant k1⩽i⩽k, the event δ i\delta_i δ i​ defines a valid rewrite r i r_i r i​ on G i−1 G_{i-1}G i−1​ and G i=r i(G i−1)G_i = r_i(G_{i-1})G i​=r i​(G i−1​).

Define the empty graph G 0=∅G_0 = \varnothingG 0​=∅. The event δ 1\delta_1 δ 1​ has no parent and thus must have an empty vertex deletion set and glueing relation. It is thus a valid rewrite r 1 r_1 r 1​ on G 0 G_0G 0​. Define G 1=r 1(G 0)G_1 = r_1(G_0)G 1​=r 1​(G 0​).

We can similarly define G i=r i(G i−1)G_i = r_i(G_{i-1})G i​=r i​(G i−1​) inductively for graphs G 2,…,G k G_2, \ldots, G_kG 2​,…,G k​ if we show for 2⩽i⩽k 2 \leqslant i \leqslant k2⩽i⩽k that the i ii-th event δ i\delta_i δ i​ defines a valid rewrite r i r_i r i​ on G i−1 G_{i-1}G i−1​. The set of vertices in G i−1 G_{i-1}G i−1​ is the union of all vertices in the replacement graph of δ 1,…,δ i−1\delta_1, \ldots, \delta_{i-1}δ 1​,…,δ i−1​ minus their vertex deletion sets

V(G i−1)=(⨆1⩽j<i V(δ j))∖(⨆1⩽j<i V j−),V(G_{i-1}) = \left(\bigsqcup_{1 \leqslant j < i} V(\delta_j)\right) \setminus \left(\bigsqcup_{1 \leqslant j < i} V^-_j\right),V(G i−1​)=(1⩽j<i⨆​V(δ j​))∖(1⩽j<i⨆​V j−​),

where V j−V^-_j V j−​ is the vertex deletion set of δ j\delta_j δ j​.

Now, by definition of the event δ i\delta_i δ i​,

V i−⊆⨆1⩽j<i V(δ j).V^-_i \subseteq \bigsqcup_{1 \leqslant j < i} V(\delta_j).V i−​⊆1⩽j<i⨆​V(δ j​).

On the other hand, because of the compatibility of all events in D D D, we know that V i−∩V j−=∅V^-_i \cap V^-_j =\varnothing V i−​∩V j−​=∅ for all 1⩽j<i 1 \leqslant j < i1⩽j<i. It thus follows V i−⊆V(G i−1)V^-_i \subseteq V(G_{i-1})V i−​⊆V(G i−1​). Hence δ i\delta_i δ i​ is indeed a valid rewrite of G i−1 G_{i-1}G i−1​, and thus r i r_i r i​ and G i G_iG i​ are well-defined.

This construction is illustrated in the following figure for the compatible set ⌊δ 5⌋∪⌊δ 6⌋\lfloor \delta_5 \rfloor \cup \lfloor \delta_6 \rfloor⌊δ 5​⌋∪⌊δ 6​⌋ of the previous example.

Applying events as rewrites in topological order. The result is a sequence of valid graph rewrites that start from the graph of δ 1\delta_1 δ 1​.

We now show that the graph G k G_kG k​ is determined uniquely by D∈Γ(D)D \in \Gamma(\mathcal{D})D∈Γ(D) and provide an explicit procedure to construct it.

Proposition 5.2Flat graph extraction

The graph G k G_kG k​ obtained by applying the set of compatible rewrites D∈Γ(D)D \in \Gamma(\mathcal{D})D∈Γ(D) in topological order on the empty graph is independent of the topological ordering chosen.

Given the set of rewrites D⊆D D \subseteq \mathcal{D}D⊆D, the procedure `FlattenHistory` returns G k G_kG k​ in time

O(m+n)O(m + n)O(m+n)

where n nn and m mm are the total number of vertices and edges across all replacement graphs in D D D.

Let us start with the definition of `FlattenHistory`:

     1def FlattenHistory(events: Set[Event]) -> Graph:
     2    all_ancestors = union([ancestors(d) for d in events])
     3    graph = Graph()
     4    for a in toposort(all_ancestors):
     5        add_graph(graph, replacement_graph(a))
     6        for (del_v, repl_v) in glueing_relation(a):
     7            move_edges(graph, repl_v, del_v)
     8        for v in deletion_set(a):
     9            remove_vertex(graph, v)
    10    return graph

`toposort` is a function that returns a topological ordering of the rewrites in D D D according to the parent-child rewrite relation, `add_graph` inserts the graph passed as second argument into the graph passed as first argument, `remove_vertex` removes the vertex along with all incident edges from the graph and `move_edges` moves all edges of the second vertex to the first vertex.

Correctness of `FlattenHistory`.It is easy to see that if the graph G k G_kG k​ that is obtained from applying the rewrites in order is independent of the choice of the toplogical ordering, then `FlattenHistory` is a correct implementation of the procedure, as it applies one rewrite at a time, in topological order.

Rewrite order invariance.Consider two rewrites δ 1, δ 2∈D\delta_1, \delta_2 \in D δ 1​,δ 2​∈D such that neither is an ancestor of the other. Let

D p r e=⌊δ 1⌋∪⌊δ 2⌋⊆D D_{pre} = \lfloor \delta_1 \rfloor \cup \lfloor \delta_2 \rfloor \subseteq D D pre​=⌊δ 1​⌋∪⌊δ 2​⌋⊆D

and proceed by induction over D p r e D_{pre}D pre​: assume the graph G p r e G_{pre}G pre​ obtained by applying the rewrites in D p r e D_{pre}D pre​ is invariant on the choice of the topological ordering of D p r e D_{pre}D pre​. Clearly this is true for D p r e=∅D_{pre} = \varnothing D pre​=∅. All that remains to be shown is that G p o s t G_{post}G post​ obtained by applying first δ 1\delta_1 δ 1​ then δ 2\delta_2 δ 2​ on G p r e G_{pre}G pre​ is equal to G p o s t′G_{post}'G post′​, obtained by applying the same rewrites in the reverse order on G p r e G_{pre}G pre​.

The vertex sets V 1−V^-_1 V 1−​ and V 2−V^-_2 V 2−​ of δ 1\delta_1 δ 1​ and δ 2\delta_2 δ 2​ must be disjoint because δ 1, δ 2∈D\delta_1, \delta_2 \in D δ 1​,δ 2​∈D and hence are compatible. Furthermore, the replacement graphs (by definition of the rewrites) and the glueing relations of δ 1\delta_1 δ 1​ and δ 2\delta_2 δ 2​ (by rewrite compatibility) cannot contain vertices in V 1−⊔V 2−V^-_1 \sqcup V^-_2 V 1−​⊔V 2−​. It follows that the order in which vertices of V 1−⊔V 2−V^-_1 \sqcup V^-_2 V 1−​⊔V 2−​ are removed from G p r e G_{pre}G pre​ does not affect the graph G p o s t G_{post}G post​. Furthermore, vertex merging is a commutative operation, and so is disjoint graph addition. It follows G p o s t=G p o s t′G_{post} = G_{post}'G post​=G post′​ and hence the result.

Runtime.In total n nn vertices and m mm edges will be added to `graph` by `add_graph` on line 5. As a result, at most n nn vertices can ever be deleted by line 9. Finally, while a naive implementation of `move_edges` of line 7 might result in the same edge being moved many times, all edge moves can be cached and only executed once at the end: notice that every time edges are moved away from a vertex, that vertex is subsequently removed from the graph. Instead of removing the vertex, keep it “hidden”, with a link to the vertex that the edges should be moved to. Once all graph operations are completed, traverse all hidden vertices and follow the links to the vertices that the edges should be moved to. This can be done in O(n)O(n)O(n) time. Then move all edges to the correct vertex, in time O(m)O(m)O(m), and delete the hidden vertices.

Now instead of exploring the space of all graphs G\mathcal{G}G reachable by repeatedly applying rewrites, we can explore the rewrite space by adding events to D\mathcal{D}D. Write f l a t(D)flat(D)f l at(D) for the graph returned by `FlattenHistory` on set D D D. If G′\mathcal{G}'G′ is the set of all graphs returned by `FlattenHistory` on compatible events

G′={ f l a t(D)∣D∈Γ(D)},\mathcal{G}' = \{\ flat(D) \mid D \in \Gamma(\mathcal{D})\},G′={ f l at(D)∣D∈Γ(D)},

then Proposition . and Proposition . combined guarantee that G′⊆G\mathcal{G}' \subseteq \mathcal{G}G′⊆G. To conclude, we show that indeed any graph in G\mathcal{G}G is in G′\mathcal{G}'G′, and hence G=G′\mathcal{G} = \mathcal{G}'G=G′.

Proposition 5.3Rewrites as valid events

Let D∈Γ(D)D \in \Gamma(\mathcal{D})D∈Γ(D) be a set of compatible events and G=f l a t(D)G = flat(D)G=f l at(D). Any rewrite r r r that can be applied on G GG defines an on G GG defines an event δ=r\delta = r δ=r that can be added to D\mathcal{D}D.

We recall that a rewrite r=(G R, V−,μ)r = (G_R, V^-, \mu)r=(G R​,V−,μ) defines an event δ=(G R, V−,μ)\delta = (G_R, V^-, \mu)δ=(G R​,V−,μ) that can be added to D\mathcal{D}D if

- P(δ)⊆D P(\delta) \subseteq \mathcal{D}P(δ)⊆D, and
- all rewrites in P(δ)P(\delta)P(δ) are compatible.

By the rewrite definition, V−⊆V(G)V^- \subseteq V(G)V−⊆V(G). It follows in particular that

V−⊆⋃δ′∈D V(δ′),V^- \subseteq \bigcup_{\delta' \in D} V(\delta'),V−⊆δ′∈D⋃​V(δ′),

and thus V−⊆V(D)V^- \subseteq V(\mathcal{D})V−⊆V(D), as well as P(δ)⊆D⊆D P(\delta) \subseteq D \subseteq \mathcal{D}P(δ)⊆D⊆D. This proves both conditions.

Starting from the empty graph D=∅\mathcal{D} = \varnothing D=∅, we can create a root event δ 0=(G,∅,∅)\delta_0 = (G, \varnothing, \varnothing)δ 0​=(G,∅,∅) with an empty vertex deletion set and glueing relation and add it to D.\mathcal{D}.D.

Clearly, f l a t({δ 0})=G flat(\{\delta_0\}) =G f l at({δ 0​})=G. We then apply Proposition . repeatedly. If we have a sequence r 1,…,r k r_1, \ldots, r_k r 1​,…,r k​ of valid rewrites that can be applied on G GG, then the sequence of events δ 1=r 1,…,δ k=r k\delta_1 = r_1, \ldots, \delta_k = r_k δ 1​=r 1​,…,δ k​=r k​ that it defines can also be added to D\mathcal{D}D in this order. As we have further seen in Proposition . and Proposition ., the graph G k G_kG k​ that is obtained as a result of the rewrites is the same graph returned by `FlattenHistory` called on D=D D = \mathcal{D}D=D.

In other words, we conclude that exploring the rewrite space on G GG is fully equivalent to exploring the space of valid events starting from D={δ 0}\mathcal{D} = \{ \delta_0 \}D={δ 0​}.

←Return to chapter