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

- 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

(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// 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

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

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) }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)

## 1 comment:

Hi,

The link you have for the paper is stale (has a servlet session id). Can you tell me what paper you are referring to?

Thanks

Post a Comment