Graph transformations

This is obviously related to the network theory work. This page is intended to contain general information on graph transformations or graph rewriting. It would be nice to be able to define a *graph grammar* (see definition 3.5.7 on p. 85 of Schneider’s book linked below or definition 3.5.10 for the generalization to hypergraphs) and then plug in some arbitrary graphs or those derived from various sorts of data and see what happens even if we already know something about what would happen via various results that can be proved about a particular grammar or graph grammars in general. This already exists to some extent in quantomatic (see links below), but it might be nice to redevelop something similar in Haskell/Coq or OCaml/Coq.

Here’s a quick review of what existed in the graph transformation field in 2010 from the *related work* section of

- Dixon L, Kissinger A. Open Graphs and Monoidal Theories. arXiv 2010 Nov;31.

There is a significant strand of work concerning graph transformations (Ehrig et al., 2006; Baldan et al., 2008) and rewriting with graph-based presentations of computational processes (Lafont, 2010; Lafont and Rannou, 2008; Lafont, 2003; Lafont, 1990). An extension of these formalisms, known as bigraphs, provides another general formalism for graphical rewriting (Milner, 2006). Bigraphs are more complex in that they use hyper-graphs and introduce a rich hierarchical structure. Another formalism for graphs, called site-graphs, is used in systems biology (Danos and Laneve, 2004). These give each vertex a set of ‘sites’ to which edges can be be connected. The distinction between these forms of graphical rewriting and our formalism is that we have an extended notion of “graph” that allows for edges to be dangling at one or both ends, or be connected to themselves. We also consider these graphs as having a fixed interface, drawn as a collection of input and output wires and consider only graph rewrite rules that preserve this interface. In this regard, we provide a kind of static checking for well-behaved graph transformation systems, much like types do for functional programs.

Here are some relevant links

- Lucas Dixon and Alex Kissinger’s open graphs have been implemented in quantomatic whose ML)/Isabelle with Java GUI code is available on github
- Robin Milner’s bigraphs
- Hans Jürgen Schneider’s page on graph transformations with book and Haskell code take’s the double-pushout approach explained in Ehrig’s book Fundamentals of algebraic graph transformation
- Sebastiano Vigna’s page on graph fibrations
- Pedro Pablo Pérez Velasco’s matrix graph grammars

Mathematically, the right framework for studying ‘graph transformations’ is a symmetric monoidal bicategory. Open graphs are morphisms in a symmetric monoidal category, as Dixon and Kissinger note. So, transformations between these should be 2-morphisms!

Unluckily, most people are scared of symmetric monoidal bicategories. Luckily, and by no coincidence, Mike Stay is writing his thesis on them. Here’s a talk:

- Mike Stay, Closed monoidal bicategories.

Here’s a somewhat old draft of a paper:

- Mike Stay, Compact closed bicategories.

‘Rewrite rules’ for electrical circuits, like the famous Y-Delta transform, are closely akin to graph transformations.