Documentation

A finite directed multigraph: a vertex type v, an edge type e, and the incidence functions src, tgt :: e -> v.

A graph homomorphism: a pair of functions on vertices and edges. Well-formedness (commuting with src/tgt) is a precondition of the functions below, not checked here — the same convention Pushout uses for its own square-commutativity.

The pushout of two graph homomorphisms sharing a domain: vertices and edges are pushed out independently in FINHASK (graph colimits, like all presheaf colimits, are computed pointwise), and the incidence functions of the result are induced from the two input graphs' incidence functions.

A graph rewrite rule: a span L <- K -> R of graph homomorphisms, together with R itself (needed, since gluing R into the result requires R's own incidence functions).

Compute the pushout complement of a rule's left leg and a match into a host graph g. Fails (calls the second continuation) if the gluing condition doesn't hold: either an identification conflict (as in plain FINHASK, on vertices or on edges), or the graph-specific dangling condition — an edge that survives the rewrite is still attached to a vertex that the rewrite deletes.

Apply a GraphRule to a host graph at a match L -> G. On success, the continuation receives the rewrite's cospan legs D -> G, D -> H and the embedding R -> H of the newly created pattern into the result H (given explicitly, since unlike a bare object in a kind-indexed category, a Graph carries data the caller needs to keep rewriting).

Example: deleting an edge

The host graph g is a single edge between two vertices:

 g:   0 --e0--> 1

The rule deletes that edge but keeps both endpoints: L has the edge, K and R don't.

 L:   0 --e--> 1        K:   0   1        R:   0   1

Matching L's edge e onto g's e0 and applying the rule keeps both vertices (tracked by r2h, the embedding of R into the result) and leaves no edges behind:

>>> import Proarrow.Category.Instance.FinHask (Fin, fromList, toList)
>>> import Proarrow.Core ((\\))
>>> let g = Graph (fromList [(0 :: Fin 1, 0 :: Fin 2)]) (fromList [(0 :: Fin 1, 1 :: Fin 2)]) :: Graph (Fin 2) (Fin 1)
>>> let k = Graph (fromList []) (fromList []) :: Graph (Fin 2) (Fin 0)
>>> let idV = fromList [(0 :: Fin 2, 0 :: Fin 2), (1 :: Fin 2, 1 :: Fin 2)]
>>> let rule = GraphRule (GraphHom idV (fromList [])) (GraphHom idV (fromList [])) k :: GraphRule (Fin 2) (Fin 0) (Fin 2) (Fin 1) (Fin 2) (Fin 0)
>>> let m = GraphHom idV (fromList [(0 :: Fin 1, 0 :: Fin 1)]) :: GraphHom (Fin 2) (Fin 1) (Fin 2) (Fin 1)
>>> (dpoStepGraph g rule m (\h _ _ r2h -> (P.show (toList (vertexMap r2h), toList (graphSrc h), toList (graphTgt h))) \\ graphSrc h) "gluing failed") :: P.String
"([(0,0),(1,1)],[],[])"

Example: the dangling condition

Same host graph g, but the rule instead deletes vertex 0 in isolation: L has one vertex and no edges, K and R are empty.

 L:   0                 K:   (empty)       R:   (empty)

Vertex 0 still has e0 attached to it in g, and e0 isn't part of the match, so deleting the vertex would leave e0 dangling — the gluing condition fails:

>>> let k' = Graph (fromList []) (fromList []) :: Graph (Fin 0) (Fin 0)
>>> let rule' = GraphRule (GraphHom (fromList []) (fromList [])) (GraphHom (fromList []) (fromList [])) k' :: GraphRule (Fin 0) (Fin 0) (Fin 1) (Fin 0) (Fin 0) (Fin 0)
>>> let m' = GraphHom (fromList [(0 :: Fin 1, 0 :: Fin 2)]) (fromList []) :: GraphHom (Fin 1) (Fin 0) (Fin 2) (Fin 1)
>>> dpoStepGraph g rule' m' (\_ _ _ _ -> "glued (unexpected)") "gluing failed"
"gluing failed"