Rachid Echahed
email: rachid.echahed@imag.fr

Aude Maignan
email: aude.maignan@imag.fr

N H Pp

⊆ P H × P H

Parallel Graph Rewriting with Overlapping Rules *

Keywords: 1998 ACM Subject Classification F.4.2 graph rewriting, parallel rewriting, overlapping rewrite systems Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p 1

We tackle the problem of simultaneous transformations of networks represented as graphs. Roughly speaking, one may distinguish two kinds of simultaneous or parallel rewrite relations over complex structures such as graphs: (i) those which transform disjoint subgraphs in parallel and hence can be simulated by successive mere sequential and local transformations and (ii) those which transform overlapping subgraphs simultaneously. In the latter situations, parallel transformations cannot be simulated in general by means of successive local rewrite steps. We investigate this last problem in the framework of overlapping graph transformation systems. As parallel transformation of a graph does not produce a graph in general, we propose first some sufficient conditions that ensure the closure of graphs by parallel rewrite relations. Then we mainly introduce and discuss two parallel rewrite relations over graphs. One relation is functional and thus deterministic, the other one is not functional for which we propose sufficient conditions which ensure its confluence.

Introduction

Graph structures are fundamental tools that help modeling complex systems. In this paper, we are interested in the evolution of such structures whenever the dynamics is described by means of systems of rewrite rules. Roughly speaking, a rewrite rule can be defined as a pair l → r where the left-hand and the right-hand sides are of the same structure. A rewrite system, consisting of a set of rewrite rules, induces a rewrite relation (→) over the considered structures. The rewrite relation corresponds to a sequential application of the rules, that is to say, a structure G rewrites into a structure G if there exits a rule l → r such that l occurs in G. Then G is obtained from G by replacing l by r.

Besides this classical rewrite relation, one may think of a parallel rewrite relation which rewrites a structure G into a structure G by firing, simultaneously, some rules whose lefthand sides occur in G. Simultaneous or parallel rewriting of a structure G into G can be used as a means to speed up the computations performed by rewrite systems and, in such a case, parallel rewriting can be simulated by successive sequential rewrite steps. However, there are situations where parallel rewrite steps cannot be simulated by sequential steps as in formal grammars [START_REF] Kleijn | A study in parallel rewriting systems[END_REF], cellular automata (CA) [START_REF] Wolfram | A new kind of science[END_REF] or L-systems [START_REF] Prusinkiewicz | The algorithmic beauty of plants[END_REF]. This latter problem is of interest in this paper in the case where structures are graphs.

Graph rewriting is a very active area where one may distinguish two main stream approaches, namely (i) the algorithmic approaches where transformations are defined by means of the actual actions one has to perform in order to transform a graph, and (ii) the algebraic approaches where graph transformations are defined in an abstract level using tools borrowed from category theory such as pushouts, pullbacks etc. [START_REF] Rozenberg | Handbook of Graph Grammars and Computing by Graph Transformations[END_REF]. In this paper, we introduce a new class of graph rewrite systems following an algorithmic approach where rewrite rules may overlap. That is to say, in the process of graph transformation, it may happen that some occurrences of left-hand sides of different rules can share parts of the graph to be rewritten. This overlapping of the left-hand sides, which can be very appealing in some cases, turns out to be a source of difficulty to define rigorously the notion of parallel rewrite steps. In order to deal with such a difficulty we follow the rewriting modulo approach (see, e.g. [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF]) where a rewrite step can be composed with an equivalence relation. Another complication comes from the fact that a graph can be reduced in parallel in a structure which is not always a graph but rather a structure we call pregraph. Thus, we propose sufficient conditions under which graphs are closed under parallel rewriting. The rewrite systems we obtain generalize some known models of computation such as CA, L-systems and more generally substitution systems [START_REF] Wolfram | A new kind of science[END_REF].

The paper is organized as follows. The next section introduces the notions of pregraphs and graphs in addition to some preliminary results linking pregraphs to graphs. In Section 3, a class of rewrite systems, called environment sensitive rewrite systems is introduced together with a parallel rewrite relation. We show that graphs are not closed under such rewrite relation and propose sufficient conditions under which the outcome of a rewrite step is always a graph. Then, in Section 4, we define two particular parallel rewrite relations, one performs full parallel rewrite steps whereas the second one uses the possible symmetries that may occur in the rules and considers only matches up to automorphisms of the left-hand sides. Section 5 illustrates our framework through some examples. Concluding remarks and related work are given in Section6.

Pregraphs and Graphs

In this section we first fix some notations and give preliminary definitions and properties. 2 A denotes the power set of A. A B stands for the disjoint union of two sets A and B.

In the following, we introduce the notion of (attributed) pregraphs, which denotes a class of structures we use to define parallel graph transformations. Elements of a pregraph may be attributed via a function λ which assigns, to elements of a pregraph, attributes in sets underlying attributes' structure A. For instance A may be a Σ-algebra [START_REF] Sannella | Foundations of Algebraic Specification and Formal Software Development[END_REF] or merely a set.

Figure 1 Example of a pregraph H such that: AH = N, NH = {n1, n2, n3, n4, n5}, PH = {p1, p2, p3}, PN H = {(p1, n1), (p1, n2), (p2, n5), (p3, n3), (p3, n4)}, PPH = {(p1, p2), (p2, p3), (p2, p1), (p3, p2)}.

PPH could be reduced to its non symmetric port-port connection {(p1, p2), (p2, p3)}. λH (ni) = {1} for i ∈ {1, 2, 4, 5}, λH (n3) = {2}. λH (pj) = ∅, for j ∈ {1, 2, 3}. Port attributes (∅) have not been reported on the figure. =}, NH = {n1, n2, n3, n4, n5}, PH = {p2, p3, p4, p5, q2, q3, q4, q5}, PN H = {(p2, n1), (p3, n1), (p4, n1), (p5, n1), (q2, n2), (q3, n3), (q4, n4), (q5, n5)}, PPH reduced to its non symmetric port-port connection is PPH = {(p2, q2), (p3, q3), (p4, q4), (p5, q5)}. λH (ni) = {xi} for i ∈ {1, 2, 3, 4, 5}, λH (pj) = λH (qj) = ∅, for j ∈ {2, 3, 4, 5}.

Example 2. Figure 1 shows an example of a pregraph where the node attributes are natural numbers. In the second example, Figure 2, node attributes are variables ranging over N. The introduction of variables as attributes allows one to model node neighborhoodsensitive dynamics at the rewriting rule level as it will be illustrated in Section 5.

Below we introduce the definition of graphs used in this paper. In order to encode classical graph edges between nodes, restrictions over port associations are introduced. Intuitively, an edge e between two nodes n 1 and n 2 will be encoded as two semi-edges (n 1 , p 1 ) and (n 2 , p 2 ) with p 1 and p 2 being ports which are linked via an association (p 1 , p 2 ).

Definition 3 (Graph).

A graph, G, is a pregraph G = (N , P, PN , PP, A, λ) such that : (i) PN is a relation ⊆ P × N which associates at most one node to every port The main idea of our proposal is based on the use of equivalence relations over nodes and ports (merging certain nodes and ports under some conditions) in order to perform parallel graph rewriting in presence of overlapping rules. Thus, to a given pregraph H, we associate two equivalence relations on ports, ≡ P , and on nodes, ≡ N , as defined below. Proof. The reflexivity and transitivity of ≡ P and ≡ N follow directly from their respective definitions. The symmetry of PP H implies directly the symmetry of ≡ P and ≡ N .

Remark. Notice that the relations ≡ P and ≡ N can be computed incrementally as follows: Initial state:

≡ P 0 = {(x, x) | x ∈ P H } ≡ N 0 = {(x, x) | x ∈ N H } Inductive steps:
Rule I: if q, q ∈ P H such that, q ≡ P i q , (q, p 1 ) ∈ PP H and (q , p 2 ) ∈ PP H then p

) ∈ (PP • PP) k . case k = 0 : p 1 ≡ P 0 p 2 thus p 1 = p 2 and (p 1 , p 2 ) ∈ (PP • PP) 0 . Induction step, case k = k + 1 : Let us assume p 1 ≡ P k +1 p 2 .
In this case, from rule I, there exist q, q ∈ P H such that, q ≡ P k q , (q, p 1 ) ∈ PP H and (q , p 2 ) ∈ PP H . q ≡ P k q implies by induction hypothesis that (q, q ) ∈ (PP

) ∈ (PP H • PP H ) i . Since (p 1 , n 1 ) ∈ PN H and (p 2 , n 2 ) ∈ PN H we conclude that (n 1 , n 2 ) ∈ (PN - H • ≡ P •PN H ) ⇐ Let n 1 ≡ N n 2 .
Then by definition of ≡ N there exists a natural number k such that

(n 1 , n 2 ) ∈ (PN - H • ≡ P •PN H ) k .
This means that there is a chain of connections constiting tuples of the form m i -p i ≡ P p i -m i+1 for i ∈ {0, ..., k} such that m 0 = n 1 and m k = n 2 . From rule III, it is easy to deduce the existence of k , such that

n 1 ≡ N k n 2 .
Intuitively, two ports or two nodes are equivalent if they are associated to a same port. The equivalence relations ≡ P and ≡ N are used to introduce the notion of quotient pregraph as defined below.

= {[n] | n ∈ N H }, P H = {[p] | p ∈ P H }, PN H = {([p], [n]) | (p, n) ∈ PN H }, PP H = {([p], [q]) | (p, q) ∈ PP H }, A H = A H and λ H ([x]) = ∪ x ∈[x] λ H (x )
A H = N, λ N H (n 1 ) = λ N H (n 4 ) = {1}, λ N H (n 2 ) = λ N H (n 3 ) = {2}, ∀i ∈ {1, ..., 6}, λ P H (p i ) = ∅,
We obtain H = (N H , P H , PN H , PP H , A H , λ H ), as depicted on the right of Figure 3, with

N H = {[n 1 ], [n 2 ]} with [n 1 ] = {n 1 , n 4 }, [n 2 ] = {n 2 , n 3 }, P H = {[p 1 ], [p 2 ], [p 5 ], [p 6 ]} with [p 1 ] = {p 1 , p 3 }, [p 2 ] = {p 2 , p 4 }, [p 5 ] = {p 5 }, [p 6 ] = {p 6 }, PN H = {([p 1 ], [n 1 ]), ([p 5 ], [n 1 ]), ([p 2 ], [n 2 ]), ([p 6 ], [n 2 ])}, PP H = {([p 1 ], [p 2 ]), ([p 5 ], [p 6 ])}, A H = A H λ N H ([n 1 ]) = {1}, λ N H ([n 2 ]) = {2}, λ P H ([p 1 ]) = λ P H ([p 2 ]) = λ P H ([p 5 ]) = λ P H ([p 6 ]) = ∅.
Example 7. Figure 4 illustrates two computations of quotient pregraphs.

Remark. If H is a graph, H = H (In fact H and H are isomorphic). Indeed, in a graph, a port can be associated (resp. linked) to at most one node (resp. one port).

The following definition introduces some vocabulary and notations. A path π H (p 1 , p k ) between two (possibly the same) nodes

p 1 and p k in a pregraph H is a sequence of ports of H written π H (p 1 , p k ) = (p 1 , p 2 , . . . , p k ) such that {(p i , p i+1 ) | i = 1, 2, . . . , k -1} ⊆ PP H and k ∈ N with k > 0. The length of a path π H (p 1 , p k ) = (p 1 , p 2 , . . . , p k ) is (π H (p 1 , p k )) = k -1.
An even path (resp. odd path) is a path such that its length is even (resp. odd). A loop is a closed path, i.e., a path π H = (p 1 , p 2 , . . . , p k ) such that p 1 = p k . An even loop (resp. odd loop) is an even closed path (resp. odd closed path).

From the definitions above, one can show the following statements. Proposition 4. Let H = (N H , P H , PN H , PP H , A H , λ H ) be a pregraph. Let q, q be two ports in P H . q ≡ P q iff there exists an even path between q and q in H.

Proof. If q ≡ P q then, by definition, (q, q ) ∈ (PP H • PP H ) * hence there exists an even path between q and q . Conversely, if there exists an even path between q and q in H then (q, q ) ∈ (PP H • PP H ) * and thus q ≡ P q . Proposition 5. Let H = (N H , P H , PN H , PP H , A H , λ H ) be a pregraph. H is a graph iff H has no odd loop.

Proof. Let H = (N H , P H , PN H , PP H , A H , , λ H ). The relations PN H and PP H are functional by construction. In order to show that H is indeed a graph, It remains to prove that PP H is not anti-reflexive iff there is an odd loop in H.

⇒ Assume that PP H is not anti-reflexive. Then, there exists q ∈ P H such that ([q], [q]) ∈ PP H . Thus, either (q, q) ∈ PP H which constitute an odd loop of length one or there exists a port q , different from q, such that (q, q ) ∈ PP H and q ≡ P q. In this last case, from Proposition4, q ≡ P q implies the existence of an even path from q to q. Then adding the link (q, q ) to this path builds a loop from q to q in H of odd length. ⇐ Assume there is an odd loop containing a port q in H. Then either the loop is of the form (q, q) and thus (q, q) ∈ PP H and in this case ([q], [q]) ∈ PP H , or there exists a port q different from q such that the loop is of the form (q, q , . . . , q). In this last case, (q, q ) ∈ PP H and the path π H (q , q) is even. Thus, [q] = [q ] which implies that ([q], [q]) ∈ PP H .

Below, we define the notion of homomorphisms of pregraphs and graphs. This notion assumes the existence of homomorphisms over attributes [START_REF] Duval | Transformation of attributed structures with cloning[END_REF]. Definition 9 (Pregraph and Graph Homomorphism). Let l = (N l , P l , PN l , PP l , A l , λ l ) and g = (N g , P g , PN g , PP g , A g , λ g ) be two pregraphs. Let a : A l → A g be a homomorphism over attributes. A pregraph homomorphism, h a : l → g, between l and g, built over attribute homomorphism a, is defined by two functions h a N : N l → N g and h a P :

P l → P g such that (i) ∀(p 1 , n 1 ) ∈ PN l , (h a P (p 1 ), h a N (n 1 )) ∈ PN g , (ii) ∀(p 1 , p 2 ) ∈ PP l , (h a P (p 1 ), h a P (p 2 )) ∈ PP g , (iii) ∀n 1 ∈ N l , a(λ l (n 1 )) ⊆ λ g (h a N (n 1 )
) and (iv) ∀p 1 ∈ P l , a(λ l (p 1 )) ⊆ λ g (h a P (p 1 )). A graph homomorphism is a pregraph homomorphism between two graphs. Notation: Let E be a set of attributes, we denote by a(E) the set a(E) = {a(e) | e ∈ E}. Proposition 6. Let H and H be two isomorphic pregraphs. Then H and H are isomorphic.

Proof. Let h a : H → H be a pregraph isomorphism. We define ha : H → H as follows: for all ports p, p in H, nodes n in H, ha

N ([n]) = [h a N (n)], ha P ([p]) = [h a P (p)], ha ([p], [n]) = ([h a P (p)], [h a N (n)]), ha ([p], [p ]) = ([h a P (p)], [h a P (p )]
). ha is clearly a pregraph isomorphism between H and H . h is well defined as illustrated in the following three items.

We show that for all ports p 1 , p 2 in H, p )) = (q 1 , q 2 , . . . q k-1 , q k ) such that q 1 = h a P (p 1 ), q k = h a P (p 2 ) and π H (h a P (p 1 ), h a P (p 2 )) is even (see, Proposition 4). It is equivalent to say that (p 1 , (h a P ) -1 (q 2 ), . . . , (h a P ) -1 (q k-1 ), p 2 ) is an even path of H because h is an isomorphism. We conclude that p 1 ≡ p H p 2 . For all nodes n 1 , n 2 in H, we show that

n 1 ≡ n H n 2 iff h a N (n 1 ) ≡ n H h a N (n 2 ). By definition, h a N (n 1 ) ≡ n H h a N (n 2 ) iff (a) h a N (n 1 ) = h a N (n 2 ) or (b) there exists q, q ∈ P H , q ≡ p H q , (q, h a N (n 1 )) ∈ PN H and (q , h a N (n 2 )) ∈ PN H or (c) there exists n ∈ N H , h a N (n 1 ) ≡ n H n and h a N (n 2 ) ≡ n H n . h a is an isomorphism thus (a) is equivalent to n 1 = n 2 and (b) is equivalent to there exists (h a P ) -1 (q), (h a P ) -1 (q ) ∈ P H , (h a P ) -1 (q) ≡ p H (h a P ) -1 (q ), ((h a P ) -1 (q), n 1 ) ∈ PN H and ((h a P ) -1 (q ), n 2 ) ∈ PN H .
The cases (a) and (b) are straight foward. Let us focus our attention on the case (c) :

h a N (n 1 ) ≡ n H h a N (n 2 ) such that it exists n ∈ N H and q, q ∈ P H which verify the condition {(q, n ), (q, h(n 1 )), (q , n ), (q , h a N (n 2 ))} ⊂ PN H . This is equivalent to : (h a N ) -1 (n ) ∈ N H and (h a P ) -1 (q), (h a P ) -1 (q ) ∈ P H which verify the condition {((h a P ) -1 (q), (h a P ) -1 (n )), ((h a P ) -1 (q), n 1 ), ((h a P ) -1 (q ), (h a N ) -1 (n )), ((h a P ) -1 (q ), n 2 )} ⊂ PN H and in that case n 1 ≡ N H n 2 . Moreover because ≡ N is transitive we obtain that (c) is equi- valent to : there exists (h a N ) -1 (n ) ∈ N H , n 1 ≡ n H (h a N ) -1 (n ) and n 2 ≡ n H (h a N ) -1 (n ). Thus, n 1 ≡ n H n 2 .
The pregraph homorphism of H → H and H → H are built over the same attribute homomorphism a, thus by construction the points (iii) and (iv) of the previous definition imply

∪ ni∈[n] a(λ H (n i )) ⊂ ∪ ni∈[n] λ H (h a N (n i )) and ∪ pi∈[p] a(λ H (p i )) ⊂ ∪ pi∈[p] λ H (h a P (p i )) thus a(λ H ([n])) ⊂ λ H ( ha N ([n])) and a(λ H ([p])) ⊂ λ H ( ha P ([p]
)) and ha is a pregraph homomorphism from H to H .

We end this section by defining an equivalence relation over pregraphs.

Definition 10 (Pregraph equivalence).

Let G 1 and G 2 be two pregraphs. We say that G 1 and G 2 are equivalent and write G 1 ≡ G 2 iff the quotient pregraphs Ḡ1 and Ḡ2 are isomorphic.

The relation ≡ over pregraphs is obviously an equivalence relation.

Graph Rewrite Systems

In this section, we define the considered rewrite systems and provide sufficient conditions ensuring the closure of graph structures under the defined rewriting process.

Definition 11 (Rewrite Rule, Rewrite System, Variant). A rewrite rule is a pair l → r where l and r are graphs over the same sets of attributes. A rewrite system R is a set of rules. A variant of a rule l → r is a rule l → r where nodes, ports as well as the variables of the attributes are renamed with fresh names.

Let l → r be a variant of a rule l → r. Then there is a renaming mapping h a , built over an attribute renaming a : A l → A l , and consisting of two maps h a N and h a P over nodes and ports respectively : h a N : N l ∪ N r → N l ∪ N r and h a P : P l ∪ P r → P l ∪ P r such that, the elements in N l and P r are new and the restrictions of h a to l → l (respectively r → r ) are graph isomorphisms.

In general, parts of a left-hand side of a rule remain unchanged in the rewriting process. This feature is taken into account in the definition below which refines the above notion of rules by decomposing the left-hand sides into an environmental part, intended to stay unchanged, and a cut part which is intended to be removed. As for the right-hand sides, they are partitioned into a new part consisting of added items and an environmental part (a subpart of the left-hand side) which is used to specify how the new part is connected to the environment.

Definition 12 (Environment Sensitive Rewrite Rule, Environment Sensitive Rewrite System).

An environment sensitive rewrite rule is a rewrite rule (ESRR for short) l → r where l and r are graphs over the same attributes A such that: ). An environment sensitive rewrite system (ESRS for short) is a set of environment sensitive rewrite rules.

l = (N l , P l , PN l , PP l , A, λ l ) where N l = N cut l N env l , P l = P cut l P env l , PN l = PN cut l PN env l , PP l = PP cut l PP env l and λ l = λ cut l 3 λ env l with some additional constraints : (1) on PN l : ∀(p, n) ∈ PN l , (n ∈ N cut l or p ∈ P cut l ) ⇒ (p, n) ∈ PN cut l . (2) on PP l : ∀(p, p ) ∈ PP l , p ∈ P cut l ⇒ (p, p ) ∈ PP cut l . (3) on λ l : ∀n ∈ N cut l , (n, λ l (n)) ∈ λ cut l ; ∀p ∈ P cut l , (p, λ l (p)) ∈ λ cut l . r = (N r , P r , PN r , PP r , A, λ r ) where N r = N new
Roughly speaking, constraints (1), ( 2) and (3) ensure that if an item (node or port) is to be removed (belonging to a "cut" component) then links involving that item should be removed too as well as its attributes (constraint (3)). Constraints ( 4) and ( 5) ensure that links, considered as new (belonging to "new" components), of a given right-hand side of a rule, should not appear in the left-hand side. Constraint [START_REF] Kleijn | A study in parallel rewriting systems[END_REF] ensures that an item (node or port) is newly attributed in the right-hand side iff it is a new item or it was assigned by λ cut l in the left-hand side.

Proposition 7. Let l → r be a an ESRR such that l = (N l = N cut l N env l , P l = P cut l P env l , PN l = PN cut l PN env l , PP l = PP cut l PP env l , A, λ l = λ cut l λ env l ) and r = (N r = N new r N env r , P r = P new r P env r , PN r = PN new r PN env r , PP r = PP new r PP env r , A, λ r = λ new
= {α 1 , α 2 , β 1 , β 2 , γ 1 , γ 2 }, PN env l = {(α 1 , α), (α 2 , α), (β 1 , β), (β 2 , β), (γ 1 , γ), (γ 2 , γ)},
and PP env l = ∅. The cut component of the left-hand side consists of three port-port connections and their corresponding symmetric connections which will not be written : PP cut l = {(α 2 , β 1 ), (β 2 , γ 1 ), (γ 2 , α 1 )}. The environment component in the righthand side allows to reconnect the newly introduced items. r env consists of the ports Finding an occurrence of a left-hand of a rule within a graph to be transformed consists in finding a match. This notion is defined below. Definition 14 (Match). Let l and g be two graphs. A match m a : l → g is defined as a graph homomorphism which is injective. a : A l → A g being an injective homomorphism over attributes.

P env r = {α 1 , α 2 , β 1 , β 2 , γ 1 , γ 2 }. r new consists of N new r = {U, V, W }, P new r = {u 1 , u 2 , u 3 , u 4 , v 1 , v 2 , v 3 , v 4 , w 1 , w 2 , w 3 , w 4 }, PN new r = {(u 1 , U ), (u 2 , U ), (u 3 , U ), (u 4 , U ), (v 1 , V ), (v 2 , V ), (v 3 , V ), (v 4 , V ), (w 1 , W ), (w 2 , W ), (w 3 , W ), (w 4 , W )} and PP new r = {(α 1 , w 2 ), (α 2 , u 1 ), (β 1 , u 2 ), (β 2 , v 1 ), (γ 1 , v 2 ), (γ 2 , w 1 ), (u 3 , w 3 ), (u 4 , v 4 ), (w 4 , v 3 )}.
Example 15. Figure 6 gives a graph l and a graph g. Two matches can be defined:

m id 1 : m id 1 (α) = E; m id 1 (β) = B; m id 1 (γ) = C; m id 1 (α 1 ) = e 1 ; m id 1 (α 2 ) = e 2 ; m id 1 (β 1 ) = b 1 ; m id 1 (β 2 ) = b 2 ; m id 1 (γ 1 ) = c 1 ; m id 1 (γ 2 ) = c 2 . m id 2 : m id 2 (α) = C; m id 2 (β) = D; m id 2 (γ) = F ; m id 2 (α 1 ) = c 3 ; m id 2 (α 2 ) = c 4 ; m id 2 (β 1 ) = d 1 ; m id 2 (β 2 ) = d 2 ; m id 2 (γ 1 ) = f 1 ; m id 2 (γ 2 ) = f 2 .
Notice that the occurrences in g of m id 1 (l) and m id 2 (l) overlap on node C.

Definition 16 (Rewrite Step). Let l → r be a rule, g a graph and m a : l → g a match. The attributes of l, r and g are assumed to range over the same set (of attributes

). Let l = (N l = N cut l N env l , P l = P cut l P env l , PN l = PN cut l PN env l , PP l = PP cut l PP env l , A, λ l = λ cut l λ env l ) and r = (N r = N new r N env r , P r = P new r P env r , PN r = PN new r PN env r , PP r = PP new r PP env r , A, λ r = λ new r λ env r )
. A graph g rewrites to g using a match m a , written g → g or g → l→r,m a g with g being a pregraph defined as follows: g = (N g , P g , PN g , PP g , A g , λ g ) such that Notation: Let p, p be ports and n be a node, in notation m a (r) above,

N g = (N g -N cut m a (l) ) N new r P g = (P g -P cut m a (l) ) P new r PN g = (PN g -PN m a (l) cut ) PN new m a (r) PP g = (PP g -PP cut m a (l) ) PP new m a (r) A g = A g and λ g = (λ g -λ cut m a (l) ) λ new m a (r)
m a (p, p ) = (m a (p), m a (p )), m a (p, n) = (m a (p), m a (n)), m a (p) = p if p ∈ P new r and m a (n) = n if n ∈ N new r .
It is easy to see that graphs are not closed under the rewrite relation defined above. That is to say, when a graph g rewrites into g , g is a pregraph. To ensure that g is a graph we provide the following conditions.

Theorem 17. Let l → r be an environment sensitive rewrite rule, g a graph and m a : l → g a match. Let g → l→r,m a g . g is a graph iff the two following constraints are verified :

1. If p ∈ P env l , (p, q) ∈ PP new r
for some port q and there is no q such that (p, q ) ∈ PP cut l , then there is no q ∈ P g such that (m a (p), q ) ∈ PP g .

If p

∈ P env l , (p, n) ∈ PN new r and there is no n such that (p, n ) ∈ PN cut l , then there is no n ∈ N g such that (m a (p), n ) ∈ PN g .
Proof. (⇐) Let p be a port of g . If the constraints 1. and 2. are verified then If p ∈ g -m a (r), p has the same connections as in g. Since g is a graph, p is connected to at most one port and one node.

If p ∈ m a (r env ), thanks to constraints 1. and 2. p has at most one connection to a node and one connection to a port in g . If p ∈ P new r . Since r is a graph, p has at most one connection to a node and one connection to a port in g . Thus, g is a graph.

(⇒) It is easy to show, by contrapositive, that in case one of the constraints (1 and 2) is not verified, a counter example can be exhibited.

Matches which fulfill the above two conditions are called well behaved matches.

Example 18. Figure 7 (a) gives an example of toy rule. Figure 7 (b) is a graph H such that the match m id 1 as defined below is a well behaved match, whereas the match m id 2 is not a well behaved match. m id 1 :

m id 1 (α) = A, m id 1 (β) = B, m id 1 (α 1 ) = a 1 , m id 1 (β 1 ) = b 1 and m id 2 : m id 2 (α) = C, m id 2 (β) = B, m id 2 (α 1 ) = c 1 , m id 2 (β 1 ) = b 1 .
The application of the toy rule on nodes B and C and the ports b 1 and c 1 (according to match m id 2 ) leads to a pregraph which is not a graph.

In order to define the notion of parallel rewrite step, we have to restrict a bit the class of the considered rewrite systems. Indeed, let l 1 → r 1 and l 2 → r 2 be two ESRR Applying these two rules in parallel on a graph g is possible only if there is "no conflict" while firing the two rules simultaneously. A conflict may occur if some element of the environment of

Parallel Graph Rewriting with Overlapping Rules

r env 1 is part of l cut 2
and vice versa. To ensure conflict free rewriting, we introduce the notion of conflict free ESRS. Let us first define the notion of compatible rules.

Definition 19 (compatible rules). Two ESRR's l 1 → r 1 and l 2 → r 2 are said to be compatible iff for all graphs g and matches m a1 1 : l 1 → g and m a2 2 :

l 2 → g, (i) no element of m a1 1 (r env 1 ) is in m a2 2 (l cut 2 ) and (ii) no element of m a2 2 (r env 2 ) is in m a1 1 (l cut 1 ).
Conditions (i) and (ii) ensure that the constructions defined by m a1 1 (r 1 ) (respectively by m a2 2 (r 2 )) can actually be performed ; i.e, no element used in m a1 1 (r 1 ) (respectively by m a2 2 (r 2 )) is missing because of its inclusion in m a2 2 (l cut 2 ) (respectively in m a1 1 (l cut 1 )). For instance, the reader can easily verify that two variants of the rule are not compatible. Verifying that two given rules are compatible is decidable and can be checked on a finite number, less than max(size(l 1 ), size(l 2 )), of graphs where the size of a graph stands for its number of nodes and ports.

Proposition 8. The problem of the verification of compatibility of two rules is decidable.

Proof. Let ρ 1 = l 1 → r 1 and ρ 2 = l 2 → r 2 be two rules. Assume that ρ 1 and ρ 2 are not compatible. Then there exists a graph G such that: there exists a match m a1 1 : l 1 → G there exists a match m a2 2 : l 2 → G w.l.o.g, we assume that there exists an element, say e, in m a1 1 (r env 1 ) which belongs also to m a2 2 (l cut 2 ). Graph G can be built as follows: Let d be a graph such that there exist two injective homomorphisms h 1 : d → m a1 1 (l 1 ) and h 2 : d → m a2 2 (l 2 ) such that G is obtained as a pushout of h 1 and h 2 . That is to say, there exit two injective homomorphisms h 1 : m a1 1 (l 1 ) → G and

h 2 : m a2 2 (l 2 ) → G such that h 1 (h 1 (d)) = h 2 (h 2 (d)
). We consider subgraphs d which contain at least h -1 1 ((m a1 1 ) -1 (e)) which is equal to h -1 2 ((m a2 2 ) -1 (e)). Notice that elements of graph d could be attributed by empty sets.

Therefore, to check whether two rules ρ 1 = l 1 → r 1 and ρ 2 = l 2 → r 2 are compatible, one has to check whether there exist a subgraph d and two injective homomorphisms h : d → l 1 and h : d → l 2 such that d contains an item, e, such that h(e) ∈ l cut 1 and h (e) ∈ r env 2 (h(e) ∈ r env l and h (e) ∈ l cut 2 ) . Since homomorphisms h and h are injective, the size (number of nodes and ports) of d is less than max(size(l 1 ), size(l 2 )). Obviously, d, h and h exist iff the two rules are not compatible. Indeed the graph G obtained as a pushout of homomorphisms h and h contains at least one item which can be matched either by l env i (and remains in r env i ) and l cut j with (i, j) ∈ {(1, 2), (2, 1)}. Since the set of possible d's is finite (up to isomorphism), verifying whether two rules are compatible is decidable. Definition 20. A conflict free environment sensitive graph rewrite system is an ESRS consisting of pairwise compatible rules.

Definition 21 (parallel rewrite step). Let R be a conflict free environment sensitive graph rewrite system R = {L i → R i | i = 1 . . . n}. Let G be a graph. Let I be a set of variants of rules in R, I = {l i → r i | i = 1 . . . k} and M a set of matches M = {m ai i : l i → G | i = 1 . . . k}. We say that graph G rewrites into a pregraph G using the rules in I and matches H = G Figure 8 A parallel rewrite step with overlapping between two triangles. Notice that two variants of RT with fresh new variables have been provided in order to produce the pregraph H. In the

quotient graph H = G , [S] = {S, Y }, [s1] = {s1, y1}, [s2] = {s2, y2}. in M , written G ⇒ I,M G , G ⇒ M G or simply G ⇒ G if G is
N H = (N G -∪ k i=1 N cut m a i i (li) ) ∪ k i=1 N new ri P H = (P G -∪ k i=1 P cut m a i i (li) ) ∪ k i=1 P new ri PN H = (PN G -∪ k i=1 PN cut m a i i (li) ) ∪ k i=1 PN new m a i i (ri) PP H = (PP G -∪ k i=1 PP cut m a i i (li) ) ∪ k i=1 PP new m a i i (ri) A H = A G and λ H = (λ G -∪ k i=1 λ cut m a i i (li) ) ∪ ∪ n i=1 λ new m a i i (ri)
second step: G = H Notice that the rewrite step G ⇒ G is a rewrite modulo step [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF] of the form G → H ≡ H.

Example 22. Let us consider the graph g depicted below and the following matches of the rule R T depicted in Figure 5.

m 1 : m 1 (α) = E; m 1 (β) = B; m 1 (γ) = C; m 1 (α 1 ) = e 1 ; m 1 (α 2 ) = e 2 ; m 1 (β 1 ) = b 1 ; m 1 (β 2 ) = b 2 ; m 1 (γ 1 ) = c 1 ; m 1 (γ 2 ) = c 2 .
The isomorphism of the port-node and port-port connections are easily deduced.

m 2 : m 2 (α) = B; m 2 (β) = D; m 2 (γ) = C; m 2 (α 1 ) = b 2 ; m 2 (α 2 ) = b 3 ; m 2 (β 1 ) = d 2 ; m 2 (β 2 ) = d 1 ; m 2 (γ 1 ) = c 3 ; m 2 (γ 2 ) = c 1 .
The two matches have an overlap.

Figure 8 shows the different steps of the application of two matches of the rule defined in Figure 5. The pregraph, H, in the middle is obtained after the first step of Definition 21. Its quotient pregraph, G , is the graph on the right. G has been obtained by merging the nodes S and Y and the ports s 1 and y 1 as well as ports s 2 and y 2 . These mergings are depicted by the quotient sets [S], [s 1 ] and [s 2 ]. For sake of readability, the brackets have been omitted for quotient sets reduced to one element.

As a quotient pregraph is not necessarily a graph (see Figure 4), the above definition of parallel rewrite step does not warranty, in general, the production of graphs only. Hence, we propose hereafter a sufficient condition, which could be verified syntactically, that ensures that the outcome of a parallel rewrite step is still a graph.

Theorem 23. Let R be a conflict free environment sensitive graph rewrite system R = {L i → R i | i = 1 . . . n}. Let G be a graph. Let I be a set of variants of rules in R,

I = {l i → r i | i = 1 . . . k}

Two Parallel Rewrite Relations

The set of matches, M , in Definition 21 is not constrained and thus the induced parallel rewrite relation is too nondeterministic since at each step one may choose several sets of matches leading to different rewrite outcomes. In this section, we are rather interested in two confluent parallel rewrite relations which are realistic and can be good candidates for implementations. The first one performs all possible reductions (up to node and port renaming) whereas the second relation is more involved and performs reductions up to lefthand sides' automorphisms.

Full Parallel Rewrite Relation

We start by a technical definition of an equivalence relation, ≈, over matches.

Definition 24 (≈). Let L → R be a rule and G a graph. Let l 1 → r 1 and l 2 → r 2 be two variants of the rule L → R. We denote by h a1 1 (respect. h a2 2 ) the (node, port and attribute) renaming mapping such that the restriction of h a1 1 (respectively, h a2 2 ) to L → l 1 (respectively L → l 2 ) is a graph isomorphism. Let m b1 1 : l 1 → G and m b2 2 : l 2 → G be two matches. We say that m b1 1 and m b2 2 are equivalent and write m b1 1 ≈ m b2 2 iff for all elements x (in

P L , N L , PP L or PN L ) L, m b1 1 (h a1 1 (x)) = m b2 2 (h a2 2 (x)) and for all x in A L , b 1 (a 1 (x)) = b 2 (a 2 (x)) .
The relation ≈ is clearly an equivalence relation. Intuitively, two matches m b1 1 :

l 1 → G and m b2 2 : l 2 → G are equivalent, m b1 1 ≈ m b2
2 , whenever (i) l 1 and l 2 are left-hand sides of two variants of one same rule, say L → R, and (ii) m b1 1 and m b2 2 coincide on each element x of L.

Definition 25 (full parallel matches). Let R be a graph rewrite system and G a graph. Let M R (G) = {m ai i : l i → G | m ai i is a match and l i → r i is a variant of a rule in R}. A set, M , of full parallel matches, with respect to a graph rewrite system R and a graph G, is a maximal set such that (i

) M ⊂ M R (G) and (ii) ∀m a1 1 , m a2 2 ∈ M, m a1 1 ≈ m a2 2 .
A set of full parallel matches M is not unique because any rule in R may have infinitely many variants. However the number of non equivalent matches could be easily proven to be finite. Proposition 9. Let M be a set of full parallel matches with respect to a graph rewrite system R and a graph G. Then M is finite.

Proof. We assume that G has a finite number of nodes, ports and attributes and R has a finite number of rules. Let l i → r i be a rule in R. Let us assume now that nodes and ports of the left-hand side l i are attributed with the empty set. In this case, matching l i with subgraphs in G remains to find a (non attributed) graph homomorphism between l i and G. Therefore, in this case, the number of possible matches of the left-hand side l i in graph G is at most ki n × k i ! where n = card(N G ) + card(P G ) and k i = card(N li ) + card(P li ). Thus card(M ) is bounded by Π 1≤i≤card(R) ki n × k i ! which is finite since n and the k i 's are finite. Let us consider now the case where l i is attributed (that is to say, there exists at leat a node or port, say x, such that λ li (x) = ∅). Let m a : l i → G be a match. m is a non-attributed graph homomorphism and a : A li → A G is an attribute homomorphism which corresponds to a match over attributes in the case where attributes in l i contain variables. We assume that the matching problem over attributes is finitary. Thus for every m there is a finite number, say C m , of possible matchings over attributes a. Let l i be the graph obtained from l i by removing all attributes (or equivalently said, by setting the attribute function λ l i to the empty set. Let C i = max(C m |m is a non-attributed graph homomorphism m : l i → G). C i exists since we assume that the matching problem is finitary. Then card(M ) is bounded by Π 1≤i≤card(R) ki n × k i ! × C i which is finite since n, the k i 's and the C i 's are finite.

Definition 26 (full parallel rewriting). Let R be a ESRS and G a graph. Let M be a set of full parallel matches with respect to R and G. We define the full parallel rewrite relation and write G ⇒ M G or simply G ⇒ G , as the parallel rewrite step G ⇒ M G . Proposition 10. Let R be a ESRS. The rewrite relation ⇒ is deterministic. That is to say, for all graphs g, (g ⇒ g 1 and g ⇒ g 2 ) implies that g 1 and g 2 are isomorphic.

Proof. The proof is quite direct. Let M 1 and M 2 be two different sets of full parallel matches such that g ⇒ M1 g 1 and g ⇒ M2 g 2 . By definition of sets of full parallel matches, for all matches m b ∈ M 1 there exists a match m b ∈ M 2 such that m b ≈ m b . Since M 1 and M 2 are finite (see Proposition 9), there exists a natural number k such that

M 1 = {m b1 1 , m b2 2 , . . . , m b k k } and M 2 = {m b 1 1 , m b 2 2 , . . . , m b k k } such that for all i ∈ {1, . . . , k}, m bi i ≈ m b i i .
Therefore, for every i such that 1 ≤ i ≤ k, there exist a rule L i → R i in R and two variants of it l i → r i and l i → r i together with two renaming mappings h ai i : L i → l i and h

a i i : L i → l i such that for all elements x ∈ L i , m bi i (h ai i (x)) = m b i i (h a i i (x))
. By Definitions 21 and 26, graphs g 1 and g 2 are quotient pregraphs of two pregraphs, respectively H 1 and H 2 , obtained after the first step of parallel rewrite steps. The sets of nodes and ports of pregraphs H 1 and H 2 are defined as follows

N H1 = (N g -∪ k i=1 N m b i i (l cut i ) ) ∪ k i=1 N r new i N H2 = (N g -∪ k i=1 N m b i i (l cut i ) ) ∪ k i=1 N r new i P H1 = (P g -∪ k i=1 P m b i i (l cut i ) ) ∪ k i=1 P r new i P H2 = (P g ∪ k i=1 P m b i i (l cut i ) ) ∪ k i=1 P r new i λ H1 = (λ g -∪ k i=1 λ cut m b i i (li) ) ∪ k i=1 λ new ri λ H2 = (λ g -∪ k i=1 λ cut m b i i (li) ) ∪ k i=1 λ new ri

Parallel Graph Rewriting with Overlapping Rules

Now, We define a map f c : H 1 → H 2 by means of three maps on nodes, ports and attributes f c N : N H1 → N H2 , f c P : P H1 → P H2 and c : A H1 → A H2 as follows

f c N (x) =    x if x ∈ (N g -∪ k i=1 N m b i i (l cut i ) ) h a i i ((h ai i ) -1 (x)) if x ∈ N r new i , f or 1 ≤ i ≤ k f c P (x) =    x if x ∈ (P g -∪ k i=1 P m b i i (l cut i ) ) h a i i ((h ai i ) -1 (x)) if x ∈ P r new i , f or 1 ≤ i ≤ k and c(x) = b i • a i • a -1 i • b -1 i (x) if ∃i ∈ {1, . . . , k}, ∃e ∈ (N H1 ∪ P H1 ), (e, x) ∈ λ new ri
x otherwise f c is clearly a pregraph isomorphism between H 1 and H 2 . As g 1 and g 2 are obtained as quotient pregraphs of H 1 and H 2 respectively, we conclude by using Proposition 6, that g 1 and g 2 are isomorphic.

Example 27.

Let us consider the rule R T defined in Figure 5 and the subgraph s depicted on the side. The reader can verify that there are six different matches, m 1 . . . m 6 , between the left-hand side of R T and graph s.

These matches are sketched below. Variants of R T have been omitted for sake of readability.

m 1 : m 1 (α) = E; m 1 (β) = B; m 1 (γ) = C; m 1 (α 1 ) = e 1 ; m 1 (α 2 ) = e 2 ; m 1 (β 1 ) = b 1 ; m 1 (β 2 ) = b 2 ; m 1 (γ 1 ) = c 1 ; m 1 (γ 2 ) = c 2 . m 2 : m 2 (α) = E; m 2 (β) = C; m 2 (γ) = B; m 2 (α 1 ) = e 2 ; m 2 (α 2 ) = e 1 ; m 2 (β 1 ) = c 2 ; m 2 (β 2 ) = c 1 ; m 2 (γ 1 ) = b 2 ; m 2 (γ 2 ) = b 1 . m 3 : m 3 (α) = B; m 3 (β) = E; m 3 (γ) = C; m 3 (α 1 ) = b 2 ; m 3 (α 2 ) = b 1 ; m 3 (β 1 ) = e 2 ; m 3 (β 2 ) = e 1 ; m 3 (γ 1 ) = c 2 ; m 3 (γ 2 ) = c 1 . m 4 : m 4 (α) = B; m 4 (β) = C; m 4 (γ) = E; m 4 (α 1 ) = b 1 ; m 4 (α 2 ) = b 2 ; m 4 (β 1 ) = c 1 ; m 4 (β 2 ) = c 2 ; m 3 (γ 1 ) = e 1 ; m 4 (γ 2 ) = e 2 . m 5 : m 5 (α) = C; m 5 (β) = B; m 5 (γ) = E; m 5 (α 1 ) = c 2 ; m 5 (α 2 ) = c 1 ; m 5 (β 1 ) = b 2 ; m 5 (β 2 ) = b 1 ; m 5 (γ 1 ) = e 2 ; m 5 (γ 2 ) = e 1 . m 6 : m 5 (α) = C; m 5 (β) = E; m 5 (γ) = B; m 5 (α 1 ) = c 1 ; m 5 (α 2 ) = c 2 ; m 5 (β 1 ) = e 1 ; m 5 (β 2 ) = e 2 ; m 5 (γ 1 ) = b 1 ; m 5 (γ 2 ) = b 2 .
Here, the homomorphisms over attributes are always the identity, that is why they have been omitted. Thanks to the six matches and the rule R T , the reader may check that the subgraph s can be rewritten, by using six different variants of rule R T , into a pregraph containing 3 × 6 new nodes and 12 × 6 new ports. The quotient pregraph has only 3 new nodes but has 42 new ports. Each pair of new nodes has 6 connections. This example shows that the full parallel rewriting has to be used carefully since it may produce non intended results due to overmatching the same subgraphs. To overcome this issue, one may use attributes in order to lower the possible matches. We call such attributes distinguishing attributes. In order to consider only one match of the subgraph s considered in Example 27 by the rule R T , one option is to apply full parallel rewrite relation with distinguishing attributes on the subgraph depicted in Figure 9 (a) and rule R T with distinguishing attributes given in Figure 9 (b), leading to a pregraph whose quotient is a graph with 3 new nodes and 12 new ports. This graph is the expected one.

Another way to mitigate the problems of overmatching subgraphs, in addition to the use of distinguishing attributes, consists in taking advantage of the symmetries that appear in the graphs of rewrite rules. This leads us to define a new rewrite relation which gets rid of multiple matches of the same left-hand-side of a fixed rule. We call this relation parallel up to automorphisms and is defined below.

Parallel Rewrite Relation up to Automorphisms

Let us consider a graph g which rewrites into g 1 and g 2 using an ESRR l → r. This means that there exist two matches m bi i : l → g with i ∈ {1, 2} such that g ⇒ l→r,m b i i g i . One may wonder whether g 1 and g 2 are the same (up to isomorphism) whenever matches m b1 1 and m b2 2 are linked by means of an automorphism of l. That is to say, when there exists an automorphism h a : l → l with m b1 1 = m b2 2 • h a . Intuitively, matches m b1 1 and m b2 2 could be considered as the same up to a permutation of nodes. We show below that g 1 and g 2 are actually isomorphic but under some syntactic condition we call symmetry condition.

Notation: Let g be a graph with attributes in A. We write H(g) to denote the set of automorphisms of g, i.e. H(g) is the set of isomorphisms h b : g → g, with b being an isomorphism on the attributes of g, b : A → A.

Proposition 11. Let l → r be an ESRR. Let g be a graph and g 1 and g 2 be two pregraphs. Let g ⇒ l→r,m b 1 1 g 1 and g ⇒ l→r,m b 2 2 g 2 be two rewrite steps such that there exists an auto-

morphism h a : l → l with m b1 1 = m b2 2 • h a .
In case there exists an automorphism h a : r → r such that for all elements x of r env , h a (x) = h a (x), then g 1 and g 2 are isomorphic.

Sketch. The proof is done in a more general case where the rules used in the rewrite steps g ⇒ m b 1 1 g 1 and g ⇒ m 2 2 g 2 are variants of the rule l → r. So, let l 1 → r 1 (resp. l 2 → r 2 ) be two variants of the rule l → r. Thus, there exist four isomorphisms (node and port renaming) reflecting the variant status of these two rules, say v c1

1 : l → l 1 , v c1 1 : r → r 1 , v c2 2 : l → l 2 and v c2 2 : r → r 2 such that l i = v ci i (l), r i = v ci i (r) and v ci i (r env i ) = v ci i (r env i ) for
The reader can check that the rule R T verifies the symmetry condition.

Definition 29 (Matches up to automorphism, ∼ l ). Let l → r be an ESRR satisfying the symmetry condition. Let l 1 → r 1 and l 2 → r 2 be two different variants of the rule l → r. Let v c1 1 : l → l 1 and v c2 2 : l → l 2 be the isomorphisms that reflect the variant status of l 1 and l 2 of l. Let m b1 1 : l 1 → g and m b2 2 : l 2 → g be two matches such that m b1 1 (l 1 ) = m b2 2 (l 2 ). We say that matches m b1 1 and m b2 2 are equal up to (l-)automorphism and write m b1 1 ∼ l m b2 2 iff there exists an automorphism h a : l → l such that m b1

1 = m b2 2 • v c2 2 • h a • v c1 1 -1 .
Definition 30 (Rewriting up to automorphisms). Let R be a conflict free environment sensitive graph rewrite system whose rules satisfy the symmetry condition and g a graph. Let M (R, g) auto = {m ai i : l i → g | l i is the left-hand side of a variant of a rule l → r in R and m ai i is a match up to automorphism}. We define the rewrite relation ⇒ auto which rewrites graph g by considering only matches up to automorphisms. I.e., the set of matches M of Definition 21 is M (R, g) auto .

Remark. For all two matches m b1 1 and m b2 2 in M (R, G) auto , m b1 1 ∼ l m b2 2 . This means that the choice of matchings in M (R, G) auto are not unique. From every equivalence class of a match w.r.t. the equivalence relation ∼ l , only one representative is considered. Therefore, one may wonder if the relation ⇒ auto is confluent. The answer is positive, that is to say, whatever the match representatives are chosen (up to automorphism), the relation ⇒ auto rewrites a given graph to a same pregraph up to isomorphism.

Theorem 31. Let R be a conflict free environment sensitive graph rewrite system whose rules satisfy the symmetry condition. Then ⇒ auto is deterministic. That is, for all graphs g, (g ⇒ auto g 1 and g ⇒ auto g 2 ) implies that g 1 and g 2 are isomorphic.

Sketch. Let M 1 (resp. M 2 ) be the set of matches used in the rewrite step g ⇒ auto g 1 (resp. g ⇒ auto g 2 ). Let us assume that M 1 = M 2 . By definition of sets M 1 and M 2 , for all matches m bi i : l i → g in M 1 , there exits a match m b i i : l i → g in M 2 such that l i and l i are the left-hand sides of two variants l i → r i and l i → r i of a rule l → r in R such that

m bi i (l i ) = m b i i (l i ).
That is to say, there exist four isomorphisms reflecting the variant status of these two rules, say

v ci i : l → l i , v ci i : r → r i , w di i : l → l i and w di i : r → r i such that l i = v ci i (l), r i = v ci i (r), l i = w di i (l), r i = w di i (r), v ci i (r env i ) = v ci i (r env i
) and

w di i (r env i ) = w di i (r env i
). From the hypotheses, there exist two automorphisms h ai i : l i → l i and h ai i : r i → r i and two isomorphisms

h i ei v : l i → l i and h i ei v : r i → r i such that h i ei v = w di i • h ai i • (v ci i ) -1 and h i ei v = w ei i • h ai i • (v ci i ) -1
. By following the same reasoning as in Proposition 11, we can build h f : g 1 → g 2 defined as follows, where µ ti i : r i → g 1 and µ ti i : r i → g 2 are induced by definition of rewrite steps (µ ti i and µ ti i play the same role, for every two rules, as m b1 1 and m b2 2 in the proof of Proposition 11).

for n ∈ N g1 , h f (n) = µ ti i (h i ei v ((µ ti i ) -1 (n))) if n ∈ µ ti i (r i ) n otherwise for p ∈ P g1 , h f (p) = µ ti i (h i ei v ((µ ti i ) -1 (p))) if p ∈ µ ti i (r i ) p otherwise for (p, n) ∈ N g1 , h f (p, n) = (h f (p), h f (n)) for (p, p ) ∈ N g 1 , h f (p, p ) = (h f (p), h f (p ))
Clearly h f is an isomorphism between pregraphs g 1 and g 2 . Therefore, by Proposition 6, g 1 (which equals ḡ1 ) is isomorphic to g 2 (which equal ḡ2 ).

Examples

We illustrate the proposed framework through three examples borrowed from different fields. We particularly provide simple confluent rewrite systems encoding cellular automata, the koch snowflake and the mesh refinement.

Cellular automata (CA)

A cellular automaton is based on a fixed grid composed of cells. Each cell computes its new state synchronously. At instant t + 1, the value of a state k, denoted x k (t + 1) may depend on the valuations at instant t of the state k itself, x k (t), and the states x n (t) such that n is a neighbor of k. Such a formula is of the following shape, where f is a given function and ν(k) is the set of the neighbors of cell k:

x k (t + 1) = f (x k (t), x n (t), n ∈ ν(k))
In the case of a graph g, the neighbors of a cell (node) k, ν(k), is defined by :

l ∈ ν(k) iff ∃p 1 , ∃p 2 , (p 1 , k) ∈ PN g ∧ (p 2 , l) ∈ PN g ∧ (p 1 , p 2 ) ∈ PP g .
Usually, the grid is oriented such that any cell of ν(k) has a unique relative position with respect to the cell k. This orientation is easily modeled by distinguishing attributes on ports. For instance, one can consider Moore's neighborhood [START_REF] Moore | Automatic scanning and computer processes for the quantitative analysis of micrographs and equivalent subjects[END_REF] on a 2-dimensional grid. This neighborhood of radius 1 is composed of 8 neighbors. The distinguishing attributes on ports belong to the set A = {e, w, n, s, ne, se, nw, sw} which defines the 8 directions where e = east, w = west, n = north, s = south etc. The grid is defined by a graph g = (N g , P g , PN g , PP g , A g , λ g ) such that : N g = {m i,j } i∈I,j∈J , where intervals I and J are defined as I = [-N, N ] ∩ Z and J = [-N , N ] ∩ Z for some natural numbers N and N . P g = {e i,j , w i,j , s i,j , n i,j , ne i,j , nw i,j , se i,j , sw i,j | i ∈ I, j ∈ J}, PN g = {(e i,j , m i,j ), (w i,j , m i,j ), (s i,j , m i,j ), (n i,j , m i,j ), (ne i,j , m i,j ), (nw i,j , m i,j ), (se i,j , m i,j ), (sw i,j , m i,j )|i ∈ I, j ∈ J}, PP g = {(e i,j , w i,j+1 ), (w i,j , e i,j-1 ), (n i,j , s i-1,j ), (s i,j , n i+1,j ), (ne i,j , sw i-1,j+1 ), (se i,j , nw i+1,j+1 ), (nw i,j , se i-1,j-1 ), (sw i,j , ne i+1,j-1 )| i ∈ I, j ∈ J}, ∀i ∈ I, ∀j ∈ J, λ g (m i,j ) ⊆ A g , ∀i ∈ I, ∀j ∈ J, λ g (e i,j ) = {e}, λ g (w i,j ) = {w},λ g (s i,j ) = {s}, λ g (n i,j ) = {n}, λ g (ne i,j ) = {ne, λ g (nw i,j ) = {nw}, λ g (se i,j ) = {se}, λ g (sw i,j ) = {sw}.

The attributes of the nodes correspond to states of the cells. They belong to a set A. To implement the dynamics of the automaton one needs only one rewrite rule {ρ = l → r} which corresponds to the function f . The rule does not modify the structure of the grid but modifies the attributes of nodes. Thus a left-hand side has a structure of a star with one central node (see Figure 11), for which the rule at hand expresses its dynamics, surrounded by its neighbors. Nodes, ports and edges of the left-hand side belong to the environment part of the rule. Only the attribute of the central node belongs to the cut part since this attribute is modified by the rule. In the left-hand-side, the attributes of nodes are variables to which values are assigned during the matches. The right-hand-side is reduced to a single node named i. Its attribute corresponds to the new part of the right-hand side. Figure 11 illustrates such rules by implementing the well known game of life. It is defined using Moore's neighborhood and the dynamics of the game is defined on a graph g such that attributes of nodes are in {0, 1} and

x i (t + 1) = (( l∈ν(i) x l (t)) =? = 3) + ((x i (t) =? = 1) ×( l∈σ(i) x l (t)) =? = 2))
where (x =? = y) ⇔ 1 if x = y 0 otherwise The neighborhood of a node i and its dynamics verify the symmetry condition, thus there is no need to define attributes on ports. The rewriting relation ⇒ auto is applied on the rewrite system R = {ρ = l → r} reduced to one rule depicted in Figure 11. More precisely the graphs of the rule as defined as follows: d), (e 1 , e), (f 1 , f ), (g 1 , g), (h 1 , h), (i 1 , i)(i 2 , i), (i 3 , i), (i 4 , i), (i 5 , i), (i 6 , i), (i 7 , i), (i 8 , i)}, PP l = PP env l = {(i 1 , a 1 )(i 2 , b 1 ), (i 3 , c 1 ), (i 4 , d 1 ), (i 5 , e 1 ), (i 6 , f 1 ), (i 7 , g 1 ), (i 8 , h 1 )}. b,c,d,e,f,g

{0} {0} {0} {0} {0} {1} {1} {0} {0} {0, 1} {1} {0} {0} {0} {0} {0} {0} {0} {0} {0} {0} {1} {1} {0} {0} {1} {1} {0} {0} {0} {0} {0} (
l = (N l , P l , PN l , PP l , A l , λ l ) with N l = N env l = {i, a, b, c, d, e, f, g, h}, P l = P env l = {i 1 , i 2 , i 3 , i 4 , i 5 , i 6 , i 7 , i 8 , a 1 , b 1 , c 1 , d 1 , e 1 , f 1 , g 1 , h 1 }, PN l = PN env l = {(a 1 , a), (b 1 , b), (c 1 , c), (d 1 ,
A l = {0, 1, x i } ∪ {y q | q ∈ {a,
(i) = {((y a + y b + y c + y d + y e + y f + y g + y h ) =? = 3) + ((x i =? = 1) × ((y a + y b + y c + y d + y e + y f + y g + y h ) =? = 2))}.
In the classical formulation of cellular automata, a cell contains one and only one value. The model we propose can deal with cells with one or several values. For instance, the initial state of the game of life can be a grid containing {0}'s except for 4 cells describing a square (see Figure 12(a)).

In this configuration one cell have 2 values which means, on the example, that the cell is dead or alive or we don't have any information on the state of the cell. The behavior of all possible trajectories is computed in parallel and the fixed point is reached. The initial state Figure 13(a) yields Figure 13(b) as a fixed point. Here we observe that the indeterminacy concerns at most 4 cells over time.

{0} {0} {0} {0} {0} {1} {0} {0} {0} {0, 1} {1} {0} {0} {0} {0} {0} {0} {0} {0} {0} {0} {0, 1} {0, 1} {0} {0} {0, 1} {0, 1} {0} {0} {0} {0} {0} (

The Koch snowflake

The well-known Koch snowflake is based on segment divisions (variants exist on surfaces, both can be modeled by our formalism). Each segment is recursively divided into three segments of equal length as described in the following picture :

Let us consider the following triangle g as an initial state. g = (N g , P g , PN g , PP g , A g , λ g ) with N g = {1, 2, 3} , P g = {p 1 , q 1 , p 2 , q 2 , p 3 , q 3 }, PN g = {(p 1 , 1), (q 1 , 1), (p 2 , 2), (q 2 , 2), (p 3 , 3), (q 3 , 3)} , PP g = {(p 1 , q 2 ), (p 2 , q 3 ), (p 3 , q 1 )}. λ g (q 1 ) = λ g (q 2 ) = λ g (q 3 ) = {+}.

The attributes of ports are distinguishing attributes. The attributes of nodes corresponds to the R 2 positions of the nodes. Every node got one attribute in R 2 , thus by abuse of notation, we get rid of the set notation of attributes and use a functional one. The ⇒ or ⇒ auto relation applied using the rule depicted in Figure 14

Mesh refinement

Mesh refinement consists in creating iteratively new partitions of the considered space. The initial mesh g we consider is depicted Figure 17. Distinguishing attributes are given on ports. Attributes on nodes are omitted but we can easily consider coordinates. Triangle refinements are given in Figure 16. The three rules verify the symmetry condition and we Figure 16 The rules R T , RU , RV are refinement rules defined e.g. in [START_REF] Bank | Refinement algorithms and data structures for regular local mesh refinement[END_REF] apply the ⇒ auto relation on g to obtain the graph g described in Figure 17. Iteratively, the rewrite system can be applied again on g and so forth.

Conclusion and Related Work

Parallel rewriting technique is a tough issue when it has to deal with overlapping reducible expressions. In this paper, we have proposed a framework, based on the notion of rewriting modulo, to deal with graph transformation where parallel reductions may overlap some parts of the transformed graph. In general, these transformations do no lead to graphs but to a structure we call pregraphs. We proposed sufficient conditions which ensure that graphs are closed under parallel transformations. We also defined two parallel transformations: (i) one that fires all possible rules in parallel (full parallel) and (ii) a second rewrite relation which takes advantage of the possible symmetries that may occur in the rules by reducing the possible number of matches that one has to consider. The two proposed parallel rewrite relations are confluent (up to isomorphisms). Our proposal subsumes some existing formalisms where simultaneous transformations are required such as cellular automata [START_REF] Wolfram | A new kind of science[END_REF] or (extensions of) L-systems [START_REF] Prusinkiewicz | The algorithmic beauty of plants[END_REF]. Indeed, one can easily write graph rewriting systems which define classical cellular automata, with possibly evolving structures (grids) and where the content of a cell, say C, may depend on cells not necessary adjacent to C. As for L-systems, they could be seen as formal (context sensitive) grammars which fire their productions in parallel over a string. Our approach here generalizes L-systems at least in two directions: first by considering graphs instead of strings and second by considering overlapping graph rewrite rules instead of context sensitive (or often context free) rewrite rules. Some graph transformation approaches could also be considered as extension of L-systems such as star-grammars [START_REF] Nagl | Graph-Grammatiken: Theorie, Anwendungen, Implementierung[END_REF] or hyperedge replacement [START_REF] Habel | Hyperedge Replacement: Grammars and Languages[END_REF]. These approaches do not consider overlapping matches but act as context free grammars. However, in [START_REF] Ehrig | Parallel graph grammars[END_REF] parallel graph grammars with overlapping matches have been considered. In that work, overlapping subgraphs remain unchanged after reductions, contrary to our framework which does not require such restrictions. The idea behind parallel graph grammars has been lifted to general replacement systems in [START_REF] Taentzer | Parallel and distributed graph transformation -formal description and application to communication-based systems[END_REF]. Amalgamation, see e.g. [START_REF] Löwe | Algebraic approach to single-pushout graph transformation[END_REF], aims at investigating how the parallel application of two rules can be decomposed into a common part followed by the remainder of the two considered parallel rules. Amalgamation does not consider full parallel rewriting as investigated in this paper. Another approach based on complex transformation has been introduced in [START_REF] Maignan | Global graph transformations[END_REF]. This approach can handle overlapping matches but requires from the user to specify the transformation of these common parts. This requires to provide detailed rules. For instance, the two first cases of the triangle mesh refinement example requires about sixteen rules including local transformations and inclusions, instead of two rules in our framework.

The strength of our approach lies in using an equivalence relation on the resulting pregraph. This equivalence plays an important role in making graphs closed under rewriting. Other relations may also be candidate to equate pregraphs into graphs. we plan to investigate such kind of relations in order to widen the class of rewrite systems that may be applied in parallel on graph structures in presence of overlaps. We also plan to investigate other issues such as stochastic rewriting and conditional rewriting which would be a plus in modeling some natural phenomena. Analysis of the proposed systems remains to be investigated further.

Figure 2

 2 Figure 2 Example of a pregraph H such that: AH= {N ∪ {x1, x2, x3, x4, x5}, +, ×, = ? =}, NH = {n1, n2, n3, n4, n5}, PH = {p2, p3, p4, p5, q2, q3, q4, q5}, PN H = {(p2, n1), (p3, n1), (p4, n1), (p5, n1), (q2, n2), (q3, n3), (q4, n4), (q5, n5)}, PPH reduced to its non symmetric port-port connection is PPH = {(p2, q2), (p3, q3), (p4, q4), (p5, q5)}. λH (ni) = {xi} for i ∈ {1, 2, 3, 4, 5}, λH (pj) = λH (qj) = ∅, for j ∈ {2, 3, 4, 5}.

Figure 3

 3 Figure 3 (a) A pregraph H (b) and its corresponding quotient pregraph H.

Figure 4

 4 Figure4(a) A pregraph H2 and its corresponding quotient pregraph H2 which is a graph. (b) A pregraph H3 and its corresponding quotient pregraph H3 which is not a graph.

,

  PN r = PN new r PN env r , PP r = PP new r PP env r , λ r = λ some additional constraints : (4) on PN r : ∀(p, n) ∈ PN r , (p, n) ∈ PN env r iff (p ∈ P env r and n ∈ N env r and (p, n) ∈ PN env l ). (5) on PP r : ∀(p, p ) ∈ PP r , (p, p ) ∈ PP env r iff (p ∈ P env r and p ∈ P env r and (p, p ) ∈ PP env l ). (6) on λ r : ∀n ∈ N env r , (∃y, (n, y) ∈ λ env r ) iff (λ env r (n) = λ env l (n)) ; ∀y ∈ P env r , (∃y, (p, y) ∈ λ env r ) iff (λ env r (p) = λ env l (p)

Example 13 .

 13 r λ env r ). Then the following properties hold: For all (p, n) ∈ PN r , (p, n) ∈ PN new r iff p ∈ P new r or n ∈ N new r or (p ∈ P env r and n ∈ N env r and (p, n) ∈ PN env l ) For all (p, p ) ∈ PP r , (p, p ) ∈ PP new r iff p ∈ P new r or p ∈ P new r or (p ∈ P env r and p ∈ P env r and (p, p ) ∈ PP env l (p)) For all x ∈ N r ∪ P r , (x, λ r (x)) ∈ λ new r iff x ∈ N new r ∪ P new r or (x, λ l (x)) ∈ λ cut l Let us consider a rule R T : l → r which specifies a way to transform a triangle into four triangle graphs. Figure 5 depicts the rule. Black parts should be understood as members of the cut component of the left-hand side, yellow items are in the environment parts. The red items are new in the right-hand side. More precisely, l env consists of N env l = {α, β, γ}, P env l

  The sets of attributes are empty in this example. Remark. From the definition of an environment sensitive rule, the environment components r env = (N env r , P env r , PN env r , PP env r , A, λ env r ) and l env = (N env l , P env l , PN env l , PP env l , A, λ env l ) are graphs. However, since PP cut l may include ports in P env l and PN cut l may include nodes in N env l or ports in P env l , the cut component l cut = (N cut l , P cut l , PN cut l , PP cut l , A, λ cut l ) is in general neither a graph nor a pregraph. For the same reasons r new = (N new r , P new r , PN new r , PP new r , A, λ new r ) is in general neither a graph nor a pregraph.

Figure 5 Figure 6

 56 Figure 5 Rule RT

Figure 7

 7 Figure 7 Example of a toy rule (a) and a graph H (b)

Figure 9

 9 Figure 9 (a) Subgraph s with distinguishing attributes on ports. The attributes are {1, 2, 3}. (b) Rule RT with distinguishing attributes.

Figure 11

 11 Figure 11 game of life rule

Figure 12

 12 Figure 12 (a) initial grid; (b) fixed point

  , h}} and λ l = λ env l ∪ λ cut l with λ cut l : {i} → A l such that λ cut l (i) = {x i } ; and λ env l : {a, b, c, d, e, f, g, h} → A l such that λ env l (q) = {y q } r = (N r , P r , PN r , PP r , A r , λ r ) with N r = N env r = {i}, P r = ∅, PN r = ∅, PP r = ∅. A r = A l Moreover, on nodes, λ r = λ new r (λ env r being empty) with λ new r : {i} → Att r and λ new r

Figure 13 Figure 14 1 2 3 6

 131413 Figure 13 (a) initial grid; (b) fixed point

  g (p 1 ) = λ g (p 2 ) = λ g (p 3 ) = {-},

2 3 x a + 1 3 x b 2 3 y a + 1 3 y b , λ g (j) = 1 2 ( 3 6 1 2 (x a + x b ) + √ 3 6 (y a -y b ) 1 2 (y a + y b ) + √ 3 6 1 3 x a + 2 3 x b 1 3 y a + 2 3 y b

 2223131311 gives the well known pictures of flakes in Figures 15. Let us denote λ g (a) = x a y a and λ g (b) = x b y b. In this example, the attributes of nodes i, j and k are defined as follows:λ g (i) = 2 3 λ g (a) + 1 3 λ g (b) = λ g (a) + λ g (b)) + √ (λ g (a) T + λ g (b) T ) = (-x a + x b ), andλ g (k) = 1 3 λ g (a) + 2 3 λ g (b) =

Figure 15

 15 Figure 15 Flake results : flake at the different time steps 1,2,3 and 4

Figure 17 g ⇒auto g

  Figure 17 g ⇒auto g

  PP is a symmetric binary relation 2 on ports, PP ⊆ P × P, such that ∀p 1 , p 2 , p 3 ∈

1

. That is to say, ∀p ∈ P, ∀n 1 , n 2 ∈ N , (PN (p, n 1 ) and PN (p, n 2 )) =⇒ n 1 = n 2 . (ii) P, (PP(p 1 , p 2 ) and PP(p 1 , p 3 )) =⇒ p 2 = p 3 and ∀p ∈ P, (p, p) ∈ PP.

  Definition 4 (≡ P , ≡ N ). Let H = (N H , P H , PN H , PP H , A H , λ H ) be a pregraph. We define two equivalence relations ≡ P and ≡ N respectively on ports (P H ) and nodes (N H ) of H as follows: ≡ P is defined as (PP H • PP H ) * ≡ N is defined as (PN - H • ≡ P •PN ) * where • denotes relation composition, -the converse of a relation and * the reflexivetransitive closure of a relation. We write [n] (respectively, [p]) the equivalence class of node n (respectively, port p). speaking, relation ≡ P is the closure of the first part of condition (ii) in Definition 3. The base case says that if two ports p 1 and p 2 are linked to one same port p, then p 1 and p 2 are considered to be equivalent. ≡ N is almost the closure of condition (i) in Definition 3. That is, two nodes n 1 and n 2 , which are associated to one same port (or two equivalent ports), are considered as equivalent nodes. Proposition 1. Let H = (N H , P H , PN H , PP H , A H , λ H ) be a pregraph. The relations ≡ P and ≡ N are equivalence relations.

	Roughly

  • PP) k . Thus (p 1 , p 2 ) ∈ (PP • PP) k +1 . Therefore for all k, p 1 ≡ P k p 2 implies (p 1 , p 2 ) ∈ (PP • PP) k , and thus, p 1 ≡ P p 2 . ⇐ Let p 1 ≡ P p 2 . By definition of ≡ P , there exists a natural number k such that (p 1 , p 2 ) ∈ (PP • PP) k . It is then straightforward that p 1 ≡ P k p 2 . Since the sets of nodes and ports are finite then the limit of the series is reached within a finite number of steps. ⇒ : Let n 1 , n 2 ∈ N H , such that n 1 ≡ N k n 2 for some k , let us prove by induction on k, that (n 1 , n 2 ) ∈≡ N . case k = 0 : obvious. Induction step, case k = k + 1 : Let us assume n 1 ≡ N k +1 n 2 . We distinguish two sub-cases according to the used rules, i.e. Rule II or Rule III. Rule III. According to Rule III, there exists a node n such that n 1 ≡ N k n and n ≡ N k n 2 . From the induction hypothesis, we have n 1 ≡ N k n =⇒ n 1 ≡ N n and n ≡ N k n 2 =⇒ n ≡ N n 2 . Then by transitivity of ≡ N we have n 1 ≡ N n 2 . Rule II. According to Rule II, there exist two ports p 1 and p 2 in P H such that (p 1 , n 1 ) ∈ PN H , (p 2 , n 2 ) ∈ PN H and p 1 ≡ P k p 2 . From Proposition 2, p 1 ≡ P k p 2 =⇒ p 1 ≡ P p 2 , and thus, there exists an index i such that (p 1 , p 2

Likewise, we can easily show the following proposition regarding relation ≡ N . Proposition 3. The limit of the series (≡ N i ) i≥0 is ≡ N .

Proof.

  Definition 5(Quotient Pregraph). Let H = (N H , P H , PN H , PP H , A H , λ H ) be a pregraph and ≡ P and ≡ N two equivalence relations over ports and nodes respectively. We write H the pregraph H = (N H , P H , PN H , PP H , A H , λ H ) where N H

Example 6. Let H = (N H , P H , PN H , PP H , A H , λ H ) be a pregraph as depicted on the left of Figure 3, with N H = {n 1 , n 2 , n 3 , n 4 }, P H = {p 1 , p 2 , p 3 , p 4 , p 5 , p 6 }, PN H = {(p 1 , n 1 ), (p 5 , n 1 ), (p 2 , n 2 ), (p 6 , n 2 ), (p 4 , n 3 ), (p 3 , n 4 )}, PP H = {(p 1 , p 2 ), (p 1 , p 4 ), (p 2 , p 3 ), (p 3 , p 4 ), (p 5 , p 6 )},

  where [x] ∈ N H P H

  obtained following the two steps below: First step: A pregraph H = (N H , P H , PN H , PP H , A H , λ H ) is computed using the different matches and rules as follows:

  and M a set of matches M = {m ai i : l i → G | i = 1 . . . k}. Let G be the pregraph such that G ⇒ I,M G . If ∀p, p ∈ P env , p belongs to the non modified part of the graph. Its connections are unchanged and thus p has at most one port-port connection.Finally, p belongs to a path which is not a loop and H = G is a graph.

		Li , (p, p ) / ∈ PP new Ri , then G is a graph.
	Proof. We have to prove that H does not contain odd loops. Because of the previous
	constraint, it is enough to prove that all ports of H are not parts of a loop.
	If p ∈ ∪ n i=1 P new Ri , it is a new port contained in the graph R i thus p has at most one
	connection port-port.
	If p ∈ ∪ n i=1 P env m a i i (Ri) , p belongs to the graph G and the only new port-port connections where p is involved are those of ∪ n i=1 P new Ri .
	Else, if p ∈ G/ ∪ n i=1 P new Ri	∪ n i=1 P env m a i i (Ri)

The relation PN could be seen as a partial function PN : P → N which associates to a given port p, a node n, PN (p) = n ; thus building a semi-edge "port-node".

The relation PP could also be seen as an injective (partial) function from ports to ports such that ∀p ∈ P, PP(p) = p and ∀p1, p2 ∈ P, PP(p1) = p2 iff PP(p2) = p1.

Here, the function λ l is considered as a set of pairs (x, λ l (x)), i.e. the graph of λ l .

This work has been partly funded by projects CLIMT(ANR/(ANR-11-BS02-016), PEPS égalité (CNRS).

Parallel Graph Rewriting with Overlapping Rules

Figure 10 Sketch of the proof of Proposition 11 i ∈ {1, 2}. The sketch of the proof is depicted in Figure 10. Let us assume that there exist two automorphisms h a : l → l and h a : r → r such that h a (r env ) = h a (r env ). From the hypotheses above, we can easily infer the exitence of two isomorphisms h cv v :

. By definition of a rewrite step, there exist a pregraph g 1 (respect. a pregraph g 2 ) and an injective homomorphism m b1 1 :

). Moreover, since, by definition, r env is included in l env for any environment sensitive rewrite rule l → r, we have m b1

1 . Let us consider x such that x is an element of r env (port or node). We have m b1

) and then we have

Then, for all elements z of the non-modified part of g which is g -m b1

1 (v c1 1 (l)) (z can be a port or a node if y is not a node) such that (z, y) ∈ g, we have that (z, y) ∈ g 1 and (z, y) ∈ g 2 and h

For all types of existing connections (y, z) of g 1 where y and z in

From h d and Proposition 6, we infer the isomorphism h (3)d : g 1 → g 2 , where g 1 = ḡ1 and g 2 = ḡ2 .

Definition 28 (Symmetry Condition

). An ESRR l → r verifies the symmetry condition iff ∀h a ∈ H(l), ∃ u c ∈ H(r), such that ∀x ∈ r env , h a (x) = u c (x)