Span rewriting is a collection of abstract category-theoretic methods of using spans to “rewrite” objects in a category by “deleting” part of them and replacing it with a substitute part that retains some of the same “connections” between the deleted part and the rest of the object.
The most common application is to the category of quivers (called (directed) graphs in the relevant literature) or related categories; thus span rewriting is often called “graph rewriting”.
There is probably not much connection to algebraic rewriting.
All the definitions below have the following context in common. A production or rule in a category (often the category Quiv of quivers) is a span
A match for this production is a morphism for some object . A derivation of a match along a production is supposed to be a new object obtained by “deleting the image of and replacing it with ”.
A production is left-linear if is a monomorphism, and linear if in addition is a monomorphism.
For this definition, we work in an adhesive category (which includes all toposes, hence in particular ). Given a left-linear production , a match satisfies the gluing condition if the pair has a pushout complement consisting of and . In this case the (double-pushout) derivation associated to the match is the pushout of along , yielding a pair of pushout squares
The restriction of to be monic is necessary to ensure that pushout complements are essentially unique when they exist. Often we further restrict to be monic to ensure overall good behavior, obtaining the notion of linear production.
Lack and Sobocinski describe the intuition in this way:
in order to perform the rewrite, we need to match as a substructure of a redex . The structure , thought of as a substructure of , is exactly the part of which is to remain invariant as we apply the rule to . Finally, parts of which are not in should be added to produce the final result of the rewrite.
Thus, an application of a rewrite rule consists of three steps. First we must match as a substructure of the redex C; secondly, we delete all of parts of the redex matched by which are not included in . Thirdly, we add all of which is not contained in , thereby producing a new structure . The deletion and addition of structure is handled, respectively, by finding a pushout complement and constructing a pushout.
In an adhesive category, the pushout of a monomorphism is also a pullback. Thus, the pushout complements involved in double-pushout rewriting are also “pullback complements”. Pullback complements are not in general unique, even in an adhesive category, but those arising as pushout complements do satisfy a universal property: they are final pullback complements.
This suggests the following generalization. In an arbitrary category, given an arbitrary production , the (sesqui-pushout) derivation associated to a match is a diagram
in which the left square is a final pullback complement and the right square is a pushout. Such a derivation may or may not exist, but if it does then it is essentially unique. Moreover, if we are in an adhesive category and is monic, then any double-pushout derivation is also a sesqui-pushout derivation.
More generally, given the construction of final pullback complements using exponential objects, if the exponential exists and the counit is an isomorphism, then such a derivation exists with . In particular, this happens in any locally cartesian closed category if and are both monomorphisms.
We can also regard a left-linear production as a partial morphism, in which case the universal property of a final pullback complement suggests the following different viewpoint. Given a left-linear production , the (single-pushout) derivation associated to a match is the pushout of and in the category of partial morphisms (if it exists).
It can be shown (see CHHK) that in a certain abstract context, any sesqui-pushout derivation of a left-linear production is also a single-pushout derivation; and that the converse holds if and only if the match is “conflict-free”, and if and only if the induced partial morphism from to the target object is total.
In Lowe10 and Lowe12 a yet more general construction is considered for span rewriting, involving diagrams consisting of a pullback, two final pullback complements, and a pushout.
H. Ehrig, M. Pfender, and H.J. Schneider, Graph-grammars: an algebraic approach, In IEEE Conf. on Automata and Switching Theory, pages 167–180, 1973.
Steve Lack and Pawel Sobocinski, Adhesive categories, PDF
Last revised on July 3, 2018 at 15:47:42. See the history of this page for a list of all contributions to it.