Keywords

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 and Background

Graph transformation (GT) is a well-developed computational model suited to describe the evolution of systems. System states are represented by graphs, and rules typically describe local changes of part of the state. One central topic in the theory of GT has been the identification of conditions that guarantee that two transformation steps from a given state are independent, and thus can be applied in any order generating the same result. Interestingly, two transformation steps commute (have the so-called diamond property) even if their matches overlap, provided that they overlap only on items that are preserved by both.

In this short paper we start comparing two classical definitions of parallel independence of transformation steps proposed for the Double-Pushout (DPO) approach to graph transformation. Not surprisingly, we show that they are equivalent for linear rules. But if rules are non-left-linear, as allowed for example in the [Reversible] Sesqui-Pushout ([R]SqPO) approach where rules can specify the cloning of items, they are not equivalent anymore: The equivalence can be recovered by reinforcing one of the two definitions with an additional condition.

The reader is assumed to be familiar with the DPO approach and recent categorical development of its theory, including the definition and some properties of adhesive categories. We briefly recall in the rest of this introductory section a few definitions (final pullback complement, DPO and (Reversible) Sesqui-Pushout approaches).

In order to fix the terminology, let us recall the standard definition of Double-Pushout transformation [13] in a generic category \(\mathbf {C}\).

Definition 1 (Double-Pushout transformation)

A production \(\rho = (L \mathop {\leftarrow }\limits ^{l} K \mathop {\rightarrow }\limits ^{r} R)\) is a span of arrows in \(\mathbf {C}\). Production \(\rho \) is left-linear if l is mono, right-linear if r is mono, and linear if both l and r are monos. A match for a production \(\rho \) in an object G is an arrow \(m: L \rightarrow G\). If the diagram in (1) can be constructed in \(\mathbf {C}\), where both squares are pushouts, then we say that there is a transformation step from G to H via \((\rho , m)\), and we write \(G \Rightarrow _{(\rho ,m)} H\). In this case we call the pair \((\rho ,m)\) a redex in G, and we call it (left-, right-) linear if so is \(\rho \). We write \(G \Rightarrow _\rho H\) if there is a match m for \(\rho \) in G such that \(G \Rightarrow _{(\rho ,m)} H\).

(1)

Therefore if \({(\rho ,m)}\) is a redex in G we know that \(\rho \) can be applied to match m in G. In diagram (1), K is called the interface and D the context.

The definition of (Reversible) Sesqui-Pushout transformation [5, 7] is very similar to DPO transformation, the only difference being the properties that the left and right squares of diagram (1) have to satisfy. We first recall the definition of final pullback complement.

Definition 2 (final pullback complement)

In diagram (2), \(K \mathop {\rightarrow }\limits ^{n} D \mathop {\rightarrow }\limits ^{a} G\) is a final pullback complement of \(K \mathop {\rightarrow }\limits ^{l} L \mathop {\rightarrow }\limits ^{m} G\) if

  1. 1.

    the resulting square is a pullback, and

  2. 2.

    for each pullback \(G \mathop {\leftarrow }\limits ^{m} L \mathop {\leftarrow }\limits ^{d} K' \mathop {\rightarrow }\limits ^{e} D' \mathop {\rightarrow }\limits ^{f} G\) and arrow \(K' \mathop {\rightarrow }\limits ^{h} K\) such that \(l \circ h = d\), there is a unique arrow \(D' \mathop {\rightarrow }\limits ^{g} D\) such that \(a \circ g = f\) and \(g \circ e = n \circ h\).

(2)

Definition 3 ((Reversible) Sesqui-Pushout transformation)

Under the premises of Definition 1, we say that there is an SqPO transformation step from G to H via \((\rho , m)\) if the diagram in (1) can be constructed in \(\mathbf {C}\), where the left square is a final pullback complement and the right square is a pushout. Similarly, there is a Reversible SqPO transformation step from G to H via \((\rho , m)\) if the diagram in (1) can be constructed in \(\mathbf {C}\), where both the left and the right squares are both final pullback complements and pushouts.

2 Comparing Definitions of Parallel Independence: The Left-Linear Case

The Local Church-Rosser Problem is presented in the following way in [6]:

Find a condition, called parallel independence, such that two alternative direct derivations are parallel independent iff there are direct derivations \(H_1 \Rightarrow _{\rho _2} X\) and \(H_2 \Rightarrow _{\rho _1} X\) such that \(G \Rightarrow _{\rho _1} H_1 \Rightarrow _{\rho _2} X\) and \(G \Rightarrow _{\rho _2} H_2 \Rightarrow _{\rho _1} X\) are equivalent.

Deliberately we leave this statement at a pretty informal level, avoiding to define formally the notion of equivalence of derivation sequence: For the interested reader, several kinds of such equivalences are discussed in [4] and in Sect. 3.5 of [6], the most relevant of which are based on the classical shift equivalence [14]. Also, for the sake of simplicity, we do not consider the related notion of sequential independence of two consecutive transformation steps.

Relevant for the present discussion is the observation that the above statement fixes a standard pattern for addressing the Local Church-Rosser Problem in the various approaches to algebraic graph transformation: first, a definition of parallel independence for transformation steps has to be provided, next a Local Church-Rosser Theorem proves that given two parallel independent transformation steps from a given graph, they can be applied in both orders obtaining the same result (up to isomorphism). Disregarding the proofs of the Local Church-Rosser Theorems, in the following we aim at relating and comparing a few definitions of parallel independence.

In [9], a standard reference for the DPO approach, two definitions of parallel independence are presented. The first one is stated in a set-theoretical way for the category \(\mathbf {Graph}\) of graphs and graph homomorphism, and for linear productions. It says that two linear redexes are parallel independent if they satisfy Condition 1.

Condition 1

(preservation of intersection of matches). In category \(\mathbf {Graph}\), \((\rho _1,m_1)\) and \((\rho _2,m_2)\) are two redexes in a graph G, as in diagram (3). The intersection of matches \(m_1\) and \(m_2\) in G is preserved along the interfaces, that is,

$$\begin{aligned} m_1(L_1) \cap m_2(L_2) \subseteq m_1(l_1(K_1)) \cap m_2(l_2(K_2)) \end{aligned}$$

or equivalently, since the reverse inclusion always holds,

$$\begin{aligned} m_1(L_1) \cap m_2(L_2) = m_1(l_1(K_1)) \cap m_2(l_2(K_2)). \end{aligned}$$
(3)

This definition conveys the precise intuition that two redexes are independent if each preserves the items needed by the other; therefore the match in G of, say, \(\rho _1\) is still available in the result of the transformation step \(G \Rightarrow _{(\rho _2,m_2)} H_2\).

Immediately after, a different characterization is presented: two linear redexes are parallel independent if they satisfy Condition 2.

Condition 2

(factorization of matches). In a category \(\mathbf {C}\), \((\rho _1,m_1)\) and \((\rho _2,m_2)\) are two redexes in an object G, as in diagram (4). The matches \(m_1\) and \(m_2\) factorize through the context, that is, there exist arrows \(m_{1d}: L_1 \rightarrow D_2\) and \(m_{2d}: L_2 \rightarrow D_1\) such that \(g_2 \circ m_{1d} = m_1\) and \(g_1 \circ m_{2d} = m_2\).

(4)

The equivalence of Conditions 1 and 2 for linear redexes and for the category of graphs is proved for example in [8] and in Fact 3.18 of [10], by exploiting specific properties of pushouts in \(\mathbf {Graph}\). The motivation for introducing Condition 2 is pragmatical: it is easier to use in the proof of the Local Church-Rosser Theorem, heavily based on diagrammatic constructions.Footnote 1

In subsequent developments of the DPO approach to categories different from graphs (including High Level Replacement (HLR) systems first [11] and DPO transformation in adhesive categories next [15]), Condition 2 has always be taken as the reference definition of parallel independence. But it is obvious that Condition 2 is not a direct translation in categorical terms of the set-theoretical Condition 1, as the authors of [11] implicitly state when they write “For HLR-systems it is easier to define independence directly by conditions 1 and 2 above (i.e. Condition 2), because this avoids to require general pullback constructions generalizing intersections”. Indeed, a direct categorical formulation of Condition 1 would read as follows.

Condition 3

(preservation of pullback of matches). In a category \(\mathbf {C}\), \((\rho _1,m_1)\) and \((\rho _2,m_2)\) are two redexes in an object G. The pullback of the matches \(m_1\) and \(m_2\) in G is preserved along the interfaces, that is, in diagram (5), where both squares are pullbacks, the mediating arrow \(i: K_1\!\times _G\! K_2\rightarrow L_1\!\times _G\!L_2\) is an isomorphism.

(5)

Therefore Condition 3 is another candidate for a definition of parallel independence, provided that the reference category \(\mathbf {C}\) has the needed pullbacks. To my knowledge, the equivalence of Conditions 2 and 3 was not discussed in the literature. Let us show that the two conditions are indeed equivalent for left-linear productions, and assuming that category \(\mathbf {C}\) is adhesive.

Proposition 1 (matches extend iff their pullback is preserved)

Let \(\mathbf {C}\) be an adhesive category. Then for left-linear redexes Conditions 2 and 3 are equivalent.

Proof

Condition 2 implies Condition 3 .   Suppose that two left-linear redexes \((\rho _1,m_1)\) and \((\rho _2,m_2)\) satisfy Condition 2 and consider diagram (6). We show that the large square is a pullback, from which \(L_1\!\times _G\!L_2\cong K_1\!\times _G\! K_2\) follows (and thus Condition 3). Therefore given an object X with arrows \(f: X \rightarrow L_2\) and \(g: X \rightarrow L_1\) such that \(m_2 \circ f = m_1 \circ g\), we have to show that there exists a unique arrow \(h: X \rightarrow K_1\!\times _G\! K_2\) such that \(l_2 \circ \pi ^K_2 \circ h = f\) and \(l_1 \circ \pi ^K_1 \circ h = g\).

(6)

Existence. Square is a pushout by construction, and by adhesivity it is also a pullback, because \(l_2\) is mono by hypothesis. Since \(X \mathop {\rightarrow }\limits ^{f} L_2 \mathop {\rightarrow }\limits ^{m_2} G = X \mathop {\longrightarrow }\limits ^{m_{1d} \circ g} D_2 \mathop {\rightarrow }\limits ^{g_2} G\) and is a pullback, there is a unique arrow \(f_g: X \rightarrow K_2\) such that \(l_2 \circ f_g = f\) and \(n_2 \circ f_g = m_{1d} \circ g\). For symmetric reasons, since also is a pullback there is a unique arrow \(g_f: X \rightarrow K_1\) such that \(l_1 \circ g_f = g\) and \(n_1 \circ g_f = m_{2d} \circ f\).

Next observe that by definition \(K_1 \mathop {\leftarrow }\limits ^{\pi ^K_1} K_1\!\times _G\! K_2\mathop {\rightarrow }\limits ^{\pi ^K_2} K_2\) is the pullback of \(K_1 \mathop {\rightarrow }\limits ^{k_1} G \mathop {\leftarrow }\limits ^{k_2} K_2\), where \(k_1\) and \(k_2\) are the diagonals of squares and , respectively. Thus since we have \(k_2 \circ f_g = m_2 \circ l_2 \circ f_g = m_2 \circ f = m_1 \circ g = m_1 \circ l_1 \circ g_f = k_1 \circ g_f\), we deduce that there is a unique arrow \(h: X \rightarrow K_1\!\times _G\! K_2\) such that \(\pi ^K_2 \circ h = f_g\) and \(\pi ^K_1 \circ h = g_f\), and thus we obtain \(l_2 \circ \pi ^K_2 \circ h = f\) and \(l_1 \circ \pi ^K_1 \circ h = g\), as desired.

Uniqueness. Suppose that there are arrows \(h_1,h_2: X \rightarrow K_1\!\times _G\! K_2\) such that \(l_2 \circ \pi ^K_2 \circ h_1 = f = l_2 \circ \pi ^K_2 \circ h_2\) and \(l_1 \circ \pi ^K_1 \circ h_1 = g = l_1 \circ \pi ^K_1 \circ h_2\). Since \(l_1\) and \(l_2\) are mono, we obtain \(\pi ^K_2 \circ h_1 = \pi ^K_2 \circ h_2\) and \(\pi ^K_1 \circ h_1 = \pi ^K_1 \circ h_2\). Then \(h_1 = h_2\) follows because \(K_1\!\times _G\! K_2\) is a pullback object, and \(k_1 \circ \pi ^K_1 \circ h_i= m_1 \circ l_1 \circ \pi ^K_1 \circ h_i = m_1 \circ g = m_2 \circ f = m_2 \circ l_2 \circ \pi ^K_2 \circ h_i = k_2 \circ \pi ^K_2 \circ h_i\), for \(i \in \{1,2\}\).

Condition 3 implies Condition 2 .   Vice versa, assume that \((\rho _1,m_1)\) and \((\rho _2,m_2)\) satisfy Condition 3. By Proposition 12 of [5] since \(l_2: K_2 \rightarrowtail L_2\) is mono and \(\mathbf {C}\) is adhesive, , is a final pullback complement of . Thus in diagram (7) the left square is a final pullback complement, the outer square is a pullback by definition, and the upper triangle commutes by (5). By the universal property of final pullback complements there is a unique arrow \(m_{1d} : L_1 \rightarrow D_2\) making the right square and the bottom triangle commute. Therefore we have \(g_2 \circ m_{1d} = m_1\), and by a symmetric argument there exists an arrow \(m_{2d} : L_2 \rightarrow D_1\) such that \(g_1 \circ m_{2d} = m_2\). Thus the two redexes satisfy Condition 2.

(7)

3 The Non-linear Case

The theory of the DPO approach was developed only for left-linear rules, because the construction of the pushout complement of arrows l and m in the left square of (1) is not uniquely determined if l is not mono, even in well-behaved situations like adhesive categories. In more recent times, the Sesqui-Pushout approach provided a conservative extension of the DPO one, allowing to handle in a deterministic way also non-left-linear rules. In fact as recalled in Definition 3 the left square of a transformation step in this case is a final pullback complement of arrows l and m, which (if it exists) is unique up to isomorphisms because it is characterized by a universal property. A definition of parallel independence for SqPO transformation for linear productions only has been proposed in [5] by using Condition 2 and assuming adhesivity (and existence of final pullback complements, required for SqPO transformation). Thus by Proposition 1 we now know that Condition 3 would have been equivalent.

More interestingly, in the framework of Reversible SqPO the authors of [7] have considered the Local Church-Rosser Problem for non-linear rules. We consider here only the case of possibly non-left-linear, but right-linear rules, i.e. we assume that morphism \(r: K \rightarrow R\) is mono. In this case, the definition of [7] can be rephrased as follows: two right-linear redexes are parallel independent if they satisfy both Conditions 2 and 4.

Condition 4

(reflection of matches). In a category \(\mathbf {C}\), \((\rho _1,m_1)\) and \((\rho _2,m_2)\) are two redexes in an object G, as in diagram (4), which satisfy Condition 2. They are reflected identically along the context, that is, the two squares in diagram (8) are pullbacks.

(8)

Essentially, as observed in [7], if productions are non-left-linear, the commutativity requirements for arrows \(m_{1d}\) and \(m_{2d}\) of Condition 2 are not sufficient and have to be reinforced with the pullback requirements of Condition 4.Footnote 2 The same condition is also implied by the definition of parallel independence proposed in [16] in the more general framework of rewriting in categories of spans, where the required pullbacks arise from span composition.

A simple example can clarify this situation. Let \(\rho _1 = ( L_1 \leftarrow K_1 \rightarrow R_1)\) and \(\rho _2 = ( L_2 \leftarrow K_2 \rightarrow R_2)\) be the productions depicted in the following figure, where \(\rho _1\) adds a second loop to a preserved node with a loop, while \(\rho _2\) duplicates the node but not the incident loop. Both can be applied using SqPO transformation to the same graph G made of a node with a loop. There are (unique) morphisms \(L_1 \rightarrow D_2\) and \(L_2 \rightarrow D_1\) satisfying Condition 2, but the two transformation steps do not enjoy the diamond property, and thus should not be considered as parallel independent. In fact, applying \(\rho _1\) to \(H_2\) one gets a graph with two nodes, one of which has two loops and the other none. Instead applying \(\rho _2\) to \(H_1\) one gets a graph with two nodes, one with two loops and the other with one loop.

figure c

It is easy to show that the depicted redexes do not satisfy neither Condition 3 nor 4. In fact, we show that in the case of non-left-linear productions, Condition 3 is equivalent to the conjunction of Conditions 2 and 4. The last part of the proof exploits results to appear in [3], and requires an additional condition on category \(\mathbf {C}\), namely that it has a partial maps classifier (or equivalently, since \(\mathbf {C}\) is assumed to have final pullback complements, a subobject classifier). We refer to [1] for the definition of partial maps classifiers and the relationship with subobject classifiers, and to [2] for their use in the AGREE approach to graph transformation.

Proposition 2 (matches factorize and are reflected identically iff their pullback is preserved)

Let \(\mathbf {C}\) be an adhesive category with final pullback complements and with a sub-object classifier. Then the conjunction of Conditions 2 and 4 is equivalent to Condition 3 for SqPO and RSqPO transformation.

Proof

Conditions 2 and 4 imply Condition 3 .    Suppose that two redexes \((\rho _1,m_1)\) and \((\rho _2,m_2)\) satisfy Conditions 2 and 4. We proceed as in the proof of Proposition 1 showing that the square of diagram (6) is a pullback.

Given an object X with arrows \(f: X \rightarrow L_2\) and \(g: X \rightarrow L_1\) such that \(m_2 \circ f = m_1 \circ g\), the existence of an arrow \(h: X \rightarrow K_1\!\times _G\! K_2\) such that \(l_2 \circ \pi ^K_2 \circ h = f\) and \(l_1 \circ \pi ^K_1 \circ h = g\) can be shown as in the proof above, considering that squares and are now pullbacks by construction, since we consider [R]SqPO transformation. For the uniqueness part, since \(l_1\) and \(l_2\) are not monic in general, we exploit Condition 4.

Thus, making still reference to diagram (6), suppose that there are arrows \(h_1,h_2: X \rightarrow K_1\!\times _G\! K_2\) such that \(l_2 \circ \pi ^K_2 \circ h_1 = f = l_2 \circ \pi ^K_2 \circ h_2\) and \(l_1 \circ \pi ^K_1 \circ h_1 = g = l_1 \circ \pi ^K_1 \circ h_2\).

(10)

Consider the cube in diagram (10): the bottom face is a pullback by Condition 4, the front-left face is a pullback by construction, the back-right face is trivially a pullback, and the front-right and back-left squares commute. Therefore by pullback splitting also the top face is a pullback. By symmetry, also a similar square with indexes 1 and 2 exchanged is a pullback. We exploit these squares in diagram (11): since the outer squares commute by hypothesis, by the pullback property we deduce that \(\pi ^K_2 \circ h_1 = \pi ^K_2 \circ h_2\) and \(\pi ^K_1 \circ h_1 = \pi ^K_1 \circ h_2\). Then \(h_1 = h_2\) follows by the same argument as in the proof of Proposition 1.

(11)

Condition 3 implies Conditions 2 and 4 .    The proof that Condition 3 implies Condition 2 is identical, and even more direct, than the corresponding proof for Proposition 1, because the left square of diagram (7) is a final pullback complement by construction.

For Condition 4, the fact that the squares in (8) are pullbacks is proved in Lemma 1 of [3] by exploiting Condition 3 and an additional condition involving the partial maps classifier, and formulated for the more general framework of AGREE transformation. The latter condition, instantiated to SqPO transformation, requires that the left square of (12) is a pullback. But this follows easily by the observation that the right square of (12) is a pullback thanks to Condition 3, and that the partial maps classifier functor \(T: \mathbf {C}\rightarrow \mathbf {C}\) preserves pullbacks [1].

(12)

4 Conclusions

The goal of this position paper was to introduce a categorical definition of parallel independence based on pullbacks, thus corresponding directly to the original set-theoretical definition, and to study its relationship with the standard definition based on the possibility of factorizing the matches through the context. The pullback-based definition works, without changes, also for productions allowing the cloning of structures. Anyway since the two alternative definitions are equivalent (under suitable assumptions on the relevant category), the choice of one over the other looks mainly a matter of taste or of convenience. In this respect, I find Condition 3 slightly more elegant than Condition 2 because it makes reference only to the productions and to the corresponding matches, and not to the context graphs obtained by the application of the productions. But Condition 2 is certainly more convenient in proofs based on diagram constructions and chasing.