The algebra of graphs: individually and collectively

i needed a graph package for a compiler i was writing and decided to put my money where my mouth is and design a little compositional graph package. i devised a little linear notation (plus a set of identities erasing the differences in serialization that don't matter) that i was expecting to have terrible complexity properties. However, after looking at several examples, i was pleasantly surprised. The design was influenced by some recent work on graph polynomials (there are a number of polynomial invariants that have been developed over the years) that shows that all of the major polynomials can be captured by a certain recurrence relation. i simply read the recurrence relation backwards to devise the little graph algebra. Two points of note

• When you calculate from one of these graph expressions the simplest polynomial satisfying the recurrence relation you realize that you need one more graph term ctor. When you add this, surprise, surprise, you get a model of multiplicative linear logic.
• Once you have a graph algebra, you can play the little trick of deriving a logic/query language from the algebra (monad). This gives you a graph query mechanism. It's pretty cool.

The recurrence relation is taken from this paper, but it's easy enough to state.

• P(G,x) := P(G-e) + x*P(G-u-v) (src(e) = u; trgt(e) = v)
  
• P(G1+G2,x) := P(G1)*P(G2)
• P(E1) := 1
  
• P(0) := 1

where G-e is the graph derived from G by removing the edge e and G-u-v is the graph derived from G by remove the vertices u and v and all the edges connected to them; G1+G2 is the disjoint sum of the two graphs; E1 is the 1-chain or graph with two vertices and a single edge between them; 0 is the empty graph
(Aside, if you know anything about knots, you will see a striking correspondence between this relation and the Kauffman bracket.)

This relation gives rise to the following term language for describing graphs.

G,H ::= Nil // empty graph

P // "pointed graph" or graph in which the vertex v
// has been selected (and possibly adjoined)
e(P,Q) // graph in which an edge connects the points of
// two pointed graphs
G*H // Disjoint union of two graphs

P,Q ::= v.G // notation for pointing

Obviously, there are lots of ways to represent the same graph in this linear notation. We erase these syntactic differences with the following laws.

This notation requires the following identities
Commutative monoid laws

G * Nil = G (= Nil * G)
G1 * (G2 * G3) = (G1 * G2) * G3
G1 * G2 = G2 * G1

Pointing laws
V1.V2.G = (V1.Nil) * V2.G (provided V1 =/= V2)
V.V.G = V.G

Connection laws
E2(V3.G1,V4.E1(V1.G2,V2.G)) = E1(V1.G2,V2.E2(V3.G1,V4.G))

Examples:
-- The graph with n vertices and no edges: V1 * ... * Vn
-- The chain with n vertices: Chain(0) = Nil
-- Chain(n) := En-1(Vn.Nil,Vn-1.Chain(n-1))
-- A two-cycle E2(V2.E1(V1,V2),V1.E1(V1,V2))
-- An n-cycle En(Vn.Chain(n),V1.Chain(n))
-- A complete graph of 4 vertices
K(4) = E43(V4,V3.E42(V4,V2.(E41(V4,V1.K(3)))))

Now, when you go to calculate a polynomial from one of these terms you will discover that removing an edge gets you to structures in which either

• you have two disjoint graphs
• you have common subgraphs

representing the latter conveniently suggests adding the following term to the grammar above

G,H ::= ...

G|H

This is also subject to commutative monoid laws. Interestingly, life is easier if we separate use-cases into constructive uses and de-constructive uses. The constructive interface mirrors the first grammar while the de-constructive interface extends the grammar with the second term. All of this mimics edges as cuts in a linear proof.

If you feed the following grammar in BNFC you can generate Haskell or Java codes for parsing these expressions as well as an in-memory set of data types for manipulating graphs.

Isolated . Graph ::= Graph "*" Graph1 ;
Folded . Graph1 ::= Graph1 "|" Graph2 ;
GraphCtor . Graph2 ::= GraphTerm ;
_ . Graph ::= Graph1 ;
_ . Graph1 ::= Graph2 ;
_ . Graph2 ::= "(" Graph ")" ;

Empty . GraphTerm ::= "Nil" ;
Pointed . GraphTerm ::= PointedExpr ;
Connected . GraphTerm ::= Edge "(" PointedExpr "," PointedExpr ")" ;

Selected . PointedExpr ::= Vertex "." Graph ;

EdgeQuotation . Edge ::= "((" Graph "))" ;
VertexQuotation . Vertex ::= "[[" Graph "]]" ;

Now, we can play the game i have been describing in many of the previous posts to derive a logic/query language for graphs. Suppose we have a read-only database of graphs and we want our graph queries to return sets of graphs. Further, suppose that L(G) denotes the set of graphs in our term language and = denotes the smallest equivalence relation containing the identities above. Then we have the following language and its corresponding semantics.

Q,R ::= true [| true |](u) = L(G)

~Q [| ~Q |](u) = L(G) \ [| Q |](u)
Q&R [| Q&R |](u) = [| Q |](u) \cap [| R |](u)

NIL [| NIL |](u) = { G \in L(G) | G = Nil }
v.Q [| v.Q |](u) = { G \in L(G) | G = v.H, H \in [| Q |](u) }
e(V,W) [| e(V,W) |](u)
=
{ G \in L(G) | G = e(P1,P2),
P1 \in [| V |](u), P2 \in [| P2 |](u) }
Q*R [| Q*R |](u)
=
{ G \in L(G) | G = G1 + G2,
G1 \in [| Q |](u), G2 \in [| R |](u) }

rec X.Q [| rec X.Q |](u)
=
\Cup { S \in Pow(L(G)) | S \subset [| Q |](u[X <- S]) }
X [| X |](u) = u(X)

V,W ::= v.Q [| v.Q |](u) = { G \in L(G) | G = v.H, H \in [| Q |](u) }