Making Sense of Attributed Typed Monographs

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

9 Attributed Typed Monographs

The notion of E-graph has been designed in [2] in order to obtain an adhesive category of graphs with attributed nodes and edges. This follows from a line of studies on Typed Attributed Graph Transformations, see [21, 22, 23]. The attributes are taken in a data type algebra and may be of different sorts (booleans, integers, strings, etc.). In the case of E-graphs only the nodes of sort values represent such attributes. But they are also typed by E-graphs, and in the type E-graphs each node of sort values represent a sort of the data type algebra. This should recall the constructions of Section 6 that we now use in order to generalize the notion of typed attributed graphs given in [2]. The idea is similarly to impose that the edges typed by a sort of a data type algebra are the elements of the corresponding carrier set.

Theorem 9.4 generalizes[3] [2, Theorem 11.3] that establishes an isomorphism between the category of attributed E-graphs typed by an attributed E-graph AT G and the category of algebras of a signature denoted AGSIGpAT Gq. In particular Theorem 11.3 of [2] requires the hypothesis that AGSIGpAT Gq should be well-structured, which means that if there is an operator name of ST whose domain sort is s then s is not a sort of the data type signature Σ. Obviously this is equivalent to requiring that only nodes of T can be considered as sorts of Σ and is linked to the fact that only values nodes of E-graphs are supposed to hold attributes. Since we are not restricted to E-graphs there is no need to require that attributes should only be nodes. This has an interesting consequence:

The approach adopted in [2, Definition 11.5] is to restrict the morphisms used in span rules to a class of monomorphisms that are extensions of Σ-isomorphisms to pΓ `Σq-homomorphisms. It is then possible to show [2, Theorem 11.11] that categories of typed attributed E-graphs are adhesive HLR categories (a notion that generalizes Definition 4.13, see [24]) w.r.t. this class of monomorphisms.

A similar result holds on categories of ATMs. For the sake of simplicity, and since rule-based graph transformations are unlikely to modify attributes such as booleans, integers or strings (and if they do they should probably not be considered as graph transformations), we will only consider morphisms that leave the data type algebra unchanged, element by element. This leaves the possibility to transform the edges whose sort is in Γ but not in Σ.

The proof that the categories ATMpT, Aq are adhesive will only be sketched below. The key point is the following lemma.

Hence the property of stabilization characterizes the difference between morphisms in Monogrz\T and morphisms in ATM(T, A). Besides, it is well-known how pushouts and pullbacks in Monogrz\T can be constructed from those in Monogr, and we have seen that these can be constructed from those in Sets.

Theorem 9.8. ATM(T, A) is adhesive.

This result does not mean that all edges that are not attributes can be freely transformed. Their adjacencies to or from attributes may impose constraints that only few morphisms are able to satisfy.

Example 9.9. Let Σ be the signature with no operation name and one sort s, and A be the Σ-algebra defined by As “ ta, bu. We consider the type monograph T “ tpe, sq,ps, equ. A monograph typed by T has any number (but at least one) of edges typed by e that must be adjacent either to a or b, and two edges typed by s, namely a and b, that must be adjacent to either the same edge x typed by e, which yields two classes of monographs

(to which may be added any number of edges typed by e and adjacent to either a or b), or a and b are adjacent to y and z respectively, and we get four more classes:

The function y, z → x is a morphism from these last two monographs to the two monographs above (respectively). There are no other morphisms between monographs from distinct classes. We therefore see that in the category ATM(T, A) it is possible to add or remove edges typed by e to which a or b are not adjacent, but there is no way to remove the edges y and z (because this would require a rule with a left morphism from an ATM without y and z to an ATM with y and z, and there is no such morphism), though they are not attributes.

Besides, we see that this category has no initial object, no terminal object, no products nor coproducts.

[3] Our proof is also much shorter than the 6 pages taken by the corresponding result on attributed typed E-graphs. This is due partly to our use of AT (Definition 6.7) and of Theorem 6.8, but also to the simplicity of monographs compared to the 5 sorts and 6 operator names of E-graphs.