Monographs, Their Morphisms, and the Rules That Bind Them

Table of Links

Abstract and 1 Introduction

2 Basic Definitions and Notations

2.1 Sets

2.2 Sequences

2.3 Signatures and Algebras and 2.4 Categories

3 Monographs and their Morphisms

4 Limits and Colimits

5 Drawing Monographs

6 Graph Structures and Typed Monographs

7 Submonographs and Partial Morphisms

8 Algebraic Transformations of Monographs

9 Attributed Typed Monographs

10 Conclusion and References

8 Algebraic Transformations of Monographs

Rule-based transformations of graphs are conceived as substitutions of subgraphs (image of a left hand side of a rule) by subgraphs (image of its right hand side). Substitutions are themselves designed as an operation of deletion (of nodes or edges) followed by an operation of addition. This last operation is conveniently represented as a pushout, especially when edges are added between existing nodes (otherwise a coproduct would be sufficient).

The operation of deletion is however more difficult to represent in category theory, since there is no categorical notion of a complement. This is a central and active issue in the field of Algebraic Graph Transformation, and many definitions have been proposed, see [12, 13, 14, 15]. The most common and natural one, known as the double pushout method [16, 17, 18], assumes the operation of deletion as the inverse of the operation of addition.

More precisely, in the following pushout diagram

Note that D is finite whenever M is finite. This proves that this gluing condition is also valid in FMonogr, and it is obviously also the case in SMonogr, O-Monogr and O-SMonogr for every set O of ordinals. It therefore characterizes the existence of D, but by no means its unicity.

One way of ensuring the unicity of D (up to isomorphism) is to assume that l is injective: this is a well-known consequence of Theorem 4.17 (see [8]). However, an analysis of the construction of D in the proof of Lemma 8.2 (sufficient condition) shows that we can always build D as a submonograph of M, hence we may as well assume that f is a canonical injection and avoid restrictions on l. We therefore adopt a restricted notion of double pushout transformation compared to the standard one.

As noted in Example 7.6, pushout of partial morphisms have a potential of removing edges. Since such pushouts always exist, they can be used to define transformations that are not restricted by the gluing condition. This is the idea of the single pushout method, that was initiated in [19] and fully developed in [20, 3].

We therefore see that single pushouts implement a semantics where edges can be silently removed, but minimally so for a monograph to be obtained. This may remove edges in a cascade, a feature that does not appear on graphs. Note that item (1) of the gluing condition may also be breached when an edge is marked more than once for removal, in which case it is deleted, but also when an edge is marked both for removal and for preservation. Example 7.6 shows that in such cases the edge is also removed. All edges marked for removal are guaranteed to be deleted, and the other edges are preserved only if this does not conflict with deletions. This semantics of transformation rules is thus dual to the previous one, and should be more appealing to the daring (or lazy) programmer.