Single-pushout rewriting in categories of spans I: the general setting

Abstract

A unifying view of all constructions of pushouts of partial morphisms considered so far in the literature of single-pushout transformation is given in this paper. Pushouts of partial morphisms are studied in an abstract category of spans formed out of two distinguished subcategories of the base category, thus generalizing previous studies in single-pushout transformation. Such spans are single pairs of morphisms, instead of equivalence classes, providing then a notion of transformation which is independent of class representatives.

A necessary and sufficient condition for the existence of the pushout of two spans is established which involves properties of the base category, from which the category of spans is derived, as well as properties of the spans themselves. Moreover, a necessary and sufficient condition for single-pushout derivations in a category of spans to subsume double-pushout derivations in the base category is established which only involves properties of the base category.