←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 $\mathcal{D}$ of events $\delta = (G_R, V^-, \mu) \in \mathcal{D}$, with

• vertex deletion set $V^- \subseteq V(\mathcal{D} \smallsetminus \delta)$ and
• glueing relation $\mu: V^- \rightharpoonup V(G_R)$.

We have extended the $V(\cdot)$ notation to $\mathcal{D}$ by defining it as the union of all vertex sets of replacement graphs in $\mathcal{D}$. We will similarly use $V(\delta)$ 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$, i.e. there is no graph such that $V^- \subseteq V(G)$. Instead,

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

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

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

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

Merges, confluent persistence and event creation #

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

Creating an event $\delta_r$ from a rewrite $r$ is the simplest type of data mutation that can be recorded in $\mathcal{D}$. For $\mathcal{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 $\delta \in \mathcal{D}$ can define graph mutation operations that apply on collections of events $P \subseteq \mathcal{D}$ – the resulting mutation is equivalent to explicitly creating a merged version of the versions in $P$, followed by the desired rewrite. In this case, the parents of $\delta$ are precisely the set $P = P(\delta)$.

In other words, the parent-child relationships of $\mathcal{D}$ is precisely the event history of $\mathcal{D}$: a directed graph with vertex set $\mathcal{D}$ and edges $\delta_1 \to \delta_2$ if $\delta_1 \in P(\delta_2)$. For $\mathcal{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 $\mathcal{D}$ can be constructed and modified in such a way that acyclicity is guaranteed. Specifically, we introduce two procedures:

• CreateEmpty constructs an empty $\mathcal{D} = \varnothing$, and
• AddEvent, adds an event $\delta$ to $\mathcal{D}$.

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

• $P(\delta) \subseteq \mathcal{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(\delta) \subseteq \mathcal{D}$ defines a partial order on events by guaranteeing that an event $\delta$ can only be defined and added to $\mathcal{D}$ after all its parents $P(\delta)$ have been added.

We say that $\mathcal{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 $\mathcal{D}$ is valid, and thus the event history of $\mathcal{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

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

we require that all sets $\{V^- \mid (G_R, V^-, \mu) \in \lfloor D \rfloor \}$ are disjoint. In the example above, events $\delta_5$ and $\delta_6$ are compatible, wheresa $\delta_5$ and $\delta_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 $\delta_1$ and $\delta_2$ such that a vertex $v$ is both

• in the read only context of $\delta_1$, i.e. $v \in V_1^- \cap dom(\mu_1)$, and thus present both before and after the application of $\delta_1$,
• in the deletion set of $\delta_2$, i.e. $v \in 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)$, where $D_A$ is the sum of the sizes of all vertex deletion sets of events in $\lfloor D \rfloor$

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

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

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

Events are rewrites on the flattened history #

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

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

For the applications of $\mathcal{D}$ that we consider, it will always be sufficient to have a unique root event $\delta_1$. Viewing $\delta_1$ as a rewrite that applies to the empty graph $G_0 = \varnothing \to G_1$, we can understand it as injecting the input graph $G_1$ into $\mathcal{D}$.

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

Consider a set of compatible events $D \in \Gamma(\mathcal{D})$. Define a topological ordering $\delta_1, \ldots, \delta_k$ of the events in $D$, i.e. if $\delta_j \in P(\delta_i)$ then $i < j$.

This construction is illustrated in the following figure for the compatible set $\lfloor \delta_5 \rfloor \cup \lfloor \delta_6 \rfloor$ of the previous example.

We now show that the graph $G_k$ is determined uniquely by $D \in \Gamma(\mathcal{D})$ and provide an explicit procedure to construct it.

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$ 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.

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

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

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

Clearly, $flat(\{\delta_0\}) =G$. We then apply Proposition . repeatedly. If we have a sequence $r_1, \ldots, r_k$ of valid rewrites that can be applied on $G$, then the sequence of events $\delta_1 = r_1, \ldots, \delta_k = r_k$ that it defines can also be added to $\mathcal{D}$ in this order. As we have further seen in Proposition . and Proposition ., the graph $G_k$ that is obtained as a result of the rewrites is the same graph returned by FlattenHistory called on $D = \mathcal{D}$.

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

←Return to chapter