Abstract graph derivations in the double pushout approach

In the algebraic theory of graph grammars, it is common practice to present some notions or results “up to isomorphism”. This allows one to reason about graphs and graph derivations without worrying about representation-dependent details.Motivated by a research activity aimed at providing graph grammars with a truly-concurrent semantics, we front in this paper the problem of formalizing what does it mean precisely to reason about graph derivations “up to isomorphism”. This needs the definition of a suitable equivalence on derivations, which should be consistent with the relevant definitions and results, in the sense that they should extend to equivalence classes. After showing that a naive equivalence is not satisfactory, we propose two requirements for equivalences on derivations which allow the sequential composition of derivations and guarantee the uniqueness of canonical derivations, respectively. Three new equivalences are introduced, the third of which is shown to be satisfy both requirements. We also define a new category having the abstract derivations as arrows, which is, in our view, a fundamental step towards the definition of a truly-concurrent semantics for graph grammars.