This is a tutorial on applied graph rewriting, using Catlab.jl to preform computations.
Algebraic graph rewriting techniques are based on a construction from category theory called a pushout. We’ll examine what these mean in the category of Set and Graph to build intuition about how to work with them.
A diagram of a pushout is below. We usually start with \(f\) and \(g\), and by extension their domain and codomain(s). Constructing a pushout means constructing \(f^\prime\) and \(g\prime\), and the pushout object \(D\).
A pushout is kind of like a discriminated union, but where some elements of the discriminated union are joined together, and which ones are joined are given by the morphisms \(f\) and \(g\). Actually, in category theory, the coproduct is a discriminated union when working in the category Set, and is a special case of a pushout (a type of limit).
In Set the way that elements of the discriminated union are joined together is given by the equivalence classes generated by \(f\) and \(g\). To make the pushout object \(D\) and the pushout morphisms \(g^\prime\) and \(f\prime\):
We reproduce the example pushout between finite sets from (Hartmut et al. 2006, p 31) below:
@present ThSet(FreeSchema) begin
X::Ob
end
@acset_type Set(ThSet)
A = @acset Set begin X = 4 end
B = @acset Set begin X = 4 end
C = @acset Set begin X = 4 end
f = ACSetTransformation(A, B; X = [1,2,2,3])
g = ACSetTransformation(A, C; X = [1,1,2,3])
g′, f′ = pushout(f,g)
D = codom(g′)
DThe discriminated union (coproduct in category Set) is a type of pushout. Specifically, when the apex \(A\) is the empty set (or the initial object for whatever category one is working in) and \(f,g\) are the trivial empty functions. We can check this below. We use apex on the coproduct object as it gives us the apex of the cocone, which is the object we are interested in. The legs of the cocone are the morphisms into that object.
A = Set()
B = @acset Set begin X = 4 end
C = @acset Set begin X = 4 end
f = ACSetTransformation(A, B)
g = ACSetTransformation(A, C)
g′, f′ = pushout(f,g)
D = codom(g′)
D′ = apex(coproduct(B, C))
D == D′trueBy setting up the coproduct as a special kind of pushout, we see pushouts generalize some other common operations. These are all in fact examples of colimits. The final example of a colimit is a co-equalizer.
We’re interested in graph rewriting. Many different types of data structures can be expressed as graphs (or as typed/labeled graphs). We will recreate the example from (Hartmut et al. 2006, p 31).
A = Graph(3)
add_edges!(A, [1,1], [2,3])
B = Graph(4)
add_edges!(B, [1,3], [2,4])
C = Graph(2)
add_edges!(C, [1,1], [1,2])
f = ACSetTransformation(A, B; V = [1,2,2], E = [1,1])
g = ACSetTransformation(A, C; V = [1,1,2], E = [1,2])
g′, f′ = pushout(f,g)Let’s look at the objects involved in the pushout. First, the graph \(A\).
draw(A)
And the graph \(B\),
draw(B)
and the graph \(C\).
draw(C)
Now let’s visualize the graph morphism \(f\) from \(A \to B\). We can see that it’s not monic (injunctive), because the two nodes which are the target of the two edges get merged into a single node in the codomain.
draw(f)
and now \(g\) from \(A \to C\), which is also not monic.
draw(g)
Now let’s see the pushout object \(D\):
draw(codom(g′))
And the morphism g′ from \(B \to D\),
draw(g′) # B -> D
and finally f′ from \(C \to D\).
draw(f′) # C -> D
We can compare this to the discriminated union, which is the coproduct.
draw(apex(cocone(coproduct(B,C))))
pushouts compose, do the 2nd one from (Hartmut et al. 2006, p 33).
D = codom(g′)
E = Graph(3)
add_edges!(E, [1], [2])
e = ACSetTransformation(B, E, V = [1,2,1,2], E = [1,1])
e′′, e′ = pushout(e, g′)
draw(codom(e′))
As in set, the apex of the pushout diagram tells us what objects to identify (glue together) in the pushout object. In this example the apex graph \(A\) only has two nodes with no edges between them. Therefore any edges connecting those two nodes in \(B\) and \(C\) must remain distinct in the pushout graph \(D\), because they do not belong to the same equivalence class. We see in \(D\) therefore the existence of two edges between nodes \(1\) and \(2\).
A = Graph(2)
B = Graph(4)
add_edges!(B, [1,1,2,3,3], [2,3,4,4,1])
C = Graph(4)
add_edges!(C, [1,3,3,4], [2,1,4,2])
f = ACSetTransformation(A, B; V = [1,2])
g = ACSetTransformation(A, C; V = [1,2])
g′, f′ = pushout(f,g)
draw(codom(g′))
Now let us include an edge between \(1 \to 2\) in the apex \(A\), which we identify with the corresponding edges in \(B\) and \(C\). There should only be a single edge between \(1\) and \(2\) in \(D\), because the \(1\to 2\) edges in \(B\) and \(C\) now belong to a single equivalence class.
A = Graph(2)
add_edges!(A, [1], [2])
f = ACSetTransformation(A, B; V = [1,2], E = [1])
g = ACSetTransformation(A, C; V = [1,2], E = [1])
g′, f′ = pushout(f,g)
draw(codom(g′))
Pullbacks are a type of limit where the pullback object and its inclusion morphism can be thought of as a selection (subset) of element (pairs) from the categorical product where the selection is given by those pairs which “agree on” \(D\), where agreement means \(f\) and \(g\) maps those elements into the same element of \(D\).
In the category Set the pullback object \(A\) can be defined as \(A = \{(c,b) | f(c) = g(b) \} \subseteq C \times B\). This example is from (Hartmut et al. 2006, p 35).
C = @acset Set begin X = 3 end
B = @acset Set begin X = 4 end
D = @acset Set begin X = 4 end
f = ACSetTransformation(C, D; X = [1,2,4])
g = ACSetTransformation(B, D, X = [1,1,2,3])
g′, f′ = pullback(f,g)
A = dom(f′)This example is from (Hartmut et al. 2006, p 35).
C = Graph(3)
add_edges!(C, [1,2], [2,3])
B = Graph(3)
add_edges!(B, [1,1], [2,3])
D = Graph(3)
add_edges!(D, [1,1,2], [2,3,3])
f = ACSetTransformation(C, D; V = [1,2,3], E = [1,3])
g = ACSetTransformation(B, D; V = [1,2,3], E = [1,2])
g′, f′ = pullback(f,g)
A = dom(f′)
draw(A)
We can compare the pullback object to the product.
draw(apex(cone(product(B,C))))
A rule consists of graphs \(L\), the preconditions, \(R\), the postconditions, and \(I\), the interface. Because it is a span, there are morphisms \(l\) and \(r\). Speaking broadly, elements \(L\setminus I\) are deleted, elements \(R\setminus I\) are added, and \(I\) is preserved.
If \(l\) is non-injective (not one to one, many elements get sent to one), then we have splitting. If \(r\) is non-injective, we have merging. When both are injective, we have replacement of graph elements (König et al. 2018).
This example is from (Hartmut et al. 2006, p 13).
G = Graph(5)
add_edges!(G, [1,1,1,3,4,2],[4,3,2,2,5,5])
I = Graph(2)
L = Graph(3)
add_edges!(L, [1,1,3], [3,2,2])
R = Graph(4)
add_edges!(R, [1,1,4,3], [3,4,2,2])
m = Search.homomorphisms(L, G)
l = CSetTransformation(I, L; V = [1,2])
r = CSetTransformation(I, R; V = [1,2])
H = rewrite_match(Rule{:DPO}(l,r,monic=true), m[1])
draw(H)
draw(G)
When a DPO rule has a non-injective left leg, one can split nodes.
Sometimes we have to be careful about setting things up to get the desired results. This is when a little bit of knowledge about the algebraic operations underlying graph rewriting can pay off. Let’s consider the case where we want a rule that takes one vertex and splits it into two vertices.
Naively, one might come up with a rule like the following. Here the apex of the span (the interface) has 2 nodes, which get mapped to a single node in the matching graph. The result should turn them into 2 nodes.
L = Graph(1)
I = Graph(2)
R = Graph(2)
l = ACSetTransformation(I, L; V = [1,1])
r = ACSetTransformation(I, R; V = [1,2])
G = Graph(1)
m = Search.homomorphisms(L, G)
H = rewrite_match(Rule{:DPO}(l,r,monic=true), m[1])
draw(H)
Hey the resulting graph looks the same as our input, what happened? The fact that \(G\) has only a single node means that the pushout complement and \(L\) must belong to a single equivalence class. Let it be the smallest, so the pushout complement only has a single node.
We can check this by looking at all the maps.
ik, kg, rh, kh = rewrite_match_maps(Rule{:DPO}(l,r,monic=true), m[1])(ACSetTransformation((V = FinFunction([1, 1], 2, 1), E = FinFunction(Int64[], 0, 0)), Graph {V = 2, E = 0}, Graph {V = 1, E = 0}), ACSetTransformation((V = FinFunction([1], 1, 1), E = FinFunction(Int64[], 0, 0)), Graph {V = 1, E = 0}, Graph {V = 1, E = 0}), ACSetTransformation((V = FinFunction([1, 1], 2, 1), E = FinFunction(Int64[], 0, 0)), Graph {V = 2, E = 0}, Graph {V = 1, E = 0}), ACSetTransformation((V = FinFunction([1], 1, 1), E = FinFunction(Int64[], 0, 0)), Graph {V = 1, E = 0}, Graph {V = 1, E = 0}))draw(ik)
draw(kg)
draw(rh)
draw(kh)
The right way to do it is to use an empty graph for \(I\).
L = Graph(1)
I = Graph(0)
R = Graph(2)
l = ACSetTransformation(I, L)
r = ACSetTransformation(I, R)
G = Graph(1)
m = Search.homomorphisms(L, G)
ik, kg, rh, kh = rewrite_match_maps(Rule{:DPO}(l,r,monic=true), m[1])
H = codom(kh)
draw(H)
We can check the pushout complement object to make sure our intution is working. It should be nothing, because \(L\) already has a single node, so the pushout with the apex the empty graph will correspond to a coproduct, and we only want one thing in the coproduct to get \(G\).
draw(codom(ik))
When a DPO rule has a non-injective right leg, one can merge nodes.
L = Graph(2)
I = Graph(2)
R = Graph(1)
l = ACSetTransformation(I, L; V = [1,2])
r = ACSetTransformation(I, R; V = [1,1])
G = Graph(2)
add_edges!(G, [1], [2])
m = Search.homomorphisms(L, G, monic = true)
H = rewrite_match(Rule{:DPO}(l,r,monic=true), m[1])
draw(H)
In order to avoid “dangling edges” we must simply create the interface \(I\) so that it includes all nodes which have edges out of \(L\) in \(G\). A formal way to say this is that all nodes in \(x \in L\) such that \(m(x)\) is the source or target of an edge \(e \in G \setminus L\) must be included as gluing points in \(I\).
In this example first node in \(L\) is the source of an edge in \(G\), so it must be included in \(I\). It is not, so the pushout complement cannot be computed.
L = Graph(2)
add_edges!(L, [1], [2])
I = Graph(1)
l = ACSetTransformation(I, L; V = [2])
G = Graph(3)
add_edges!(G, [1,1], [2,3])
m = Search.homomorphisms(L, G, monic = true)
can_pushout_complement(l, m[1])falseOne of the reasons that most modern graph rewriting systems rely on the single-pushout (SPO) or sesqui-pushout (SqPO) rewriting is that deletion (and addition) in unknown contexts is not possible in DPO. The main reason is that the pushout complement \(K\) must be a legal graph.