SPO-Rewriting of Constrained Partial Algebras

Abstract

Recently, single-pushout rewriting (SPO) has been applied to arbitrary partial algebras (PA). On the one hand, this allows a simple and straightforward integration of (base type) attributes into graph transformation. On the other hand, SPO-PA-rewriting comes equipped with an easy-to-check application condition, namely that an operation cannot be defined twice on the same set of arguments. This provides very natural termination criteria for example in model transformation.

In this paper, we generalise this approach to constrained partial algebras. We allow two different types of constraints, namely (i) requiring some operations to be total and (ii) enforcing some consistency conditions on the algebras by suitable conditional equations. We show that this generalisation again induces an easy to check application condition and provides considerably more expressive power: For example, constraints allow a straightforward algebraic model for the object-oriented concept of inheritance with runtime specialisation and generalisation of objects.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In [18, 20], we introduced single-pushout rewriting (SPO) in categories of partial morphisms over partial algebras (PA) wrt. arbitrary signatures. Therefore, we gave up the usual restriction of SPO-rewriting to graph structures which are signatures with unary operation symbols only, compare [13]. Categories of partial morphisms constructed over graph structures have an initial object and all pushouts, which means that all finite co-limits can be constructed. This property leads to a rich theory, compare again [13]. This is no longer the case if we admit constants and operation symbols with more than one argument even if we pass from total to partial algebras.

Partial algebras, however, allow a simple reduction to total graph structures which are constrained by a set of Horn-formulas. The reduction provides an easy to check and characterising condition for the existence of pushouts of partial morphisms, namely that the pushout of partial algebras coincides with the pushout constructed in the underlying graph structure.¹

In this paper, we discuss which types of additional constraints on categories of partial algebras preserve this property that the operational semantics is just well-known rewriting of graph structures. We present two types of such constraints. The first type uses arbitrary conditional equations, which can for example be used to specify that some operations are injective or that different compositions of operations lead to the same result if applied to the same argument.² The second type of constraints discussed in this paper specifies that some unary operations shall be total, i.e. defined for all arguments. Total and injective operations can be used to model the object-oriented concept of inheritance by sub-type inclusions, compare Sect. 5.

The paper is structured as follows. In Sect. 2, we recapitulate our notion of partial algebra and the reduction to hierarchical graph structures. Section 3 presents and generalises the results of [18] concerning existence and characterisation of pushouts in categories of partial morphism over partial algebras. On the basis of these results, the main Sect. 4 introduces new constraints which preserve the operational semantics of SPO-rewriting for graph structures and, therefore, can be interpreted as global application conditions. Section 5 demonstrates the gain in expressive power which we obtain by using constrained partial algebras. Finally, Sect. 6 discusses related word and future research issues.

2 Partial Algebras and Hypergraphs

A signature $\varSigma =\left( S,O\right)$ consists of a set of sort names S and a domain- and co-domain-indexed family of operation names $O=\left( O_{w,v}\right) _{w,v\in S^{*}}$. A partial $\varSigma$ -algebra $A=\left( A_{S},O^{A}\right)$ is a family $A_{S}=\left( A_{s}\right) _{s\in S}$ of carrier sets together with a partial map $o^{A}:A^{w}\rightarrow A^{v}$ for every operation symbol $o\in O_{w,v}$ with $w,v\in S^{*}$.³

A homomorphism $h:A\rightarrow B$ between two partial algebras A and B wrt. the same signature $\varSigma =\left( S,O\right)$ is a family of mappings $h=\left( h_{s}:A_{s}\rightarrow B_{s}\right) _{s\in S}$, such that, for all operation symbols $o\in O_{w,v}$, the following condition is satisfied: If $o^{A}(x)$ is defined in A for $x\in A^{w}$, then $o^{B}(h^{w}(x))$ is defined in B and $h^{v}\left( o^{A}(x)\right) =o^{B}\left( h^{w}(x)\right)$.⁴ A homomorphism $h=\left( h_{s}:A_{s}\rightarrow B_{s}\right) _{s\in S}$ is closed, if we have for every operation $o\in O_{w,v}$: Whenever $o^{B}$ is defined for $h^{w}(x)$ there is $x'\in A^{w}$ with $h^{w}(x)=h^{w}(x')$ and $o^{A}$ is defined for $x'$.⁵

The category of all partial $\varSigma$-algebras and all homomorphisms between them is denoted by $\mathcal {A}_{\varSigma }$. By $\underline{\mathcal {A}}_{\varSigma }$ we denote the subcategory of all total $\varSigma$-algebras. Note that all homomorphisms in $\underline{\mathcal {A}}_{\varSigma }$ are closed.

A (constructive) $\varSigma$-contraint is given by an epimorphism $c:P\twoheadrightarrow C$ from a $\varSigma$-algebra P, called the premise, to a $\varSigma$-algebra C which is called the conclusion. A homomorphism $h:P\rightarrow A$ solves the constraint $c:P\twoheadrightarrow C$, written $h\,\models \, c$, if there is homomorphism $h^{*}:C\rightarrow A$ such that $h^{*}\circ c=h$. An algebra A satisfies a constraint $c:P\twoheadrightarrow C$, written $A\,\models \, c$, if every morphism $h:P\rightarrow A$ solves c. Given a set $\mathfrak {C}$ of $\varSigma$-constraints, $\mathcal {A}_{\varSigma ,\mathfrak {C}}$ denotes the full sub-category of $\mathcal {A}_{\varSigma }$ of all algebras that satisfy all the constraints $c\in \mathfrak {C}$. Such a category specified by $\varSigma$-constraints is called a quasi-variety. It is well-known that a full sub-category of $\mathcal {A}_{\varSigma }$ is a quasi-variety, if and only if it is an epi-reflective sub-category of $\mathcal {A}_{\varSigma }$.⁶ Typically, a constraint is syntactically presented as an implication from a syntactical presentation of the premise to a syntactical presentation of the conclusion.

By contrast to total algebras, epimorphisms in categories of partial algebras need not be surjective in each component.⁷ Thus, constraints can express some definedness requirements. Consider as an example the (unconditional) clause $\mathtt {x\in S:f(f(x))=f(x)}$ for a signature $\mathtt {\varSigma }$ with an operation symbol $\mathtt {f:S\rightarrow S}$. It requires $\mathtt {f}$ to be idem-potent and total.

Given a signature $\varSigma =\left( S,O\right)$, $\varSigma ^{\mathrm {u}}=\left( S^{\mathrm {u}},O^{\mathrm {u}}\right)$ denotes the underlying graph structure which is defined on sorts by:

$$\begin{aligned} S^{\mathrm {u}}= & {} S\uplus \biguplus _{w,v\in S^{*}}O_{w,v}. \end{aligned}$$

For every operation symbol $o\in O_{s_{1}\dots s_{j}\,,\,s_{j+1}\dots s_{j+k}}$ in $\varSigma$ with $j,k\ge 0$, $O_{o,s_{i}}^{\mathrm {u}}$ contains an operation symbol $\mathrm {d}_{i}^{o}$ for $1\le i\le j$ and $O_{o,s_{j+i}}^{\mathrm {u}}$ contains an operation symbol $\mathrm {c}_{i}^{o}$ for $1\le i\le k$.⁸ There are no other operation symbols in $O^{\mathrm {u}}$.

Note that the signature $\varSigma ^{\mathrm {u}}=\left( S^{\mathrm {u}},O^{\mathrm {u}}\right)$ constitutes a hierarchical graph structure in the sense of [13].⁹ In $S^{\mathrm {u}}$, the sorts in S are on level 0 and the sorts in $\biguplus _{w,v\in S^{*}}\!O_{w,v}$ are on level 1. All operations in $O^{\mathrm {u}}$ are unary and map from sorts on level 1 to sorts on level 0. Thus, a total algebra wrt. $\varSigma ^{\mathrm {u}}=\left( S^{\mathrm {u}},O^{\mathrm {u}}\right)$ can be interpreted as a hypergraph having vertices typed in $S^{\mathrm {u}}$ and hyperedges typed in $O^{\mathrm {u}}$.

Let $\mathcal {G}_{\varSigma }$ denote the category of all total $\varSigma ^{\mathrm {u}}$-algebras and $\varSigma ^{\mathrm {u}}$-homomorphisms, i.e. $\mathcal {G}_{\varSigma }$ is short for $\underline{\mathcal {A}}_{\varSigma ^{\mathrm {u}}}$.¹⁰ Then there is a full and faithful functor $\gamma :\mathcal {A}_{\varSigma }\rightarrow \mathcal {G}_{\varSigma }$ mapping each partial algebra $A\in \mathcal {A}_{\varSigma }$ to $\gamma (A)\in \mathcal {G}_{\varSigma }$ by setting

• 1. for each sort $s\in S$: $\gamma (A)_{s}=A_{s}$ and

• 2. for each operation $o\in O_{s_{1}\dots s_{j}\,,\,s_{j+1}\dots s_{j+k}}$ with $j,k\ge 0$:

  • (a) $\gamma (A)_{o}=o^{A}$ and

  • (b) for all $(x,y)=(\left( x_{1},\dots ,x_{j}\right) ,\left( y_{1},\dots ,y_{k}\right) )\in o^{A}$, $1\le m\le j$, $1\le n\le k$:¹¹

    • i. $\left( \mathrm {d}_{m}^{o}\right) ^{\gamma (A)}(x,y)=x_{m}$ and

    • ii. $\left( \mathrm {c}_{n}^{o}\right) ^{\gamma (A)}(x,y)=y_{n}$

and each homomorphism $h:A\rightarrow B$ in $\mathcal {A}_{\varSigma }$ to $\gamma (h):\gamma (A)\rightarrow \gamma (B)$ by setting

• 1. for each sort $s\in S$: $\gamma (h)_{s}=h_{s}$ and

• 2. for each operation $o\in O_{w,v}$ with $w,v\in S^{*}$: $\gamma (h)_{o}\left( x,y\right) =\left( h^{w}(x),h^{v}(y)\right)$.

Proposition 1 (Preservation of Epimorphisms)

If $\gamma :\mathcal {A}_{\varSigma }\rightarrow \mathcal {G}_{\varSigma }$ is the full and faithful functor from partial $\varSigma$-algebras to the underlying hierarchical $\varSigma ^{\mathrm {u}}$-graph-structures, then $\gamma (h):\gamma (A)\rightarrow \gamma (B)$ is epimorphism, if and only if $h:A\rightarrow B$ is a closed epimorphism.

Proof

“$\Leftarrow$”: Every closed epimorphism is surjective on all sorts and, by definition of closedness, also on “operations”. “$\Rightarrow$”: Suppose $\gamma (h):\gamma (A)\rightarrow \gamma (B)$ is epimorphism, i.e. is surjective in each component. Then $h_{s}=\gamma (h)_{s}$ is surjective for each sort s. Thus, h is epimorphism. If $o^{B}$ is defined for $h^{w}(x)$, $\left( h^{w}(x),y\right) \in o^{B}$. Since $\gamma (h)_{o}$ is surjective for every operation o, $\left( h^{w}(x),y\right) =\gamma (h)_{o}\left( x',y'\right)$ which means that $h^{w}(x)=h^{w}(x')$ and $o^{A}$ is defined for $x'$. Therefore, h is closed.   $\square$

Unfortunately, the functor $\gamma$ is not isomorphism-dense ¹², such that $\mathcal {A}_{\varSigma }$ and $\mathcal {G}_{\varSigma }$ are not equivalent. We have to further restrict $\mathcal {G}_{\varSigma }$ by the following family of constraints which formalises uniqueness of partial maps:

$$\begin{aligned} \mathcal {U}=\left( \forall e_{1},e_{2}\in o\,:\,\left( \mathrm {d}_{i}^{o}(e_{1})=\mathrm {d}_{i}^{o}(e_{2})\right) _{1\le i\le \mid w\mid }\implies e_{1}=e_{2}\right) _{w,v\in S^{*},o\in O_{w,v}} \end{aligned}$$

(1)

By $C_{\mathcal {U}}$, we denote the constraints (epimorphisms) presented by the implications $\mathcal {U}$. Figure 1 illustrates the correspondence between $\mathcal {U}$ and $C_{\mathcal {U}}$ for the sample signature $\mathtt {\varSigma _{f2}}$. Since there is only one operation, namely $\mathtt {f:\,S,S\rightarrow S}$, $C_{\mathcal {U}}$ contains a single epimorphism only, which is depicted in Fig. 1 by the dotted arrows.¹³

Fig. 1.

Example for a uniqueness constraint

In the following, $\mathcal {P}_{\varSigma }\subseteq \mathcal {G}_{\varSigma }$ denotes the quasi-variety of all algebras in $\mathcal {G}_{\varSigma }$ satisfying all the constraints in $\mathcal {U}$, i.e. $\mathcal {P}_{\varSigma }=\underline{\mathcal {A}}_{\varSigma ^{\mathrm {u}},C_{\mathcal {U}}}$. Since $\mathcal {P}_{\varSigma }$ is an epi-reflection of the category $\mathcal {G}_{\varSigma }$, we obtain a pair $\left( F(A)\in \mathcal {P}_{\varSigma },\eta _{A}:A\twoheadrightarrow F(A)\right)$ for every $A\in \mathcal {G}_{\varSigma }$ such that for every other pair $\left( X\in \mathcal {P}_{\varSigma },f:A\rightarrow X\right)$, there is a unique $f^{*}:F(A)\rightarrow X$ with $f^{*}\circ \eta _{A}=f$. Since every image of $\gamma$ is in $\mathcal {P}_{\varSigma }$ and $\gamma$ is isomorphism-dense wrt. $\mathcal {P}_{\varSigma }$, we have:

Fact 2

(Partial Algebras as Hypergraphs). $\mathcal {A}_{\varSigma }$ and $\mathcal {P}_{\varSigma }$ are equivalent.

Therefore, partial algebras can be considered as special hypergraphs which do not allow multiple edges of the same type between the same domain vertices.

Since $\mathcal {A}_{\varSigma }$ and $\mathcal {P}_{\varSigma }$ are equivalent, all results we obtain for $\mathcal {P}_{\varSigma }$ in the following are also valid in $\mathcal {A}_{\varSigma }$. Since $\mathcal {P}_{\varSigma }$ is an epi-reflection of $\mathcal {G}_{\varSigma }$, $\mathcal {P}_{\varSigma }$ is closed wrt. sub-objects and products. Thus, pullbacks in $\mathcal {P}_{\varSigma }$ coincide with pullbacks in $\mathcal {G}_{\varSigma }$. Pushouts in $\mathcal {P}_{\varSigma }$ are quotients of pushouts in $\mathcal {G}_{\varSigma }$ in the following sense: The pushout of $(f:A\rightarrow B,g:A\rightarrow C)$ in $\mathcal {P}_{\varSigma }$ is given by $(\eta _{D}\circ g^{*}:B\rightarrow D',\eta _{D}\circ f^{*}:C\rightarrow D')$ where $(g^{*}:B\rightarrow D,f^{*}:C\rightarrow D)$ is the pushout of f and g in $\mathcal {G}_{\varSigma }$ and $\eta _{D}:D\twoheadrightarrow D'$ is the epi-reflector that transfers the $\mathcal {G}_{\varSigma }$-object D into $\mathcal {P}_{\varSigma }$.

3 Partial Morphisms for Algebras and Hypergraphs

The single-pushout approach to rewriting uses partial morphisms as rules, total morphisms as matches, and pushouts in categories of partial morphisms as direct derivations. Therefore, we have to proceed from the categories $\mathcal {G}_{\varSigma }$ and $\mathcal {P}_{\varSigma }$ with total morphisms to the categories $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ and $\mathcal {P}_{\varSigma }^{\mathrm {P}}$ of hypergraphs and partial algebras with partial morphisms.

A concrete partial morphism in $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ is a span of $\mathcal {\mathcal {G}}_{\varSigma }$-morphisms $(p:K\rightarrowtail P,q:K\rightarrow Q)$ such that p is monic. Two concrete partial morphisms $(p_{1},q_{1})$ and $(p_{2},q_{2})$ are equivalent and denote the same abstract partial morphism if there is an isomorphism i such that $p_{1}\circ i=p_{2}$ and $q_{1}\circ i=q_{2}$; in this case we write $(p_{1},q_{1})\equiv (p_{2},q_{2})$ and $[(p,q)]_{\equiv }$ for the class of spans that are equivalent to (p, q). The category of partial morphisms $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ over $\mathcal {G}_{\varSigma }$ has the same objects as $\mathcal {G}_{\varSigma }$ and abstract partial morphisms as arrows. The identities are defined by $\text {id}_{A}^{\mathcal {G}_{\varSigma }^{\mathrm {P}}}=\left[ (\text {id}_{A}^{\mathcal {G}_{\varSigma }},\text {id}_{A}^{\mathcal {G}_{\varSigma }})\right] _{\equiv }$ and composition of partial morphisms $\left[ (p:K\rightarrowtail P,q:K\rightarrow Q)\right] _{\equiv }$ and $\left[ (r:J\rightarrowtail Q,s:J\rightarrow R)\right] _{\equiv }$ is given by

$$ \left[ (r,s)\right] _{\equiv }\circ _{\mathcal {G}_{\varSigma }^{\mathrm {P}}}\left[ (p,q)\right] _{\equiv }=\left[ (p\circ _{\mathcal {G}_{\varSigma }}r':M\rightarrowtail P,s\circ _{\mathcal {G}_{\varSigma }}q':M\rightarrow R)\right] _{\equiv } $$

where $(M,r':M\rightarrowtail K,q':M\rightarrow J)$ is pullback of q and r. Note that there is the faithful embedding functor $\iota :\mathcal {G}_{\varSigma }\rightarrow \mathcal {G}_{\varSigma }^{\mathrm {P}}$ defined by identity on objects and $\left( f:A\rightarrow B\right) \mapsto [\mathrm {id}_{A}:A\rightarrowtail A,f:A\rightarrow B]$ on morphisms. We call $[d:A'\rightarrowtail A,f:A'\rightarrow B]$ a total morphism and, by a slight abuse of notation, write $[d,f]\in \mathcal {\mathcal {G}}_{\varSigma }$, if d is an isomorphism. From now on, we mean the abstract partial morphism $\left[ f,g\right] _{\equiv }$ if we write $\left( f:B\rightarrowtail A,g:B\rightarrow C\right)$. If the monic component in a partial morphism is an inclusion, we also write $g:A\overset{B}{\dashrightarrow }C$ for $\left( f:B\hookrightarrow A,g:B\rightarrow C\right)$. We omit the annotation of the arrow, if the sub-object of the partial morphism is irrelevant or uniquely determined by some universal properties.

It is well-known that $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ is complete and co-complete.¹⁴

Fig. 2.

Pushout in $\mathcal {G}_{\varSigma }^{\mathrm {P}}$

Construction 3

(Pushout in $\mathcal {G}^{\mathrm {P}}_{\varSigma }$ ). For partial morphisms $r:L\overset{K}{\dashrightarrow }R$ and $q:L\overset{P}{\dashrightarrow }Q$, the pushout morphisms $r^{*}:Q\overset{K^{*}}{\dashrightarrow }H$ and $q^{*}:R\overset{P^{*}}{\dashrightarrow }H$ are constructed as follows, compare Fig. 2:

• 1. D is the largest sub-algebra in $K\cap P$ satisfying:

  • (a) $r(x)=r(y)\wedge x\in D\implies y\in D\;\mathrm {and}$

  • (b) $q(x)=q(y)\wedge x\in D\implies y\in D.$

• 2. $\overline{l}:D\hookrightarrow P$ and $\overline{p}:D\hookrightarrow K$ are the corresponding inclusions.

• 3. $P^{*}$ and $K^{*}$ are the largest sub-algebras in $R-r(K-D)$ resp. $Q-q(P-D)$.

• 4. $p^{*}:P^{*}\hookrightarrow R$ and $l^{*}:K^{*}\hookrightarrow Q$ are the corresponding inclusions.

• 5. $\overline{r}:D\rightarrow P^{*}$ is defined by $d\mapsto r(d)$ and $\overline{q}:D\rightarrow K^{*}$ by $d\mapsto q(d)$.

• 6. $(q^{*},r^{*})$ is the pushout of $(\overline{q},\overline{r})$ in $\mathcal {G}_{\varSigma }$.

Remark

Construction 3 leads to the four commutative squares (1)–(4) in Fig. 2. They possess the following properties:

• 1. Squares (2) and (3) are pullbacks such that $r^{*}\circ q=q^{*}\circ r$.

• 2. Squares (1)–(3) make up a final triple in the sense of [19].

• 3. Square (4) is hereditary pushout in $\mathcal {G}_{\varSigma }$ since all pushouts in $\mathcal {G}_{\varSigma }$ are hereditary, compare Definition 4 below.

Therefore, Construction 3 provides a pushout in $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ due to the following general fact: A diagram as in Fig. 2 is pushout of partial morphisms over an arbitrary category $\mathcal {C}$, if and only if (1)–(3) make up a final triple in $\mathcal {C}$ and (4) is hereditary pushout in $\mathcal {C}$, compare [19, 20].

Definition 4

(Hereditary Pushout). A pushout $(p',q')$ of (p, q) in an arbitrary category is hereditary, if for each commutative cube as in Fig. 3, which has pullback squares $(q_{i},i_{0})$ and $(p_{i},i_{0})$ of $(i_{1},q)$ and $(i_{2},p)$ resp. as back faces with monic $i_{1}$ and $i_{2}$ the following compatibility between pushouts and pullbacks holds: In the top square, $(q_{i}',p_{i}')$ is pushout of $(p_{i},q_{i})$, if and only if, in the front faces, $(p_{i}',i_{1})$ and $(q_{i}',i_{2})$ are pullbacks of $(i_{3},p')$ and $(i_{3},q')$ resp. and $i_{3}$ is monic.¹⁵

Fig. 3.

Hereditary pushout

$\mathcal {P}_{\varSigma }^{\mathrm {P}}$ is the full sub-category of $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ determined by the object inclusion of $\mathcal {P}_{\varSigma }\subseteq \mathcal {G}_{\varSigma }$. $\mathcal {P}_{\varSigma }^{\mathrm {P}}$ does not possess all pushouts. $\mathcal {P}_{\varSigma }$ has all final triples but not all pushouts in $\mathcal {P}_{\varSigma }$ are hereditary. Final triples are constructed as in $\mathcal {G}_{\varSigma }$, since steps (1)–(5) of Construction 3 produce sub-objects D, $P^{*}$, and $K^{*}$ which satisfy all Horn-formulae in $\mathcal {U}$ (compare (1) on p. x), if L, R, and Q do. Hereditariness of pushouts in $\mathcal {P}_{\varSigma }$ is characterised by an easy to check condition.

Fact 5

(Hereditrary Pushouts in $\mathcal {P}_\varSigma$ ). A pushout in $\mathcal {P}_{\varSigma }$ is hereditary, if and only if it is pushout in $\mathcal {G}_{\varSigma }$.

The proofs for this fact are provided by the proofs for Proposition 7 ($\Leftarrow$) and Proposition 8 ($\Rightarrow$) in [18]. Since all arguments in these proofs do not refer to the concrete structure of the formulae in $\mathcal {U}$, the result can be generalised as follows:

Theorem 6

(Hereditary Pushouts in Reflective Sub-categories of $\mathcal {G}_\varSigma$ ). For every epi-reflective sub-category $\mathcal {C}_{\varSigma }$ of $\mathcal {G}_{\varSigma }$, we have:

• 1. Pushouts in $\mathcal {C}_{\varSigma }$ are hereditary, if and only if they are pushouts in $\mathcal {G}_{\varSigma }$.

• 2. Let $\mathcal {C}_{\varSigma }^{\mathrm {P}}$ be the full sub-category of $\mathcal {G}_{\varSigma }^{\mathrm {P}}$ determined by the object inclusion of $\mathcal {C}_{\varSigma }\subseteq \mathcal {G}_{\varSigma }$: If a pushout for a pair of morphisms in $\mathcal {C}_{\varSigma }^{\mathrm {P}}$ exists, then it coincides with the pushout of the pair constructed in $\mathcal {G}_{\varSigma }^{\mathrm {P}}$.

4 SPO-Rewriting of Constrained Partial Algebras

Fact 5 shows that SPO-rewriting in $\mathcal {P}_{\varSigma }^{\mathrm {P}}$ is just SPO-rewriting in graph structures from the operational point of view. It only adds an application condition, namely that rewriting a partial algebra (as a graph structure) must result in a graph structure that represents a partial algebra.

Fig. 4.

Examples for impossible rewrites

Figure 4 presents three typical impossible rewrites in $\mathcal {P}_{\varSigma _{f}}^{\mathrm {P}}$. The mappings of the rule morphisms, which are all total in the three examples, are depicted by black straight arrows and the mappings of the match morphisms by dotted arrows. In the situation (a), the rule tries to add a definition of $\mathtt {f}$ to an object in the host graph that possesses a definition of $\mathtt {f}$ already. Situation (b) wants to add a new object as the result of the application of $\mathtt {f}$ for two existing objects. The match identifies the two existing objects. Rewriting in the underlying graph structure produces two parallel “edges” between the old and the new object which does not satisfy the uniqueness condition $\mathcal {U}$, compare (1) on p. x. Situation (c) is kind of symmetric to situation (b). Here two existing objects have the same result under application of $\mathtt {f}$. The rule tries to merge these two objects, which again leads to two parallel “edges” violating $\mathcal {U}$.

If we add more constraints on partial algebras that are subject to SPO-rewriting, we want to preserve this fundamental property, i.e.:

Operational Semantics. Every SPO-rewrite of a constrained partial algebra coincides with the SPO-transformation of the underlying graph structure.

Theorem 6 provides a first sort of constraints that satisfy this criteria: namely arbitrary constraints wrt. $\mathcal {G}_{\varSigma }$.¹⁶ But these constraints do not one-to-one correspond to general constraints on $\mathcal {P}_{\varSigma }$. Constraints on partial algebras can formulate conditional equalities and definedness requirements, since epimorphisms in categories of partial algebras need not be surjective. Therefore, we have to restrict the constraints to those that do not implicitly formulate definedness requirements. By Proposition 1, these constraints are exactly characterised by the epimorphism that are closed. We call a constraint of this type conditional equation, since its conclusion in the syntactical presentation as an implication consists of equalities between variables only. Note that the set of constraints presented by $\mathcal {U}$ on p. x is a set of conditional equations.

Corollary 7

(Conditional Equation). If $\mathcal {A}_{\varSigma }$ is a category of partial algebras and E a set of conditional equations wrt. $\varSigma$, then every pushout in $\mathcal {A}_{\varSigma ,E}^{\mathrm {P}}$ coincides with the pushout constructed in $\mathcal {G}_{\varSigma }^{\mathrm {P}}$.

Conditional equations provide a rich supply for useful constraints on partial algebras which are subject to rewriting, for example:

• Singleton: $x=x'$,

• Injectivity: $f(x)=f(x')\implies x=x'$,

• Joint-Injectivity: $f_{1}(x)=f_{1}(x'),\dots ,f_{n}(x)=f_{n}(x')\implies x=x'$,

• Commutativity: $f(g(x))=z,h(x)=z'\implies z=z'$,

• Inverse: $f(x)=z,g(z)=x'\implies x=x'$, and

• Mutual Inverse: $f(x)=z,g(z)=x',f(x')=z'\implies x=x',z=z'$.

Note that the last five examples require equalities only in situations where the operations are “defined enough”, i.e. the premises can be satisfied.

Up to this point, we do not have any means to require some sort of definedness. As it has been shown in [13], requiring definedness of operation symbols having more than one argument or none can lead to situations in which a final triple does not exist, compare steps (1)–(5) of Construction 3. Even worse: If operations with at least two arguments are required to be defined for a certain range of arguments, there are no obvious conditions which decide whether or not the final triple in Construction 3 exists.

Therefore, we restrict definedness requirements to unary operations here as well. Unfortunately, we cannot be as liberal as we want to at this point. This is due to the fact that even definedness requirements for unary operations may heavily interact with other constraints in form of conditional equations in an undesirable way.

Fig. 5.

Operation cycles

Example 8

(Interference of Equations and Definedness). A good example for such an interference is depicted in Fig. 5. The shown specification requires its two unary operations $\mathtt {\underline{f}}$ and $\mathtt {\underline{i}}$ to be total, i.e. to be defined for all arguments. We – here and in the following – indicate this requirement by underlining the affected operations. Additionally, the operation $\mathtt {\underline{i}}$ is forced to be injective.

The right part of the figure shows a pushout of two morphisms from L to R and L to G indicated by the black straight and dotted arrows resp. Note that the pushout does not coincide with the pushout constructed in the underlying graph structure. But it is hereditary.

This is mainly due to the fact, that G admits five sub-algebras only, namely the empty graph, G itself, and the three possible sub-graphs consisting of elements of the sort $\mathtt {S'}$ only. Only three of them can occur in a commutative cube as in Fig. 3, namely the empty graph, G, and the sub-graph consisting of the two $\mathtt {S'}$-elements. And all these three cubes satisfy the hereditariness requirement.   $\square$

Example 8 shows a situation that violates our requirement “Operational Semantics” on p. y: We have hereditariness without coincidence of the pushout in the constrained and the unconstrained category. This is mainly due to the cyclic structure induced by the operation $\mathtt {\underline{f}}$. Therefore, we restrict definedness requirements of unary operations to those that do not lead to cycles, i.e. to those that produce a hierarchical underlying graph structure.

Definition 9

(Constrained Category of Partial Algebras). A constrained category $\mathcal {R}_{(\varSigma ,C,T)}$ of partial algebras is syntactically given by a triple $(\varSigma ,C,T)$, where $\varSigma =(S,O)$ is a signature, C is a set of conditional equations and $T=(T_{s,w}\subseteq O_{s,w})_{s\in S,w\in S^{*}}$ is a sub-set of the unary operations in O satisfying the following hierarchy condition: There is no family $\left( o_{i}\in T_{s_{i},w_{i}}\right) _{i\in \mathbb {N}}$, such that, for all $i\in \mathbb {N}$, $w_{i}=v_{i}s_{i+1}u_{i}$ with $v_{i},u_{i}\in S^{*}$. The semantics of $\mathcal {R}_{(\varSigma ,C,T)}$ is the full sub-category of $\mathcal {A}_{\varSigma ,E}^{\mathrm {P}}$ of those algebras in which all operations in T are total.

As a generalisation of Propositions 7 and 8 in [18], we obtain:

Theorem 10

(Hereditariness in Constrained Categories). A pushout in $\mathcal {R}_{(\varSigma ,C,T)}$ is hereditary, if and only if it is pushout in the underlying graph structure $\mathcal {G}_{\varSigma }$.

Proof

“$\Leftarrow$”: In addition to the arguments in the proof of Proposition 7 in [18], we have to show that a pushout $(f^{*}:C\rightarrow D,g^{*}:B\rightarrow D)$ in $\mathcal {G}_{\varSigma }$ for $(f:A\rightarrow B,g:A\rightarrow C)$ satisfies the definedness requirements specified by T. So let $o\in T_{s,w}$ and $x\in D_{s}$. Then $x=f^{*}(x_{c})$ or $x=g^{*}(x_{b})$. Without loss of generality assume the first. Since C satisfies the definedness requirements, $o^{C}(x_{c})$ is defined. Since $\left( f^{*}\right) ^{w}(o^{C}(x_{c}))=o^{P}(f_{s}^{*}(x_{c}))=o^{P}(x)$, $o^{P}$ is defined for x.

“$\Rightarrow$” (Sketch): Here, we can repeat the arguments in the proof of Proposition 8 in [18]. Let $(f:A\rightarrow B,g:A\rightarrow C)$ be given, $(f^{*}:C\rightarrow D,g^{*}:B\rightarrow D)$ the pushout in $\mathcal {G}_{\varSigma }$, and $(f':C\rightarrow E,g':B\rightarrow E)$ the pushout in $\mathcal {R}_{(\varSigma ,C,T)}$. Since D satisfies all definedness requirements (see above), E is a quotient of D and the two pushout morphisms $(f',g')$ are jointly surjective. If the two pushouts are different, there are two elements $x,y\in B\uplus C$ which are mapped to the same element z by $f'$ and/or $g'$ in E and to different elements $z_{1},z_{2}$ by $f^{*}$ and/or $g^{*}$ in $D$. Now, we construct sub-algebras of $A'\subseteq _{A}A$, $B'\subseteq _{B}B$, and $C'\subseteq _{C}C$ by erasing x and recursively its minimal context in all three algebras such that $(\subseteq _{A},f_{\mid A'})$ becomes the pullback of $(\subseteq _{B},f$) and $(\subseteq _{A},g_{\mid A'})$ becomes the pullback of $(\subseteq _{C},g$). Since all total operations are hierarchical and x and y are not identified by $f^{*}$ and $g^{*}$, the element y remains in $B'$ or $C'$ and we obtain $z'=f'_{\mid A'}(y)$ or $z'=g'_{\mid A'}(y)$ as an element in the pushout $(E',f'_{\mid A'}:C'\rightarrow E',g'_{\mid A'}:B'\rightarrow E'$ of $(f_{\mid A'},g_{\mid B'})$. The universal morphism u from $E'$ to E maps $z'$ to z. Now, we have $u(z')=z$ and $f'(x)=z'$ or $g'(x)=z'$. Since by construction, x is neither in $B'$ nor in $C'$, either $(\subseteq _{B},g'_{\mid A'})$ is not pullback of $(u,g')$ or $(\subseteq _{C},f'_{\mid A'})$ is not pullback of $(u,f')$.   $\square$

Having this result about hereditary pushouts, we can conclude:

Corollary 11

(Rewriting in Constrained Categories). Every pushout in the category $\mathcal {R}_{(\varSigma ,C,T)}^{\mathrm {P}}$ of partial morphisms wrt. a constrained category $\mathcal {R}_{(\varSigma ,C,T)}$ coincides with the pushout constructed in the underlying graph structure $\mathcal {G}_{\varSigma }^{\mathrm {P}}$.

Remark

Note that step (1) in Construction 3 on p. z needs a marginal modification. Now we construct D as the largest sub-algebra satisfying all definedness constraints in T with properties (1a) and (1b). This algebra always exists, since all total operations are unary and the construction ends up in the standard cascade-on-delete behaviour that is well-known from single-pushout rewriting.¹⁷

The results of this section offer better ways to specify the structures that are subject to single-pushout rewriting. The appropriate framework is provided by the notion of constrained category of partial algebras, compare Definition 9. By Corollary 11, a simple operational semantics for rewrites in constrained categories is guaranteed. Therefore, there is a good chance to transfer some SPO-theory from graph structures to partial algebras and even to constrained partial algebras. This is subject of future research. In the rest of the paper, we want to present the gain of expressive power for SPO-rewriting of constrained structures.

5 Inheritance – The Algebraic Way

SPO-rewriting in categories of constrained partial algebras provides mechanisms to model many object-oriented concepts incl. inheritance in a straightforward and appropriate way. The inheritance model which we introduce below goes beyond all existing ones,¹⁸ since it provides easy means for “runtime” type-specialisation and -generalisation of objects. Here is the general recipe how object-oriented class and type models are translated into constrained categories of partial algebras:

Immutable base types, like Integer and String, and the operations on these base types, like concatenation (+) of strings and addition (+), subtraction (-), multiplication (), and division (/) of integers are just modelled as a part of the underlying signature by appropriate sort and operation symbols. On the object-level, i.e. on the level of the objects that are subject to SPO-transformation these sort and operation symbols are interpreted by the standard carrier sets and partial operations. Note that the interpretation as partial operations provides an adequate model for overflow-situations or division-by-zero. In transformation rules, partial term algebras over a suitable set of variables are used. By contrast to total term algebras which are almost always infinite, the partial term algebras used in rules can always be chosen as finite algebras.¹⁹

Classes are modelled by sorts. So all types (base or not) are modelled by sorts.

An attribute a of base type T in a class C is modelled (i) by a partial operation $\mathtt {a:C\rightarrow T}$, if its multiplicity is zero or one (0...1), (ii) a total operation $\mathtt {\underline{a}:C\rightarrow T}$,²⁰ if its multiplicity is exactly one (1)²¹ (iii) by a predicate $\mathtt {a:C,T}\rightarrow \{*\}$, if its multiplicity is many incl. none () without double assignments of the same value to the same object,²² and (iii) by an additional sort symbol $\mathtt {A}$ and total operations $\mathtt {\underline{a_{o}}:A\rightarrow C}$ and $\mathtt {\underline{a_{t}}:A\rightarrow T}$, if its multiplicity is many incl. none  () and multiple assignments of the same value to the same object are allowed.²³

An association r between classes $\mathtt {C}$ and $\mathtt {D}$ is modelled as follows: If the multiplicity of $\mathtt {r}$ at both ends is many incl. none (), we devise a predicate $\mathtt {r:C,D\rightarrow \{*\}}$ if multiple links between the same pair of objects are forbidden or we add an additional sort $\mathtt {R}$ and two total operations $\mathtt {\underline{r_{C}}:R\rightarrow C}$ and $\mathtt {\underline{r_{D}}:R\rightarrow D}$ otherwise. If the multiplicity at the $\mathtt {D}$-end is zero or one (0...1), we provide a partial map $\mathtt {r:C\rightarrow D}$ which obtains an additional injectivity constraint of the form $\mathtt {c\in C:r(c)=r(c')\implies c=c'}$, if the $\mathtt {C}$-end has multiplicity 0...1 as well. If the multiplicity at the $\mathtt {D}$-end is exactly one (1), we can devise a total operation $\mathtt {\underline{r}:C\rightarrow D}$, as long as the signature remains hierarchical.²⁴

A qualified association q between classes $\mathtt {C}$ and $\mathtt {D}$ using a T-typed attribute or association a of D as “key” is modelled by a partial operation $\mathtt {q:C,T\rightarrow D}$.

If a set $\mathtt {a_{1},\dots ,a_{n}}$ of 0...1-attributes and/or associations of the same class $\mathtt {C}$ is a key to the objects of $\mathtt {C}$, we add an injectivity constraint of the following form:

$$ \mathtt {c,c'\in C:a_{1}(c)=a_{1}(c'),\dots ,a_{n}(c)=a_{n}(c')\implies c=c'} $$

Inheritance of sub-class $\mathtt {S}$ from super-class $\mathtt {G}$, is modelled by a total and injective operation $\mathtt {\underline{i_{S,G}}:S\rightarrow G}$ and for every diamond-situation, defined by , , , and , we add a commutativity constraint like:

$$ \mathtt {x\in S;y,y'\in G:\underline{i_{G_{1},G}}(\underline{i_{S,G_{1}}}(x))=y,\underline{i_{G_{2},G}}(\underline{i_{S,G_{2}}}(x))=y'\implies y=y'} $$

Let us apply this recipe to the class model for file systems in Fig. 6. We obtain the signature and constraints File System below. Note the seamless integration of the “base type” String: On the one hand, it is used as “value-provider” for attributes name and contents. On the other hand, it is integrated in “graphical” structures as in contains. The constraints a1 and a2 specify the injectivity of the sub-type embeddings. Constraint a3 specifies the multiple inheritance of Directory and the diamond situation wrt. Component. Constraint a4 specifies that the index, that is used by a Container to manage its Containees, is consistent with the naming of the contained Components. Constraint a5 stems from the 0...1-multiplicity at the container-end of the contains-association.

Fig. 6.

Class model for file systems

Fig. 7.

Rewrite rule: move containee

On the basis of the specification File System, operations that change the system’s structure can be specified by SPO rewrite rules. Figure 7, for example, specifies the operation that moves a Containee (2) from Container (1) to Container (4). Note that this operation fails, if the receiving container already contains a containee named y. This is due to the fact that the index “contains” is specified as a partial operation that needs to be unique.

The rules in Fig. 8 demonstrate the ability of the chosen inheritance model to change the types of objects at “runtime”.²⁵ The rule read from left to right converts a Link (2) to a File (1) into a file with the same contents as (1). This is possible by exchanging the Link-part of object (2) by a File-part.²⁶ The rule read from right to left has the inverse effect, namely it converts a file (2) that happens to have the same contents as another file (1) into a link to the file (1). Note that the context (other contains- and references-connections) of the manipulated entity on the Containee-level is not change, since all Containee-parts are preserved.

Fig. 8.

Rewrite rule: convert to file/convert to link

6 Related Work and Future Research

There are only a few articles in the literature that address rewriting of partial algebras, for example [3] and [2] 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 [10], 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, the approach presented in [18] and further developed in this paper is original. It proposes to start with partial algebras in the first place and to require total operations where needed.²⁷ This is the other way around as most other approaches do: they start with total algebras and add some partiality where needed. Future research will show which approach is more suitable. Another topic for future research is the transfer of SPO-theory to the presented constrained framework. And finally, bigger case studies must be elaborated in order to confirm practical applicability.