Graph rewriting in some categories of partial morphisms

Abstract

We present a definition of term graph rewriting as the taking of a pushout in a category of partial morphisms, adapting the rather ad hoc definitions we gave in [Ken87] so as to use a standard category-theoretic concept of partial morphism. This single-pushout construction is shown to coincide with the well-known double-pushout description of graph rewriting whenever the latter is defined. In general, the conditions for the single pushout to exist are weaker than those required for the double pushout. In some categories of graphs, no conditions at all are necessary.