We introduce Single-Pushout Rewriting for arbitrary partial algebras. Thus, we give up the usual restriction to graph structures, which are algebraic categories 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.
1 Typically, some negative application conditions [
The paper is a short version of [
hO = ⇣hfO : f G ! f H ⌘ 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 partial 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) 2 f implies b1 = b2. Instead, a partial map f : A ! B is a triple (f, df : f ! A, cf : f ! B) consisting of a set f of map entries together with two total maps df : f ! A and cf : f ! B which provide the argument and the return value for every entry respectively. The uniqueness condition (⇤) above translates to 8 e1, e2 2 f : df (e1) = df (e2) =) e1 = e2 in this set-up.
A signature ⌃ = (S, O) consists of a set of sort names S and a domain- and co-domain-indexed family of operation names O = (Ow,v)w,v2 S⇤ .3 A graph G wrt. a signature consists of a carrier set Gs (of vertices) for every sort name s 2 S and a set of hyperedges ⇣f G, dfG : f G ! Gw, cfG : f G ! Gv⌘ for every operation name f 2 Ow,v and w, v 2 S⇤ where the total mappings dfG and cfG provide the “arguments” and “return values”.4 A graph morphism h : G ! H between to graphs G and H wrt. the same signature ⌃ = (S, O) consists of a family of vertex mappings h = (hs : Gs ! Hs)s2 S and a family of edge mappings f2 O
such that for all operation names f 2 Ow,v and for 3 Note that we generalise the usual notion of signature which allows single sorts as co-domain specification for operation names only. Operation names in Ow,✏ will be interpreted as predicates, operation names in Ow,v with |v| > 1 will be interpreted as operations which deliver several results simultaneously. 4 For w 2 S⇤ and a family (Gs)s2S of sets, Gw is recursively defined by (i) G✏ = {⇤}, (ii) Gw = Gs if w = s 2 S and (iii) Gw = Gv ⇥ Gu if w = vu. all edges e 2 f G the following homomorphism condition holds:5
(h) dfH hfO(e) = hw dfG(e) and cfH hfO(e) = hv cfG(e) .
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 ⇡ BB⇥ C : B ⇥ (m,n) C ! B and ⇡ CB⇥ C : B ⇥ (m,n) C ! C: 8 s 2 S : B ⇥ (m,n) C s = {(x, y) :: ms(x) = ns(y)} 8 f 2 Ow,v : f (B⇥ (m,n)C) =
(x, y) :: mfO(x) = nfO(y) 8f 8f 2 Ow,v : d(fB⇥ (m,n)C) ::= (x, y) 7! dfB(x) ||w dfC (y) 2 Ow,v : cf(B⇥ (m,n)C) ::= (x, y) 7! cfB(x) ||v cfC (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 2 G⌃ =(S,O) is a partial algebra, if it satisfies the following condition for all f 2 O: (u) 8 e1, e2 2 f G : dfG(e1) = dfG(e2) =) e1 = e2.
The full sub-category of G⌃ consisting of all partial algebras7 is denoted by A⌃ in the following. In a partial algebra A, operation names f 2 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. Symmetrically, operation names p 2 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 operation names f 2 O✏,✏, there is only two possible interpretations in A, namely f A = ; (false) or f A = {(⇤, ⇤) } (true). Thus, f A is just a boolean flag in this case.
Due to (u) being a set of Horn-axioms, A⌃ is an epireflective sub-category of G⌃ , i. e. there is a reflection ⌘ : G⌃ ! A⌃ that maps a graph G 2 G⌃ to 5 Given a sort indexed family of mappings (fs : Gs ! Hs)s2S , f w : Gw ! Hw is recursively defined for every w 2 S⇤ by (i) f ✏ = {(⇤ , ⇤ )}, (ii) f w = fs if w = s 2 S, and (iii) f w = f v ⇥ f u, if w = vu. 6 The identity morphisms 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 name f 2 Ow,v in a partial algebra A is indeed a partial mapping: due to the uniqueness condition (u), the assignment mfaAp, dfrfAom:f AAw! tAowA, vc.fA A:nfdA, !forAav p7!artialdmfA(aep),fcfA:(eA) w::!e 2 AfvA, thperroeviisdetshea ipnavretrisael mapping f 7! f, dfA ::= (d, c) 7! d, cfA ::= (d, c) 7! c up to renaming of the elements in f A. a pair GA 2 A⌃ , ⌘ G : G ! GA such that any graph morphism h : G ! A with A 2 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 map co-limits to co-limits. In general, however, the co-limits in A⌃ do not coincide with the colimits 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 2 A⌃ , A⌃ #M A denotes the category of all sub-algebras of A. The objects in A⌃ #M A are all monomorphisms m : M ⇢ A and a morphism in A⌃ #M A from m : M ⇢ A to n : N ⇢ A is a (mono)morphism h : M ⇢ N in A⌃ such that n h = m. For every A⌃ M B ! A⌃ #M morphism g : A ! B, the inverse imageMfuBncttoor⇡ AgA⇤ ⇥ M: A: ⌃ A#⇥ (g,m) M A maps an object m : M ! B 2 A⌃ # ! 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 ⇡ AA⇥ N g⇤ (h) = ⇡ AA⇥ M and ⇡ NA⇥ N g⇤ (h) = h ⇡ MA⇥ M .
Fact 1. In a category A⌃ of partial algebras, every inverse image functor g⇤ : A⌃ #MB ! 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 inclusion morphism g⇤ (m) : g⇤ (M ) ,! B as follows:
8s 2 S : g⇤ (M )s = b 2 Bs :: 8 a 2 gs 1(b) 9 x 2 M : ms(x) = a and 8 f 2 Ow,v : f g⇤ (M) = ne 2 f B :: 8 ea 2 gfO 1 (e) 9 ex 2 M : mfO(ex) = eao , such that dfg⇤( M) = dfB |fg⇤ (M) and cfg⇤( M) = cfB |fg⇤ (M) for every operation symbol.
The co-unit " : g⇤ (g⇤ (m : M ⇢ A)) ! (m : M ⇢ A) can be defined on every element (a, b) 2 A ⇥ (g,g⇤ (m)) g⇤ (M ) by "(a, b) = c such that m(c) = a. Note that " is completely defined, since, by definition of g⇤ (m), a must have a pre-image wrt. m for every pair (a, b) 2 A ⇥ (g,g⇤ (m)) g⇤ (M ). It is uniquely defined, since m is monic. By definition of ", m that " is a morphism in A⌃ #MA.
Now, let an object x : X ⇢ B 2 A⌃ #M B and a morphism k : g⇤ (x) ! m 2 A⌃ #MA, i. e. m k = ⇡ AA⇥ (g,x)X be given. We construct k⇤ : x ! g⇤ (m) by e 7! x(e) for every e 2 X. The mappings of k⇤ are completely defined: (i) if x(e) 2/ g(A), x(e) 2 g⇤ (M ) because |g 1(x(e))| = | (g m) 1 (x(e))| = 0, and, otherwise, the existence of k with m k = ⇡ AA⇥ (g,x)X enforces that every g-preimage 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 ) " = g⇤ (g⇤ (m)) = ⇡ AA⇥ (g,g⇤ (m))g⇤ (M) which means manadpsk((aa,,ee)) =toc(0aw, ikt⇤ h(em))(.c0T) h=u s⇡,AA"⇥ ((gg⇤,x()kX⇤ ()a(a,e,e))=) =a. "S(ian,cke⇤ m(e)i)s =mocnwici,thc =m(cc0). T=hae morphism k⇤ is uniquely determined, since g⇤ (M ) ✓ B and g⇤ (m) is monic. tu 3
In order to obtain a framework for single-pushout rewriting, we proceed from the category A⌃ of partial algebras with total morphisms to the category A⌃P of partial algebras and partial morphisms. In this section, we investigate the conditions under which pushouts can be constructed in A⌃P .
A concrete partial morphism over an arbitrary complete category C is a span of C-morphisms (p : K ⇢ P, q : K ! Q) such that p is monic. Two concrete partial morphisms (p1, q1) and (p2, q2) are equivalent and denote the same abstract 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 partial morphisms CP over C has the same objects as C and abstract partial morphisms as arrows. The identities are defined by idCAP = [(idA, idA)]⌘ and composition of partial morphisms [(p : K ⇢ P, q : K ! Q)]⌘ and [(r : J ⇢ Q, s : J ! R)]⌘ is given by [(r, s)]⌘
CP [(p, q)]⌘ = [(p r0 : M ⇢ P, s q0 : M ! R)]⌘ where (M, r0 : M ⇢ K, q0 : M ! J ) is an arbitrarily chosen but fixed pullback of q and r. Note that there is the faithful embedding functor ◆ : C ! CP defined by identity on objects and (f : A ! B) 7! [idA : A ⇢ A, f : A ! B] on morphisms. We call [d : A0 ⇢ A, f : A0 ! B] a total morphism and, by a slight abuse of notation, write [d, f ] 2 C, if d is an isomorphism. From now on, we mean the abstract 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 CP of partial morphisms based on the notions final triple and hereditary pushout in the underlying category C of total morphisms. Definition 2. (Final triple) A triple for a pair ((l, r) , (p, q)) of CP-morphisms with common domain is given by a collection p, p⇤ , r, l, l⇤ , q of C-morphisms such that p⇤ , p, l⇤ , and l are monic and (i) (r, p) is pullback of (r, p⇤ ), (ii) (q, l) is pullback of (q, l⇤ ), and (iii) l p = p l. A triple p, p⇤ , r, l, l⇤ , q for ((l, r) , (p, q)) is final, if, for any other triple p0, p0 ⇤ , r0, l0, l0 ⇤ , q0 , there is a unique collection (u1, u2, u3) of C-morphisms such that (iv) p u1 = p0, (v) l u1 = l0, (vi) p⇤ u2 = p0 ⇤ , (vii) u2 r0 = r u1, (viii) l⇤ u3 = l0 ⇤ , and (ix) u3 q0 = q u1, compare left part of Fig. 1.
Definition 3. (Hereditary pushout) A pushout (q0, p0) of (p, q) in C is hereditary if for each commutative cube as in the right part of Fig. 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 monomorphisms, in the top square, (qi0, p0i) is pushout of (pi, qi), if
D0
q0 K0 p⇤
B0 i2
B pi p q0 i D0
i3 D p0 i p0
i1 C and only if, in the front faces, (p0i, i1) and (qi0, i2) are pullbacks of (i3, p0) and (i3, q0) resp. and i3 is monic.8 Fact 4. (Pushout in CP) Two partial morphisms (l : K ⇢ L, r : K ! R) and (p : P ⇢ L, q : P ! Q) have a pushout ((l⇤ , r⇤ ) , (p⇤ , q⇤ )) in CP, if and only if there is (i) a final 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 hereditary pushout (r⇤ : K⇤ ! H, q⇤ : P ⇤ ! H) for (q, r) in C, compare sub-diagrams (1) – (3) and (4) resp. in Figure 2.
L p P q Q l (1) p l (3) l⇤
K D K⇤ r (2) r r⇤ q (4)
R p⇤ q⇤ P ⇤
H
The proof can be found in [
Since A⌃ is complete, we can construct the category A⌃P of partial algebras
and partial morphisms. We use the partial product as the chosen pullback for
morphism composition, compare above. The general results about pushouts of
partial morphisms carry over to A⌃P as follows:
8 For details on hereditary pushouts see [
Proof. (Sketch) The existence of final triples follows from A⌃P being co-complete
and having right adjoints for all inverse image functors, compare Fact 1. A
detailed proof can be found in [
Corollary 6. (Pushout in A⌃P ) A pair of morphisms (l : K ⇢ L, r : K ! R) and (p : P ⇢ L, q : P ! Q) has a pushout in A⌃P , if and only if the A⌃ -pushout of (q, r) is hereditary, where l : D ! P , p : D ! K, r : D ! P ⇤ , q : D ! K⇤ , p⇤ : P ⇤ ! R, l⇤ : K⇤ ! Q is final triple of ((l, r) , (p, q)), see Figure 2. Proof. Direct consequence of Fact 4 and Proposition 5.
It is well-known that all pushouts in the category of sets and mappings and in arbitrary categories G⌃ of graphs over a given signature are hereditary. This provides the following sufficient criterion for hereditary pushouts in A⌃ . Proposition 7. (Sufficient condition) If a pushout in A⌃ is also pushout in the larger category G⌃ of graphs, then it is hereditary in A⌃ .
Proof. Let an arbitrary 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⌃ , due to A⌃ being 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, D0 together with p0i and qi0 is pushout in G⌃ . Since (i) A⌃ is closed wrt. sub-algebras, (ii) D is in A⌃ , and (iii) i3 is monic, D0 is also in A⌃ and its reflector ⌘ D0 is an isomorphism. Thus, D0 together with p0i and qi0 is pushout in A⌃ .
Let (D0, qi0, p0i) be pushout of (pi, qi) in A⌃ . Construct (D00, qi00, p00) as pushout i of (pi, qi) in G⌃ . We obtain the epic reflector ⌘ D00 : D00 ⇣ D0 with p0i = ⌘ D00 p0i0 and qi0 = ⌘ D00 qi00. Since D00 is pushout, we also get i03 : D00 ⇢ D with i03 p0i0 = p0 i1 and i03 qi00 = q0 i2. Since i3 ⌘ D00 p0i0 = i3 p0i = p0 i1 = i03 p0i0 and i3 ⌘ D00 qi00 = i3 qi0 = q0 i2 = i03 qi00, we can conclude i3 ⌘ D00 = i03. Since all pushouts in G⌃ are hereditary, i03 is monic implying that ⌘ D00 is monic as well. Thus, ⌘ D00 is an isomorphism and D0 is also the pushout in G⌃ . This immediately provides monic i3 and pullbacks in the front faces of the cube in the right part ofFig. 1. tu
But not all pushouts in A⌃ are hereditary. Here is a typical example: Example 8. Consider the signature ⌃ c = (Sc, Oc) with
Sc = {s} c Ow,v = ({f } ; w = ✏, v = s otherwise, pi b qi0s = qs0 i2s = idBs
p b L99 f B i0 = idA
i1 = idC a q0
qi = q d L99 f D d L99 f D q i3 = idD c L99 f C p0i = p0
p0
C ::= Cs = {c}, f C = {f C }, dfC (f C ) = ⇤, c fC (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}, dfD(f D) = ⇤, c fD(f D) = d and the two morphisms p0 : C ! D ::= c 7! d, f C 7! f D q0 : B ! D ::= b 7! d, f B 7! f D.
This pushout is depicted at the bottom of Fig. 3 and is not hereditary. We construct the following cube of morphisms, compare Fig. 3: A0 = A, i0 = idA, B0 is defined by Bs0 = Bs and f B0 = ;, i2 maps b in Bs0 to b in Bs, C0 = 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 (D0 = D, p0i = p0, qi0 ::= b 7! d) as the pushout of (p0, q0), we obtain i3 = idD. But (i2, qi0) is not pullback of (q0, i3): B ⇥ (q0,i3) D0 contains a defined constant for f , since i3(f D) = q0(f B), and B0 does not. tu
Note that the A⌃ -pushout of the morphisms p and q in Example 8 does not coincide with the pushout of p and q constructed in the larger category G⌃ of graphs. The pushout in G⌃ is the graph G ::= Gs = {g}, f G = {fCG, fBG}, dfG(fCG) = dfG(fBG) = ⇤, c fG(fCG) = cfG(fBG) = g together with the morphisms p00 : C ! G ::= c 7! g, f C 7! f G
C q00 : B ! G ::= b 7! g, f B 7! fBG.
The partial algebra D is the epireflection of the graph G and the reflector ⌘ G : G ! D maps as follows: g 7! d, fCG 7! f D, and f G B 7! f D. The identification ⌘ G(fCG) = ⌘ G(fBG) = f D of the reflector provided the possibility to construct the cube in Example 8 that disproves 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.
Proposition 9. (Necessary condition) If a pushout in A⌃ is hereditary, it is also pushout in the larger category G⌃ of graphs.
Proof. Let (p : A ! B, q : A ! C) be a span of morphisms in A⌃ , let (E, q00 : B ! E, p00 : C ! E) be its pushout in G⌃ , and let (q0 : B ! D, p0 : C ! D) be its pushout in A⌃ . Since A⌃ is epireflective sub-category of G⌃ , we know that D = EA, q0 = ⌘ E q00 and p0 = ⌘ E p00 where ⌘ E : E ! EA is the reflector for the graph E. Suppose D and E are not isomorphic, then there are e1 6= e2 with ⌘ E (e1) = ⌘ E (e2). We distinguish two cases: e1, e2 2 Es for some sort s 2 S and e1, e2 2 f E for some operation name f 2 Ow,v and w, v 2 S⇤ .
In the first case, construct the following commutative cube, compare right part of Fig. 1: A0, B0, and C0 have the same carrier sets as A, B, and C respectively, their operations, however, are completely undefined. The embeddings i0, i1, and i2 are identities on the carriers and empty mappings on the operations. The morphisms qi and pi coincide with q and p respectively on the carriers and are empty for all operations. Note that (qi, i0) and (pi, i0) are pullbacks of (q, i1) and (p, i2) respectively. Construct (qi0 : B0 ! D0, p0i : C0 ! D0) as the pushout of (pi, qi) in G⌃ . Since all operations are undefined, it is also pushout in A⌃ . And we know, that D0s = Es for all sorts s 2 S. Thus, e1 6= e2 in D0 and i3 is not monic.
In the second case, we can, without loss of generality, suppose Es = Ds for all sorts s 2 S. Since p0 and q0 are jointly epic, both e1 and e2 have preimages under p0 and/or q0. Let e01, e02 2 f B ] f C be those pre-images and suppose, without loss of generality, e01 2 f B. Since e1 6= e2, we conclude [e01]⌘ f 6= [ne⇣02]⌘ f , where the equivalence ⌘ f ✓ f B ] f C ⇥ f B ] f C is generated by pfO(e), qfO(e) :: e 2 f Ao. Construct the following cube à la Fig. 1(right part): ⌘ The algebras A0, B0, and C0 coincide in all carriers and operations except f with A, B, and C respectively. For f , we let f B0 = f B { e 2 [e01]⌘ f :: e 2 f B} f C0 = f C { e 2 [e01]⌘ f :: e 2 f C } f A0 = f A { e 2 f A :: qfO (e) 2 [e01]⌘ f _ pfO (e) 2 [e01]⌘ f }.
By this construction, we erase the whole structure that generated [e01]⌘ f from A, B, and C. Note that, due to [e01]⌘ f 6= [e02]⌘ f , e02 is kept in f B or f C . Let i0, i1, and i2 be the natural inclusions. And let qi and pi be the restrictions of q and p to A0. Since we erased the whole equivalence class [e01]⌘ f , (qi, i0) and (pi, i0) are pullbacks of (q, i1) and (p, i2) respectively. Let (D0, qi0, p0 ) be i the pushout of (qi, pi). Then, (i2, qi0) is not pullback of (i3, q0): By assumption, q0(e01) = e1 = i3(x) where x = qi0(e02) or x = p0i(e02). The function entry e0 , 1 however, does not possess a pre-image under i2. tu Theorem 10. A pushout in A⌃ is hereditary, if and only if it is pushout in G⌃ . Proof. Direct consequence of Propositions 7 and 9.
Corollary 11. Morphisms (l : K ⇢ L, r : K ! R) and (p : P ⇢ L, q : P ! Q) have a pushout in A⌃P , if and only if the A⌃ -pushout of (q, r) is pushout in G⌃ , where l, p, r, q, p⇤ , l⇤ is final triple for ((l, r) , (p, q)), compare Figure 2. 4
In this section, we introduce single-pushout rewriting of partial algebras. We restrict rules to partial morphisms (l : K ⇢ L, r : K ⇢ R) that do not identify items, i. e. the right-hand side of which are injective. Furthermore, we only allow matches that produce total co-matches. For this set-up, we can characterise the application conditions stipulated by the absence of some pushouts in categories of partial algebras with partial morphisms. And we can show a close connection of single-pushout and sesqui-pushout rewriting. In the following, let A⌃P be a category of partial algebras and partial morphisms with respect to a given signature ⌃ = ⇣S, (Ow,v)w,v2 S⇤ ⌘.
Definition 12. (Rule, match, and transformation) A transformation rule t is a partial morphism t = (l : K ⇢ L, r : K ⇢ R) the right-hand side r of which is injective. A match for a rule t : L ! R in a host algebra G is a total morphism m : L ! G. A direct transformation with a rule t : L ! R at a match m : L ! G from algebra G to algebra t@m exists if there is a total co-match m hti : R ! t@m and a partial trace t hmi : G ! t@m, such that (t hmi , m hti) is pushout of t and m in A⌃P .
There are two reasons why a transformation with a rule r at a match m
cannot be performed: (i) There is no pushout of t and m in A⌃P and (ii) the
comatch in the pushout of t and m is not total. Therefore, we have some application
conditions as in the double-pushout approach [
L G m s⇤ s x z
K D m⇤ w w⇤ K⇤ mhli (4) r r⇤
R
mhti 2. the rule does not add operation definitions that are already present in the host graph G, i. e. for all w, v 2 S⇤ , f 2 Ow,v, x 2 Lw, eR 2 f R, eG 2 f G : dfR(eR) = tw(x) ^ dfG(eG) = mw(x) =) 9 eL 2 f L : m(eL) = eG, 3. and the match does not identify domains of different added operation definitions, i. e. for all w, v 2 S⇤ , f 2 Ow,v, e1 6= e2 2 f R : m htiw dfR(e1) = m htiw dfR(e2) =) 9 e01 2 f L : e1 = tfO(e01).
Note that the second clause above also implies t(eL) = eR and the third clause also implies 9e 02 : e2 = tfO(e02).
Proof. The first condition is the well-known condition which is called
conflictfree in [
Since we restricted transformations to total co-matches, we obtain a close
connection of our transformations to Sesqui-Pushout Rewritings in the sense of
[
k A C n idC idC idA B
n⇤ D k k⇤ is total. It remains to show that hereditary pushouts along monomorphisms are final pullback complements as well: Let (k⇤ , n⇤ ) be hereditary pushout of n and monic k. We construct the commutative cube in Fig. 5, in which the morphisms k, idC , and idA are monic, the top and left face are pullbacks and the back face is pushout. By (k⇤ , n⇤ ) being hereditary, the bottom and the right face are pullbacks and k⇤ is monic. Moreover in the left face, (idC , n) is final pullback complement of (n, idA) and the back face is hereditary. Thus, the left and the back face constitute a pushout in the category of partial morphisms. The front face is hereditary and, therefore, pushout in the category of partial morphisms. Since (idA, idA) = (k, idA) (idA, k) and (idC , idC ) = (k⇤ , idC ) (idC , k⇤ ), the right face must be pushout in the category of partial morphisms and (k⇤ , n) must be final pullback complement of (n⇤ , k). tu
Thus, single-pushout rewriting with right-linear rules and total co-matches is
almost Sesqui-Pushout Rewriting. This analysis provides good chances to
reestablish most of the theory known for the single- and the sesqui-pushout approach,
for example with respect to parallel and sequential independence, concurrency,
and amalgamation. And it shows that our approach is closely connected to some
other current research lines, for example [
Example 16. (Transformation Decomposition) In the standard single-pushout approach at injective matches, rule decomposition carries over to transformations: If a rule t can be decomposed into two rules t1 and t2, i. e. t = t2 t1, every transformation with rule t at an injective match m can be decomposed into a transformation with t1 followed by a transformation with t2, such that t hmi = t2 hm ht1ii t1 hmi and m hti = (m ht1i) ht2i. This is no longer true in the new set-up. Consider again the signature of Example 8, the partial algebras L ::= Ls = {l}, f L = ;, E ::= Es = {e}, f E = {f E }, dfE (f E ) = ⇤, c fE (f E ) = e , R ::= Rs = {r}, f R = ;, and
G ::= Gs = {g}, f G = {f G}, dfG(f G) = ⇤, c fG(f G) = g , the rules t1 : L ! E ::= l 7! e and t2 : E ! R ::= e 7! r, and the match m : L ! G ::= l 7! g. Note that t2 is partial, since it does not map the operation definition in E. Since t2 t1 : L ! R is a rule without new operation definitions in R, there is the transformation (t2 t1) @m. The rule t1, however, cannot be applied at m due to a violation of the second condition in Proposition 13. tu
The careful analysis of these new features is left to future research. 5
The new behaviour discovered in Example 16, can be usefully exploited in many practical applications as a condition that prevents rule application. Our first sorts O, Int opns i:O --> Int ( +:Int,Int --> Int ) o i set o i o i i' change o i i' example is a simple integer attribute i that can be set or changed for objects of type O. Figure 6 shows the underlying signature10 and the two rules. Note that the set-rule can only be applied in a situation where the i-attribute of o has not been set yet, compare the second condition in Proposition 13. If there is an old value, the change-rule must be applied.
sorts O opns ≤:O,O ( ) o reflexive o o o o transitive o o o
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, compare the second condition in Proposition 13. If all abbreviations are added, also the rule transitive is not applicable any more.
The last example shows a typical copying process, here for a tree structure, compare Figure 8. The partial dyadic operation t builds up trees, the unary predicate r marks the root for the copy process, the start and the three copy rules perform the copy process, and the operation c keeps track of already built copies. Again, the application conditions of single pushout rewriting for partial 10 In the signature, we declare the visualisations for the operations in brackets. sorts N opns t:N,N --> N ( c:N r:N --> N ( ( ( ) ) ) ) start cocpoyp2y1 algebras guarantee that exactly one copy is made. Note that this copy mechanism also works if t builds up arbitrary hierarchical or even cyclic structures.
This last example describes a typical software engineering situation in the area of model transformation: some structured model, for example a class model, has to be transformed into another structured system, for example a relational database. In this context, keeping track of already finished transformations is essential for the control flow of the transformation process and to avoid that some parts are performed twice.
More detailed examples in this area can be found in [
We have introduced single-pushout rewriting of arbitrary partial algebras. As
usual, transformations are defined by a single pushout of partial morphisms.
Thus, general composition and decomposition 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 characterisation
of the situations which admit pushouts by hereditariness of underlying pushouts
of total morphisms, compare Theorem 10. 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 conditions for
system design and the termination of derivation sequences. (More examples can be
found in [
There are only a few articles in the literature that address rewriting of partial
algebras, for example [
Aspects of partial algebras occur in all papers that are concerned with
relabelling of nodes and edges, for example [