nLab
span rewriting

Span rewriting

Span rewriting

Idea

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.

Definitions

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

LlKrR. L \xleftarrow{l} K \xrightarrow{r} R.

A match for this production is a morphism f:LCf:L\to C for some object CC. A derivation of a match along a production is supposed to be a new object obtained by “deleting the image of LL and replacing it with RR”.

A production is left-linear if ll is a monomorphism, and linear if in addition rr is a monomorphism.

Double pushout rewriting

For this definition, we work in an adhesive category (which includes all toposes, hence in particular QuivQuiv). Given a left-linear production LlKrR L \xleftarrow{l} K \xrightarrow{r} R, a match f:LCf:L\to C satisfies the gluing condition if the pair (l,f)(l,f) has a pushout complement consisting of g:KEg:K\to E and v:ECv:E\to C. In this case the (double-pushout) derivation associated to the match is the pushout of gg along rr, yielding a pair of pushout squares

L l K r R f g C v E D.\array{ L & \xleftarrow{l} & K & \xrightarrow{r} & R \\ ^f\downarrow && \downarrow^{\mathrlap{g}} && \downarrow \\ C & \xleftarrow{v} & E & \to & D.}

The restriction of ll to be monic is necessary to ensure that pushout complements are essentially unique when they exist. Often we further restrict rr 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 LL as a substructure of a redex CC. The structure KK, thought of as a substructure of LL, is exactly the part of LL which is to remain invariant as we apply the rule to CC. Finally, parts of RR which are not in KK 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 LL as a substructure of the redex C; secondly, we delete all of parts of the redex matched by LL which are not included in KK. Thirdly, we add all of RR which is not contained in KK, thereby producing a new structure DD. The deletion and addition of structure is handled, respectively, by finding a pushout complement and constructing a pushout.

Sesqui-pushout rewriting

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 LlKrR L \xleftarrow{l} K \xrightarrow{r} R , the (sesqui-pushout) derivation associated to a match f:LCf:L\to C is a diagram

L l K r R f g C v E D.\array{ L & \xleftarrow{l} & K & \xrightarrow{r} & R \\ ^f\downarrow && \downarrow^{\mathrlap{g}} && \downarrow \\ C & \xleftarrow{v} & E & \to & D.}

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 ll 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 Π fl\Pi_f l exists and the counit f *Π fllf^* \Pi_f l \to l is an isomorphism, then such a derivation exists with E=Π flE = \Pi_f l. In particular, this happens in any locally cartesian closed category if ff and ll are both monomorphisms.

Single pushout rewriting

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 LlKrR L \xleftarrow{l} K \xrightarrow{r} R , the (single-pushout) derivation associated to a match f:LCf:L\to C is the pushout of (l,r)(l,r) and ff 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 RR to the target object DD is total.

General gluing constructions

In Lowe10 and Lowe12 a yet more general construction is considered for span rewriting, involving 3×33\times 3 diagrams consisting of a pullback, two final pullback complements, and a pushout.

References

  • 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

  • Andrea Corradini, Tobias Heindel, Frank Hermann, and Barbara König, Sesqui-pushout rewriting, 2006, springerlink, pdf.
  • Michael Löwe, Graph rewriting in Span-categories, 2010, springerlink
  • Michael Löwe, Refined graph rewriting in Span-categories, 2012, springerlink
  • Nicolas Behr, Pawel Sobocinski, Rule Algebras for Adhesive Categories, arXiv:1807.00785

Last revised on July 3, 2018 at 11:47:42. See the history of this page for a list of all contributions to it.