# The Azimuth Project Graph transformations (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

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

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.