On Single-Pushout Rewriting of Partial Algebras Electronic Communications of the EASST Volume 73 (2016) Graph Computation Models Selected Revised Papers from GCM 2015 On Single-Pushout Rewriting of Partial Algebras Michael Löwe and Marius Tempelmeier 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 On Single-Pushout Rewriting of Partial Algebras Michael Löwe1 and Marius Tempelmeier2 1 michael.loewe@fhdw.de Fachhochschule für die Wirtschaft Hannover, Germany 2 marius@tempelmeier.de Sennheiser electronic GmbH & Co. KG Abstract: We introduce Single-Pushout Rewriting for arbitrary partial algebras. Thus, we give up the usual restriction to graph structures, which are algebraic cat- egories with unary operators only. By this generalisation, we obtain an integrated and straightforward treatment of graphical structures (objects) and attributes (data). We lose co-completeness of the underlying category. Therefore, a rule is no longer applicable at any match. We characterise the new application condition and make constructive use of it in some practical examples. Keywords: Graph Transformation, Single Pushout Rewriting, Partial Algebras 1 Introduction The current frameworks for the (algebraic) transformation of typed graphs are not completely satisfactory from the software engineering perspective. For example, it is hardly possible to spe- cify and handle associations with “at-most-one”-multiplicity, since most frameworks are based on some (adhesive) categories of graphs which allow multiple edges between the same pair of vertices.1 Another example is the handling of attributes. The standard approaches to the transforma- tion of attributed graphs, compare for example [4, 14], explicitly distinguish two parts, i. e. the structure part (objects and links) which can be changed by transformations and the base-type and -operation part (data) which is immutable. Typically, objects can be attributed with data via some special edges the source of which is in the structure part and the target of which is data. This set-up either leads to set-valued or immutable attribute structures. Both is not satisfactory from the software engineering point of view.2 Another problem in current frameworks for attributed graphs is the infiniteness of rules stip- ulated by the infiniteness of the term algebra which is typically used in the rules. Even if the algebra for the objects which are subject to transformation is finite (for example integers modulo some maximum), the term algebra tends to contain infinitely many terms. All these problems are more or less caused by the usage of total algebras. In this paper, we use partial algebras instead as the underlying category for single-pushout rewriting. In partial al- gebras, operation definitions can be changed without deleting and adding an object (edge). Thus, 1 Typically, some negative application conditions [8] are employed to handle these requirements making the frame- work more complicated. 2 In object-oriented programming languages, for example, attributes have the standard multiplicity 0..1. 1 / 21 Volume 73 (2016) mailto:michael.loewe@fhdw.de mailto:marius@tempelmeier.de On Single-Pushout Rewriting of Partial Algebras we get a straightforward model for “at-most-one” associations. We also give up the distinction between structure and data, i. e. we allow arbitrary signatures which are able to integrate both parts. We lose co-completeness of the base category and import some application conditions into single-pushout rewriting. But we gain a seamless integration of structure and data. Finally, partial term algebras in the rules help to keep rules finite. The paper is a short version of [17] and an extended version of [15]. Section 2 introduces our concept of partial algebra. We show explicitly the similarities between partial algebras and hy- pergraphs. Section 3 provides sufficient and necessary conditions for the existence of pushouts in categories of partial algebras and partial morphisms. It contains our main results. Section 4 defines the new single-pushout approach and compares it to the sesqui-pushout approach [3]. Section 5 demonstrates by some examples that the application conditions in the introduced re- writing approach are useful in many situations. Finally, Section 6 discusses related work and provides some conclusions. 2 Graphs and Partial Algebras In this section, we introduce the basic notions and constructions for partial algebras. We use a rather unusual approach in order to emphasise the close connection of categories of par- tial algebras to categories of hypergraphs. We employ a kind of objectification for partial mappings. A partial map f : A → B is not just a subset of A × B satisfying the uniqueness condition (∗) (a,b1),(a,b2) ∈ f implies b1 = b2. Instead, a partial map f : A → B is a triple ( f ,d f : f → A,c f : f → B) consisting of a set f of map entries together with two total maps d f : f → A and c f : f → B which provide the argument and the return value for every entry respect- ively. The uniqueness condition (∗) above translates to ∀e1,e2 ∈ f : d f (e1) = d f (e2) =⇒ e1 = e2 in this set-up. A signature Σ = (S,O) consists of a set of sorts S and a domain- and co-domain-indexed family of operations O = (Ow,v)w,v∈S∗. 3 A graph G wrt. a signature consists of a carrier set Gs (of vertices) for every sort s ∈ S and a set of hyperedges ( f G,dGf : f G → Gw,cGf : f G → Gv ) for every operation f ∈ Ow,v and w,v ∈ S∗ where the total mappings dGf and c G f provide the “arguments” and “return values”.4 A graph morphism h : G → H between two graphs G and H wrt. the same signature Σ = (S,O) consists of a family of vertex mappings h = (hs : Gs → Hs)s∈S and a family of edge mappings hO = ( hOf : f G → f H ) f∈O such that, for all operations f ∈ Ow,v and for all edges e ∈ f G, we have:5 dHf ( hOf (e) ) = hw ( dGf (e) ) and cHf ( hOf (e) ) = hv ( cGf (e) ) . 3 Note that we generalise the usual notion of signature which allows single sorts as co-domain specification for operations only. Operations in Ow,ε will be interpreted as predicates, operations in Ow,v with |v|> 1 will be interpreted as operations which deliver several results simultaneously. 4 For w ∈ S∗ and a family (Gs)s∈S of sets, G w is recursively defined by (i) Gε = {∗}, (ii) Gw = Gs if w = s ∈ S and (iii) Gw = Gv ×Gu if w = vu. 5 Given a sort-indexed family of mappings ( fs : Gs → Hs)s∈S, f w : Gw → H w is recursively defined for every w ∈ S∗ by (i) f ε ={(∗,∗)}, (ii) f w = fs if w = s ∈ S, and (iii) f w = f v × f u, if w = vu. Selected Revised Papers from GCM 2015 2 / 21 ECEASST The category of all graphs and graph morphisms wrt. a signature Σ is denoted by GΣ in the following.6 GΣ is complete and co-complete. All limits and co-limits can be constructed component-wise on the underlying sets. The pullback for a co-span B m→ A n← C is given by the partial product B×(m,n) C with the two projection morphisms π B×CB : B×(m,n) C → B and π B×C C : B×(m,n) C →C: ∀s ∈ S : ( B×(m,n) C ) s = {(x,y) :: ms(x) = ns(y)} ∀ f ∈ Ow,v : f (B×(m,n)C) = { (x,y) :: mOf (x) = n O f (y) } ∀ f ∈ Ow,v : d (B×(m,n)C) f ::= (x,y) 7→ d B f (x)|| w dCf (y) ∀ f ∈ Ow,v : c (B×(m,n)C) f ::= (x,y) 7→ c B f (x)|| v cCf (y), where the operator ||w : Bw ×Cw → (B×C)w transforms pairs of w-tuples into w-tuples of pairs:(( x1,...,x|w| ) , ( y1,...,y|w| )) 7→ ( (x1,y1),... ( x|w|,y|w| )) . A graph G ∈ GΣ=(S,O) is a partial al- gebra, if it satisfies for all f ∈ O: ∀e1,e2 ∈ f G : dGf (e1) = d G f (e2) =⇒ e1 = e2. (1) The full sub-category of GΣ consisting of all partial algebras7 is denoted by AΣ in the follow- ing. In a partial algebra A, operations f ∈ Oε,v with |v|> 0 are interpreted as (partial) constants, i. e. f A : Aε → Av is a partial map from the standard one-element set Aε = {∗} into Av. Sym- metrically, operations p ∈ Ow,ε with |w| > 0 are interpreted as predicates, since pA : Aw →{∗} is a partial map into the standard one-element set, i. e. it determines a subset on Aw only, namely the part of Aw where it is defined. Finally for operations f ∈ Oε,ε , there are only two possible interpretations in A, namely f A = /0 (false) or f A ={(∗,∗)} (true). Thus f A is just a boolean flag. Due to formulae (1) being a set of Horn-axioms, AΣ is an epireflective sub-category of GΣ, i. e. there is a reflection that maps a graph G ∈ GΣ to a pair ( GA ∈ AΣ,ηG : G → GA ) such that any graph morphism h : G→A with A∈AΣ has a unique extension h∗ : GA →A with h∗◦ηG = h. Since epireflective subcategories are closed wrt. products and sub-objects defined by regular monomorphisms (equalisers), the limits in AΣ coincide with the limits constructed in GΣ. AΣ has also all co-limits, since epireflections preserve co-limits. In general, however, the co-limits in AΣ do not coincide with the co-limits constructed in GΣ. The reflection provides the necessary correction. If, for example, (b : A → B,c : A →C) is a span in AΣ and (c∗ : B → D,b∗ : C → D) is its pushout constructed in GΣ, ( ηD ◦c∗ : B → DA ,ηD ◦b∗ : C → DA ) is the pushout in AΣ. Besides being complete and co-complete, the most important property of AΣ for the rest of the paper is the existence of right adjoints to all inverse image functors. If we fix an algebra A ∈ AΣ, AΣ ↓M A denotes the category of all (weak) sub-algebras of A. The objects in AΣ ↓M A 6 The identities in GΣ are given by families of identity mappings, and composition of morphisms is provided by component-wise composition of the underlying mappings. 7 Note that the interpretation of an operation f ∈ Ow,v in a partial algebra A is a partial map: Due to condition (1), the assignment ( f A,dAf : f A → Aw,cAf : f A → Av ) 7→ {( dAf (e),c A f (e) ) :: e ∈ f A } provides a partial map from Aw to Av. And, for a partial map f : Aw → Av, there is the inverse assignment f 7→ ( f , dAf ::= (d,c) 7→ d, c A f ::= (d,c) 7→ c) up to renaming of the elements in f A. 3 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras are all monomorphisms m : M � A and a morphism in AΣ↓MA from m : M � A to n : N � A is a (mono)morphism h : M � N in AΣ such that n◦h = m.8 For an AΣ-morphism g : A → B, the inverse image functor g∗ : AΣ↓M B → AΣ↓M A maps an object m : M → B ∈ AΣ↓M B to π A×MA : A×(g,m) M → A and a morphism h : (m : M → B) → (n : N → B) to the uniquely determined morphism g∗(h) : A×(g,m) M → A×(g,n) N such that π A×NA ◦g ∗(h) = π A×MA and π A×N N ◦g ∗(h) = h◦π A×MM . Proposition 1 In a category AΣ of partial algebras, every inverse image functor g∗ : AΣ ↓M B → AΣ↓MA has a right adjoint called g∗ : AΣ↓MA → AΣ↓MB. Proof. Given a sub-algebra m : M � A, we construct the sub-algebra g∗(M) ⊆ B and the inclu- sion morphism g∗(m) : g∗(M) ↪→ B as follows: ∀s ∈ S : g∗(M)s = { b ∈ Bs :: ∀a ∈ g−1s (b)∃x ∈ M : ms(x) = a } and ∀ f ∈ Ow,v : f g∗(M) = { e ∈ f B :: ∀ea ∈ gOf −1 (e)∃ex ∈ M : mOf (ex) = ea } , such that d g∗(M) f = d B f | f g∗(M) and c g∗(M) f = c B f | f g∗(M) for every operation. The co-unit εm : g∗(g∗(m : M � A))→(m : M � A) can be defined on every element (a,b)∈ A×(g,g∗(m)) g∗(M) by εm(a,b) = c such that m(c) = a. Note that εm is completely defined, since, by definition of g∗(m), a must have a pre-image wrt. m for every pair (a,b)∈ A×(g,g∗(m)) g∗(M). It is uniquely defined, since m is monic. By definition of εm, m◦εm = g∗(g∗(m)) = π A×(g,g∗(m))g∗(M) A which means that εm is a morphism in AΣ↓MA. Now, let an object x : X � B ∈ AΣ↓MB and a morphism k : g∗(x)→ m ∈ AΣ↓MA, i. e. m◦k = π A×(g,x)X A be given. We construct k ∗ : x → g∗(m) by e 7→ x(e) for every e ∈ X . The map- pings of k∗ are completely defined: (i) if x(e) /∈ g(A), x(e) ∈ g∗(M) because g−1(x(e)) = /0, and, otherwise, the existence of k with m ◦ k = π A×(g,x)X A enforces that every g-pre-image of x(e) has a pre-image under m. By definition, g∗(m)◦ k∗ = x. By definition of the inverse image functor, g∗(k∗) : ( A×(g,x) X ) → ( A×(g,g∗(m)) g∗(M) ) maps (a,e) to (a,k∗(e)). Thus, ε (g∗(k∗)(a,e)) = ε(a,k∗(e)) = c with m(c) = a and k(a,e) = c′ with m(c′) = π A×(g,x)X A (a,e) = a. Since m is monic, c = c′. The morphism k∗ is uniquely determined, since g∗(M) ⊆ B and g∗(m) is monic. Corollary 1 If g is monic, the co-units of g∗ are isomorphisms. For every algebra A, the category AΣ↓M A of all (weak) sub-algebras of A has two important sub-categories, namely AΣ ↓F A and AΣ ↓C A, i. e. the category of all full respectively closed sub-algebras of A. A morphism m : M → A is full, if for every e ∈ f A, f ∈ Ow,v, and w,v ∈ S∗ with dAf (e) = m w(x) and cAf (e) = m v(y) for some (x,y) ∈ Mw × Mv there is e′ ∈ f M with e = m(e′); it is closed, if for every e ∈ f A, f ∈ Ow,v, and w,v ∈ S∗ with dAf (e) = m w(x) for x ∈ Mw there is e′ ∈ f M with e = m(e′).9 By definition, AΣ↓CA ⊆ AΣ↓FA ⊆ AΣ↓MA for every 8 Note that every sub-graph of A is a sub-algebra of A, since all monomorphisms in GΣ are regular and epireflective sub-categories are closed wrt. regular sub-objects. 9 Note that, in the case of total algebras, every inclusion morphism is closed! Selected Revised Papers from GCM 2015 4 / 21 ECEASST A ∈ AΣ. The three different sorts of sub-algebras induce three factorisation systems in every category of partial algebras, namely factorisations in (i) closed epimorphisms10 and arbitrary monomorphisms, (ii) morphisms with surjective vertex mappings and full monomorphisms, and (iii) arbitrary epimorphisms and closed monomorphisms. Since pullbacks preserve full and closed monomorphisms11, we obtain restrictions g∗F : AΣ↓ F B → AΣ↓FA and g∗C : AΣ↓ CB → AΣ↓CA of the inverse image functor g∗ : AΣ↓MB → AΣ↓MA for every morphism g : A → B. Proposition 2 In a category AΣ of partial algebras, every inverse image functor g∗F : AΣ↓ FB → AΣ ↓F A has a right adjoint called gF∗ : AΣ ↓F A → AΣ ↓F B. If g is monic, the co-units of gF∗ are isomorphisms. Proof. We show that g∗ : AΣ↓MA →AΣ↓MB maps full monomorphisms to full monomorphisms. Let m : M � A be full, e ∈ f B with f ∈ Ow,v, and w,v ∈ S∗ such that (i) dBf (e) = g∗(m) w (x) and (ii) cBf (e) = g∗(m) v (y). If g(e′) = e, properties (i) and (ii) together with the construction of g∗ in the proof of Proposition 1 imply dAf (e ′) = mw(x′) and cAf (e ′) = mv(y′) for some (x′,y′)∈Mw×Mv. Since m is full, e′ = mOf (e ′′). Thus, every e′ with g(e′) = e has a pre-image under mOf which implies that e has a pre-image under g∗(m)Of . The inverse image functors between closed sub-algebras do not possess right adjoints in gen- eral as the following examples illustrate: Example 1 (Missing right adjoint) Consider the signature Σ2 = ( S2,O2 ) with S2 = {s} and O2w,v = { { f} w = ss,v = s /0 otherwise , the three algebras A ::= As ={2}, f A = /0, B ::= Bs ={0,1,2}, f B = ( { f B}, dBf ( f B) = (0,1), cBf ( f B) = 2 ) , M ::= Ms = /0, f M = /0, the morphism g : A → B ::= 2 7→ 2, and the closed monomorphism m : M � A ::= /0. There are seven closed sub-algebras of B, namely B itself and six algebras ⊆x: Bx → B, x ∈{1,2,3,4,5,6} with completely undefined f and carriers B1s = /0, B 2 s = {0}, B3s = {1}, B4s = {2}, B5s = {0,2}, and B6s ={1,2} for sort s.12 None of these algebras can be the right adjoint object for m: B itself and cases x ∈{4,5,6} are excluded since there is no object in M where the object (2,2) in the partial product A×(g,⊆x) Bx can be mapped to. The cases x ∈{1,2,3} provide an empty partial product of ⊆x with g. Thus, there is the empty morphism from πA : A×(g,⊆x) Bx → A to m which can play the role of the co-unit. But there is no morphism from ⊆2 to ⊆1 or ⊆3 and there is no morphisms from ⊆3 to ⊆2. Thus, having Ow,v 6= /0 for |w|≥ 2 and |v|≥ 1 in the signature prevents the existence of right adjoints in some cases. 10 A morphism h : A → B is closed, if its image in B is a closed sub-algebra of B. 11 Pullbacks preserve all monomorphisms in a class N , if the underlying category has an epi-mono-factorisation system (E ,N ). 12 Note that the carrier {0,1} for s is not closed! 5 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras Also constants, i. e. operations in Oε,v with |v|≥ 1, are harmful. A simple example provides the signature Σ0 = ( S0,O0 ) with S0 = {s} and O0w,v = { { f} w = ε,v = s /0 otherwise , the three algebras A ::= As ={ f ,0}, f A = ( { f A}, dAf ( f A) =∗, cAf ( f A) = f ) B ::= Bs ={ f}, f B = ( { f B}, dBf ( f B) =∗, cBf ( f B) = f ) M ::= Ms ={ f ,}, f M = ( { f M}, dMf ( f M) =∗, cMf ( f M) = f ) the morphism g : A → B ::= f 7→ f ,0 7→ f , and the closed monomorphism m : M � A ::= f 7→ f . There is only one closed sub-algebra of B, namely B itself. But idB cannot be the right adjoint object for m, since there is no map ε : ( πA : A×(g,idB) B ) → m. The problematic object in A×(g,idB) B is (0, f ) the A-projection of which provides 0 which has no pre-image under m. Definition 1 (Graph Structure) A graph structure Γ = (S,(Ow,v)w,v∈S∗) is a signature with unary operations only, i. e. Ow,v = /0 if v 6= ε and |w| 6= 1.13 Proposition 3 For a graph structure Γ, the inclusion functor ⊆: AΓ↓CA → AΓ↓FA has a right adjoint. Proof. (Sketch) Given a graph structure Γ = (S,O) and a full sub-algebra (m : M � A) ∈ AΓ, construct the following family of carriers:( M′s ={x ∈ Ms :: f A(x)∈ M′ v for all v ∈ S∗ and f ∈ Os,v} ) s∈S . Let M′ be the largest full sub-algebra of A contained in (M′s)s∈S. Since M ′ ⊆ M, we can use this inclusion as the required co-unit. It is easy to see, that M′ is a closed sub-algebra of A. And, by construction, any other closed sub-algebra of A the carriers of which are contained in M is a sub-algebra of M′. Corollary 2 Given a graph structure Γ, every inverse image functor g∗C : AΓ↓ CB→AΓ↓CA has a right adjoint called gC∗ : AΓ↓CA → AΓ↓CB. If g is monic, the co-units of gC∗ are isomorphisms. 3 Partial Morphisms on Partial Algebras In order to obtain frameworks for single-pushout rewriting, we proceed from the category of partial algebras with total morphisms to the categories of partial algebras and partial morphisms. In this section, we investigate the conditions under which pushouts can be constructed in these categories. 13 Note that this notion of graph structure is a straightforward extension of the one in [12] to signatures with predicate symbols and operations with products as co-domain! Selected Revised Papers from GCM 2015 6 / 21 ECEASST 3.1 Pushouts in Arbitrary Categories of Partial Morphisms Let C be a category and S a sub-class of its monomorphisms such that (C1) C has a factorisation system (E ,S ) for a class of (epi)morphisms E , (C2) S contains all isomorphisms and is closed wrt. composition and prefix14, (C3) C has pullbacks along S -morphisms which preserve S -morphisms15. A concrete S -partial morphism is a span of C -morphisms (p : K � P,q : K → Q) such that p ∈ S . Two concrete S -partial morphisms (p1,q1) and (p2,q2) are equivalent and denote the same abstract S -partial morphism if there is an isomorphism i such that p1 ◦ i = p2 and q1 ◦ i = q2; in this case we write (p1,q1) ≡ (p2,q2) and [(p,q)]≡ for the class of spans that are equivalent to (p,q). The category of S -partial morphisms C S over C has the same objects as C and abstract S -partial morphisms as arrows. The identity idC S A for an object A is defined by idC S A = [(idA,idA)]≡ and composition of S -partial morphisms [(p : K � P,q : K → Q)]≡ and [(r : J � Q,s : J → R)]≡ is given by [(r,s)]≡◦C S [(p,q)]≡ = [ (p◦C r′ : M � P,s◦C q′ : M → R) ] ≡ where (M,r′ : M � K,q′ : M → J) is an arbitrarily chosen pullback of q and r. Note that there is the faithful embedding functor ι : C → C S defined by identity on objects and ( f : A → B) 7→ [idA : A � A, f : A → B]≡ on morphisms. We call [d : A′� A, f : A′→ B]≡ a total morphism, if d is an isomorphism, and, by a slight abuse of notation, write [d, f ]∈C . From now on, we mean the abstract S -partial morphism [ f ,g]≡ if we write ( f : B � A,g : B →C). The single-pushout approach defines direct derivations by a single pushout in a category of partial morphisms. There is a general result for the existence of pushouts in a category C S of partial morphisms based on the notions final S -triple and S -hereditary pushout in the underly- ing category C of total morphisms. Definition 2 (Final S -triple) A S -triple for a pair ((l,r),(p,q)) of morphisms in C S with common domain is given by a collection ( p, p∗,r,l,l∗,q ) of C -morphisms such that p∗, p, l∗, l are in S and (i) (r, p) is pullback of (r, p∗), (ii) (q,l) is pullback of (q,l∗), and (iii) l ◦ p = p ◦ l. A S -triple ( p, p∗,r,l,l∗,q ) for ((l,r),(p,q)) is final, if, for any other S -triple( p′, p′ ∗ ,r′,l′, l′ ∗ ,q′ ) , there is a unique collection (u1,u2,u3) of (S -)morphisms such that (iv) p◦ u1 = p′, (v) l◦u1 = l′, (vi) p∗◦u2 = p′ ∗, (vii) u2◦r′ = r◦u1, (viii) l∗◦u3 = l′ ∗, and (ix) u3◦q′ = q◦u1, compare left part of Fig. 1. In [13], a sufficient condition for the existence of final S -triples is shown. Proposition 4 A category C S of partial morphisms has all final S -triples, if (i) the inverse image functor g∗S : AΣ ↓ S B → AΣ ↓S A has a right adjoint for each morphism g : A → B and (ii) every S -chain (mi : Ai+1 � Ai)i∈N0 has a limit (li : A ∗ � Ai)i∈N0 . 16 14 Closure of S wrt. composition and prefix means that, given g ∈ S , g◦ f ∈ S ⇔ f ∈ S . 15 I. e. g′ ∈ S , if ( f ′,g′) is pullback in f ◦g′ = g◦ f ′ and g ∈ S . 16 That the chain morphisms are in S is implied by the existence of (E ,S )-factorisations. 7 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras L K R A′ C′ P D P∗ B′ D′ D′ P′ A C Q K∗ B D K′ l r qi pi i0 p′i i1 p q l q p r p∗ q′i i2 i3 p′ r′ q′ l′ u1 p′∗ u2 q p p′ l∗ q′ l′∗ u3 Figure 1: Final Triple and Hereditary Pushout Definition 3 (S -Hereditary pushout) A pushout (q′, p′) of (p,q) in C is S -hereditary if for each commutative cube as in the right part of Figure 1, which has pullback squares (pi,i0) and (qi,i0) of (i2, p) and (i1,q) resp. as back faces such that i1 and i2 are in S , in the top square, (q′i, p ′ i) is pushout of (pi,qi), if and only if, in the front faces, (p ′ i,i1) and (q ′ i,i2) are pullbacks of (i3, p′) and (i3,q′) resp. and i3 is in S .17 Note that (q′i, p ′ i) is hereditary pushout of (pi,qi) in Figure 1, if (q ′, p′) is hereditary pushout of (p,q). Proposition 5 (Pushout in C S ) A given span of partial morphisms (l : K � L,r : K → R) and (p : P � L,q : P → Q) has a pushout ((l∗,r∗),(p∗,q∗)) in C S , if and only if there is (i) a fi- nal S -triple l : D → P, p : D → K, r : D → P∗, q : D → K∗, p∗ : P∗ → R, l∗ : K∗ → Q for ((l,r),(p,q)) and (ii) a S -hereditary pushout (r∗ : K∗ → H,q∗ : P∗ → H) for (q,r) in C , com- pare sub-diagrams (1) – (3) and (4) resp. in Figure 2. L K R P D P∗ Q K∗ H (1) l r (2)p q l q p r p∗ q∗(3) l∗ r∗ (4) Figure 2: Pushout in C S The proof can be found in [16]. A version of the proof that does not presuppose a choice of pullbacks that is compatible with pullback composition and decomposition is contained in [17]. 17 For details on hereditary pushouts see [10, 11] Selected Revised Papers from GCM 2015 8 / 21 ECEASST 3.2 Pushouts of Partial Morphisms on Partial Algebras With the results of Section 2, we can construct categories with three different types of partial morphisms over partial algebras, namely A M Σ , A F Σ , and A C Γ where M is the class of all, F the class of all full, C the class of all closed monomorphisms, Σ is an arbitrary signature, and Γ is a graph structure. The general results about pushouts of partial morphisms carry over to these categories as follows: Proposition 6 (Final triple) In A M Σ , A F Σ , and A C Γ , every pair ((l,r),(p,q)) of partial morph- isms with common domain has a final triple. Proof. We use the condition of Proposition 4. The existence of right adjoints to inverse image functors is given by Propositions 1 and 2 as well as Corollary 2. Limits of S -chains exist, since AΣ has all limits. Corollary 3 (Pushout) Partial morphisms (l : K � L,r : K → R) and (p : P � L,q : P → Q) have a pushout in A M Σ , A F Σ , and A C Γ , if and only if the pushout of (q,r) is M-, F-, or C-hereditary respectively, where l : D → P, p : D → K, r : D → P∗, q : D → K∗, p∗ : P∗ → R, l∗ : K∗ → Q is a final M-, F-, or C-triple of ((l,r),(p,q)), see Figure 2. Proof. Direct consequence of Proposition 5 and Proposition 6. Thus, the existence of pushouts in A M Σ , A F Σ , or A C Γ only depends on the involved AΣ-pushout being M-, F-, or C-hereditary, resp. We start with the analysis of M-hereditary pushouts in AΣ. Proposition 7 (Sufficient condition for M-hereditariness) If a pushout in AΣ is also pushout in GΣ, then it is M-hereditary in AΣ. Proof. Let a commutative cube as in the right part of Fig. 1 in AΣ be given such that the back faces are pullbacks. Then this is also a situation in GΣ and the back faces are also pullbacks in GΣ, since AΣ is an epireflection of GΣ. Let the front faces be pullbacks in AΣ and i3 be a monomorphism. Then the front faces are also pullbacks in GΣ. Since all pushouts in GΣ are hereditary, D′ together with p′i and q ′ i is pushout in GΣ. Since (i) AΣ is closed wrt. sub-algebras, (ii) D is in AΣ, and (iii) i3 is monic, D′ is also in AΣ and its reflector ηD′ is an isomorphism.18 Thus, D′ together with p′i and q ′ i is pushout in AΣ. Let (D′,q′i, p ′ i) be pushout of (pi,qi) in AΣ. Construct (D ′′,q′′i , p ′′ i ) as pushout of (pi,qi) in GΣ. We obtain the epic reflector ηD′′ : D′′ � D′ with p′i = ηD′′ ◦ p ′′ i and q ′ i = ηD′′ ◦q ′′ i . Since D ′′ is pushout, we also get i′3 : D ′′ � D with i′3 ◦ p ′′ i = p ′◦ i1 and i′3 ◦q ′′ i = q ′◦ i2. Since i3 ◦ηD′′ ◦ p′′i = i3◦ p′i = p ′◦i1 = i′3◦ p ′′ i and i3◦ηD′′◦q ′′ i = i3◦q ′ i = q ′◦i2 = i′3◦q ′′ i , we can conclude i3◦ηD′′ = i ′ 3. Since all pushouts in GΣ are hereditary, i′3 is monic implying that ηD′′ is monic as well. Thus, ηD′′ is an isomorphism and D′ is also the pushout in GΣ. This immediately provides monic i3 and pullbacks in the front faces of the cube in the right part of Fig. 1. But not all pushouts in AΣ are M-hereditary. Here is a typical example: 18 Note that morphisms in G Σ that are both epic and monic are isomorphisms. 9 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras a c L99 f C b d L99 f D a c L99 f C b L99 f B d L99 f D qi=q pi i0=idA p′i=p ′ i1=idC q′i s=q ′ s i2 s=idBs i3=idD q p p′ q′ Figure 3: Simple Non-Hereditary Pushout in AΣ Example 2 Consider the signature Σc = (Sc,Oc) with Sc = {s} and Ocw,v = { { f} w = ε,v = s /0 otherwise, the three algebras A ::= As ={a}, f A = /0, B ::= Bs ={b}, f B = ( { f B}, dBf ( f B) =∗, cBf ( f B) = b ) , C ::= Cs ={c}, f C = ( { f C}, dCf ( f C) =∗, cCf ( f C) = c ) , and the two morphisms p : A → B ::= a 7→ b and q : A →C ::= a 7→ c. The pushout of (p,q) in A P Σc consists of the algebra D ::= Ds ={d}, f D = ( { f D}, dDf ( f D) =∗, cDf ( f D) = d ) and the two morphisms p′ : C → D ::= c 7→ d, f C 7→ f D q′ : B → D ::= b 7→ d, f B 7→ f D. This pushout is depicted in the bottom of Fig. 3 and is not M-hereditary. We construct the follow- ing cube of morphisms, compare Fig. 3: A′ = A, i0 = idA, B′ is defined by B′s = Bs and f B′ = /0, i2 maps b in B′s to b in Bs, C ′ = C, i1 = idC, qi = q, and pi maps a to b. Note that (i0,qi) is pullback of (q,i1) and (i0, pi) is pullback of (p,i2). Constructing (D′ = D, p′i = p ′,q′i ::= b 7→ d) as the pushout of (p′,q′), we obtain i3 = idD. But (i2,q′i) is not pullback of (q ′,i3): B×(q′,i3) D ′ contains a defined constant for f , since i3( f D) = q′( f B), and B′ does not. Note that the A Σ -pushout of the morphisms p and q in Example 2 does not coincide with the pushout of p and q constructed in the larger category GΣ. The pushout in GΣ is the graph G ::= Gs ={g}, f G = ( { f GC , f G B },d G f ( f G C ) = d G f ( f G B ) =∗,c G f ( f G C ) = c G f ( f G B ) = g ) Selected Revised Papers from GCM 2015 10 / 21 ECEASST together with the morphisms p′′ : C → G ::= c 7→ g, f C 7→ f GC q′′ : B → G ::= b 7→ g, f B 7→ f GB . The partial algebra D is the epireflection of the graph G and the reflector ηG : G → D maps as follows: g 7→ d, f GC 7→ f D, and f GB 7→ f D. The identification ηG( f GC ) = ηG( f G B ) = f D of the reflector provided the possibility to construct the commutative cube in Example 2 that disproves M-hereditariness of the pushout of (p,q). The following proposition shows that this construction of a counterexample is always possible if the pushouts in AΣ and GΣ are different. As a prerequisite, we need the following construction. Definition 4 (Vertex- and hyperedge-generated sub-span) Let a signature Σ = (S,O) and an AΣ- span B p ←− A q −→C be given. For s ∈ S, let ≡p,qs ⊆ (Bs ]Cs)×(Bs ]Cs) denote the equivalence generated by {(ps(z),qs(z)) :: z ∈ As} and, for f ∈ O, let ≡ p,q f ⊆ ( f B ] f C ) × ( f B ] f C ) denote the equivalence generated by {(pOf (z),q O f (z)) :: z ∈ f A}. For a vertex e ∈ Bs, the sub-algebras Be ⊆ B, Ce ⊆ C, and Ae ⊆ A are defined by Bes = Bs ∩ [e]≡p,qs , C e s = Cs ∩ [e]≡p,qs , A e s = {a ∈ As :: ps(a) ∈ [e]≡p,qs }, B e s′ = C e s′ = A e s′ = /0 for all s ′ 6= s, and f B = f C = f A = /0 for all f ∈ O. For a hyperedge e ∈ f B with dBf (e) = (d1,...,dn) and c B f (e) = (c1,...,cm), the sub-algebras Be ⊆ B, Ce ⊆ C, and Ae ⊆ A are defined by Bes = ⋃ x∈e↔ B x s , C e s = ⋃ x∈e↔ C x s , A e s = ⋃ x∈e↔ A x s , f B e = f B∩[e]≡p,qf , f Ce = f C∩[e]≡p,qf , f Ae ={n ∈ f A :: pOf (n)∈ [e]≡p,qf }, and f ′Be = f ′C e = f ′A e = /0 for all f ′ 6= f ∈ O where e↔ ={d1,...,dn,c1,...,cm}. Proposition 8 (Necessary condition for M-hereditariness) If a pushout in AΣ is M-hereditary, it is also pushout in GΣ. Proof. Let (p : A → B,q : A → C) be a span of morphisms in AΣ, let (E,q′′ : B → E, p′′ : C → E) be its pushout in GΣ, and let (q′ : B → D, p′ : C → D) be its pushout in AΣ. Since AΣ is epireflective sub-category of GΣ, we know that D = EA , q′ = ηE ◦q′′ and p′ = ηE ◦ p′′ where ηE : E → EA is the reflector for the graph E. Suppose D and E are not isomorphic, then there are x,y ∈ E such that x 6= y and ηE(x) = ηE(y) = z. Since p′′ and q′′ are jointly epic in GΣ, both x and y have pre-images under p′′ and/or q′′. Let x′′,y′′∈ B]C be these pre-images and suppose, without loss of generality, x′′ ∈ B. We construct a cube as in Fig. 1(right part) using the construction of Definition 4 for x′′: Let B′ = Bx ′′ , C′ = Cx ′′ , and A′ = Ax ′′ , i0 : A′ � A, i1 : C′ � C, and i2 : B′ � B be the sub-algebra inclusions, and let p′ = p|A′ and q ′ = q|A′. By construction, (pi,i0) and (qi,i0) are pullbacks. Since x 6= y, we have [x′′]≡p,q 6= [y ′′]≡p,q and can conclude that y ′′ has neither a pre-image under i1 nor under i2. Construct the AΣ-pushout (p′i : C ′ → D′,q′i : B ′ → D′) of (q′, p′) which provides the morphisms i′3 : D ′ → E and i3 = ηE ◦ i′3 : D ′ → D making the whole cube commute. By construction, z = ηE(x) = ηE ◦q′′(x′′) = ηE ◦q′′◦ i2(x′′) = ηE ◦ i′3 ◦q ′ i(x ′′) = i3 ◦q′i(x ′′). Thus, z has a pre-image under i3 and z = q′(y′′) or z = p′(y′′). Since y′′ has neither a pre-image under i1 nor under i2, one of the front faces of the constructed cube fails to be a pullback. Theorem 1 A pushout in AΣ is M-hereditary, iff it is also pushout in GΣ. 11 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras Now, we investigate F-hereditary pushouts in AΣ. In Example 2, the morphism i2 is not full, compare Figure 3. If monomorphisms are restricted to full ones, the situation in Figure 3 cannot occur. This observation leads to the following characterisation of F-hereditary pushouts in AΣ. Theorem 2 A pushout (q′, p′) of (p,q) in AΣ is F-hereditary, iff (q′s, p ′ s) is pushout of (ps,qs) in the category of sets and mappings for all sorts s ∈ Σ. Proof. “⇐”: Let a commutative cube as in the right part of Fig. 1 in AΣ be given such that the back faces are pullbacks. Let the top be pushout in AΣ. Then, for every sort s, the pushout( Es, q′′i s : B ′ s → E s, p′′i s : C ′ s → E s ) of ( pi s , qi s) provides epic us : E s → D′s. Since all pushouts of mappings are hereditary, we obtain monic i′3 s : E s → Ds with i3 s◦us = i ′ 3 s. Thus, us is monic and epic which implies, for all sorts s, (D′s, p ′ i s , q ′ i s) is pushout, i3 s is monic, and ( p ′ i s , i1 s) as well as (q′i s , i2 s) are pullbacks. That i3 is full, follows from p ′ and q′ being jointly epic and i1 and i2 being full. Given d ∈ f D with d = i3(d′) and d = p′(c), there is c′ ∈ f C ′ with i1(c′) = c and p′i(c) = d ′, since i1 is full. Therefore (p′i,i1) is pullback. An analog argument provides that (q′i,i2) is pullback. Vice versa, if i3 is full monomorphism and (p ′ i,i1) as well as (q ′ i,i2) are pullbacks, they are pullbacks for each sort mapping. This implies that ( p′i s , q ′ i s) is pushout for every sort s. It remains to show that p′i and q ′ i are jointly epic on hyperedges. But this is a direct consequence of p′ and q′ being jointly epic and i1 and i2 being full. “⇒”: We repeat the argument in the proof of Proposition 8: Let there be a sort s, such that the pushout (Es,q′′s : Bs → Es, p′′s : Cs → Es) is different from (Ds,q′s, p′s). Then there are x 6= y such that us(x) = z = us(y) for the unique morphism us : Es → Ds with us ◦q′′s = q′s and us ◦ p′′s = p′s. Without loss of generality, assume y has a pre-image y′′ under p′′ and/or q′′ and x = q′′s (x ′′). Consider again the sub-span of (p,q) induced by x′′: Let A′, B′, and C′ be the full sub-algebras of A, B, and C induced by Ax ′′ , Bx ′′ , and Cx ′′ respectively, let pi = p|A′ and qi = q|A′, and let i0 : A ′ � A, i1 : C ′ � C, and i2 : B ′ � B be the inclusions. We obtain pullbacks (i0, p′) and (i0,q′). Constructing the pushout (q′i, p ′ i) of (pi,qi), z has a pre-image under i3. We also know z = q′(y′′) or z = p′(y′′). By construction, y′′ has neither a pre-image under i1 nor under i2. Thus, either (i2,q′i) or (i1, p ′ i) is no pullback. The analysis of C-hereditary pushouts in AΓ for a graph structure Γ is more complicated than the analysis of M- and F-hereditary pushouts as the following example demonstrates. Example 3 (C-hereditary pushout) Consider the span (p : A → B,q : A → C) in AΓ where the underlying graph structure ΓC = ( SC,OC ) is defined by SC = {s} and OCw,v = { { f} w = s,v = s /0 otherwise, the three algebras A, B, and C are given by A ::= As ={a1;1,a1;3,a3;1}, f A = /0, B ::= Bs ={b1,b2,b3}, f B ::= b1 7→ b2, b2 7→ b3, C ::= Cs ={c1,c2,c3}, f C ::= c1 7→ c2, c2 7→ c3, Selected Revised Papers from GCM 2015 12 / 21 ECEASST and the two morphisms p and q map as follows: ps : As → Bs ::= a1;1 7→ b1,a1;3 7→ b1,a3;1 7→ b3 qs : As →Cs ::= a1;1 7→ c1,a1;3 7→ c3,a3;1 7→ c1. The pushout of (p,q) in AΓ consists of the algebra D ::= Ds ={d2;2,d1,3;1,3}, f D ::= d2;2 7→ d1,3;1,3,d1,3;1,3 7→ d2;2 and the two morphisms p′ : C → D ::= c1 7→ d1,3;1,3,c2 7→ d2;2,c3 7→ d1,3;1,3 q′ : B → D ::= b1 7→ d1,3;1,3,b2 7→ d2;2,b3 7→ d1,3;1,3. This pushout in AΓ does not induce a pushout in the category of sets and maps for the sort s, since p′s(c2) = d2;2 = q ′ s(b2) without b2 ≡p,q c2. Nevertheless, it is C-hereditary, since the only possible sub-spans of (p,q) in a commutative cube as in Figure 1(right part) with pullbacks in the back faces and closed monomorphisms i1 and i2 are (/0, /0) and (p,q) itself. Having, for example c2 in C′ requires also c3 ∈ C′. This implies b1,b2,b3 ∈ B′ due to p(a1;3) = b1 and q(a1;3) = c3. Now, p(a3;1) = b3 and q(a3;1) = c1 requires c1 ∈C′. Thus, having one of the elements of B and C in the sub-span requires having all of the elements in the sub-span. This is due to the cyclic structure established by f B, f C, and the mapping of a1;3 and a3;1 by p and q. Definition 5 (Hierarchical span) Given a graph structure Γ = (S,O) and a span (p : A → B,q : A → C) in AΓ, its reachability relation R on the disjoint union ⊎ s∈S Bs ] ⊎ s∈S Cs of the carriers of B and C is defined by xRy if (i) x ≡p,qs y for some sort s, (ii) (z1,...,zn) = f B]C(x) for some f ∈ Os,v, n ≥ 1, and y = zi for 1 ≤ i ≤ n, or (iii) xRz and zRy.19 A span (p,q) is hierarchical, if xRy and yRx implies x ≡p,q y. R(x) denotes the elements reachable from x, i. e. R(x) = {z ∈⊎ s∈S Bs ] ⊎ s∈S Cs :: xRz} Theorem 3 A pushout (q′ : B → D, p′ : C → D) of a hierarchical span (p,q) in AΓ is C- hereditary, iff (q′s, p ′ s) is pushout of (ps,qs) for all sorts s ∈ Σ. Proof. (Sketch) For the “⇐”-part, we can repeat the arguments in the “⇐”-part of the proof for Theorem 2 substituting fullness by closedness. The “⇒”-part also follows the outline given by the “⇒”-part of the proof for Theorem 2. Having x 6= y ∈ Es and us(x) = us(y) where (Es, p′′s : Cs →Es,q′′s : Bs →Es) is the pushout of (qs, ps) and us : Es →Ds the mediating map with us◦p′′s = p′s and us◦q′′s = q′s, we know for the pre-images x′′ of x and y′′ of y under p′′ and/or q′′ that either x′′ is not reachable from y′′ or y′′ is not reachable from x′′. Without loss of generality, suppose the second case and construct B′ as the full sub-algebra of B induced by B∩R(x′′), C′ as the full sub-algebra of C induced by C ∩ R(x′′), and A′ as the full sub-algebra of A induced by {a ∈ A :: p(a)∈ R(x′′)}. Let i0 : A′→ A, i1 : C′→C, and i2 : B′→ B be the corresponding closed inclusions and pi = p|A′ and qi = q|A′. Since we know that y ′′ neither has a pre-image under i1 nor under i2, either (i1, p′i) or (i2,q ′ i) is not a pullback. 19 f B]C : Bs ]Cs → Bv]Cv is the uniquely determined co-product of f B and f C . 13 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras L K R G K∗ t@m m l m〈l〉 r m〈t〉(1) l〈m〉 r〈m〉 (2) Figure 4: Single- versus Sesqui-Pushout Transformation Definition 6 (Hierarchical graph structure) A graph structure Γ = (S,O) is hierarchical, if the reflexive/transitive closure of the relation � on S defined by s � s′ if there is f ∈ Os,vs′u with v,u ∈ S∗ is a partial order. Corollary 4 For a hierarchical graph structure Γ, a pushout (q′, p′) of a span (p,q) in AΓ is C-hereditary, iff (q′s, p ′ s) is pushout of (ps,qs) for all sorts s ∈ Σ. 4 Rewriting of Partial Algebras: Some Theory In this section, we introduce single-pushout rewriting in the categories of partial algebras. For a rich theory, we restrict transformations to those that produce total co-matches. All definitions and propositions in the following presuppose an arbitrary underlying category A M Σ , A F Σ , and A C Γ for a signature Σ or hierarchical graph structure Γ.20 Definition 7 (Rule and transformation) A transformation rule t is a partial morphism t = (l : K � L,r : K → R). There is a direct transformation of a host graph G to the result graph t@m with a rule t : L→R if there are total morphisms m : L→G and m〈t〉 : R→ t@m as well as a partial morphism t〈m〉= (l〈m〉 : K∗→ G,r〈m〉 : K∗→ t@m) : G → t@m such that (t〈m〉,m〈t〉) is pushout of (t,m). In a direct transformation, m is called match, m〈t〉 co-match, and t〈m〉 trace of the transformation.21 Since we restricted transformations to total co-matches, we obtain a close connection of our transformations to Sesqui-Pushout Rewritings in the sense of [3], which are composed of final pullback complements and pushouts. Theorem 4 (Single- and sesqui-pushout transformation) There is a transformation with rule t = (l : K � L,r : K � R), match m : L →G, (total) co-match m〈t〉 : R→ t@m and trace t〈m〉= (l〈m〉 : K∗ � G,r〈m〉 : K∗ � t@m), if and only if there is a total morphism m〈l〉 : K → K∗ such that (i) (l,m〈l〉) is pullback of (m,l〈m〉), (ii) l〈m〉 = m∗(l), and (iii) (r〈m〉,m〈t〉) is hereditary pushout of (r,m〈l〉), compare (1) and (2) in Fig. 4. Proof. Direct consequence of the construction of final triples in [17] and the fact that the match and the co-match are total. 20 Note that the theory in this section is also valid in A C Σ for arbitrary signatures, although existence of a direct transformation with a rule at a given match is unpredictable in this general case, compare Section 3. 21 The graph t@m is uniquely determined up to isomorphism by the transformation! Selected Revised Papers from GCM 2015 14 / 21 ECEASST L1 K1 R1 L2 K2 R2 L′1 K ′ 1 M K ′ 2 R ′ 2 G D1 t1@m1 D2 t2@m2 m1 e′′1 m1〈l1〉 e′1 l1 r1 m1〈t1〉 e1 m2 e2 m2〈l2〉 e′2 l2 r2 m2〈t2〉 e′′2 s′1 l′1 r ′ 1 s1 s s2 l′2 r ′ 2 s′2 l1〈m1〉 r1〈m1〉 l2〈m2〉 r2〈m2〉 Figure 5: Hereditary Pushout and Final Pullback Complement Thus, our set-up of single-pushout rewriting is Sesqui-Pushout Rewriting at left-linear rules with the additional requirement that the involved pushout on the transformation’s right-hand side is hereditary. This close connection between Single-Pushout and Sesqui-Pushout Rewriting leads to a rich theory for Single-Pushout Rewriting with total co-matches in general and in the special case of partial algebra transformation. In this paper, we present the concurrency theorem. It is a good example to demonstrate how far the theory for Single-Pushout Rewriting of total algebras carries over to partial algebras and where the differences are. We additionally presuppose: (C4) C has all finite co-limits and (C5) For every morphism g ∈ S , all co-units of g∗ are isomorphisms. Definition 8 (Concurrent rule) Two transformations t1〈m1〉 : G→t1@m1 and t2〈m2〉 : t1@m1→ t2@m2 with rules t1 : L1 → R1 and t2 : L2 → R2 constitute a concurrent rule t2〈m2〉◦t1〈m1〉 : G → t2@m2, if the co-match of the first and the match of the second are “jointly epic”, i. e. the co- product morphisms {m1〈t1〉,m2} : R1+L2 → t1@m1 making the diagram commute is in E .22 Theorem 5 Given two transformations t1〈m1〉 : G → t1@m1 and t2〈m2〉 : t1@m1 → t2@m2, there is a direct transformation with a concurrent rule t2〈n2〉◦ t1〈n1〉 at a match n, such that (t2〈n2〉◦t1〈n1〉)〈n〉= t2〈m2〉◦t1〈m1〉. Proof. Consider Figure 5. The first transformation uses rule t1 = (l1 : K1 → L1,r1 : K1 → R1) at match m1 and produces trace t1〈m1〉= (l1〈m1〉,r1〈m1〉) and co-match m1〈t1〉 and the second uses rule t2 = (l2 : K2 → L2,r2 : K2 → R2) at match m2 with trace t2〈m2〉= (l2〈m2〉,r2〈m2〉) and co-match m2〈t2〉. Let (R1 + L2,i1 : R1 → R1 + L2,i2 : L2 → R1 + L2) be the co-product of R1 and L2 and let {m1〈t1〉,m2} : R1 + L2 → t1@m1 be the unique morphism with {m1〈t1〉,m2}◦ i1 = m1〈t1〉 and {m1〈t1〉,m2}◦i2 = m2. Construct (e : R1 + L2 → M,s : M � t1@m1) as the (E ,S )- factorisation of {m1〈t1〉,m2} and set e1 = e◦i1 and e2 = e◦i2. Now, e1 and e2 are “jointly epic”. Construct (s1,r′1) as the pullback of (r1〈m1〉,s) and let e ′ 1 be the morphism making the dia- gram commute. Since pullbacks preserve morphisms in S , s1 ∈ S . Now, (r′1,e1) is hereditary pushout of (e′1,r1), since (i) (r1〈m1〉,s◦e1) is hereditary pushout of (r1,m1〈l1〉), (ii) (e1,idR1) is 22 Compare (C1) on page 7! 15 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras pullback of (m1〈t1〉,s), (iii) (e′1,idK1) is pullback of (m1〈l1〉,s1), and (iv) (r1,idK1) is pullback of (idR1,r1). Properties (ii) and (iii) are implied by s and s1 being monic. Construct (s ′ 1,l ′ 1) such that (l′1,s1) is pullback of (l1〈m1〉,s ′ 1) and s ′ 1 = l1〈m1〉∗(s1) and e ′′ 1 as the morphism making the diagram commute. Since also (e′1,idK1) is pullback of (m1〈l1〉,s1), (e ′′ 1,idL1) is pullback of (m1,s′1), (l1,idK1) is pullback of (idL1,l1), and final pullback complements are stable under pull- backs, l′1 = e ′′ 1 ∗(l1). Thus, (l ′ 1,r ′ 1) and e1 constitute a pushout of (l1,r1) and e ′′ 1 in C S . This implies that (t1〈m1〉,s) is pushout of (l′1,r ′ 1) and s ′ 1. Construct (s2,l′2) as the pullback of (l2〈m2〉,s) and let e ′ 2 be the morphism making the dia- gram commute such that s2 ∈ S . Since also (e′2,idK2) is pullback of (m2〈l2〉,s2), (e2,idL2) is pullback of (m2,s), and (l2,idK2) is pullback of (idL2,l2), l ′ 2 = e2 ∗(l2). Finally, let (r ′ 2,e ′′ 2) be the pushout of (r2,e′2) and s ′ 2 the morphism making the diagram commute. Since the push- out (r2〈m2〉,m2〈t2〉) is hereditary, (e′2,idK2) is pullback of (l ′ 2,s2), and (idK2,r2) is pullback of (idR2,r2), we conclude that (e ′′ 2,r ′ 2) is hereditary pushout of (e ′ 2,r2). Thus, (l ′ 2,r ′ 2) and e ′′ 2 consti- tute a pushout of (l2,r2) and e2 in C S , and (t2〈m2〉,s′2) is pushout of (l ′ 2,r ′ 2) and s. Since pushouts compose, we found the concurrent rule t2〈e2〉◦t1〈e′′1〉 and the match s ′ 1 such that (t2〈e2〉◦t1〈e′′1〉)〈s ′ 1〉= t2〈m2〉◦t1〈m1〉. The opposite of Theorem 5, i. e. that every transformation with a concurrent rule at a match in S can be decomposed into transformations with the component rules, is true in suitable categor- ies of total algebra where all pushouts are hereditary. This is no longer the case in categories of partial algebras as the following example demonstrates. Example 4 (Hidden “element”) Consider again the signature Σc of Example 2, the category A M Σc , the partial algebras A ::= As ={a}, f A = /0 and B ::= Bs ={b}, f B = ( { f B}, dBf ( f B) =∗, cBf ( f B) = b ) , and the total morphism p : A → B ::= ps(a) = b. Instantiate the diagram in Fig. 5 by L1 = L′1 = K1 = K′1 = K2 = K ′ 2 = R2 = R ′ 2 := A, R1 = L2 = M := B, l1 = l ′ 1 = e ′′ 1 = e ′ 1 = r2 = r ′ 2 = e ′ 2 = e′′2 := idA, e1 = e2 = idB, and r1 = r ′ 1 = l2 = l ′ 2 := p. These definitions result in t2 ◦ t1 : L1 → R2 = (idA,idA). Now let G = B and s′1 = p. Then t2 ◦t1 is applicable at s ′ 1 and produces the trace t2 ◦t1〈s′1〉 = (idB,idB) and the co-match s ′ 1〈t2 ◦t1〉 = p. But t1 is not applicable at s ′ 1 ◦e ′′ 1 = p, since the transformation in G M Σ results in a pushout as in Figure 3 which is not hereditary in A M Σ . Thus, the fact that not all pushouts in categories of partial algebras are hereditary hinders transfer of some theoretical results from the total case to partial algebras. This disadvantage in theory pays off in practical applications as the examples in the next section will show. 5 Rewriting of Partial Algebras: Some Applications Given a signature Σ, rewriting in A M Σ , A F Σ , and A C Γ differs in the possibilities for a rule’s left- hand side to delete hyperedges23 and the concrete application conditions stipulated by the fact 23 In A M Σ , arbitrary hyperedges (operation and/or predicate definitions) can be deleted without deleting any vertex, in A F Σ , deletion of a hyperedge requires simultaneous deletion of at least one vertex adjacent to the hyperedge (in the Selected Revised Papers from GCM 2015 16 / 21 ECEASST that a transformation requires a hereditary pushout on its right-hand side. In this section, we consider examples in A M Σ only, since the application conditions can easily be checked. Proposition 9 For rule t = (l,r) and match candidate m in A M Σ , there is a morphism m〈l〉 such that (l,m〈l〉) is pullback of (m∗(l),m), if and only if m is conflict-free, i. e. m(x) = m(y) and t defined for x implies that t is defined for y.24 Proof. Using the construction of the right adjoint in Proposition 1, it is easy to check that the co-unit of m∗ for l is an isomorphism, iff this condition holds. This result leads to the following procedure for rule application at a given match candidate: Algorithm 1 Application of rule (l : K � L,r : K → R) at match candidate m : L → G is performed in five steps: 1. Check the condition of Proposition 9! Proceed, if valid, abort otherwise! 2. Construct (m∗(l) : K∗→G) and l〈m〉 : K→K∗, such that (l〈m〉,l) is pullback of (m,m∗(l))! 3. Construct the pushout (r〈m〉 : K∗ → H,m〈t〉 : R → H) of r and l〈m〉 in GΣ! 4. Check uniqueness condition (1) on page 3 for H! 5. Finish transformation if the check in 4 is positive, rollback otherwise! sorts O, Int opns i:O --> Int ( ) +:Int,Int --> Int o i o i setset o i i' o changechange i i' Figure 6: Setting and Changing an Attribute The application condition in Algorithm 1(4), can be usefully exploited in many practical ap- plications as a condition that prevents rule application. Our first example is a simple integer attribute i that can be set or changed for objects of type O. Figure 6 shows the underlying signa- ture25 and the two rules. Note that, due to the check in Algorithm 1(4), the set-rule can only be applied in a situation where the i-attribute of o has not been set yet. If there is an old value, the change-rule must be applied. sorts O opns ≤:O,O ( ) o o reflexivereflexive transitivetransitive o o o o o o Figure 7: Reflexive/Transitive Closure domain or codomain), and, in A C Γ , deletion of a hyperedge is only possible, if the domain vertex of this hyperedge is deleted as well. 24 This condition is called conflict-freeness in [12] and [3] as well. 25 In the signature, we declare the visualisations for the operations in brackets. 17 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras The next example handles the reflexive and transitive closure of a relation on the set O. We just apply the two rules reflexive and transitive as long as there are matches. Note that the algorithm terminates, since the rule reflexive cannot add loops to objects that possess a loop already. This is again due to the application condition in Algorithm 1(4). If all “abbreviations” are added, also the rule transitive is not applicable any more. The next example in Figure 8 shows a typical copying process, here for a structure that is built up by the partial dyadic operation t. The unary predicate r marks the root of the structure to be copied. The start and the three copy rules perform the actual copy process. And the operation c keeps track of already built copies. Again, the application condition of single pushout rewriting for partial algebras guarantees that exactly one copy is made. Note that this copy mechanism works for hierarchical and even cyclic structures. sorts N ( ) opns t:N,N --> N ( ) c:N --> N ( ) r:N ( ) startstart copycopy11 copycopy11 copycopy11 copycopy22 copycopy11 copycopy33 Figure 8: Copying A situation as in the preceding example often occurs in the software engineering area of model transformation where objects in a source model must be mapped to objects in a target model. The transformation process starts with a completely undefined mapping and stops if the map- ping is sufficiently defined. Uniqueness of the mapping has to be guaranteed during the whole transformation process. This is a perfect application scenario for our new rewriting approach. As an example consider the mapping of (small) object-oriented models to relational database MT = OO + DB + opns to: Class --> Table ( ) to: Attribute --> Column ( ) to: Association --> Table ( ) Figure 9: Object-oriented Model, Relational Schema, and Inter-Model Mapping schemata. The underlying signature is depicted in Figure 9. Here, an object-oriented model Selected Revised Papers from GCM 2015 18 / 21 ECEASST (OO-part in Fig. 9) consists of classes, (untyped) attributes, and binary associations. A relational schema (DB-part in Fig. 9) comprises tables and columns. Columns can be marked as primary and/or foreign keys. The transformation signature is completed by the inter-model mapping in the MT-part in Figure 9. It specifies that classes shall be mapped to tables, attributes to columns, and associations to (junction) tables. The three rules that implement this transformation process are depicted in Figure 10. The condition in Algorithm 1(4) guarantees that the process stops if everything is mapped. Figure 10: Transformation of Classes, Attributes, and Associations The mapping of classes, attributes, and associations is one-to-one (up to some implementation details). It becomes more intricate, if inheritance comes into play. Figure 11 shows the extended object-oriented model and two variants MTI1 and MTI2 for the extension of the mapping. OOI = OO + opns super: Class --> Class ( ) MTI1= MT + OOI + opns to: Class, Class --> Table ( ) MTI2= MT + OOI + opns to: Class, Class --> ForeignKey ( ) Figure 11: Object-Orientation with Inheritance The first variant can be used to realise the pattern called Single Table Inheritance in [6], which puts a complete inheritance hierarchy into one table. The corresponding transformation rule single is depicted in Figure 12(left part).26 The second variant is appropriate for the pattern called Class Table Inheritance in [6], which implements inheritance by a foreign key constraint on the primary key of the table for the sub-class referencing the primary key of the table for the super-class. The transformation rule join for this pattern can be found in Figure 12(right part). Figure 12: Handling Inheritance 26 Note that the right-hand side of the rule is not injective! 19 / 21 Volume 73 (2016) On Single-Pushout Rewriting of Partial Algebras All examples in this section demonstrate that the built-in application condition in Single- Pushout Rewriting for Partial Algebras is useful to control termination in transformations. 6 Related Work and Conclusions We have introduced single-pushout rewriting of arbitrary partial algebras. As usual, transform- ations are defined by a single pushout of partial morphisms. Thus, general composition and de- composition properties of pushouts can be exploited for a rich theory. The new approach is built on a category of partial morphisms that does not have all pushouts. We provided a good char- acterisation of the situations which admit pushouts by hereditariness of underlying pushouts of total morphisms, compare Theorems 1, 2, and 3. Informally, pushouts can be built if the applied rule does not try to define operations where they are defined already. This application condition can easily be checked in every concrete situation. By some examples, we showed the practical relevance of the application condition for system design and the termination of derivation se- quences. Within our approach, we do not have to distinguish between graph structures (objects and links) and data structures (base-types and -operations). We can easily model associations and attributes with at-most-one-multiplicity. There are only a few articles in the literature that address rewriting of partial algebras, for example [2] and [1] for the double- and single-pushout approach resp. But both papers stay in the framework of signatures with unary operation symbols only and aim at an underlying category of partial morphisms that is co-complete. Aspects of partial algebras occur in all papers that are concerned with relabelling of nodes and edges, for example [9], or that invent mechanisms for exchanging the attribute value without deleting and adding an object, for example [7]. Most of these approaches avoid “real” partial algebras by completing them to total ones by some undefined-values. Thus, our approach is new, seems promising wrt. theoretical results, and shows some application potentials. References [1] Peter Burmeister, Miquel Monserrat, Francesc Rosselló, and Gabriel Valiente. Algebraic transformation of unary partial algebras II: single-pushout approach. Theor. Comput. Sci., 216(1-2):311–362, 1999. [2] Peter Burmeister, Francesc Rosselló, Joan Torrens, and Gabriel Valiente. Algebraic trans- formation of unary partial algebras I: double-pushout approach. Theor. Comput. Sci., 184(1- 2):145–193, 1997. [3] Andrea Corradini, Tobias Heindel, Frank Hermann, and Barbara König. Sesqui-pushout re- writing. In Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, and Grzegorz Rozenberg, editors, ICGT, volume 4178 of Lecture Notes in Computer Science, pages 30– 45. Springer, 2006. [4] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic Graph Transformation. Springer, 2006. Selected Revised Papers from GCM 2015 20 / 21 ECEASST [5] Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors. Graph Transformations - 6th International Conference, ICGT 2012, Bremen, Germany, September 24-29, 2012. Proceedings, volume 7562 of Lecture Notes in Computer Science. Springer, 2012. [6] Martin Fowler. Patterns of Enterprise Application Architecture. Addison-Wesley, 2003. [7] Ulrike Golas. A general attribution concept for models in M-adhesive transformation sys- tems. In Ehrig et al. [5], pages 187–202. [8] Annegret Habel, Reiko Heckel, and Gabriele Taentzer. Graph grammars with negative application conditions. Fundam. Inform., 26(3/4):287–313, 1996. [9] Annegret Habel and Detlef Plump. M,n-adhesive transformation systems. In Ehrig et al. [5], pages 218–233. [10] Tobias Heindel. Hereditary pushouts reconsidered. In Hartmut Ehrig, Arend Rensink, Grzegorz Rozenberg, and Andy Schürr, editors, ICGT, volume 6372 of Lecture Notes in Computer Science, pages 250–265. Springer, 2010. [11] Richard Kennaway. Graph rewriting in some categories of partial morphisms. In Hartmut Ehrig, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors, Graph-Grammars and Their Application to Computer Science, volume 532 of Lecture Notes in Computer Science, pages 490–504. Springer, 1990. [12] Michael Löwe. Algebraic approach to single-pushout graph transformation. Theor. Com- put. Sci., 109(1&2):181–224, 1993. [13] Michael Löwe. A unifying framework for algebraic graph transformation. Technical Report 2012/03, FHDW-Hannover, 2012. [14] Michael Löwe, Martin Korff, and Annika Wagner. An algebraic framework for the trans- formation of attributed graphs. In M. R. Sleep et al, editor, Term Graph Rewriting: Theory and Practice, pages 185 – 199. Wiley, 1993. [15] Michael Löwe and Marius Tempelmeier. Single-pushout rewriting of partial algebras. In Detlef Plump, editor, Proceedings of the 6th International Workshop on Graph Computa- tion Models, L’Aquila, Italy, July 20, 2015, volume 1403 of CEUR Workshop Proceedings, pages 82–96. CEUR-WS.org, 2015. [16] Miquel Monserrat, Francesc Rossello, Joan Torrens, and Gabriel Valiente. Single pushout rewriting in categories of spans I: The general setting. Technical Report LSI-97-23-R, De- partment de Llenguatges i Sistemes Informtics, Universitat Politcnica de Catalunya, 1997. [17] Marius Tempelmeier and Michael Löwe. Single-Pushout Transformation partieller Al- gebren. Technical Report 2015/1 (in German), FHDW-Hannover, 2015. 21 / 21 Volume 73 (2016) Introduction Graphs and Partial Algebras Partial Morphisms on Partial Algebras Pushouts in Arbitrary Categories of Partial Morphisms Pushouts of Partial Morphisms on Partial Algebras Rewriting of Partial Algebras: Some Theory Rewriting of Partial Algebras: Some Applications Related Work and Conclusions