Composition of M,N-adhesive Categories with Application to Attribution of Graphs Electronic Communications of the EASST Volume 73 (2016) Graph Computation Models Selected Revised Papers from GCM 2015 Composition of M ,N -adhesive Categories with Application to Attribution of Graphs Christoph Peuser and Annegret Habel 21 pages Guest Editors: Detlef Plump Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Composition of M ,N -adhesive Categories with Application to Attribution of Graphs Christoph Peuser1∗ and Annegret Habel2 1peuser@informatik.uni-oldenburg.de 2habel@informatik.uni-oldenburg.de Carl von Ossietzky Universität Oldenburg, Germany Abstract: This paper continues the work on M ,N -adhesive categories and shows some important composition properties for these categories. We present a new concept of attributed graphs and show that the corresponding category is M ,N - adhesive. As a consequence, we inherit all nice properties for M ,N -adhesive sys- tems such as the Local Church-Rosser Theorem, the Parallelism Theorem, and the Concurrency Theorem for this type of attributed graphs. Keywords: Graph transformation, attributed graphs, composition, adhesive cate- gories, adhesive systems 1 Introduction The double-pushout approach to graph transformation, which was invented in the early 1970’s, is the best studied framework for graph transformation [Roz97, EEKR99, EKMR99, EEPT06, EEGH15]. As applications of graph transformation come with a large variety of graphs and graph-like structures, the double-pushout approach has been generalized to the abstract settings of high-level replacement systems, adhesive, M -adhesive, M ,N -adhesive, and W -adhesive categories. This paper continues the work of Habel and Plump [HP12] on M ,N -adhesive categories. In the literature, there are several variants of attribution concepts, e.g. typed attributed graphs in the sense of Ehrig et al. [EEPT06], attributed graphs in the sense of Poskitt and Plump [PP12], attributed graphs as a graph with a marked sub-graph in the sense of Kastenberg and Rensink [KR12], separation of the graph structure and their attribution and data in the sense of Golas [Gol12], and attributed structures in the sense of Duval et al. [DEPR14]. The use of attributed graphs allows a more compact representation of a system. While graph transformation systems are Turing complete, representing numerical values as part of the graph can lead to very large representations of parts of a system that may be comparatively unimportant. Instead attributes allow us to concentrate on graphically representing those parts of a system we are primarily interested in. Our main aim is to consider composition of categories to make it easier to define new models for transformation systems. To this end we prove closure results of M ,N -adhesive categories against product, functor, slice and coslice, comma, string and multiset category. We apply our ∗ This work is supported by the German Research Foundation through the Research Training Group (DFG GRK 1765) SCARE (www.scare.uni-oldenburg.de). 1 / 21 Volume 73 (2016) mailto:peuser@informatik.uni-oldenburg.de mailto:habel@informatik.uni-oldenburg.de Composition of M ,N -adhesive Categories results to the construction of a category AttGraphs of attributed graphs from the well-known cat- egory Graphs of unlabelled graphs and a category Att of attribute collections. By closure results for M ,N -adhesive categories, we obtain that the category AttGraphs is M ,N -adhesive. By the results in [HP12], the Local Church-Rosser Theorem, the Parallelism Theorem and the Con- currency Theorem hold for the new type of attributed graphs provided that the HLR+-properties [HP12] are satisfied. The paper is structured as follows. In Section 2, we recall the definition of M ,N -adhesive categories. In Section 3, we prove some basic composition results and show that the string and multiset categories are M ,N -adhesive provided that an underlying category is. In Section 4, we introduce the category AttGraphs of attributed graphs and show that it is M ,N -adhesive. In Section 5 we present some related work and, in Section 6 some concluding remarks. This paper is an extended version of the paper [PH15]. It contains all proofs and additional examples. 2 M ,N -adhesive Categories In this section, we recall the definition of M ,N -adhesive categories, introduced in [HP12], generalizing the one of M -adhesive categories [EGH10]. We assume that the reader is familiar with the basic concepts of category theory; standard references are [EEPT06, Awo10]. Definition 1 (M ,N -adhesive Categories) A category C is M ,N -adhesive, where M is a class of monomorphisms and N a class of morphisms, if the following properties are satisfied: 1. M and N contain all isomorphisms and are closed under composition and decomposition. Moreover, N is closed under M -decomposition, that is, f ; g ∈ N , g ∈ M implies f ∈ N . 2. C has M ,N -pushouts and M -pullbacks. Also, M and N are stable under pushouts and pullbacks. 3. M ,N -pushouts are M ,N -van Kampen squares. In the following we might sometimes use ’M ,N -adhesive’ without specifying M and N explicitly, especially in the sense of ’preserving M ,N -adhesiveness’. Remark 1 C has M ,N -pushouts, if there is a pushout whenever one of the given morphisms is in M and the other morphism is in N . C has M -pullbacks, if there exists a pullback whenever at least one of the given morphisms is in M . A class X ∈{M ,N } is stable under M ,N - pushouts if, given the M ,N -pushout (1) in Figure 1, m ∈ X implies n ∈ X and stable under M -pullbacks if, given the M -pullback (1) in Figure 1, n ∈ X implies m ∈ X . An M ,N - pushout is an M ,N -van Kampen square if for the commutative cube (2) in Figure 1 with the pushout (1) as bottom square, b,c,d,m ∈ M , f ∈ N , and the back faces being pullbacks, we have that the top square is a pushout if and only if the front faces are pullbacks. In [HP12], it is shown that all M -adhesive categories are M ,N -adhesive. Selected Revised Papers from GCM 2015 2 / 21 ECEASST A C B D f g m n (1) A A′ B B′ C C′ D D′ b c d f m n g(2) Figure 1: M ,N -pushout and M ,N -van Kampen square Lemma 1 (M -adhesive ⇒ M ,N -adhesive [HP12]) Let C be any category and N be the class of all morphisms in C. Then C is M ,N -adhesive if and only if C is M -adhesive. In the following, we give some examples of categories that are M ,N -adhesive. Lemma 2 (Basic M ,N -adhesive Categories [EEPT06]) The following categories are M - adhesive and, by Lemma 1, M ,N -adhesive where N is the class of all morphisms in C: The category Sets of sets and functions, where M is the class of all injective functions. The category Graphs of graphs and graph morphisms, where M is the class of all injective graph morphisms. The category LGraphs of labelled graphs and graph morphisms, where M is the class of all injective graph morphisms. The discrete category1 over some set L, referred to as Disc(L), is M -adhesive: Disc(L) only has identity morphisms, for which proving the required properties becomes trivial. The category PLGraphs of partially labelled graphs and graph morphisms is M ,N -adhesive, but not M -adhesive [HP12]: M and N are the classes of all injective and all (injective) undefinedness-preserving2 graph morphisms, respectively. 3 Composition of M ,N -Adhesive Categories There are various ways to construct new categories from given ones. Beside the standard con- structions (product, slice and coslice, functor and comma category as defined in [EEPT06]) we consider the constructions of a string category and a multiset category. For each of these con- structions, we prove a composition result, saying more or less, whenever we start with Mi,Ni- adhesive categories, then the new constructed category is M ,N -adhesive for some M ,N . We briefly recall the definition of the comma category, we refer to [EEPT06] for the definiton of product, slice and coslice and functor category. Definition 2 (Comma Category[EEPT06]) Given two functors F1 : C1 → C and F2 : C2 → C and an index set I , the comma category ComCat(F1,F2,I ) is defined as follows: The objects are all triples (C1,C2,op) with C1 an object in C1, C2 an object in C2, and a family of morphisms 1 The discrete category over some collection S has S as objects and only identity morphisms. 2 A morphism f : G → H preserves undefinedness, if it maps unlabelled items in G to unlabelled items in H. 3 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories op = [opi]i∈I where opi : F1(C1)→F2(C2) is a morphism in C. The morphisms from (C1,C2,op) to (C′1,C ′ 2,op ′) are all pairs (g,h) where g : C1 → C′1 and h : C2 → C ′ 2 are morphisms in C1 and C2 respectively, such that the following diagram commutes for all i ∈ I : F1(C1) F2(C2) F1(C′1) F2(C′2) opi F2(h) F1(g) op′i= The composition of morphisms in ComCat(F1,F2,I ) is defined componentwise, and the iden- tities are pairs of identities in the component categories C1 and C2. First, we consider the standard constructions: product, slice and coslice, functor, and comma category ([EEPT06] A2 and A6). Theorem 1 (Standard Constructions) M ,N -adhesive categories can be constructed as fol- lows: 1. If Ci is Mi,Ni-adhesive (i = 1,2), then the product category C1 ×C2 is M ,N - adhesive where M = M1 ×M2 and N = N1 ×N2. 2. If C is M ,N -adhesive and X is an object of C, then the slice category C\X and the coslice category X\C over X are M ′,N ′-adhesive where the morphism classes M ′,N ′ are restricted to the slice and coslice category, i.e., for X ∈{M ,N }, X ′ = X ∩C\X and X ′ = X ∩X\C, respectively. 3. If C is M ,N -adhesive, then for every category X, the functor category [X,C] is Mft,Nft- adhesive with functor transformations Mft and Nft.3 4. Let Ci be Mi,Ni-adhesive and Fi : Ci → C be functors (i = 1,2), where F1 preserves M1,N1-pushouts and F2 preserves M2-pullbacks. Then the comma category ComCat(F1,F2,I ) is M c,N c-adhesive where M c = (M1×M2)∩Mor, N c = (N1×N2)∩Mor, and Mor is the set of all morphisms of the comma category. Remark 2 Statement 4 in Theorem 1 above also holds for the case of a comma category ComCat(F1,F2,I ), with |I | = 1 and both functors F1,F2 pointing into Sets, where the mor- phism op is always bijective. We will use F1 ↓bij F2 as a shorthand for these categories. Proof. The proof is a slight generalization of the corresponding one for M -adhesive categories (see Theorem 4.15 in [EEPT06]). 1. The product category C1×C2 is M ,N -adhesive, because M and N inherit the required composition and decomposition properties from M1 and M2 and N1 and N2 respectively. Pushouts along (M ,N )-pairs of morphisms can be constructed componentwise. So can 3 For a class X , Xft denotes the class of natural transformations t : F → G, where all morphisms tX : F(X)→ G(X) are in X . Selected Revised Papers from GCM 2015 4 / 21 ECEASST the van Kampen square, since pullbacks can also be constructed componentwise. The stability of M and N is inherited from pushouts and pullbacks in Ci. 2. Morphisms, pullbacks and pushouts can similarly be constructed componentwise for both slice categories C\X and coslice categories X\C. This construction also ensures that M ′ and N ′ are stable under pushout and pullback. 3. The functor category [X,C], where Mft and Nft are functor transformations, is M ,N - adhesive, because the functor transformations Mft (or Nft) are monomorphisms in [X,C] and the required composition and decomposition properties are inherited from M (or N ). Pushouts and pullbacks and the M ,N -van Kampen square are constructed pointwise, i.e. for each object X ∈ [X,C]. The pointwise construction also ensures that Mft and Nft are stable under pushout and pullback. 4. The comma category ComCat(F1,F2,I ) is M c,N c-adhesive, because M c and N c in- herit the required composition and decompostion properties from Mi and Ni. M c,N c- pushouts can be constructed componentwise, since F1 preserves them. M c-pullbacks can be constructed componentwise, since F2 preserves them. Consequently M c,N c-van Kampen squares can equally constructed componentwise. All of these constructions can also be done if we restrict ourselves to objects with a bijective morphism op. The compo- nentwise construction ensures that M c and N c are stable under pushout and pullback. Example 1 ([EEPT06]) The category Graphs of unlabelled graphs is isomorphic to the functor category [ E V ,Sets]. For the type graph T G, the category GraphsT G of graphs typed over T G is isomorphic to the slice category Graphs\T G. Given a category C, we construct a string category C∗ and prove that M ,N -adhesive cate- gories are closed under string construction. Definition 3 (String Category) Given a category C, the string category C∗ is defined as follows: The objects are strings a1 ...am of objects of C, including the empty string λ . The morphisms between two strings a1 ...am and b1 ...bn with m ≤ n are strings of morphisms such that a1 ...am is embedded in b1 ...bn, i.e. f1 : a1 → bi+1,..., fm : am → bi+m in C. The empty string λ is an initial element for C∗. a1 ... am b1 ... bi bi+1 ... bi+m bi+m+1 ... bn f1 fm Remark 3 Our definition for a string category is close to that of a free monoidal category, but is not a free monoidal category because we allow morphisms that do not preserve length. Such morphisms prevent us from defining a monoidal product on arrows. In the absence of these morphisms we cannot formulate rules that add elements to a string or remove them. 5 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories Lemma 3 For every morphism f : A → B, the commuting square consisting of f and the iden- tities idA,idB is a pushout and a pullback. Proof. Follows from standard category theory. Theorem 2 (C M ,N -adhesive ⇒ C∗ M∗,N ∗-adhesive) If C is M ,N -adhesive, then the string category C∗ over C is M∗,N ∗-adhesive where M∗ and N ∗ contain those morphisms which are strings of morphisms in M and N , respectively. N ∗ is further restricted to mor- phisms that preserve length, i.e. where domain and codomain are of equal length. We will use this decomposition frequently in the following proofs. Lemma 4 (Decomposition of String Morphisms) Any string morphism f : a1 ...am → b1 ...bn can be decomposed into f= : a1 ...am →bi+1 ...bi+m that preserves length and f+ : bi+1 ...bi+m → b1 ...bn an embedding that consists of identity morphisms in C such that f = f=; f+. Both mor- phisms are in M∗ or N ∗, if f is in M∗ or N ∗ respectively. Proof. Straightforward. Proof of Theorem 2. By inspection of Definition 1. 1. Closure properties: M∗ and N ∗ contain all isomorphisms, since an isomorphism in C∗ must be a list of isomorphisms in C and M and N , respectively contain all isomorphisms in C. Isomorphisms must further be lists of equal length and M∗ and N ∗ contain all morphisms with domain and codomain of equal length. Composition and decomposition properties can be inherited from C, e.g. the composition of morphisms in M∗ and N ∗ implies the composition of a list of morphisms in M and N , respectively, which is possible since C is M ,N -adhesive. This also applies to the closure of N ∗ under M∗-decomposition, since f ; g ∈ N ∗ implies a domain and codomain of equal length, which in turn implies f ∈ N ∗. 2a. Existence of M∗,N ∗-pushouts and M∗-pullbacks: Given the morphisms f : a1 ...am → b1 ...bn and g : a1 ...am → c1 ...cm, where f ∈ M∗ and g ∈ N ∗ we can construct M∗,N ∗- pushouts as follows (see Figure 4b): We decompose f into f= and f+ as in Lemma 4. We can construct (1) as a pushout componentwise from pushouts in the underlying category C. If we have a string of length zero, the resulting pushout will be the identity square of λ . The mor- phisms f+,i+ in (2) consists entirely of identity morphisms in C, making each component of (2) a pushout in C by Lemma 3. Then (2) is a pushout in C∗. By composition of pushouts (1)+(2) is a pushout. Note that the remaining morphisms in b1 ...bn → d1 ...dn must be isomorphisms for (2) to be a pushout, since the pushout object is only unique up to isomorphism we can assume, without loss of generality, that the remaining morphisms are identities. 2b. C∗ has pullbacks along M∗-morphisms: Given two morphisms f : a1 ...am →c1 ...co ∈ M∗ and g : b1 ...bn → c1 ...co the pullback object is constructed by identifying the largest sub- string ci ...ci+x where all elements c j have a coimage in both a1 ...am and b1 ...bn and construct- ing their pullbacks in C. If there is no such common substring, the empty string λ is the pullback object instead. 3. M∗,N ∗-pushouts are M∗,N ∗-van Kampen squares: Selected Revised Papers from GCM 2015 6 / 21 ECEASST A A′′ A′ B= B′′= B′= B B′′ B′ C C′′ C′ D= D′′= D′= D D′′ D′ i1i2 i3i4 C′ C′′ C D′= D′′= D= D′ D′′ D B′ B′′ B i2 i4 (1) (2) (3) (4) (5) (6) Figure 2: Van Kampen square for the string category (I) The top face is a pushout ⇒ the front faces are pullbacks: 1. We construct the cube in Figure 2 by decomposing the pushout at the top face as seen above into a pushout with morphisms that preserve length and another where the horizontal morphisms do not preserve length and decomposing all vertical morphisms in the commutative cube into pairs according to Lemma 4. 2.The morphisms in the middle layer of the cube are determined by those in the bottom layer, since the vertical morphisms in the lower half of the cube consist of identity morphisms only. As a result the middle layer consists of pushouts as well. 3. The core cube in the upper back is a van Kampen square, with the pushout of A′′ →C′′ and A′′ → B′′= as bottom face. This core cube can be constructed componentwise from cubes in C, since all morphisms preserve length. If these strings are of length 0 this is an identity cube of empty strings λ . 4. Since the top face of the core cube is a pushout, (1) consists of pullbacks in C by the van Kampen property and is therefore a pullback in C∗. 5. (2) and (3) are pullbacks, since their vertical and horizontal morphisms respectively consist of identity morphisms only and and the morphism shared with (1) preserve length. The pullback objects are then limited to the length of D′′= and we can construct the pullbacks componentwise from pullbacks in C according to Lemma 3. 6. The commuting square (4) consists entirely of morphisms composed of identity morphisms in C. Then D′′= is the largest string for which each element has a pullback in C and therefore (4) is a pullback. 7. We examine the commutative square (5) componentwise: Some of its components have a coimage in the front right square of the core cube via the morphisms i1 ...i4. Since these morphisms consists of identity morphisms in C, these components are pullbacks. The remaining components of (5) have horizontal morphisms that coincide with those morphisms that are part of the top and bottom pushout that are identities, making these components pullbacks as well. Thus, (5) is a pullback. 8. (6) is a pullback, by Lemma 3 since B′′ → B, D′′ → D consist of identity morphisms in C. 7 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories A A′′ A′ B= B′′= B′= B B′′ B′ C C′′ C′ D= D′′= D′= D D′′ D′ i1i2 i3i4 A′ B′= B′ C′ D′= D′ i1i2 (1) (2) Figure 3: Van Kampen square for the string category (II) 9. By composition of pullbacks (1)+(2)+(3)+(4) and (5)+(6) are pullbacks. The front faces are pullbacks ⇒ the top face is a pushout: 1. We decompose the vertical morphisms and the bottom pushout as in the cube in Figure 3. Additionally we construct the pushouts in the middle layer analogously. 2. The commutative cube in the upper back is a van Kampen square. We construct this cube componentwise from cubes in C, since all morphisms preserve length. 3. Since the upper square at the right front face is a pullback and i1,i2,i3,i4 consist of idenities, B′=,B ′′ =,D ′ =,D ′′ = is a pullback. 4. Then (1) is a pushout by the van Kampen property of C, i.e. all component cubes have front faces as pullbacks, therefore all components of the top face are pushouts. 5. (2) is a pushout by Lemma 3, since i1,i2 consists of identities. 6. By composition of pushouts, (1)+(2) is a pushout. This concludes the proof. Example 2 The category Strings = Disc(L)∗ of strings, where Disc(L) is the discrete category over some alphabet L, is M∗,N ∗-adhesive. Given a category C, we construct a multiset category C⊕ and prove that M ,N -adhesive categories are closed under multiset construction. In contrast to the above construction for a string category, we can construct a multiset category by ignoring the order of elements. We use {|...|} to denote a multiset, e.g {|a,a,b|} denotes the multiset with elements a,a and b. Definition 4 (Multiset Category) Given a category C, the multiset category C⊕ is defined as follows: The objects are multisets {|A1 ...Am|} of objects of C, including the empty multiset /0. The morphisms between two objects {|A1 ...Am|} and {|B1 ...Bn|} (with m ≤ n) are strings of morphisms fi : Ai → B ji in C, where ji = jk implies i = k, i ∈{1,...,m}. Remark 4 A category of multisets MUL has previously been discussed for example in [SI13]. In contrast to those definitions we define a multiset category C⊕ over a different category C. Selected Revised Papers from GCM 2015 8 / 21 ECEASST A C′ C B′ B D E F G f g (1) (2) (2′) (3) (a) A pushout in C⊕ a1...am c1...cm bi+1...bi+m b1...bn di+1...di+m d1...dn g f= f+ i+ f (1) (2) (b) A pushout in C∗ Figure 4: Pushouts in String and Multiset Categories Theorem 3 (C M ,N -adhesive ⇒ C⊕ M⊕,N ⊕-adhesive) If C is M ,N -adhesive, then the multiset category C⊕ over C is M⊕,N ⊕- adhesive where M⊕ and N ⊕ contain those morphisms which are strings of morphisms in M and N , respectively. Lemma 4 applies to morphisms in M⊕ or N ⊕. Proof. By inspection of Definition 1. 1. Closure properties: M⊕ and N ⊕ contain all isomorphisms, since an isomorphism in C∗ must be a list of isomorphisms in C and M and N , respectively contain all isomorphisms in C. Composition and decomposition properties can be inherited from C, e.g. the composition of morphisms in M⊕ and N ⊕ implies the composition of a list of morphisms in M and N , respectively, which is possible since C is M ,N -adhesive. 2a. Existence of M⊕,N ⊕-pushouts and M⊕-pullbacks: Given the morphisms f : A → B and g : A → C, where f ∈ M⊕ and g ∈ N ⊕ and #A = l,#B = m,#C = n 4, we can construct M⊕,N ⊕-pushouts as follows (see Figure 4a): We decompose f : A → B as in Lemma 4, where f= preserves cardinality and f+ consists of identities in C. We decompose g analogously. We can construct (1) as a pushout componentwise from pushouts in the underlying category C. If #A = 0 then A,B,C,D are the empty multiset /0. (2) (and analogously (2’)) is a pushout by Lemma 3. (3) consists entirely of identity morphisms in C and is therefore a pushout as well. By composition of pushouts (1)+(2)+(2′)+(3) is a pushout. 2b. C⊕ has pullbacks along M⊕-morphisms: Given two morphisms f : A1 ...Am →C1 ...Co ∈ M⊕ and g : B1 ...Bn → C1 ...Co the pullback object is constructed by identifying the largest subset Ci ...Ci+x where all elements C j have a coimage in both A1 ...Am and B1 ...Bn and con- structing their pullbacks in C. If there is no such common subset, the empty multiset /0 is the pullback object instead. 3. M⊕,N ⊕-pushouts are M⊕,N ⊕-van Kampen squares: The top face is a pushout ⇒ the front faces are pullbacks: 1. We decompose the top and bottom pushout as in Figure 5. 4 # denotes the cardinality of a multiset, i.e. for a multiset f : A →N, #A = ∑a∈A f (a). 9 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories A A′′ A′ B= B′′= B′= B B′′ B′ C= C′′= C′= E E′′ E′ F F′′ F′ C C′′ C′ G G′′ G′ D D′′ D′ Figure 5: Van Kampen square for the multiset category 2. We decompose all vertical morphisms in the cube into pairs where the first morphism preserves cardinality and the second morphism is an inclusion consisting of identity morphisms in C (see Lemma 4). 3. We construct the interior morphisms shown in the cube above analogoulsy to the construc- tion in the proof for the string category, once along A → B and once along A →C. 4. The remaining pullbacks on the front sides can also be constructed analogously to the construction in the previous proof, using Lemma 3. The front faces are pullbacks ⇒ the top face is a pushout: 1. We decompose the bottom pushout as in the cube in Figure 5. 2. We decompose all vertical morphisms in the cube into pairs where the first morphism preserves cardinality and the second morphism is an inclusion consisting of identity morphisms in C (see Lemma 4). 3. We construct the interior morphisms shown in the cube above analogoulsy to the construc- tion in the proof for the string category, once along A → B and once along A →C. 4. The remaining pushouts on the top side can also be constructed analogously to the con- struction in the previous proof, using Lemma 3. This concludes the proof. Example 3 The categories MultiSets = Disc(L)⊕ of multisets is M⊕,N ⊕-adhesive for suit- able M ,N . Finally, we will look at the possibilities that these compositions give us. Example 4 (Library System) Assume we have a library system modeled as a transformation system over labelled graphs, with books, authors, readers and a catalog as in [EK80]. We would like to extend this system with queues, such that a reader can reserve a book if it is currently unavailable. One straightforward way to implement this would be extending the rules to include the creation and management of such queues as additional nodes and edges in the graph. This Selected Revised Papers from GCM 2015 10 / 21 ECEASST may, however lead to a large part of the graph structure consisting of these queues, when they are in fact a minor element of the overall model. We sketch a rule in this setting below, adding a reader to the end of a queue that is associated with a catalog number. Reserve(catnr, readernr): catalog catnr readernr tail elem − ⇒ catalog catnr readernr tail elem elem − We could instead introduce queues as distinct components of the underlying model, using the compositions detailed in this chapter: We define the category PLGraphs×Disc(R×C)∗, where R is a fixed set of reader numbers and C a set of catalog numbers and Disc(A) is the discrete category over some set A. An object of this category is a labelled graph together with a string of pairs of readers and catalog numbers. Instead of adding additional nodes like in the rule above, we append a pair of catalog number and reader number to the queue 〈q〉. Note that we would a notion of abstract rules here that allow us to refer to a queue of arbitrary length, such as e.g. the rule schemata in GP [PP12]. Reserve(catnr, readernr): catalog catnr readernr 〈q〉 − ⇒ catalog catnr readernr 〈q,(catnr,readernr)〉 − If we want to separate queues for every title in the library we could instead have used a comma category: We define the category PLGraphs ↓bij Q, where Q : (Disc(R)∗)⊕→ Sets is some func- tor that preserves pullbacks and PLGraphs is analogous to Graphs, mapping a graph to a union of its nodes and edges. The definition contains a multiset ((Disc(R)∗)⊕), since we may need more than one instance of a certain queue as transformations might otherwise have unwanted side effects. Now the rule can instead add the reader number directly to the queue associated with the catalog number. Again, some notion of abstract rules would be required. Reserve(catnr, readernr): catalog catnr 〈q〉 readernr − ⇒ catalog catnr 〈q,readernr〉 readernr − In all of the above cases, the resulting category is M ,N -adhesive, since PLGraphs and dis- crete categories are M ,N -adhesive and the constructions we used preserve M ,N -adhesiveness. 4 Attributed Graphs In this section we define attributed graphs, where attribute values can be changed analogously to relabelling. The addition or removal of attributes to a node or edge should also be possible. 11 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories Defining a category of attribute collections which collect all the attributes of a node or an edge is our first step. These attribute collections consist of a set of names, each of which is associated with a value. Attributed graphs are defined, where each node or edge is associated with such an attribute collection. We start by defining a category PL for representing the values. Since we can view labels as isolated attribute values, we will consider the simpler case of labels in the following definition. Let L be a label set including the symbol ⊥ indicating undefinedness. As morphisms we use all identities as well as all morphisms from ⊥ to a label in L. Lemma 5 (PL is a Category) For each alphabet L, the class of all elements in L∪{⊥}5 as objects and all morphisms of the form ⊥→ x and x → x (x ∈ L∪{⊥}) forms the category PL where the composition of x → y and y → z is x → z and the identity on x is x → x. a b . . . z ⊥ Proof. Follows directly from the definiton. It can be shown that the category PL is M ,N -adhesive. Lemma 6 (PL is M ,N -adhesive) The category PL is M ,N -adhesive where M and N are the classes of all morphisms and all identities, respectively. Proof. By inspection of Definition 1: 1. Closure properties: M and N contain all identity morphisms, which are the only isomor- phisms in PL. They are also closed under composition and decompostion. Since f ; g ∈ N ⇒ f ,g ∈ N , N is closed under M -decomposition. 2. PL has M ,N -pushouts: Since N contains only identity morphisms, there are only two cases, with either ⊥→ l or another identity morphism as the horizontal morphism: l l l l m f g n (3) ⊥ l ⊥ l m f g n (4) The diagrams (3) and (4) are pushouts: the morphisms g,n are the only possible morphisms to obtain commutativity and the universal property holds. Since PL contains the initial element ⊥, PL has all M -pullbacks. M is trivially stable under pushouts and pullbacks, since M contains all morphisms. N is stable under pushouts and pullbacks because in the two cases above, the only possible morphisms f ,g are identity morphisms and therefore in N . 3. In PL, M ,N -pushouts are M ,N -van Kampen squares: Let (1) be a pushout, where m ∈ M and f ∈ N . We have to show that, given a commutative cube (2) with (1) as bottom 5 We assume that ⊥ is not an element of L. Selected Revised Papers from GCM 2015 12 / 21 ECEASST l l l l l l l l (a) ⊥ ⊥ l l ⊥ ⊥ l l (b) l ⊥ l ⊥ l ⊥ l ⊥ (c) ⊥ ⊥ l ⊥ ⊥ ⊥ l ⊥ (d) Figure 6: Possible commutative cubes in PL face, b,c,d ∈ M and pullbacks as back faces, the following holds: the top face is a pushout ⇔ the front faces are pullbacks We have already identified the possible pushouts (3) and (4) above. These pushouts lead to four possible cases for back faces that are pullbacks (see Figure 6): For the pushout (3): The possible spans to construct the back faces of the cube with are: • l ← l → l, which lead to the identity cube (a). Then all faces in the cube are pushouts as well as pullbacks and, therefore, constitute an M ,N -van Kampen square. • ⊥←⊥→⊥, which leads to the cube (c) with pullbacks as back faces. Then the top face is the pushout (3) and the front faces are pullbacks. • l ←⊥→ l, ⊥←⊥→ l, for both of which at least one of the back faces will not be a pullback For the pushout (4): The possible spans to construct the back faces of the cube with are: • ⊥←⊥→ l, which leads to the cube (b) with pullbacks as back faces. Then the top face is the pushout (4) and the front faces are pullbacks. • ⊥←⊥→⊥, which leads to the cube (d) with pullbacks as back faces. Then the top face is the pushout (3) and the front faces are pullbacks. In both cases it is possible to contruct different commutative cubes, but all of these do not have pushouts as top faces nor pullbacks as front faces. Definition 5 (Graphs : Graphs → Sets) The functor Graphs : Graphs → Sets is defined to map graphs to their underlying set of nodes and edges and is given as follows: For a graph G′ = (V ′,E′,s′,t′), let Graphs(G′) = V ′ + E′ and for a graph morphism fG′ : A → B, let Graphs( fG′) be a functor, defined by Graphs( f )(x) = fV ′(x) if x ∈V ′ and fE′(x) otherwise. Lemma 7 The functor Graphs : Graphs → Sets preserves M ,N -pushouts, where M is the class of injective graph morphisms, N is the class of all morphisms. Proof. Given a pushout (P) in Graphs, we have to show that Graphs((P)) is a pushout in Sets, i.e. for every pair of commuting morphisms g1 : Graphs(B)→ X and g2 : Graphs(C)→ X there is a unique morphism g : Graphs(D)→ X . 13 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories A C B D f1 f2 π1 π2 (P) Graphs(A) Graphs(C) Graphs(B) Graphs(D) X Graphs( f1) Graphs( f2) Graphs(π1) Graphs(π2) g1 g2 g Graphs((P)) Let x∈D, then either x∈B or x∈C. If x∈B, then g1(x)∈X , if otherwise x∈C then g2(x)∈X . We can thus define g(x) = { g1(x) if x ∈ B g2(x) otherwise It remains to show that g is unique: The above construction follows directly from g1,g2 and Graphs(π1),Graphs(π2). If we assume a different morphism g′ : Graphs(D)→ X it would have to follow these same constraints, hence g′ = g. Definition 6 (PL : PL⊕ → Sets) The functor PL : PL⊕ → Sets is defined to map a multiset of labels to a set with distinct elements and is given as follows: For a multiset of labels m′ : L′ →N let PL(m) = ⋃ l′∈L′ m̄(l ′), where for l′ ∈ L′, m̄(l′) = {l′1,...,l ′ k} iff m(l ′) = k. For a morphism f : m1 → m2 let PL( f ) = PL(m1)→ PL(m2) be a morphism in Sets, such that PL( f )(l′1) = l ′ 2 iff PL(l1) = l′1,PL(l2) = l ′ 2 and f (l1) = l2 with l1,l2 ∈ m1,m2 respectively. Example 5 Given a morphism f : {|a,a,b|}→{|a,a,b,b|} in Disc(L)⊕, PL( f ) is the morphism {a1,a2,b1}→{a1,a2,b1,b2}. PL ’flattens’ a multiset into a set by making sure that there are distinct elements in the set for all elements in a multiset. Lemma 8 The functor PL : PL⊕ → Sets preserves pullbacks. Proof. Given a pullback (P) in PL⊕, we have to show that PL((P)) is a pullback in Sets, i.e. for every pair of commuting morphisms g1 : X → PL(B) and g2 : X → PL(C) there is a unique morphism g : X → PL(A). A C B D π1 π2 f1 f2 (P) PL(A) PL(C) PL(B) PL(D) X PL(π1) PL(π2) PL( f1) PL( f2) g1 g2 g PL((P)) Let x ∈ A, then both x ∈ B and x ∈C due to the morphisms π1,π2. We can thus define g(x′) = x if g1(x′) = PL(π1(x)) with x′ ∈ X . Selected Revised Papers from GCM 2015 14 / 21 ECEASST It remains to show that g is unique: The above construction follows directly from g1,g2 and PL(π1),PL(π2). If we assume a different morphism g′ : X →PL(A) it would have to follow these same constraints, hence g′ = g. Definition 7 (Att = idSets ↓bij PL) The category Att of attribute collections is the comma cat- egory idSets ↓bij PL where idSets denotes the identity functor over Sets. Lemma 9 (Att is M c,N c-adhesive) The category Att of attribute collections is M c,N c- adhesive where M c,N c are the classes of morphisms induced by the comma category con- struction. Proof. Att = idSets ↓bij PL is M c,N c-adhesive, since Sets and PL are M ,N -adhesive and a multiset and comma category construction preserve M ,N -adhesiveness. To construct attributed graphs we define a functor from multisets of these attribute collections to sets for later use in the definition of a comma category. We also prove that this functor pre- serves pullbacks, since this is required for the comma category to preserve M ,N -adhesiveness. Definition 8 (Att : Att⊕→ Sets) The functor Att : Att⊕→ Sets is defined to map attribute col- lections to sets with distinct values and is given by the following: A triple (idSets(S),PL(m),op)⊕ is mapped to the set S⊕+PL(m)⊕ where ⊕ is flattened analogously to the way PL does (see Def- inition 6). A morphism f : A → B in Att⊕ is mapped to a morphism Att( f ): Att(A) → Att(B), where elements in Att(A) are mapped to elements in Att(B) based on the original mappings in Att⊕. Lemma 10 (Att preserves pullbacks) The functor Att : Att⊕ → Sets preserves pullbacks. Proof. In the same way that the defintion of Att is analogous to that of PL the preservation of pullbacks can be proven in a similar way. Definition 9 (AttGraphs = Graphs ↓bij Att) The category AttGraphs of attributed graphs is the comma category Graphs ↓bij Att. Now we are able to show that the category AttGraphs of attributed graphs is M ,N -adhesive. The categories Graphs of graphs and Att of attribute collections are MG,NG and MA,NA- adhesive and the compositions of multiset category and comma category preserve M ,N -adhesiveness. Theorem 4 (AttGraphs is M c,N c-adhesive) The category AttGraphs of attributed graphs is M c,N c-adhesive where M c,N c are the classes of morphisms induced by the comma category construction. Proof. The proof is illustrated in Figure 7. By Lemmata 2 and 9, Graphs and Att are MG,NG and MA,NA-adhesive, respectively. MG,NG are monomorphisms in Graphs and MA,NA are the classes of morphisms induced by the comma category construction of Att. By Theorem 3, Att⊕ is M⊕,N ⊕-adhesive. By Theorem 1 and Lemmata 7 and 10, Graphs ↓bij Att is M c,N c- adhesive. By Definition 9, AttGraphs is M c,N c-adhesive. 15 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories Graphs Lem 2 Att Lem 9 Att⊕ Graphs ↓bij Att AttGraphs Thm 3 Thm 1 = Def 9 Figure 7: Proof of “AttGraphs is M c,N c-adhesive”. Example 6 Figure 8 shows an attributed graph in our setting. The functor Graphs maps the unlabelled graph U given below to a set {v1,v2,e1} of nodes and edges. The functor Att maps the multiset {|a = 4,b = 5,a = 4|} to the set {a1,b1,a2}: whenever an element x occurs n times in the multiset, the symbols x1,...,xn occur in the corresponding set. In our case, there is a bijective morphism op : Sets → Sets. Now we get an attributed graph G = (U,lG) from the unlabelled graph U and the multiset {|a = 4,b = 5,a = 5|} by defining attG(x) = Att−1(op(Graphs(x))) for each item x in U . The resulting attributed graph is given in the picture below. To represent an attributed graph we write its attribute collections into their corresponding nodes or next to their corresponding edges. v1 v2 e1 {v1,v2,e1} {a1,b1,a2} {|a = 4,b = 5,a = 4|} Graphs Sets Sets Att⊕ a = 4 v1 b = 5 v2 a = 4 e1 AttGraphs attG(x) = Att −1(op(Graphs(x))) Graphs Attop bijective Figure 8: Example of an object of AttGraphs Figure 9 shows a rule containing the same graph. Note that, unlike the labelling function in partially labelled graphs, op does not change, instead the attribute collections themselves are transformed. For this reason we may need multiple instances of these attribute collections, hence the use of a multiset. The elements of the multiset Att⊕ are in turn transformed in a way analogous to these attributed graphs. Selected Revised Papers from GCM 2015 16 / 21 ECEASST AttGraphs Graphs Sets Sets Att⊕ a = 4 v1 b = 5 v2 a = 4 e1 a = 4 v1 b =⊥ v2 a =⊥ e1 a = 4 v1 b = 6 v2 a = 3 e1 v1 v2 e1 {v1,v2,e1} {a1,b1,a2} {|a=4,b=⊥,a=⊥|} {a1,b1,a2} {|a=4,b=6,a=3|} {a1,b1,a2} {|a=4,b=5,a=4|} opL PLL Graphs opK PLK opR PLR Figure 9: Example rule over AttGraphs a = 4 v1 b =⊥ v2 a =⊥ e1 a = 4, c = 7 v1 b = 6 v2 a = 3 e1 Figure 10: Matches need not specify all attributes AttGraphs versus PLGraphs We based our approach on partially labelled graphs and we have to consider whether we have actually gained anything with this new category. We could, for example, define partially labelled graphs over an alphabet of sequences of 〈name,value〉- pairs which would also allow us to model graphs with attributes (this is close to the approach to attribution in [PP12]). In contrast to labels in PLGraphs, the attribute collections in AttGraphs have an internal structure. This allows us to write rules which specify only those attributes that we want to change, such as in Figure 10. Unlike in a sequence of attributes, named attributes can be deleted without implicitly changing the meaning of other, following attributes. On Attributed Graph Transformation So far we have only considered rules that use concrete attribute values. In practice we would want to have more abstract rules with variables, such that a rule may e.g. compute the sum of two attributes and write the result to a third attribute. To allow computations in our rules we could adopt rule schemata as in e.g. [PP12]. A rule schema may contain variables or terms in place of attribute values. These variables are instantiated during matching and the terms evaluated, resulting in a concrete rule that we can handle with our approach. Alternatively we would have to prove that relevant algebra form an M ,N -adhesive category to be able to handle computations directly, such as in [Gol12] or [DEPR14]. 5 Related Concepts Throughout the literature, various versions of adhesive and quasiadhesive, weak adhesive HLR, partial map adhesive, and M -adhesive categories exist. In [EGH10], all these categories are 17 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories shown to be also M -adhesive ones. The categories of labelled graphs, typed graphs, and typed attributed graphs in [EEPT06], are known to be M -adhesive categories if one chooses M to be the class of injective graph morphisms [EGH10]. Each such category induces a class of M - adhesive systems for which several classical results of the double-pushout approach hold. Unfortunately, the framework of M -adhesive systems does not cover graph transformation with relabelling. In [HP12], the authors generalize M -adhesive categories to M ,N -adhesive categories, where N is a class of morphisms containing the vertical morphisms in double- pushouts, and show that the category of partially labelled graphs is M ,N -adhesive, where M and N are the classes of injective and injective, undefinedness-preserving graph morphisms, respectively. Independently, Golas [Gol12] provided a general framework for attributed objects, so-called W -adhesive systems which allows undefined attributes in the interface of a rule to change attributes, which is similar to relabelling. By Lemma 1 and Theorem 5 in [PH15], the hierarchy of adhesive categories in [EGH10] is extended in the following way: adhesive adhesive HLR M -adhesive M ,N -adhesive W -adhesive ⇒ 6⇐ ⇒ 6⇐ ⇒ 6⇐ ⇒ 6⇐ Composition of adhesive categories has previously been considered for M -adhesive cate- gories: the standard constructions of product, slice and coslice, functor, and comma categories are given in [EEPT06]. Parisi-Presicce et al. [PEM87] impose a simple structure on the sets of labels to allow variables both graphs and rules. As special case, they consider a preordering on the sets of labels to allow partially labelled graphs, i.e., partial labelling functions, and to allow the label-preserving matching morphisms. It is easy to see that this situation is a special case of [PEM87], 3.2 and 3.4 obtained by imposing a flat ordering on the labelling alphabet with a new “label” as top element. As far as we see, this is the first time where a special class of matching morphisms is considered. In the literature, there are several variants of attribution concepts, e.g.: Ehrig et al. Ehrig et al. [EEPT06] introduce typed attributed graphs, expanding the graph by including an algebra for attribute values. To facilitate attribution, typed attributed graphs extend graphs by attribution nodes and attribution edges. All possible data values of the algebra are assumed to be part of the graph. Nodes and edges are attributed by adding an attribution edge that leads to an attribution node. In contrast to typed attributed graphs our attributed graphs can have at most one value for an attribute. We constructed untyped graphs and even the attributes themselves have no types. Typed attributed graphs require that the graph is typed and thus do not allow e.g. the addition of attributes to a node or edge. Poskitt and Plump. Poskitt and Plump [PP12] use a different approach to attribution. Here la- bels are replaced by sequences of attributes. Rules are complemented by rule schemata in which terms over the attributes are specified. These variables are substituted with attribute values and evaluated during rule application. Adding or removing attributes is possible, since the graphs are not typed. It is, however, not possible to find a match without fully specifying other, potentially uninteresting, attributes. Golas. Attributed structures, as presented by Golas [Gol12], are likely the closest to our ap- proach. Attributed structures can be defined over arbitrary M -adhesive categories but are strictly limited to attribution. Only some of the results established for M ,N -adhesive transformation Selected Revised Papers from GCM 2015 18 / 21 ECEASST Source Typing Add/Remove Attributes Computation Results [EEPT06] mandatory - via algebra M LCR, Par, Con, Amalg [PP12] none yes via rule schemata M ,N LCR, Par, Con [Gol12] mandatory - via algebra W LCR [DEPR14] none yes via algebra sesqui-PO LCR this paper optional yes not considered M ,N LCR, Par, Con Table 1: Comparison of Attribution Concepts systems have been proven for these attributed structures. Since attributes are added to elements of the underlying structure based on a type, addition or removal of attributes is not possible. Duval et al. Duval et al. [DEPR14] base their approach on sesqui-pushout rewriting to allow for cloning and merging of nodes. The addition or removal of attributes is also possible. In most of these approaches attributes are based on an algebra that allows performing some computations on the attributes, in our setting this would require additional work to prove M ,N - adhesiveness for a suitable category. Fortunately we only need to provide this proof for such attributes once, enabling us to construct many different attributed structures without concerning ourselves with e.g. the underlying graphs. Alternatively we could follow the approach of [PP12] and introduce rule schemata to allow for computations over attributes. The comparison is summarized in Table 1, based on the necessity of typing the graph, the ability to add or remove attributes via rules, whether computations over attribute values are supported and what properties have been shown for these approaches, where LCR is the Local- Church-Rosser Theorem, Par is the Parallelism Theorem, Con is the Concurrency Theorem and Amalg is the Amalgamation Theorem. Further approaches are e.g. Löwe et al. [LKW93] which views graphs as a special case of algebras. These algebras can then additionally specify types for attributes. Kastenberg and Rensink. [KR12] take a similar approach to [EEPT06], but instead of only encoding the data values, operations and constants are also included in the graph. 6 Conclusion In this paper, we have continued the work on M ,N -adhesive categories and have presented several examples (see Table 2). The main contributions of the paper are the following: (1) Closure results for M ,N -adhesive categories: product, slice/coslice, functor, comma, string, and multiset categories. (2) A new concept of attributed graphs with a proof of M ,N -adhesiveness. (3) An application to transformation systems saying that for these attributed graphs the Local Church-Rosser Theorem, the Parallelism Theorem and the Concurrency Theorem hold provided that the HLR+-properties [HP12] are satisfied. 19 / 21 Volume 73 (2016) Composition of M ,N -adhesive Categories Category Structures Adhesiveness Reference Sets sets M -adhesive [EEPT06] PL sets of labels M ,N -adhesive Lemma 6 Att attribute collections M ,N -adhesive Lemma 9 Graphs unlabelled graphs M -adhesive [EEPT06] LGraphs labelled graphs M -adhesive [Ehr79] PLGraphs partially labelled graphs M ,N -adhesive [HP12, PH15] AttGraphs attributed graphs M ,N -adhesive Theorem 4 Table 2: Examples of M ,N -adhesive categories Further topics might be: (1) Proof of the HLR+-properties for the category AttGraphs to obtain the Local Church- Rosser Theorem, the Parallelism Theorem and the Concurrency Theorem for this type of attributed graphs. (2) Generalization of the approach to systems with so-called left-linear rules, i.e., rules where only the left morphism of the rule is required to be in M as, e.g., in [BGS11]. Acknowledgements. We would like to thank the anonymous referees as well as Wolfram Kahl and Berthold Hoffmann for helpful feedback on earlier versions of this paper. Bibliography [Awo10] S. Awodey. Category Theory. Oxford University Press, 2010. [BGS11] P. Baldan, F. Gadducci, P. Sobociński. Adhesivity Is Not Enough: Local Church- Rosser Revisited. In Mathematical Foundations of Computer Science (MFCS 2011). Lecture Notes in Computer Science 6907, pp. 48–59. 2011. [DEPR14] D. Duval, R. Echahed, F. Prost, L. Ribeiro. Transformation of Attributed Structures with Cloning. In Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science 8411, pp. 310–324. 2014. [EEGH15] H. Ehrig, C. Ermel, U. Golas, F. Hermann. Graph and Model Transformation - General Framework and Applications. Monographs in Theoretical Computer Science. Springer, 2015. [EEKR99] H. Ehrig, G. Engels, H.-J. Kreowski, G. Rozenberg (eds.). Handbook of Graph Grammars and Computing by Graph Transformation. Volume 2: Applications, Lan- guages and Tools. World Scientific, 1999. [EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Trans- formation. EATCS Monographs of Theoretical Computer Science. Springer, 2006. Selected Revised Papers from GCM 2015 20 / 21 ECEASST [EGH10] H. Ehrig, U. Golas, F. Hermann. Categorical Frameworks for Graph Transformation and HLR Systems based on the DPO Approach. Bulletin of the EATCS 112:111–121, 2010. [Ehr79] H. Ehrig. Introduction to the Algebraic Theory of Graph Grammars. In Graph- Grammars and Their Application to Computer Science and Biology. Lecture Notes in Computer Science 73, pp. 1–69. 1979. [EK80] H. Ehrig, H.-J. Kreowski. Applications of Graph Grammar Theory to Consistency, Synchronization and Scheduling in Data Base Systems. Information Systems 5:225– 238, 1980. [EKMR99] H. Ehrig, H.-J. Kreowski, U. Montanari, G. Rozenberg (eds.). Handbook of Graph Grammars and Computing by Graph Transformation. Volume 3: Concurrency, Paral- lelism, and Distribution. World Scientific, 1999. [Gol12] U. Golas. A General Attribution Concept for Models in M -adhesive Transforma- tion Systems. In Graph Transformations (ICGT’12). Lecture Notes in Computer Sci- ence 7562, pp. 187–202. 2012. [HP12] A. Habel, D. Plump. M ,N -adhesive Transformation Systems. In Graph Transfor- mations (ICGT 2012). Lecture Notes in Computer Science 7562, pp. 218–233. 2012. Long version available at: http://formale-sprachen.informatik.uni-oldenburg.de/pub/ index.html. [KR12] H. Kastenberg, A. Rensink. Graph Attribution Through Sub-Graphs. Technical re- port TR-CTIT-12-27, University of Twente, 2012. [LKW93] M. Löwe, M. Korff, A. Wagner. An Algebraic Framework for the Transformation of Attributed Graphs. In Term Graph Rewriting: Theory and Practice. Pp. 185–199. John Wiley, 1993. [PEM87] F. Parisi-Presicce, H. Ehrig, U. Montanari. Graph Rewriting with Unification and Composition. In Graph Grammars and Their Application to Computer Science. Lec- ture Notes in Computer Science 291, pp. 496–514. 1987. [PH15] C. Peuser, A. Habel. Attribution of Graphs by Composition of M ,N -adhesive Cat- egories. In Proceedings of the 6th International Workshop on Graph Computation (GCM 2015). CEUR Workshop Proceedings 1403, pp. 66–81. 2015. [PP12] C. M. Poskitt, D. Plump. Hoare-Style Verification of Graph Programs. Fundamenta Informaticae 118(1-2):135–175, 2012. [Roz97] G. Rozenberg (ed.). Handbook of Graph Grammars and Computing by Graph Trans- formation. Volume 1: Foundations. World Scientific, 1997. [SI13] D. Singh, A. I. Isah. A Note on Category of Multisets (MUL). International Journal of Algebra 7(2):73–78, 2013. 21 / 21 Volume 73 (2016) http://formale-sprachen.informatik.uni-oldenburg.de/pub/index.html http://formale-sprachen.informatik.uni-oldenburg.de/pub/index.html Introduction M,N-adhesive Categories Composition of M,N-Adhesive Categories Attributed Graphs Related Concepts Conclusion