=Paper=
{{Paper
|id=Vol-1403/paper7
|storemode=property
|title=Single-Pushout Rewriting of Partial Algebras
|pdfUrl=https://ceur-ws.org/Vol-1403/paper7.pdf
|volume=Vol-1403
|dblpUrl=https://dblp.org/rec/conf/gg/LoweT15
}}
==Single-Pushout Rewriting of Partial Algebras==
https://ceur-ws.org/Vol-1403/paper7.pdf
Single-Pushout Rewriting of Partial Algebras
Michael Löwe ⇤ and Marius Tempelmeier †
⇤
Fachhochschule für die Wirtschaft (FHDW) Hannover
†
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 categories with unary operators only. By this general-
isation, we obtain an integrated and straightforward treatment of graph-
ical 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 con-
structive use of it in some practical examples.
1 Introduction
The current frameworks for the (algebraic) transformation of typed graphs are
not completely satisfactory from the software engineering perspective. For ex-
ample, it is hardly possible to specify 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 transformation of attributed graphs, compare for example [5,13], 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 infinite-
ness of rules stipulated by the infiniteness of the term algebra which is typic-
ally 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 algeb-
ras. In this paper, we use partial algebras instead as the underlying category
for single-pushout rewriting. In partial algebras, operation definitions can be
1
Typically, some negative application conditions [8] are employed to handle these
requirements making the framework more complicated.
2
In object-oriented programming languages, for example, attributes have the standard
multiplicity 0..1.
changed without deleting and adding an object (edge). Thus, we get a straight-
forward 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 seam-
less integration of structure and data. Finally, partial term algebras in the rules
help to keep rules finite.
The paper is a short version of [15], where many more examples and de-
tails can be found. Section 2 introduces our concept of partial algebra. We show
explicitly the similarities between partial algebras and hypergraphs. Section 3
provides sufficient and necessary conditions for the existence of pushouts in cat-
egories of partial algebras and partial morphisms. It contains our main results.
Section 4 defines the new single-pushout approach and shows similarities and
differences to the sesqui-pushout approach [3]. Section 5 demonstrates by some
example that the new application conditions are useful in many situations. Fi-
nally, 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 algeb-
ras. 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 8e1 , 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,v2S ⇤ .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 , dG f :f
G
! Gw , c G
f :f
G
! Gv for every
operation name f 2 Ow,v and w, v 2 S ⇤ where the total mappings dG f and cf
G
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
⌘ h = (hs : Gs ! Hs )s2S and a family of edge mappings
family⇣of vertex mappings
hO = h O
f :f
G
! fH such that for all operation names f 2 Ow,v and for
f 2O
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) dH O
f hf (e) = h
w
dG H O
f (e) and cf hf (e) = h
v
cG
f (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
m n
co-span B ! A C is given by the partial product B ⇥(m,n) C with the two
B⇥C B⇥C
projection morphisms ⇡B : B ⇥(m,n) C ! B and ⇡C : B ⇥(m,n) C ! C:
8s 2 S : B ⇥(m,n) C s = {(x, y) :: ms (x) = ns (y)}
8f 2 Ow,v : f (B⇥(m,n) C ) = (x, y) :: mO O
f (x) = nf (y)
(B⇥(m,n) C )
8f 2 Ow,v : df ::= (x, y) 7! dB w C
f (x) || df (y)
(B⇥(m,n) C )
8f 2 Ow,v : cf ::= (x, y) 7! cB v C
f (x) || cf (y),
w
where the operator ||w : B w ⇥ C w ! (B ⇥ C) 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) 8e1 , e2 2 f G : dG G
f (e1 ) = df (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 ! H w 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 com-
position 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
f A , dA
f : f
A
! Aw , c A
f : f
A
! Av 7! dA A
f (e), cf (e) :: e 2 f
A
provides a partial
map from Aw to Av . And, for a partial map f : Aw ! Av , there is the inverse
mapping f 7! f, dA f ::= (d, c) 7! d, cf ::= (d, c) 7! c up to renaming of the elements
A
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 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 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⌃ -
morphism g : A ! B, the inverse image functor g ⇤ : A⌃ #M B ! A⌃ #M
A⇥M
A maps an object m : M ! B 2 A⌃ #M B to ⇡A : A ⇥(g,m) M ! A
and a morphism h : (m : M ! B) ! (n : N ! B) to the uniquely determined
A⇥N A⇥M
morphism g ⇤ (h) : A ⇥(g,m) M ! A ⇥(g,n) N such that ⇡A g ⇤ (h) = ⇡A
A⇥N A⇥M
and ⇡N g (h) = h ⇡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
n 1
o
8f 2 Ow,v : f g⇤ (M ) = e 2 f B :: 8 ea 2 gfO (e) 9 ex 2 M : mO f (e x ) = e a ,
g g
such that df⇤(M ) = dBf |f g⇤ (M ) and cf
⇤(M )
f |f g⇤ (M ) for every operation symbol.
= cB
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
A⇥ g⇤ (M )
is monic. By definition of ", m " = g ⇤ (g⇤ (m)) = ⇡A (g,g⇤ (m)) which means
that " is a morphism in A⌃ #MA.
Now, let an object x : X ⇢ B 2 A⌃ #M B and a morphism k : g ⇤ (x) !
A⇥ X
m 2 A⌃ #M A, i. e. m k = ⇡A (g,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
1
x(e) 2/ g(A), x(e) 2 g⇤ (M ) because |g 1 (x(e))| = | (g m) (x(e))| = 0, and,
A⇥ X
otherwise, the existence of k with m k = ⇡A (g,x) enforces that every g-pre-
image of x(e) has a pre-image under m. By definition, g⇤ (m) k ⇤ = x. By defini-
tion 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
A⇥ X
and k(a, e) = c0 with m(c0 ) = ⇡A (g,x) (a, e) = a. Since m is monic, c = c0 . The
morphism k ⇤ is uniquely determined, since g⇤ (M ) ✓ B and g⇤ (m) is monic. t u
3 Partial Morphisms on Partial Algebras
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 AP ⌃
of partial algebras and partial morphisms. In this section, we investigate the
conditions under which pushouts can be constructed in AP ⌃.
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 ab-
stract 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 C P over C
has the same objects as C and abstract partial morphisms as arrows. The iden-
P
tities are defined by idCA = [(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)]⌘ C P [(p, q)]⌘ = [(p r0 : M ⇢ P, s q 0 : M ! R)]⌘
where (M, r0 : M ⇢ K, q 0 : M ! J) is an arbitrarily chosen but fixed pullback of
q and r. Note that there is the faithful embedding functor ◆ : C ! C P 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 C P 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 C P -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 , q 0 , 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 q 0 = q u1 , compare
left part of Fig. 1.
Definition 3. (Hereditary pushout) A pushout (q 0 , p0 ) of (p, q) in C is heredit-
ary 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
l r qi
L K R A0 C0
pi
p p p⇤ i0 i1
p0i
l p0 r ⇤
p0 ⇤ 0 0
P D P B D
qi0
u1 u2
l0
0 r0 q
q q D P0 A C
i2 p i3
p0
l⇤
Q K⇤ q0 B D
q0
u3
l0 ⇤
K0
Figure 1. Final Triple and Hereditary Pushout
and only if, in the front faces, (p0i , i1 ) and (qi0 , i2 ) are pullbacks of (i3 , p0 ) and
(i3 , q 0 ) resp. and i3 is monic.8
Fact 4. (Pushout in C P ) Two partial morphisms (l : K ⇢ L, r : K ! R) and
(p : P ⇢ L, q : P ! Q) have a pushout ((l⇤ , r⇤ ) , (p⇤ , q ⇤ )) in C P , 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 r
L K R
p (1) p (2) p⇤
l r
P D P⇤
q (3) q (4) q⇤
Q K⇤ H
l⇤ r⇤
Figure 2. Pushout in G P
The proof can be found in [14]. A version of the proof that does not pre-
suppose a choice of pullbacks that is compatible with pullback composition and
decomposition is contained in [15].
Since A⌃ is complete, we can construct the category AP ⌃ 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 AP ⌃ as follows:
8
For details on hereditary pushouts see [10,11]
Proposition 5. (Final triple) Every pair ((l, r) , (p, q)) of AP
⌃ -morphisms with
common domain has a final triple.
Proof. (Sketch) The existence of final triples follows from AP
⌃ being co-complete
and having right adjoints for all inverse image functors, compare Fact 1. A de-
tailed proof can be found in [15].
Corollary 6. (Pushout in AP ⌃ ) A pair of morphisms (l : K ⇢ L, r : K ! R)
and (p : P ⇢ L, q : P ! Q) has a pushout in AP ⌃ , 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 , p00i ) as pushout
of (pi , qi ) in G⌃ . We obtain the epic reflector ⌘D00 : D00 ⇣ D0 with p0i = ⌘D00 p00i
and qi0 = ⌘D00 qi00 . Since D00 is pushout, we also get i03 : D00 ⇢ D with i03 p00i =
p0 i1 and i03 qi00 = q 0 i2 . Since i3 ⌘D00 p00i = i3 p0i = p0 i1 = i03 p00i
and i3 ⌘D00 qi00 = i3 qi0 = q 0 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. t
u
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 {f } w = ✏, v = s
Ow,v =
; otherwise,
qi = q
a c L99 f C
pi
i0 = idA i1 = idC
p0i = p0
b d L99 f D
qi0 s = qs0
q
a c L99 f C
i2 s = idBs p i3 = idD
p0
b L99 f B
d L99 f D
q0
Figure 3. Simple Non-Hereditary Pushout in A⌃
the three algebras
A ::= As = {a}, f A = ;,
B ::= Bs = {b}, f B = {f B }, dB B B B
f (f ) = ⇤, cf (f ) = b ,
C ::= Cs = {c}, f C = {f C }, dC C C C
f (f ) = ⇤, cf (f ) = c ,
and the two morphisms p : A ! B ::= a 7! b and q : A ! C ::= a 7! c.
The pushout of (p, q) in AP
⌃ c consists of the algebra
D ::= Ds = {d}, f D = {f D }, dD D D D
f (f ) = ⇤, cf (f ) = d
and the two morphisms
p0 : C ! D ::= c 7! d, f C 7! f D
q 0 : 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 , B 0
0
is defined by Bs0 = Bs and f B = ;, i2 maps b in Bs0 to b in Bs , C 0 = 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 , q 0 ), we obtain i3 = idD . But (i2 , qi0 ) is not pullback of (q 0 , i3 ): B ⇥(q0 ,i3 ) D0
contains a defined constant for f , since i3 (f D ) = q 0 (f B ), and B 0 does not. t
u
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 }, dG G G G G G G G
f (fC ) = df (fB ) = ⇤, cf (fC ) = cf (fB ) = g
together with the morphisms
p00 : C ! G ::= c 7! g, f C 7! fCG
q 00 : 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 fBG 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, q 00 :
B ! E, p00 : C ! E) be its pushout in G⌃ , and let (q 0 : B ! D, p0 : C ! D) be
its pushout in A⌃ . Since A⌃ is epireflective sub-category of G⌃ , we know that
D = E A , q 0 = ⌘E q 00 and p0 = ⌘E p00 where ⌘E : E ! E A 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 , B 0 , and C 0 have the same carrier sets as A, B, and C respect-
ively, 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 : B 0 ! D0 , p0i : C 0 ! 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 q 0 are jointly epic, both e1 and e2 have pre-
images under p0 and/or q 0 . Let e01 , e02 2 f B ] f C be those pre-images and sup-
pose, without loss of generality, e01 2 f B . Since e1 6= e2 , we conclude [e01 ]⌘f 6=
[e02 ]⌘f , where the
n⇣ ⌘ equivalence
o ⌘f ✓ f B ] f C ⇥ f B ] f C is generated by
pO O
f (e), qf (e) :: e 2 f
A
. Construct the following cube à la Fig. 1(right part):
The algebras A0 , B 0 , and C 0 coincide in all carriers and operations except f with
A, B, and C respectively. For f , we let
0
fB = fB {e 2 [e01 ]⌘f :: e 2 f B }
0
fC = fC {e 2 [e01 ]⌘f :: e 2 f C }
0
fA = fA {e 2 f A :: qfO (e) 2 [e01 ]⌘f _ pO 0
f (e) 2 [e1 ]⌘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 , p0i ) be
the pushout of (qi , pi ). Then, (i2 , qi0 ) is not pullback of (i3 , q 0 ): By assumption,
q 0 (e01 ) = e1 = i3 (x) where x = qi0 (e02 ) or x = p0i (e02 ). The function entry e01 ,
however, does not possess a pre-image under i2 . t
u
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 AP ⌃ , 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 Single-Pushout Rewriting of Partial Algebras
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 connec-
tion of single-pushout and sesqui-pushout rewriting. In the following, let AP ⌃ be
a category of partial
⇣ algebras and
⌘ partial morphisms with respect to a given
signature ⌃ = S, (Ow,v )w,v2S ⇤ .
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 AP
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 AP ⌃ and (ii) the co-
match in the pushout of t and m is not total. Therefore, we have some application
conditions as in the double-pushout approach [5]. Since we restricted the rules
to right-hand sides which do not identify any items, the application conditions
can easily be characterised.9
Proposition 13. (Application conditions) A transformation with a rule t : L !
R at a match m : L ! G exists, if and only if
1. the match does not identify items that are preserved with items that are
deleted by the rule, i. e. for all x 6= y 2 L : m(x) = m(y) and t defined for x
implies that t is also defined for y,
9
Note that Definition 12 can be generalised to arbitrary right-hand sides in rules. In
the general case, however, the application condition introduced by the requirement
that participating pushouts are hereditary is more complex.
K0
x w
l r
L K L K R
s⇤
m m ⇤ y m (3) mhli (4) mhti
s
G D G K⇤ t@m
l⇤ r⇤
z w⇤
D0
Figure 4. Single- versus Sesqui-Pushout Transformation
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 :
dR w G w L
f (eR ) = t (x) ^ df (eG ) = m (x) =) 9eL 2 f : m(eL ) = eG ,
3. and the match does not identify domains of different added operation defin-
itions, i. e. for all w, v 2 S ⇤ , f 2 Ow,v , e1 6= e2 2 f R :
w w
m hti dR
f (e1 ) = m hti dR
f (e2 ) =) 9e01 2 f L : e1 = tO 0
f (e1 ).
Note that the second clause above also implies t(eL ) = eR and the third
clause also implies 9e02 : e2 = tO 0
f (e2 ).
Proof. The first condition is the well-known condition which is called conflict-
free in [12] that characterises matches that produce pushouts in G⌃ with total
co-match. Conditions 2 and 3 translate the result of Corollary 11 to the concrete
situation where r is monic and p, p, and p⇤ are isomorphisms. t
u
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.
Definition 14. (Final Pullback Complement) In a pullback (s⇤ , m⇤ ) of (m, s),
compare left part of Fig. 4, the pair (s, m⇤ ) constitutes a final pullback comple-
ment of (m, s⇤ ), if for any other pullback (x, y) of (m, z) and morphism w such
that s⇤ w = x there is a unique morphism w⇤ with s w⇤ = z and w⇤ y = m⇤ w.
Theorem 15. (Single- and Sesqui-Pushout Transformation) Given a rule t =
(l : K ⇢ L, r : K ⇢ R), a match m : L ! G, and a direct transformation
(m hti , t hmi = (l⇤ : K ⇤ ⇢ G, r⇤ : K ⇤ ⇢ t@m)), then there is a total morphism
m hli : K ! K ⇤ such that (l⇤ , m hli) and (r⇤ , m hli) are final pullback comple-
ments of (m, l) and (m hti , r) resp., compare (3) and (4) in Fig. 4.
Proof. That (l⇤ , m hli) is final pullback complement of (m, l) is a direct con-
sequence of the construction of final triples in [15] and the fact that the co-match
idA
A A
idA
n k n
A B
k
idC
C C
n idC n⇤
k⇤
C D
k⇤
Figure 5. Hereditary Pushout and Final Pullback Complement
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). t
u
Thus, single-pushout rewriting with right-linear rules and total co-matches is
almost Sesqui-Pushout Rewriting. This analysis provides good chances to rees-
tablish 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 [4]. But the application conditions for
transformations in AP ⌃ in Proposition 13 also produce some new and unfamiliar
behaviour, for example if decomposition of rules is concerned.
Example 16. (Transformation Decomposition) In the standard single-pushout
approach at injective matches, rule decomposition carries over to transforma-
tions: 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 ht1 ii t1 hmi and m hti = (m ht1 i) ht2 i. 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 }, dE E E E
f (f ) = ⇤, cf (f ) = e ,
R ::= Rs = {r}, f R = ;, and
G ::= Gs = {g}, f G = {f G }, dG G G G
f (f ) = ⇤, cf (f ) = 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. t
u
The careful analysis of these new features is left to future research.
5 Examples
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
i change i
opns i:O --> Int ( ) o i set o i o o
i' i'
+:Int,Int --> Int
Figure 6. Setting and Changing an Attribute
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 transitive
o o o o o o
Figure 7. Reflexive/Transitive Closure
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 con-
dition 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 ( ) start copy
copy 1 1
opns t:N,N --> N ( )
c:N --> N ( )
copy
copy 2 1 copy
copy 3 1
r:N ( )
Figure 8. Copying
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 [15].
6 Related Work and Conclusions
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 sys-
tem design and the termination of derivation sequences. (More examples can be
found in [15].) 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 that is co-complete.
Aspects of partial algebras occur in all papers that are concerned with re-
labelling of nodes and edges, for example [9], or that invent mechanisms for
exchanging the attribute value without deleting and adding an object, for ex-
ample [7]. Most of these approaches avoid “real” partial algebras by completing
them to total ones by some undefined-values.
Thus, our approach is new, shows some application potentials, and seems
promising wrt. theoretical results.
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. Algeb-
raic transformation 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 rewriting. 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. Vincent Danos, Tobias Heindel, Ricardo Honorato-Zimmer, and Sandro Stucki.
Reversible sesqui-pushout rewriting. In Graph Transformation - 7th International
Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014.
Proceedings, pages 161–176, 2014.
5. Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundament-
als of Algebraic Graph Transformation. Springer, 2006.
6. Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, and Grzegorz Rozenberg, ed-
itors. Graph Transformations - 6th International Conference, ICGT 2012, Bremen,
Germany, September 24-29, 2012. Proceedings, volume 7562 of Lecture Notes in
Computer Science. Springer, 2012.
7. Ulrike Golas. A general attribution concept for models in M-adhesive transforma-
tion systems. In Ehrig et al. [6], 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. [6], pages 218–233.
10. Tobias Heindel. Hereditary pushouts reconsidered. In Hartmut Ehrig, Arend Ren-
sink, 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.
Comput. Sci., 109(1&2):181–224, 1993.
13. Michael Löwe, Martin Korff, and Annika Wagner. An algebraic framework for the
transformation of attributed graphs. In M. R. Sleep et al, editor, Term Graph
Rewriting: Theory and Practice, pages 185 – 199. Wiley, 1993.
14. Miquel Monserrat, Francesc Rossello, Joan Torrens, and Gabriel Valiente. Single
pushout rewriting in categories of spans I: The general setting. Technical Re-
port LSI-97-23-R, Department de Llenguatges i Sistemes Informtics, Universitat
Politcnica de Catalunya, 1997.
15. Marius Tempelmeier and Michael Löwe. Single-Pushout Transformation partieller
Algebren. Technical Report 2015/1 (in German), FHDW-Hannover, 2015.