An Algebra of Graphs and Graph Rewriting

In this paper we propose an axiomatization of ‘partially abstract graphs’, i.e., of suitable classes of monomorphisms in a category of graphs, which may be interpreted as graphs having both a concrete part and an abstract part (defined up to isomorphism). Morphisms between pa-graphs are pushout squares. We show that the basic notions of the algebraic theory of graph grammars [Eh79] (instantiated to a suitable category of graphs) can be rephrased in a natural way using partially abstract graphs. The terms of the algebra we propose are built over a small set of operators, including parallel composition, substitution application, and restriction. By equipping the algebra of terms with a categorical structure (arrows are equivalence classes of monadic contexts), we show that there is a full and faithful embedding (with a right adjoint) of the category of partially abstract graphs into the category of (well-formed) terms. This embedding is exploited to show that rewriting (in the sense of term rewriting systems) over this algebra models faithfully the direct derivations of graphs, described by a double pushout construction along the guidelines of [Eh79]. In particular, we show that also graph productions having non-discrete gluing graphs can be represented as term rewrite rules without loss of information, unlike a similar approach proposed in [BC87].