Parallel Graph Rewriting with Overlapping Rules

TL;DR

This paper investigates the complexities of parallel graph rewriting, especially when overlapping subgraphs are transformed simultaneously, and proposes conditions for ensuring the closure and confluence of such transformations.

Contribution

It introduces and analyzes two parallel rewrite relations for graphs, providing conditions for their closure and confluence, advancing understanding of overlapping graph transformations.

Findings

Proposed sufficient conditions for graph closure under parallel rewriting.

Introduced two parallel rewrite relations: one deterministic, one non-functional.

Established conditions for confluence in non-functional parallel rewriting.

Abstract

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.

Equations

$$\{((h_P^a{)}^{-1}(q),(h_P^a{)}^{-1}(n^{\prime \prime })),((h_P^a{)}^{-1}(q),n_1),((h_P^a{)}^{-1}(q^{\prime }),(h_N^a{)}^{-1}(n^{\prime \prime })),((h_P^a{)}^{-1}(q^{\prime }),n_2)\}\subset {\mathcal{PN}}_H$$

$$f_N^c(x)=\{\begin{array}{ll}x& \text{if }x\in ({\mathcal{N}}_g-{\cup }_{i=1}^k{\mathcal{N}}_{m_i^{b_i}(l_i)}^{cut})\\ {h^{\prime }}_i^{a_i^{\prime }}((h_i^{a_i}{)}^{-1}(x))& \text{if }x\in {\mathcal{N}}_{r_i}^{new},for1\le i\le k\end{array}$$

$$f_P^c(x)=\{\begin{array}{ll}x& \text{if }x\in ({\mathcal{P}}_g-{\cup }_{i=1}^k{\mathcal{P}}_{m_i^{b_i}(l_i)}^{cut})\\ {h^{\prime }}_i^{a_i^{\prime }}((h_i^{a_i}{)}^{-1}(x))& \text{if }x\in {\mathcal{P}}_{r_i}^{new},for1\le i\le k\end{array}$$

Full text

0.1 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.

Rewriting techniques are being investigated for different structures such as strings [4], trees [1] or graphs [20].

Roughly speaking, a rewrite rule can be defined as a pair $l\to 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 ($\to$) 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^{\prime}$ if there exits a rule $l\to r$ such that $l$ occurs in $G$. Then $G^{\prime}$ 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^{\prime}$ by firing, simultaneously, some rules whose left-hand sides occur in $G$. Simultaneous or parallel rewriting of a structure $G$ into $G^{\prime}$ 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 [11], cellular automata (CA) [23] or L-systems [19]. 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. [20]. 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. [16]) 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 [23].

As a simple example illustrating this work, we may refer to mesh refinement [5] and adaptative mesh refinement (AMR) which constitute a very usefull technique in physics [3, 17], astrophysics [12, 6] or in biology [18].

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 0.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 0.4, we define two particular parallel rewrite relations, one performs full parallel rewrite steps whereas the second relation uses the possible symmetries that may occur in the rules and considers only matches up to automorphisms of the left-hand sides. Section 0.5 illustrates our framework through some examples. Concluding remarks and related work are given in Section 0.6.

0.2 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\uplus 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 $\lambda$ which assigns, to elements of a pregraph, attributes in some sets which underly a considered attributes’ structure ${\cal A}$. For instance ${\cal A}$ may be a $\Sigma$-algebra [21] or merely a set.

Definition 1** (Pregraph).**

A pregraph $H$ is a tuple $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ such that :

• •

${\cal N}_{H}$* is a finite set of nodes and ${\cal P}_{H}$ is a finite set of ports,*

• •

${\cal PN}_{H}$* is a relation ${\cal PN}_{H}\subseteq{\cal P}_{H}\times{\cal N}_{H}$,*

• •

${\cal PP}_{H}$* is a symmetric binary relation on ports, ${\cal PP}_{H}\subseteq{\cal P}_{H}\times{\cal P}_{H}$,*

• •

${\cal A}_{H}$* is a structure of attributes,*

• •

$\lambda_{H}$* is a function $\lambda_{H}:{\cal P}_{H}\uplus{\cal N}_{H}\rightarrow 2^{{{\cal A}_{H}}}$ such that $\forall x\in{\cal N}_{H}\uplus{\cal P}_{H},card(\lambda_{H}(x))$ is finite.*

An element $(p,n)$ in ${\cal PN}_{H}$ means that port $p$ is associated to node $n$. An element $(p_{1},p_{2})$ in ${\cal PP}_{H}$ means that port $p$ is linked to port $p_{2}$. In a pregraph, a port can be associated (resp. linked) to several nodes (resp. ports).

Example 1**.**

Figure 1 shows an example of a pregraph where

the node attributes are natural numbers and Figure 2 shows an example where attributes could be expressions such as $\frac{x+y}{2}$.

In Figure 3, node attributes are variables ranging over $\mathbb{N}$. The introduction of variables as attributes allows one to model node neighborhood-sensitive 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 2** (Graph).**

A graph, $G$, is a pregraph $G=({\cal N},{\cal P},{\cal PN},{\cal PP},{\cal A},\lambda)$ such that :

• (i)

${\cal PN}$* is a relation $\subseteq{\cal P}\times{\cal N}$ which associates at most one node to every port111The relation ${\cal PN}$ could be seen as a partial function ${\cal PN}:{\cal P}\rightarrow{\cal N}$ which associates to a given port $p$, a node $n$, ${\cal PN}(p)=n$ ; thus building a semi-edge “port-node”.. That is to say, $\forall p\in{\cal P},\forall n_{1},n_{2}\in{\cal N},((p,n_{1})\in{\cal PN}\;and\;(p,n_{2})\in{\cal PN})\implies n_{1}=n_{2}$.*

• (ii)

${\cal PP}$* is a symmetric binary relation222The relation ${\cal PP}$ could also be seen as an injective (partial) function from ports to ports such that $\forall p\in{\cal P},{\cal PP}(p)\neq p$ and $\forall p_{1},p_{2}\in{\cal P},{\cal PP}(p_{1})=p_{2}$ iff ${\cal PP}(p_{2})=p_{1}$. on ports, ${\cal PP}\subseteq{\cal P}\times{\cal P}$, such that $\forall p_{1},p_{2},p_{3}\in{\cal P},((p_{1},p_{2})\in{\cal PP}$ and $(p_{1},p_{3})\in{\cal PP})\implies p_{2}=p_{3}$ and $\forall p\in{\cal P},(p,p)\not\in{\cal PP}$.*

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, $\equiv^{P}$, and on nodes, $\equiv^{N}$, as defined below.

Definition 3** ($\equiv^{P}$, $\equiv^{N}$).**

Let $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ be a pregraph. We define two relations $\equiv^{P}$ and $\equiv^{N}$ respectively on ports (${\cal P}_{H}$) and nodes (${\cal N}_{H}$) of $H$ as follows:

• •

$\equiv^{P}$* is defined as $({\cal PP}_{H}\bullet{\cal PP}_{H})^{*}$*

• •

$\equiv^{N}$* is defined as $({\cal PN}_{H}^{-}\bullet\equiv^{P}\bullet{\cal PN})^{*}$*

where $\bullet$ denotes relation composition, - the converse of a relation and ∗ the reflexive-transitive closure of a relation. We write $[n]$ (respectively, $[p]$) the equivalence class of node $n$ (respectively, port $p$).

Roughly speaking, relation $\equiv^{P}$ is the closure of the first part of condition (ii) in Definition 2. The base case says that if two ports $p_{1}$ and $p_{2}$ are linked to a same port $p$, then $p_{1}$ and $p_{2}$ are considered to be equivalent. $\equiv^{N}$ is almost the closure of condition (i) in Definition 2. That is, two nodes $n_{1}$ and $n_{2}$, which are associated to a same port (or two equivalent ports), are considered as equivalent nodes.

Proposition 1**.**

Let $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ be a pregraph. The relations $\equiv^{P}$ and $\equiv^{N}$ are equivalence relations.

Proof.

The reflexivity and transitivity of $\equiv^{P}$ and $\equiv^{N}$ follow directly from their respective definitions. The symmetry of ${\cal PP}_{H}$ implies directly the symmetry of $\equiv^{P}$ and $\equiv^{N}$.

∎

Remark 1**.**

The relations $\equiv^{P}$ and $\equiv^{N}$ can be computed incrementally as follows:

Base cases: $\equiv^{P}_{0}=\{(x,x)\mid x\in{\cal P}_{H}\}$ and   $\equiv^{N}_{0}=\{(x,x)\mid x\in{\cal N}_{H}\}$

Inductive steps:

Rule I*: if $q,q^{\prime}\in{\cal P}_{H}$ such that, $q\equiv^{P}_{i}q^{\prime}$, $(q,p_{1})\in{\cal PP}_{H}$ and $(q^{\prime},p_{2})\in{\cal PP}_{H}$ then $p_{1}\equiv^{P}_{i+1}p_{2}$. *

Rule II*: if $p_{1}\in{\cal P}_{H}$, $p_{2}\in{\cal P}_{H}$, $(p_{1},n_{1})\in{\cal PN}_{H}$, $(p_{2},n_{2})\in{\cal PN}_{H}$ and $p_{1}\equiv^{P}_{i}p_{2}$ then $n_{1}\equiv^{N}_{i+1}n_{2}$. *

Rule III*: If $n_{1}\equiv^{N}_{i}n^{\prime}$ and $n^{\prime}\equiv^{N}_{i}n_{2}$ then $n_{1}\equiv^{N}_{i+1}n_{2}$.*

Proposition 2**.**

The limit of the series $(\equiv_{i}^{P})_{i\geq 0}$ is $\equiv^{P}$.

Proof.

Since the set of ports is finite then the limit of the series is reached within a finite number of steps.

$\Rightarrow$ : Let $p_{1},p_{2}\in{\cal P}_{H}$, such that $p_{1}\equiv_{k}^{P}p_{2}$ for some $k$, let us prove by induction on $k$, that $(p_{1},p_{2})\in({\cal PP}\bullet{\cal PP})^{k}$.

• •

case $k=0$ : $p_{1}\equiv_{0}^{P}p_{2}$ thus $p_{1}=p_{2}$ and $(p_{1},p_{2})\in({\cal PP}\bullet{\cal PP})^{0}$.

• •

Induction step, case $k=k^{\prime}+1$ : Let us assume $p_{1}\equiv_{k^{\prime}+1}^{P}p_{2}$. In this case, from rule I, there exist $q,q^{\prime}\in{\cal P}_{H}$ such that, $q\equiv^{P}_{k^{\prime}}q^{\prime}$, $(q,p_{1})\in{\cal PP}_{H}$ and $(q^{\prime},p_{2})\in{\cal PP}_{H}$. $q\equiv^{P}_{k^{\prime}}q^{\prime}$ implies by induction hypothesis that $(q,q^{\prime})\in({\cal PP}\bullet{\cal PP})^{k^{\prime}}$. Thus $(p_{1},p_{2})\in({\cal PP}\bullet{\cal PP})^{k^{\prime}+1}$.

• •

Therefore for all $k$, $p_{1}\equiv_{k}^{P}p_{2}$ implies $(p_{1},p_{2})\in({\cal PP}\bullet{\cal PP})^{k}$, and thus, $p_{1}\equiv^{P}p_{2}$.

$\Leftarrow$ Let $p_{1}\equiv^{P}p_{2}$. By definition of $\equiv^{P}$, there exists a natural number $k$ such that $(p_{1},p_{2})\in({\cal PP}\bullet{\cal PP})^{k}$. It is then straightforward that $p_{1}\equiv_{k}^{P}p_{2}$. ∎

Likewise, we can easily show the following proposition regarding relation $\equiv^{N}$.

Proposition 3**.**

The limit of the series $(\equiv_{i}^{N})_{i\geq 0}$ is $\equiv^{N}$.

Proof.

Since the sets of nodes and ports are finite then the limit of the series is reached within a finite number of steps. $\Rightarrow$ : Let $n_{1},n_{2}\in{\cal N}_{H}$, such that $n_{1}\equiv_{k}^{N}n_{2}$ for some $k$ , let us prove by induction on $k$, that $(n_{1},n_{2})\in\equiv^{N}$.

• •

case $k=0$ : obvious.

• •

Induction step, case $k=k^{\prime}+1$ : Let us assume $n_{1}\equiv_{k^{\prime}+1}^{N}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^{\prime}$ such that $n_{1}\equiv_{k^{\prime}}^{N}n^{\prime}$ and $n^{\prime}\equiv_{k^{\prime}}^{N}n_{2}$. From the induction hypothesis, we have $n_{1}\equiv_{k^{\prime}}^{N}n^{\prime}\implies n_{1}\equiv^{N}n^{\prime}$ and $n^{\prime}\equiv_{k^{\prime}}^{N}n_{2}\implies n^{\prime}\equiv^{N}n_{2}$. Then by transitivity of $\equiv^{N}$ we have $n_{1}\equiv^{N}n_{2}$.

• Rule II.

According to Rule II, there exist two ports $p_{1}$ and $p_{2}$ in ${\cal P}_{H}$ such that $(p_{1},n_{1})\in{\cal PN}_{H}$, $(p_{2},n_{2})\in{\cal PN}_{H}$ and $p_{1}\equiv^{P}_{k^{\prime}}p_{2}$. From Proposition 2, $p_{1}\equiv^{P}_{k^{\prime}}p_{2}\implies p_{1}\equiv^{P}p_{2}$, and thus, there exists an index $i$ such that $(p_{1},p_{2})\in({\cal PP}_{H}\bullet{\cal PP}_{H})^{i}$. Since $(p_{1},n_{1})\in{\cal PN}_{H}$ and $(p_{2},n_{2})\in{\cal PN}_{H}$ we conclude that $(n_{1},n_{2})\in({\cal PN}_{H}^{-}\bullet\equiv^{P}\bullet{\cal PN}_{H})$

$\Leftarrow$ Let $n_{1}\equiv^{N}n_{2}$. Then by definition of $\equiv^{N}$ there exists a natural number $k$ such that $(n_{1},n_{2})\in({\cal PN}_{H}^{-}\bullet\equiv^{P}\bullet{\cal PN}_{H})^{k}$. This means that there is a chain of connections consisting of tuples of the form $(m_{i},p_{i}).p_{i}\equiv^{P}p^{\prime}_{i}.(p^{\prime}_{i},m_{i+1})$ for $i\in\{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^{\prime}$, such that $n_{1}\equiv^{N}_{k^{\prime}}n_{2}$.

∎

The equivalence relations $\equiv^{P}$ and $\equiv^{N}$ are used to introduce the notion of quotient pregraph as defined below.

Definition 4** (Quotient Pregraph).**

Let $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ be a pregraph and $\equiv^{P}$ and $\equiv^{N}$ two equivalence relations over ports and nodes respectively. We write $\overline{H}$ the pregraph  $\overline{H}=({\cal N}_{\overline{H}},{\cal P}_{\overline{H}},{\cal PN}_{\overline{H}},{\cal PP}_{\overline{H}},{\cal A}_{\overline{H}},\lambda_{\overline{H}})$ where ${\cal N}_{\overline{H}}=\{[n]\;|\;n\in{\cal N}_{H}\}$, ${\cal P}_{\overline{H}}=\{[p]\;|\;p\in{\cal P}_{H}\}$, ${\cal PN}_{\overline{H}}=\{([p],[n])\;|\;(p,n)\in{\cal PN}_{H}\}$, ${\cal PP}_{\overline{H}}=\{([p],[q])\;|\;(p,q)\in{\cal PP}_{H}\}$, ${\cal A}_{\overline{H}}={\cal A}_{H}$ and $\lambda_{\overline{H}}([x])=\cup_{x^{\prime}\in[x]}\lambda_{H}(x^{\prime})$ where ${[x]}\in{\cal N}_{\overline{H}}\uplus{\cal P}_{\overline{H}}$

Example 2**.**

*Let $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ be a pregraph as depicted on the left of Figure 4, with ${\cal N}_{H}=\{n_{1},n_{2},n_{3},n_{4}\}$, ${\cal P}_{H}=\{p_{1},p_{2},p_{3},p_{4},p_{5},p_{6}\}$, ${\cal 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})\}$, ${\cal PP}_{H}=\{(p_{1},p_{2}),(p_{1},p_{4}),(p_{2},p_{3}),(p_{3},p_{4}),(p_{5},p_{6})\}$,

${\cal A}_{H}=\mathbb{N}$, $\lambda_{{\cal N}_{H}}(n_{1})=\lambda_{{\cal N}_{H}}(n_{4})=\{1\}$, $\lambda_{{\cal N}_{H}}(n_{2})=\lambda_{{\cal N}_{H}}(n_{3})=\{2\}$, $\forall i\in\{1,...,6\},\lambda_{{\cal P}_{H}}(p_{i})=\emptyset$,*

We obtain $\overline{H}=({\cal N}_{\overline{H}},{\cal P}_{\overline{H}},{\cal PN}_{\overline{H}},{\cal PP}_{\overline{H}},{\cal A}_{\overline{H}},\lambda_{\overline{H}})$, as depicted on the right of Figure 4, with

• •

${\cal N}_{\overline{H}}=\{[n_{1}],[n_{2}]\}$* with $[n_{1}]=\{n_{1},n_{4}\}$, $[n_{2}]=\{n_{2},n_{3}\}$,*

• •

${\cal P}_{\overline{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}\}$,*

• •

${\cal PN}_{\overline{H}}=\{([p_{1}],[n_{1}]),([p_{5}],[n_{1}]),([p_{2}],[n_{2}]),([p_{6}],[n_{2}])\}$,

• •

${\cal PP}_{\overline{H}}=\{([p_{1}],[p_{2}]),([p_{5}],[p_{6}])\}$,

• •

${\cal A}_{\overline{H}}={\cal A}_{H}$**

• •

$\lambda_{{\cal N}_{\overline{H}}}([n_{1}])=\{1\}$, $\lambda_{{\cal N}_{\overline{H}}}([n_{2}])=\{2\}$, $\lambda_{{\cal P}_{\overline{H}}}([p_{1}])=\lambda_{{\cal P}_{\overline{H}}}([p_{2}])=\lambda_{{\cal P}_{\overline{H}}}([p_{5}])=\lambda_{{\cal P}_{\overline{H}}}([p_{6}])=\emptyset$.

Example 3**.**

Figure 5 illustrates two computations of quotient pregraphs.

Remark 2**.**

If $H$ is a graph, $\overline{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.

Definition 5** (Path, Loop).**

• •

A path $\pi_{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 $\pi_{H}(p_{1},p_{k})=(p_{1},p_{2},\ldots,p_{k})$ such that $\{(p_{i},p_{i+1})\;|\;i=1,2,\ldots,k-1\}\subseteq{\cal PP}_{H}$ and $k\in\mathbb{N}$ with $k>0$.

• •

The length of a path $\pi_{H}(p_{1},p_{k})=(p_{1},p_{2},\ldots,p_{k})$ is $\sharp({\pi_{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 $\pi_{H}=(p_{1},p_{2},\ldots,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=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ be a pregraph. Let $q,q^{\prime}$ be two ports in ${\cal P}_{H}$. $q\equiv^{P}q^{\prime}$ iff there exists an even path between $q$ and $q^{\prime}$ in $H$.

Proof.

If $q\equiv^{P}q^{\prime}$ then, by definition, $(q,q^{\prime})\in({\cal PP}_{H}\bullet{\cal PP}_{H})^{*}$ hence there exists an even path between $q$ and $q^{\prime}$. Conversely, if there exists an even path between $q$ and $q^{\prime}$ in $H$ then $(q,q^{\prime})\in({\cal PP}_{H}\bullet{\cal PP}_{H})^{*}$ and thus $q\equiv^{P}q^{\prime}$. ∎

Proposition 5**.**

Let $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ be a pregraph. $\overline{H}$ is a graph iff $H$ has no odd loop.

Proof.

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

• $\Rightarrow$

Assume that ${\cal PP}_{\overline{H}}$ is not anti-reflexive. Then, there exists $q\in{\cal P}_{H}$ such that $([q],[q])\in{\cal PP}_{\overline{H}}$. Thus, either $(q,q)\in{\cal PP}_{H}$ which constitute an odd loop of length one or there exists a port $q^{\prime}$, different from $q$, such that $(q,q^{\prime})\in{\cal PP}_{H}$ and $q^{\prime}\equiv^{P}q$. In this last case, from Proposition4, $q^{\prime}\equiv^{P}q$ implies the existence of an even path from $q^{\prime}$ to $q$. Then adding the link $(q,q^{\prime})$ to this path builds a loop from $q$ to $q$ in $H$ of odd length.

• $\Leftarrow$

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)\in{\cal PP}_{H}$ and in this case $([q],[q])\in{\cal PP}_{\overline{H}}$, or there exists a port $q^{\prime}$ different from $q$ such that the loop is of the form $(q,q^{\prime},\ldots,q)$. In this last case, $(q,q^{\prime})\in{\cal PP}_{H}$ and the path $\pi_{H}(q^{\prime},q)$ is even. Thus, $[q]=[q^{\prime}]$ which implies that $([q],[q])\in{\cal PP}_{\overline{H}}$.

∎

Below, we define the notion of homomorphisms of pregraphs and graphs. This notion assumes the existence of homomorphisms over attributes [7].

Definition 6** (Pregraph and Graph Homomorphism).**

Let $l=({\cal N}_{l},{\cal P}_{l},{\cal PN}_{l},{\cal PP}_{l},{\cal A}_{l},\lambda_{l})$ and $g=({\cal N}_{g},{\cal P}_{g},{\cal PN}_{g},{\cal PP}_{g},{\cal A}_{g},\lambda_{g})$ be two pregraphs. Let $a:{\cal A}_{l}\to{\cal A}_{g}$ be a homomorphism over attributes. A pregraph homomorphism, $h^{a}:l\rightarrow g$, between $l$ and $g$, built over attribute homomorphism $a$, is defined by two functions $h^{a}_{N}:{\cal N}_{l}\rightarrow{\cal N}_{g}$ and $h^{a}_{P}:{\cal P}_{l}\rightarrow{\cal P}_{g}$ such that (i) $\forall(p_{1},n_{1})\in{\cal PN}_{l}$, $(h^{a}_{P}(p_{1}),h^{a}_{N}(n_{1}))\in{\cal PN}_{g},$ (ii) $\forall(p_{1},p_{2})\in{\cal PP}_{l}$, $(h^{a}_{P}(p_{1}),h^{a}_{P}(p_{2}))\in{\cal PP}_{g}$, (iii) $\forall n_{1}\in{\cal N}_{l},a(\lambda_{l}(n_{1}))\subseteq\lambda_{g}(h^{a}_{N}(n_{1}))$ and (iv) $\forall p_{1}\in{\cal P}_{l},a(\lambda_{l}(p_{1}))\subseteq\lambda_{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\in E\}$.

Proposition 6**.**

Let $H$ and $H^{\prime}$ be two isomorphic pregraphs. Then $\overline{H}$ and $\overline{H^{\prime}}$ are isomorphic.

Proof.

Let $h^{a}:H\to H^{\prime}$ be a pregraph isomorphism. We define ${\overline{h^{a}}}:\overline{H}\to\overline{H}^{\prime}$ as follows: for all ports $p,p^{\prime}$ in $H$, nodes $n$ in H, ${\overline{h^{a}_{N}}}([n])={[h^{a}_{N}(n)]}$, ${\overline{h^{a}_{P}}}([p])={[h^{a}_{P}(p)]}$, ${\overline{h^{a}}}([p],[n])={([h^{a}_{P}(p)],[h^{a}_{N}(n)])}$, ${\overline{h^{a}}}([p],[p^{\prime}])={([h^{a}_{P}(p)],[h^{a}_{P}(p^{\prime})])}$.

$\overline{h^{a}}$ is clearly a pregraph isomorphism between $\overline{H}$ and $\overline{H^{\prime}}$. $\overline{h}$ is well defined as illustrated in the following three items.

• •

We show that for all ports $p_{1},p_{2}$ in $H$, $p_{1}\equiv_{H}^{P}p_{2}$ iff $h^{a}_{P}(p_{1})\equiv_{H^{\prime}}^{P}h^{a}_{P}(p_{2})$ :

$h^{a}_{P}(p_{1})\equiv_{H^{\prime}}^{p}h^{a}_{P}(p_{2})$ iff there exists a path $\pi_{H^{\prime}}(h^{a}_{P}(p_{1}),h^{a}_{P}(p_{2}))=(q_{1},q_{2},\ldots q_{k-1},q_{k})$ such that $q_{1}=h^{a}_{P}(p_{1})$, $q_{k}=h^{a}_{P}(p_{2})$ and $\sharp_{\pi_{H^{\prime}}}(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}),\ldots,(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}\equiv_{H}^{p}p_{2}$.

• •

For all nodes $n_{1},n_{2}$ in $H$, we show that $n_{1}\equiv_{H}^{n}n_{2}$ iff $h^{a}_{N}(n_{1})\equiv_{H^{\prime}}^{n}h^{a}_{N}(n_{2})$.

By definition, $h^{a}_{N}(n_{1})\equiv_{H^{\prime}}^{n}h^{a}_{N}(n_{2})$ iff (a) $h^{a}_{N}(n_{1})=h^{a}_{N}(n_{2})$ or (b) there exists $q,q^{\prime}\in{\cal P}_{H^{\prime}}$, $q\equiv_{H^{\prime}}^{p}q^{\prime}$, $(q,h^{a}_{N}(n_{1}))\in{\cal PN}_{H^{\prime}}$ and $(q^{\prime},h^{a}_{N}(n_{2}))\in{\cal PN}_{H^{\prime}}$ or (c) there exists $n^{\prime\prime}\in{\cal N}_{H^{\prime}}$, $h^{a}_{N}(n_{1})\equiv_{H^{\prime}}^{n}n^{\prime\prime}$ and $h^{a}_{N}(n_{2})\equiv_{H^{\prime}}^{n}n^{\prime\prime}$.

$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^{\prime})\in{\cal P}_{H}$, $(h^{a}_{P})^{-1}(q)\equiv_{H^{\prime}}^{p}(h^{a}_{P})^{-1}(q^{\prime})$, $((h^{a}_{P})^{-1}(q),n_{1})\in{\cal PN}_{H}$ and $((h^{a}_{P})^{-1}(q^{\prime}),n_{2})\in{\cal PN}_{H}$. The cases (a) and (b) are straight foward. Let us focus our attention on the case (c) : $h^{a}_{N}(n_{1})\equiv_{H^{\prime}}^{n}h^{a}_{N}(n_{2})$ such that it exists $n^{\prime\prime}\in{\cal N}_{H^{\prime}}$ and $q,q^{\prime}\in{\cal P}_{H^{\prime}}$ which verify the condition $\{(q,n^{\prime\prime}),(q,h(n_{1})),(q^{\prime},n^{\prime\prime}),(q^{\prime},h^{a}_{N}(n_{2}))\}\subset{\cal PN}_{H^{\prime}}$. This is equivalent to : $(h^{a}_{N})^{-1}(n^{\prime\prime})\in{\cal N}_{H}$ and $(h^{a}_{P})^{-1}(q),(h^{a}_{P})^{-1}(q^{\prime})\in{\cal P}_{H}$ which verify the condition

[TABLE]

and in that case $n_{1}\equiv^{N}_{H}n_{2}$. Moreover because $\equiv^{N}$ is transitive we obtain that (c) is equivalent to : there exists $(h^{a}_{N})^{-1}(n^{\prime\prime})\in{\cal N}_{H}$, $n_{1}\equiv_{H}^{n}(h^{a}_{N})^{-1}(n^{\prime\prime})$ and $n_{2}\equiv_{H}^{n}(h^{a}_{N})^{-1}(n^{\prime\prime})$. Thus, $n_{1}\equiv_{H}^{n}n_{2}$.

• •

The pregraph homorphism of $H\to H^{\prime}$ and $\overline{H}\to\overline{H}^{\prime}$ are built over the same attribute homomorphism $a$, thus by construction the points (iii) and (iv) of the previous definition imply $\cup_{n_{i}\in[n]}a(\lambda_{H}(n_{i}))\subset\cup_{n_{i}\in[n]}\lambda_{H^{\prime}}(h^{a}_{N}(n_{i}))$ and $\cup_{p_{i}\in[p]}a(\lambda_{H}(p_{i}))\subset\cup_{p_{i}\in[p]}\lambda_{H^{\prime}}(h^{a}_{P}(p_{i}))$

thus $a(\lambda_{\overline{H}}([n]))\subset\lambda_{\overline{H}^{\prime}}(\overline{h}^{a}_{N}([n]))$ and $a(\lambda_{\overline{H}}([p]))\subset\lambda_{\overline{H}^{\prime}}(\overline{h}^{a}_{P}([p]))$ and $\overline{h^{a}}$ is a pregraph homomorphism from $\overline{H}$ to $\overline{H}^{\prime}$.

∎

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

Definition 7** (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}\equiv G_{2}$ iff the quotient pregraphs $\overline{G_{1}}$ and $\overline{G_{2}}$ are isomorphic.

The relation $\equiv$ over pregraphs is obviously an equivalence relation.

0.3 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 8** (Rewrite Rule, Rewrite System, Variant).**

A rewrite rule is a pair $l\rightarrow r$ where $l$ and $r$ are graphs over the same sets of attributes. A rewrite system $\mathcal{R}$ is a set of rules. A variant of a rule $l\rightarrow r$ is a rule $l^{\prime}\rightarrow r^{\prime}$ where nodes, ports as well as the variables of the attributes are renamed with fresh names.

Let $l^{\prime}\rightarrow r^{\prime}$ be a variant of a rule $l\rightarrow r$. Then there is a renaming mapping $h^{a}$, built over an attribute renaming $a:{\cal A}_{l}\to{\cal A}_{l^{\prime}}$, and consisting of two maps $h^{a}_{N}$ and $h^{a}_{P}$ over nodes and ports respectively : $h^{a}_{N}:{\cal N}_{l}\cup{\cal N}_{r}\to{\cal N}_{l^{\prime}}\cup{\cal N}_{r^{\prime}}$ and $h^{a}_{P}:{\cal P}_{l}\cup{\cal P}_{r}\to{\cal P}_{l^{\prime}}\cup{\cal P}_{r^{\prime}}$ such that, the elements in ${\cal N}_{l^{\prime}}$ and ${\cal P}_{r^{\prime}}$ are new and the restrictions of $h^{a}$ to $l\to l^{\prime}$ (respectively $r\to r^{\prime}$) 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 9** (Environment Sensitive Rewrite Rule, Environment Sensitive Rewrite System).**

An environment sensitive rewrite rule is a rewrite rule (ESRR for short) $l\rightarrow r$ where $l$ and $r$ are graphs over the same attributes ${\cal A}$ such that:

-

$l=({\cal N}_{l},{\cal P}_{l},{\cal PN}_{l},{\cal PP}_{l},{\cal A},\lambda_{l})$* where*

${\cal N}_{l}={\cal N}_{l}^{cut}\uplus$* ${\cal N}_{l}^{env},{\cal P}_{l}={\cal P}_{l}^{cut}\uplus{\cal P}_{l}^{env},{\cal PN}_{l}={\cal PN}_{l}^{cut}\uplus{\cal PN}_{l}^{env},{\cal PP}_{l}={\cal PP}_{l}^{cut}\uplus{\cal PP}_{l}^{env}and\ \lambda_{l}=\lambda_{l}^{cut}\uplus$333Here, the function $\lambda_{l}$ is considered as a set of pairs $(x,\lambda_{l}(x))$, i.e. the graph of $\lambda_{l}$. $\lambda_{l}^{env}$ with some additional constraints :*

• (1)

on ${\cal PN}_{l}$ :* $\forall(p,n)\in{\cal PN}_{l},(n\in{\cal N}_{l}^{cut}$ or $p\in{\cal P}_{l}^{cut})\Rightarrow(p,n)\in{\cal PN}_{l}^{cut}$.*

• (2)

on ${\cal PP}_{l}$ :* $\forall(p,p^{\prime})\in{\cal PP}_{l},p\in{\cal P}_{l}^{cut}\Rightarrow(p,p^{\prime})\in{\cal PP}_{l}^{cut}$.*

• (3)

on $\lambda_{l}$ :* $\forall n\in{\cal N}_{l}^{cut},(n,\lambda_{l}(n))\in\lambda_{l}^{cut}$   and   $\forall p\in{\cal P}_{l}^{cut},(p,\lambda_{l}(p))\in\lambda_{l}^{cut}$.*

-

$r=({\cal N}_{r},{\cal P}_{r},{\cal PN}_{r},{\cal PP}_{r},{\cal A},\lambda_{r})$* where*

${\cal N}_{r}={\cal N}_{r}^{new}\uplus{\cal N}_{r}^{env},{\cal P}_{r}={\cal P}_{r}^{new}\uplus{\cal P}_{r}^{env},{\cal PN}_{r}={\cal PN}_{r}^{new}\uplus{\cal PN}_{r}^{env},{\cal PP}_{r}={\cal PP}_{r}^{new}\uplus{\cal PP}_{r}^{env},\lambda_{r}=\lambda_{r}^{new}\uplus\lambda_{r}^{env}$* such that ${\cal N}_{r}^{env}\subseteq{\cal N}_{l}^{env}$, ${\cal P}_{r}^{env}\subseteq{\cal P}_{l}^{env}$, ${\cal N}_{r}^{new}\cap{\cal N}_{l}^{env}=\emptyset$ and ${\cal P}_{r}^{new}\cap{\cal P}_{l}^{env}=\emptyset$ with some additional constraints :*

• (4)

on ${\cal PN}_{r}$ :* $\forall(p,n)\in{\cal PN}_{r},(p,n)\in{\cal PN}_{r}^{env}$ iff $(p\in{\cal P}_{r}^{env}$ and $n\in{\cal N}_{r}^{env}$ and $(p,n)\in{\cal PN}_{l}^{env})$.*

• (5)

on ${\cal PP}_{r}$ :* $\forall(p,p^{\prime})\in{\cal PP}_{r},(p,p^{\prime})\in{\cal PP}_{r}^{env}$ iff $(p\in{\cal P}_{r}^{env}$ and $p^{\prime}\in{\cal P}_{r}^{env}$ and $(p,p^{\prime})\in{\cal PP}_{l}^{env})$.*

• (6)

on $\lambda_{r}$ :* $\forall n\in{\cal N}_{r}^{env},(\exists y,(n,y)\in\lambda_{r}^{env})$ iff $(\lambda_{r}^{env}(n)=\lambda_{l}^{env}(n))$  ;  *

$\forall y\in{\cal P}_{r}^{env},(\exists y,(p,y)\in\lambda_{r}^{env})$* iff $(\lambda_{r}^{env}(p)=\lambda_{l}^{env}(p)).$*

An environment sensitive rewrite system (ESRS for short) is a set of environment sensitive rewrite rules.

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 (6) 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 $\lambda_{l}^{cut}$ in the left-hand side.

Proposition 7**.**

Let $l\rightarrow r$ be a an ESRR such that $l=({\cal N}_{l}={\cal N}_{l}^{cut}\uplus{\cal N}_{l}^{env},{\cal P}_{l}={\cal P}_{l}^{cut}\uplus{\cal P}_{l}^{env},{\cal PN}_{l}={\cal PN}_{l}^{cut}\uplus{\cal PN}_{l}^{env},{\cal PP}_{l}={\cal PP}_{l}^{cut}\uplus{\cal PP}_{l}^{env},{\cal A},\lambda_{l}=\lambda_{l}^{cut}\uplus\lambda_{l}^{env})$ and $r=({\cal N}_{r}={\cal N}_{r}^{new}\uplus{\cal N}_{r}^{env},{\cal P}_{r}={\cal P}_{r}^{new}\uplus{\cal P}_{r}^{env},{\cal PN}_{r}={\cal PN}_{r}^{new}\uplus{\cal PN}_{r}^{env},{\cal PP}_{r}={\cal PP}_{r}^{new}\uplus{\cal PP}_{r}^{env},{\cal A},\lambda_{r}=\lambda_{r}^{new}\uplus\lambda_{r}^{env})$.

Then the following properties hold:

• •

For all $(p,n)\in{\cal PN}_{r}$, $(p,n)\in{\cal PN}_{r}^{new}$ iff $p\in{\cal P}_{r}^{new}$ or $n\in{\cal N}_{r}^{new}$ or $(p\in{\cal P}_{r}^{env}$ and $n\in{\cal N}_{r}^{env}$ and $(p,n)\not\in{\cal PN}_{l}^{env})$

• •

For all $(p,p^{\prime})\in{\cal PP}_{r}$, $(p,p^{\prime})\in{\cal PP}_{r}^{new}$ iff $p\in{\cal P}_{r}^{new}$ or $p^{\prime}\in{\cal P}_{r}^{new}$ or $(p\in{\cal P}_{r}^{env}$ and $p^{\prime}\in{\cal P}_{r}^{env}$ and $(p,p^{\prime})\not\in{\cal PP}_{l}^{env}(p))$

• •

For all $x\in{\cal N}_{r}\cup{\cal P}_{r}$, $(x,\lambda_{r}(x))\in\lambda_{r}^{new}$ iff $x\in{\cal N}_{r}^{new}\cup{\cal P}_{r}^{new}$ or $(x,\lambda_{l}(x))\in\lambda_{l}^{cut}$

Example 4**.**

*Let us consider a rule $R_{T}:l\rightarrow r$ which specifies a way to transform a triangle into four triangle graphs. Figure 6 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 ${\cal N}_{l}^{env}=\{\alpha,\beta,\gamma\}$, ${\cal P}_{l}^{env}=\{\alpha_{1},\alpha_{2},\beta_{1},\beta_{2},\gamma_{1},\gamma_{2}\}$, ${\cal PN}_{l}^{env}=\{(\alpha_{1},\alpha),(\alpha_{2},\alpha),(\beta_{1},\beta),(\beta_{2},\beta),$ $(\gamma_{1},\gamma),(\gamma_{2},\gamma)\}$, and ${\cal PP}_{l}^{env}=\emptyset$. The cut component of the left-hand side consists of three port-port connections and their corresponding symmetric connections which will not be written : ${\cal PP}_{l}^{cut}=\{(\alpha_{2},\beta_{1}),(\beta_{2},\gamma_{1}),(\gamma_{2},\alpha_{1})\}$. The environment component in the right-hand side allows to reconnect the newly introduced items. $r^{env}$ consists of the ports ${\cal P}_{r}^{env}=\{\alpha_{1},\alpha_{2},\beta_{1},\beta_{2},\gamma_{1},\gamma_{2}\}$. $r^{new}$ consists of ${\cal N}_{r}^{new}=\{U,V,W\}$, ${\cal P}_{r}^{new}=\{u_{1},u_{2},u_{3},u_{4},v_{1},v_{2},v_{3},v_{4},w_{1},w_{2},w_{3},w_{4}\}$,

${\cal PN}_{r}^{new}=\{(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 ${\cal PP}_{r}^{new}=\{(\alpha_{1},w_{2}),(\alpha_{2},u_{1}),(\beta_{1},u_{2}),(\beta_{2},v_{1}),(\gamma_{1},v_{2}),(\gamma_{2},w_{1}),(u_{3},w_{3}),\\ (u_{4},v_{4}),(w_{4},v_{3})\}$. The sets of attributes are empty in this example.*

Remark 3**.**

From the definition of an environment sensitive rule, the environment components $r^{env}=({\cal N}_{r}^{env},{\cal P}_{r}^{env},{\cal PN}_{r}^{env},{\cal PP}_{r}^{env},{\cal A},\lambda_{r}^{env})$ and $l^{env}=({\cal N}_{l}^{env},{\cal P}_{l}^{env},{\cal PN}_{l}^{env},{\cal PP}_{l}^{env},{\cal A},\lambda_{l}^{env})$ are graphs. However, since ${\cal PP}_{l}^{cut}$ may include ports in ${\cal P}_{l}^{env}$ and ${\cal PN}_{l}^{cut}$ may include nodes in ${\cal N}_{l}^{env}$ or ports in ${\cal P}_{l}^{env}$, the cut component $l^{cut}=({\cal N}_{l}^{cut},{\cal P}_{l}^{cut},{\cal PN}_{l}^{cut},{\cal PP}_{l}^{cut},{\cal A},\lambda_{l}^{cut})$ is in general neither a graph nor a pregraph. For the same reasons $r^{new}=({\cal N}_{r}^{new},{\cal P}_{r}^{new},{\cal PN}_{r}^{new},{\cal PP}_{r}^{new},\\ {\cal A},\lambda_{r}^{new})$ is in general neither a graph nor a pregraph.

Finding an occurrence of a left-hand side of a rule within a graph to be transformed consists in finding a match. This notion is defined below.

Definition 10** (Match).**

Let $l$ and $g$ be two graphs. A match $m^{a}:l\to g$ is defined as an injective graph homomorphism. $a:{\cal A}_{l}\to{\cal A}_{g}$ being an injective homomorphism over attributes.

Example 5**.**

Figure 7 gives a graph $l$ and a graph $g$.

Because of ports attributes, only two matches, $m_{1}^{id}$ and $m_{2}^{id}$ can be defined from $l$ to $g$:

• •

$m_{1}^{id}$* : $m_{1}^{id}(\alpha)=E;m_{1}^{id}(\beta)=B$; $m_{1}^{id}(\gamma)=C$; $m_{1}^{id}(\alpha_{1})=e_{1};m_{1}^{id}(\alpha_{2})=e_{2};m_{1}^{id}(\beta_{1})=b_{1};m_{1}^{id}(\beta_{2})=b_{2}$; $m_{1}^{id}(\gamma_{1})=c_{1}$; $m_{1}^{id}(\gamma_{2})=c_{2}$.*

• •

$m_{2}^{id}$* : $m_{2}^{id}(\alpha)=C;m_{2}^{id}(\beta)=D$; $m_{2}^{id}(\gamma)=F$; $m_{2}^{id}(\alpha_{1})=c_{3};m_{2}^{id}(\alpha_{2})=c_{4};m_{2}^{id}(\beta_{1})=d_{1};m_{2}^{id}(\beta_{2})=d_{2}$; $m_{2}^{id}(\gamma_{1})=f_{1}$; $m_{2}^{id}(\gamma_{2})=f_{2}$.*

Notice that the occurrences in $g$ of $m_{1}^{id}(l)$ and $m_{2}^{id}(l)$ overlap on node $C$.

Definition 11** (Rewrite Step).**

Let $l\rightarrow r$ be a rule, $g$ a graph and $m^{a}:l\rightarrow g$ a match. Let $l=({\cal N}_{l}={\cal N}_{l}^{cut}\uplus{\cal N}_{l}^{env},{\cal P}_{l}={\cal P}_{l}^{cut}\uplus{\cal P}_{l}^{env},{\cal PN}_{l}={\cal PN}_{l}^{cut}\uplus{\cal PN}_{l}^{env},{\cal PP}_{l}={\cal PP}_{l}^{cut}\uplus{\cal PP}_{l}^{env},{\cal A},\lambda_{l}=\lambda_{l}^{cut}\uplus\lambda_{l}^{env})$ and $r=({\cal N}_{r}={\cal N}_{r}^{new}\uplus{\cal N}_{r}^{env},{\cal P}_{r}={\cal P}_{r}^{new}\uplus{\cal P}_{r}^{env},{\cal PN}_{r}={\cal PN}_{r}^{new}\uplus{\cal PN}_{r}^{env},{\cal PP}_{r}={\cal PP}_{r}^{new}\uplus{\cal PP}_{r}^{env},{\cal A},\lambda_{r}=\lambda_{r}^{new}\uplus\lambda_{r}^{env})$. A graph $g$ rewrites to $g^{\prime}$ using a match $m^{a}$, written $g\rightarrow g^{\prime}$ or $g\rightarrow_{l\rightarrow r,m^{a}}g^{\prime}$ with $g^{\prime}$ being a pregraph defined as follows: $g^{\prime}=({\cal N}_{g^{\prime}},{\cal P}_{g^{\prime}},{\cal PN}_{g^{\prime}},{\cal PP}_{g^{\prime}},{\cal A}_{g^{\prime}},\lambda_{g^{\prime}})$ such that

• •

${\cal N}_{g^{\prime}}=({\cal N}_{g}-{\cal N}^{cut}_{m^{a}(l)})\uplus{\cal N}^{new}_{r}$**

• •

${\cal P}_{g^{\prime}}=({\cal P}_{g}-{\cal P}^{cut}_{m^{a}(l)})\uplus{\cal P}^{new}_{r}$**

• •

${\cal PN}_{g^{\prime}}=({\cal PN}_{g}-{\cal PN}_{m^{a}(l)}^{cut})\uplus{\cal PN}^{new}_{m^{a}(r)}$**

• •

${\cal PP}_{g^{\prime}}=({\cal PP}_{g}-{\cal PP}^{cut}_{m^{a}(l)})\uplus{\cal PP}^{new}_{m^{a}(r)}$**

• •

${\cal A}_{g^{\prime}}={\cal A}_{g}$* and $\lambda_{g^{\prime}}=(\lambda_{g}-\lambda^{cut}_{m^{a}(l)})\uplus\lambda^{new}_{m^{a}(r)}$*

Notation: Let $p,p^{\prime}$ be ports and $n$ be a node, in notation $m^{a}(r)$ above, $m^{a}(p,p^{\prime})=(m^{a}(p),m^{a}(p^{\prime}))$, $m^{a}(p,n)=(m^{a}(p),m^{a}(n))$, $m^{a}(p)=p$ if $p\in{\cal P}_{r}^{new}$ and $m^{a}(n)=n$ if $n\in{\cal N}_{r}^{new}$.

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^{\prime}$, $g^{\prime}$ is a pregraph. To ensure that $g^{\prime}$ is a graph we provide the following conditions.

Theorem 1**.**

Let $l\rightarrow r$ be an environment sensitive rewrite rule, $g$ a graph and $m^{a}:l\rightarrow g$ a match. Let $g\rightarrow_{l\rightarrow r,m^{a}}g^{\prime}$. $g^{\prime}$ is a graph iff the two following constraints are verified :

If $p\in{\cal P}_{l}^{env}$, $(p,q)\in{\cal PP}_{r}^{new}$ for some port $q$ and there is no $q^{\prime}$ such that $(p,q^{\prime})\in{\cal PP}_{l}^{cut}$, then there is no $q^{\prime\prime}\in{\cal P}_{g}$ such that $(m^{a}(p),q^{\prime\prime})\in{\cal PP}_{g}$. 2. 2.

If $p\in{\cal P}_{l}^{env}$ , $(p,n)\in{\cal PN}_{r}^{new}$ and there is no $n^{\prime}$ such that $(p,n^{\prime})\in{\cal PN}_{l}^{cut}$, then there is no $n^{\prime\prime}\in{\cal N}_{g}$ such that $(m^{a}(p),n^{\prime\prime})\in{\cal PN}_{g}$.

Proof.

$(\Leftarrow)$ Let $p$ be a port of $g^{\prime}$. If the constraints 1. and 2. are verified then

• •

If $p\in g^{\prime}-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\in 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^{\prime}$.

• •

If $p\in{\cal P}_{r}^{new}$. Since $r$ is a graph, $p$ has at most one connection to a node and one connection to a port in $g^{\prime}$.

Thus, $g^{\prime}$ is a graph.

$(\Rightarrow)$ 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 6**.**

Figure 8 (a) gives an example of toy rule. Figure 8 (b) is a graph $H$ such that the match $m_{1}^{id}$ as defined below is a well behaved match, whereas the match $m_{2}^{id}$ is not a well behaved match. $m_{1}^{id}:m_{1}^{id}(\alpha)=A,m_{1}^{id}(\beta)=B,m_{1}^{id}(\alpha_{1})=a_{1},m_{1}^{id}(\beta_{1})=b_{1}$ and $m_{2}^{id}:m_{2}^{id}(\alpha)=C,m_{2}^{id}(\beta)=B,m_{2}^{id}(\alpha_{1})=c_{1},m_{2}^{id}(\beta_{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_{2}^{id}$) 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}\rightarrow r_{1}$ and $l_{2}\rightarrow 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 $r_{1}^{env}$ is part of $l_{2}^{cut}$ 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 12** (compatible rules).**

Two ESRR’s $l_{1}\rightarrow r_{1}$ and $l_{2}\rightarrow r_{2}$ are said to be compatible iff for all graphs $g$ and matches $m_{1}^{a_{1}}:l_{1}\rightarrow g$ and $m_{2}^{a_{2}}:l_{2}\rightarrow g$, (i) no element of $m_{1}^{a_{1}}(r_{1}^{env})$ is in $m_{2}^{a_{2}}(l_{2}^{cut})$ and (ii) no element of $m_{2}^{a_{2}}(r_{2}^{env})$ is in $m_{1}^{a_{1}}(l_{1}^{cut})$.

Conditions (i) and (ii) ensure that the constructions defined by $m_{1}^{a_{1}}(r_{1})$ (respectively by $m_{2}^{a_{2}}(r_{2})$) can actually be performed ; i.e, no element used in $m_{1}^{a_{1}}(r_{1})$ (respectively by $m_{2}^{a_{2}}(r_{2})$) is missing because of its inclusion in $m_{2}^{a_{2}}(l_{2}^{cut})$ (respectively in $m_{1}^{a_{1}}(l_{1}^{cut})$). 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 $\rho_{1}=l_{1}\rightarrow r_{1}$ and $\rho_{2}=l_{2}\rightarrow r_{2}$ be two rules. Assume that $\rho_{1}$ and $\rho_{2}$ are not compatible. Then there exists a graph $G$ such that:

• •

there exists a match $m_{1}^{a_{1}}:l_{1}\to G$

• •

there exists a match $m_{2}^{a_{2}}:l_{2}\to G$

• •

w.l.o.g, we assume that there exists an element, say $e$, in $m_{1}^{a_{1}}(r_{1}^{env})$ which belongs also to $m_{2}^{a_{2}}(l_{2}^{cut})$.

Graph $G$ can be built as follows: Let $d$ be a graph such that there exist two injective homomorphisms $h_{1}:d\rightarrow m_{1}^{a_{1}}(l_{1})$ and $h_{2}:d\rightarrow m_{2}^{a_{2}}(l_{2})$ such that $G$ is obtained as a pushout of $h_{1}$ and $h_{2}$. That is to say, there exist two injective homomorphisms $h^{\prime}_{1}:m_{1}^{a_{1}}(l_{1})\to G$ and $h^{\prime}_{2}:m_{2}^{a_{2}}(l_{2})\to G$ such that $h^{\prime}_{1}(h_{1}(d))=h^{\prime}_{2}(h_{2}(d))$. We consider subgraphs $d$ which contain at least $h_{1}^{-1}((m_{1}^{a_{1}})^{-1}(e))$ which is equal to $h_{2}^{-1}((m_{2}^{a_{2}})^{-1}(e))$. Notice that elements of graph $d$ could be attributed by empty sets.

Therefore, to check whether two rules $\rho_{1}=l_{1}\rightarrow r_{1}$ and $\rho_{2}=l_{2}\rightarrow r_{2}$ are compatible, one has to check whether there exist a subgraph $d$ and two injective homomorphisms $h:d\rightarrow l_{1}$ and $h^{\prime}:d\rightarrow l_{2}$ such that $d$ contains an item, $e$, such that $h(e)\in l_{1}^{cut}$ and $h^{\prime}(e)\in r_{2}^{env}$ ($h(e)\in r_{l}^{env}$ and $h^{\prime}(e)\in l_{2}^{cut}$) . Since homomorphisms $h$ and $h^{\prime}$ 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^{\prime}$ exist iff the two rules are not compatible. Indeed the graph $G^{\prime}$ obtained as a pushout of homomorphisms $h$ and $h^{\prime}$ contains at least one item which can be matched either by $l_{i}^{env}$ (and remains in $r_{i}^{env}$) and $l_{j}^{cut}$ with $(i,j)\in\{(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 13**.**

A conflict free environment sensitive graph rewrite system is an ESRS consisting of pairwise compatible rules.

Definition 14** (parallel rewrite step).**

Let $\mathcal{R}$ be a conflict free environment sensitive graph rewrite system $\mathcal{R}=\{L_{i}\rightarrow R_{i}\mid i=1\ldots n\}$. Let $G$ be a graph. Let $I$ be a set of variants of rules in $\mathcal{R}$, $I=\{l_{i}\rightarrow r_{i}\mid i=1\ldots k\}$ and $M$ a set of matches $M=\{m_{i}^{a_{i}}:l_{i}\rightarrow G\mid i=1\dots k\}$. We say that graph $G$ rewrites into a pregraph $G^{\prime}$ using the rules in $I$ and matches in $M$, written $G\Rightarrow_{I,M}G^{\prime}$, $G\Rightarrow_{M}G^{\prime}$ or simply $G\Rightarrow G^{\prime}$ if $G^{\prime}$ is obtained following the two steps below:

First step:* A pregraph $H=({\cal N}_{H},{\cal P}_{H},{\cal PN}_{H},{\cal PP}_{H},{\cal A}_{H},\lambda_{H})$ is computed using the different matches and rules as follows:*

• •

${\cal N}_{H}=({\cal N}_{G}-\cup_{i=1}^{k}{\cal N}_{m_{i}^{a_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal N}_{r_{i}}^{new}$**

• •

${\cal P}_{H}=({\cal P}_{G}-\cup_{i=1}^{k}{\cal P}_{m_{i}^{a_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal P}_{r_{i}}^{new}$**

• •

${\cal PN}_{H}=({\cal PN}_{G}-\cup_{i=1}^{k}{\cal PN}_{m_{i}^{a_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal PN}_{m_{i}^{a_{i}}(r_{i})}^{new}$**

• •

${\cal PP}_{H}=({\cal PP}_{G}-\cup_{i=1}^{k}{\cal PP}_{m_{i}^{a_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal PP}_{m_{i}^{a_{i}}(r_{i})}^{new}$**

• •

${\cal A}_{H}={\cal A}_{G}$* and $\lambda_{H}=(\lambda_{G}-\cup_{i=1}^{k}\lambda_{m_{i}^{a_{i}}(l_{i})}^{cut})\cup\cup_{i=1}^{n}\lambda_{m_{i}^{a_{i}}(r_{i})}^{new}$*

second step*: $G^{\prime}=\overline{H}$*

Notice that the rewrite step $G\Rightarrow G^{\prime}$ is a rewrite modulo step [16] of the form $G\to H\equiv\overline{H}$.

Example 7**.**

Let us consider the graph $g$ depicted below and the following two matches, $m_{1}$ and $m_{2}$, of the rule $R_{T}$ depicted in Figure 6.

• •

$m_{1}$* : $m_{1}(\alpha)=E;m_{1}(\beta)=B$; $m_{1}(\gamma)=C$; $m_{1}(\alpha_{1})=e_{1};m_{1}(\alpha_{2})=e_{2};m_{1}(\beta_{1})=b_{1};m_{1}(\beta_{2})=b_{2}$; $m_{1}(\gamma_{1})=c_{1}$; $m_{1}(\gamma_{2})=c_{2}$. The isomorphism of the port-node and port-port connections are easily deduced.*

• •

$m_{2}$* : $m_{2}(\alpha)=B;m_{2}(\beta)=D$; $m_{2}(\gamma)=C$; $m_{2}(\alpha_{1})=b_{2};m_{2}(\alpha_{2})=b_{3};m_{2}(\beta_{1})=d_{2};m_{2}(\beta_{2})=d_{1}$; $m_{2}(\gamma_{1})=c_{3}$; $m_{2}(\gamma_{2})=c_{1}$.*

The two matches overlap.

Figure 9 shows the different steps of the application of two matches of the rule defined in Figure 6. The pregraph, $H$, in the middle is obtained after the first step of Definition 14. Its quotient pregraph, $G^{\prime}$, is the graph on the right. $G^{\prime}$ 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 5), 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 2**.**

Let $\mathcal{R}$ be a conflict free environment sensitive graph rewrite system $\mathcal{R}=\{L_{i}\rightarrow R_{i}\mid i=1\ldots n\}$. Let $G$ be a graph. Let $I$ be a set of variants of rules in $\mathcal{R}$, $I=\{l_{i}\rightarrow r_{i}\mid i=1\ldots k\}$ and $M$ a set of matches $M=\{m_{i}^{a_{i}}:l_{i}\rightarrow G\mid i=1\dots k\}$. Let $G^{\prime}$ be the pregraph such that $G\Rightarrow_{I,M}G^{\prime}$. If $\forall p,p^{\prime}\in{\cal P}_{L_{i}}^{env}$, $(p,p^{\prime})\notin{\cal PP}_{R_{i}}^{new}$, then $G^{\prime}$ 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\in\cup_{i=1}^{n}{\cal P}_{R_{i}}^{new}$, it is a new port contained in the graph $R_{i}$ thus $p$ has at most one connection port-port.

• •

If $p\in\cup_{i=1}^{n}{\cal P}_{m_{i}^{a_{i}}(R_{i})}^{env}$, $p$ belongs to the graph $G$ and the only new port-port connections where $p$ is involved are those of $\cup_{i=1}^{n}{\cal P}_{R_{i}}^{new}$.

• •

Else, if $p\in G/\cup_{i=1}^{n}{\cal P}_{R_{i}}^{new}\uplus\cup_{i=1}^{n}{\cal P}_{m_{i}^{a_{i}}(R_{i})}^{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 $\overline{H}=G^{\prime}$ is a graph.

∎

0.4 Two Parallel Rewrite Relations

The set of matches, $M$, in Definition 14 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 left-hand sides’ automorphisms.

0.4.1 Full Parallel Rewrite Relation

We start by a technical definition of an equivalence relation, $\approx$, over matches.

Definition 15** ($\approx$).**

Let $L\to R$ be a rule and $G$ a graph. Let $l_{1}\to r_{1}$ and $l_{2}\to r_{2}$ be two variants of the rule $L\to R$. We denote by $h^{a_{1}}_{1}$ (respect. $h^{a_{2}}_{2}$) the (node, port and attribute) renaming mapping such that the restriction of $h^{a_{1}}_{1}$ (respectively, $h^{a_{2}}_{2}$) to $L\to l_{1}$ (respectively $L\to l_{2}$) is a graph isomorphism. Let $m^{b_{1}}_{1}:l_{1}\to G$ and $m^{b_{2}}_{2}:l_{2}\to G$ be two matches. We say that $m^{b_{1}}_{1}$ and $m^{b_{2}}_{2}$ are equivalent and write $m^{b_{1}}_{1}\approx m^{b_{2}}_{2}$ iff for all elements $x$ (in ${\cal P}_{L}$, ${\cal N}_{L}$, ${\cal PP}_{L}$ or ${\cal PN}_{L}$) of $L$, $m^{b_{1}}_{1}(h^{a_{1}}_{1}(x))=m^{b_{2}}_{2}(h^{a_{2}}_{2}(x))$ and for all $x$ in ${\cal A}_{L}$, ${b_{1}}({a_{1}}(x))={b_{2}}({a_{2}}(x))$ .

The relation $\approx$ is clearly an equivalence relation. Intuitively, two matches $m^{b_{1}}_{1}:l_{1}\to G$ and $m^{b_{2}}_{2}:l_{2}\to G$ are equivalent, $m^{b_{1}}_{1}\approx m^{b_{2}}_{2}$, whenever (i) $l_{1}$ and $l_{2}$ are left-hand sides of two variants of a same rule, say $L\to R$, and (ii) $m^{b_{1}}_{1}$ and $m^{b_{2}}_{2}$ coincide on each element $x$ of $L$.

Definition 16** (full parallel matches).**

*Let $\mathcal{R}$ be a graph rewrite system and $G$ a graph. Let ${\cal M}_{\mathcal{R}}(G)=\{m^{a_{i}}_{i}:l_{i}\to G\;|\;m^{a_{i}}_{i}\mbox{ is a match and }l_{i}\to r_{i}\mbox{ is a variant of a rule in }\mathcal{R}\}$. A set, $M$, of full parallel matches, with respect to a graph rewrite system $\mathcal{R}$ and a graph $G$, is a maximal set such that (i) $M\subset{\cal M}_{{\cal R}}(G)$ and (ii) $\forall m^{a_{1}}_{1},m^{a_{2}}_{2}\in M,m^{a_{1}}_{1}\not\approx m^{a_{2}}_{2}$. *

A set of full parallel matches $M$ is not unique because any rule in $\mathcal{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 $\mathcal{R}$ and a graph $G$. Then $M$ is finite.

Proof.

We assume that $G$ has a finite number of nodes, ports and attributes and $\mathcal{R}$ has a finite number of rules. Let $l_{i}\to r_{i}$ be a rule in $\mathcal{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 $\binom{k_{i}}{n}\times k_{i}!$ where $n=card({\cal N}_{G})+card({\cal P}_{G})$ and $k_{i}=card({\cal N}_{l_{i}})+card({\cal P}_{l_{i}})$. Thus $card(M)$ is bounded by $\Pi_{1\leq i\leq card(\mathcal{R})}\binom{k_{i}}{n}\times 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 $\lambda_{l_{i}}(x)\not=\emptyset$). Let $m^{a}:l_{i}\to G$ be a match. $m$ is a non-attributed graph homomorphism and $a:{\cal A}_{l_{i}}\to{\cal 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^{\prime}_{i}$ be the graph obtained from $l_{i}$ by removing all attributes (or equivalently said, by setting the attribute function $\lambda_{l^{\prime}_{i}}$ to the empty set. Let $C_{i}=max({C_{m}|m\mbox{ is a non-attributed graph homomorphism }m:l^{\prime}_{i}\to G})$. $C_{i}$ exists since we assume that the matching problem is finitary. Then $card(M)$ is bounded by $\Pi_{1\leq i\leq card(\mathcal{R})}\binom{k_{i}}{n}\times k_{i}!\times C_{i}$ which is finite since $n$, the $k_{i}$’s and the $C_{i}$’s are finite.

∎

Definition 17** (full parallel rewriting).**

Let $\mathcal{R}$ be an ESRS and $G$ a graph. Let $M$ be a set of full parallel matches with respect to $\mathcal{R}$ and $G$. We define the full parallel rewrite relation and write $G\displaystyle\rightrightarrows_{M}G^{\prime}$ or simply $G\displaystyle\rightrightarrows G^{\prime}$, as the parallel rewrite step $G\Rightarrow_{M}G^{\prime}$.

Proposition 10**.**

Let $\mathcal{R}$ be an ESRS. The rewrite relation $\displaystyle\rightrightarrows$ is deterministic. That is to say, for all graphs $g$, $(g\displaystyle\rightrightarrows g_{1}\;and\;g\displaystyle\rightrightarrows 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\displaystyle\rightrightarrows_{M_{1}}g_{1}$ and $g\displaystyle\rightrightarrows_{M_{2}}g_{2}$. By definition of sets of full parallel matches, for all matches $m^{b}\in M_{1}$ there exists a match $m^{\prime b^{\prime}}\in{M}_{2}$ such that $m^{b}\approx m^{\prime b^{\prime}}$. Since $M_{1}$ and $M_{2}$ are finite (see Proposition 9), there exists a natural number $k$ such that $M_{1}=\{m_{1}^{b_{1}},m_{2}^{b_{2}},\ldots,m_{k}^{b_{k}}\}$ and $M_{2}=\{m_{1}^{\prime b_{1}^{\prime}},m_{2}^{\prime b^{\prime}_{2}},\ldots,m_{k}^{\prime b^{\prime}_{k}}\}$ such that for all $i\in\{1,\dots,k\}$, $m_{i}^{b_{i}}\approx m_{i}^{\prime b^{\prime}_{i}}$. Therefore, for every $i$ such that $1\leq i\leq k$, there exist a rule $L_{i}\to R_{i}$ in $\mathcal{R}$ and two variants of it $l_{i}\to r_{i}$ and $l^{\prime}_{i}\to r^{\prime}_{i}$ together with two renaming mappings $h_{i}^{a_{i}}:L_{i}\to l_{i}$ and $h_{i}^{\prime a^{\prime}_{i}}:L_{i}\to l^{\prime}_{i}$ such that for all elements $x\in L_{i}$, $m_{i}^{b_{i}}(h_{i}^{a_{i}}(x))=m_{i}^{\prime b^{\prime}_{i}}(h_{i}^{\prime a^{\prime}_{i}}(x))$.

By Definitions 14 and 17, 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

• •

${\cal N}_{H_{1}}=({\cal N}_{g}-\cup_{i=1}^{k}{\cal N}_{m_{i}^{b_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal N}_{r_{i}}^{new}$

• •

${\cal N}_{H_{2}}=({\cal N}_{g}-\cup_{i=1}^{k}{\cal N}_{{m^{\prime}}_{i}^{b^{\prime}_{i}}({l^{\prime}}_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal N}_{{r^{\prime}}_{i}}^{new}$

• •

${\cal P}_{H_{1}}=({\cal P}_{g}-\cup_{i=1}^{k}{\cal P}_{m_{i}^{b_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal P}_{r_{i}}^{new}$

• •

${\cal P}_{H_{2}}=({\cal P}_{g}\cup_{i=1}^{k}{\cal P}_{{m^{\prime}}_{i}^{b^{\prime}_{i}}({l^{\prime}}_{i})}^{cut})\uplus\cup_{i=1}^{k}{\cal P}_{{r^{\prime}}_{i}}^{new}$

• •

$\lambda_{H_{1}}=(\lambda_{g}-\cup_{i=1}^{k}\lambda_{m_{i}^{b_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}\lambda_{r_{i}}^{new}$

• •

$\lambda_{H_{2}}=(\lambda_{g}-\cup_{i=1}^{k}\lambda_{{m^{\prime}}_{i}^{{b^{\prime}}_{i}}(l_{i})}^{cut})\uplus\cup_{i=1}^{k}\lambda_{r_{i}}^{new}$

Now, We define a map $f^{c}:H_{1}\to H_{2}$ by means of three maps on nodes, ports and attributes $f^{c}_{N}:{\cal N}_{H_{1}}\to{\cal N}_{H_{2}}$, $f^{c}_{P}:{\cal P}_{H_{1}}\to{\cal P}_{H_{2}}$ and $c:{\cal A}_{H_{1}}\to{\cal A}_{H_{2}}$ as follows

[TABLE]

[TABLE]

and $c(x)=\begin{cases}b_{i}^{\prime}\circ a_{i}^{\prime}\circ a_{i}^{-1}\circ b_{i}^{-1}(x)&\text{if }\exists i\in\{1,\ldots,k\},\exists e\in({\cal N}_{H_{1}}\cup{\cal P}_{H_{1}}),(e,x)\in\lambda^{new}_{r_{i}}\\ x&\text{otherwise}\end{cases}$

$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 8**.**

**

Let us consider the rule $R_{T}$ defined in Figure 6 and the subgraph $s$ depicted on the side. The reader can verify that there are six different matches, $m_{1}\ldots 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}(\alpha)=E;m_{1}(\beta)=B$; $m_{1}(\gamma)=C$; $m_{1}(\alpha_{1})=e_{1};m_{1}(\alpha_{2})=e_{2};m_{1}(\beta_{1})=b_{1};m_{1}(\beta_{2})=b_{2}$; $m_{1}(\gamma_{1})=c_{1}$; $m_{1}(\gamma_{2})=c_{2}$.*

• •

$m_{2}$* : $m_{2}(\alpha)=E;m_{2}(\beta)=C$; $m_{2}(\gamma)=B$; $m_{2}(\alpha_{1})=e_{2};m_{2}(\alpha_{2})=e_{1};m_{2}(\beta_{1})=c_{2};m_{2}(\beta_{2})=c_{1}$; $m_{2}(\gamma_{1})=b_{2}$; $m_{2}(\gamma_{2})=b_{1}$.*

• •

$m_{3}$* : $m_{3}(\alpha)=B;m_{3}(\beta)=E$; $m_{3}(\gamma)=C$; $m_{3}(\alpha_{1})=b_{2};m_{3}(\alpha_{2})=b_{1};m_{3}(\beta_{1})=e_{2};m_{3}(\beta_{2})=e_{1}$; $m_{3}(\gamma_{1})=c_{2}$; $m_{3}(\gamma_{2})=c_{1}$.*

• •

$m_{4}$* : $m_{4}(\alpha)=B;m_{4}(\beta)=C$; $m_{4}(\gamma)=E$; $m_{4}(\alpha_{1})=b_{1};m_{4}(\alpha_{2})=b_{2};m_{4}(\beta_{1})=c_{1};m_{4}(\beta_{2})=c_{2}$; $m_{3}(\gamma_{1})=e_{1}$; $m_{4}(\gamma_{2})=e_{2}$.*

• •

$m_{5}$* : $m_{5}(\alpha)=C;m_{5}(\beta)=B$; $m_{5}(\gamma)=E$; $m_{5}(\alpha_{1})=c_{2};m_{5}(\alpha_{2})=c_{1};m_{5}(\beta_{1})=b_{2};m_{5}(\beta_{2})=b_{1}$; $m_{5}(\gamma_{1})=e_{2}$; $m_{5}(\gamma_{2})=e_{1}$.*

• •

$m_{6}$* : $m_{5}(\alpha)=C;m_{5}(\beta)=E$; $m_{5}(\gamma)=B$; $m_{5}(\alpha_{1})=c_{1};m_{5}(\alpha_{2})=c_{2};m_{5}(\beta_{1})=e_{1};m_{5}(\beta_{2})=e_{2}$; $m_{5}(\gamma_{1})=b_{1}$; $m_{5}(\gamma_{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\times 6$ new nodes and $12\times 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 8 by the rule $R_{T}$, one option is to apply full parallel rewrite relation with distinguishing attributes on the subgraph depicted in Figure 10 (a) and rule $R_{T}$ with distinguishing attributes given in Figure 10 (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.

0.4.2 Parallel Rewrite Relation up to Automorphisms

Let us consider a graph $g$ which rewrites into $g_{1}$ and $g_{2}$ using an ESRR $l\to r$. This means that there exist two matches $\mu^{\beta_{i}}_{i}:l\to g$ with $i\in\{1,2\}$ such that $g\Rightarrow_{l\rightarrow r,\mu^{\beta_{i}}_{i}}g_{i}$. One may wonder whether $g_{1}$ and $g_{2}$ are the same (up to isomorphism) whenever matches $\mu^{\beta_{1}}_{1}$ and $\mu^{\beta_{2}}_{2}$ are linked by means of an automorphism of $l$. That is to say, when there exists an automorphism $h^{a}:l\to l$ with $\mu^{\beta_{1}}_{1}=\mu^{\beta_{2}}_{2}\circ h^{a}$. Intuitively, matches $\mu^{\beta_{1}}_{1}$ and $\mu^{\beta_{2}}_{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 ${\cal A}$. We write $H(g)$ to denote the set of automorphisms of $g$, i.e. $H(g)$ is the set of isomorphisms $h^{a}:g\to g$, with $a$ being an isomorphism on the attributes of $g$, $a:{\cal A}\to{\cal A}$.

Proposition 11**.**

Let $l\to r$ be an ESRR. let $l_{1}\to r_{1}$ and $l_{2}\to r_{2}$ be two variants of the rule $l\to r$. Let $v_{1}^{c_{1}}$, $v_{1}^{\prime c_{1}}$, $v_{2}^{c_{2}}$, $v_{2}^{\prime c_{2}}$ be the isomorphisms reflecting the variant status of these two rules with $v_{1}^{c_{1}}:l\to l_{1}$, $v_{1}^{\prime c_{1}}:r\to r_{1}$, $v_{2}^{c_{2}}:l\to l_{2}$ and $v_{2}^{\prime c_{2}}:r\to r_{2}$ such that $l_{i}=v_{i}^{c_{i}}(l)$, $r_{i}=v_{i}^{\prime c_{i}}(r)$ and $v_{i}^{c_{i}}(r_{i}^{env})=v_{i}^{\prime c_{i}}(r_{i}^{env})$ for $i\in\{1,2\}$. Let $g$ be a graph and $g^{\prime}_{1}$ and $g^{\prime}_{2}$ be two pregraphs. Let $g\Rightarrow_{l_{1}\rightarrow r_{1},m^{b_{1}}_{1}}g_{1}^{\prime}$ and $g\Rightarrow_{l_{2}\rightarrow r_{2},m^{b_{2}}_{2}}g_{2}^{\prime}$ be two rewrite steps such that there exist two automorphisms $h^{a}:l\to l$ and $h^{\prime a}:r\to r$ such that (i) with $m^{b_{1}}_{1}=m^{b_{2}}_{2}\circ v_{2}^{c_{2}}\circ h^{a}\circ(v_{1}^{c_{1}})^{-1}$ and (ii) for all elements $x$ of $r^{env}$, $h^{\prime a}(x)=h^{a}(x)$. Then, $g_{1}^{\prime}$ and $g_{2}^{\prime}$ are isomorphic.

Sketch.

The sketch of the proof is depicted in Figure 11. The attributes structures used in the rule $l\to r$ (respectively, $l_{1}\to r_{1}$ and $l_{2}\to r_{2}$) are denoted $A$ (respectively, $A_{1}$ and $A_{2}$) whereas the attibutes structure of the transfomed graph $g$ is denoted $B$. From the hypotheses, we can easily infer the exitence of two isomorphisms $h_{v}^{c_{v}}:l_{1}\to l_{2}$ and $h_{v}^{\prime c_{v}}:r_{1}\to r_{2}$ such that $h_{v}^{c_{v}}=v_{2}^{c_{2}}\circ h^{a}\circ(v_{1}^{c_{1}})^{-1}$ and $h_{v}^{\prime c_{v}}=v_{2}^{\prime c_{v}}\circ h^{\prime a}\circ(v_{1}^{\prime c_{1}})^{-1}$. And we have $c_{v}=c_{2}\circ a\circ c_{1}^{-1}$.

Let $g\Rightarrow_{l_{1}\rightarrow r_{1},m_{1}^{b_{1}}}g_{1}^{\prime}$ and $g\Rightarrow_{l_{2}\rightarrow r_{2},m_{2}^{b_{2}}}g_{2}^{\prime}$ such that $m_{1}^{b_{1}}(l_{1})=m_{2}^{b_{2}}(l_{2})$. By definition of a rewrite step, there exist a pregraph $g_{1}$ (respect. a pregraph $g_{2}$) and an injective homomorphism $m_{1}^{\prime b_{1}}:r_{1}\to g_{1}$ (respect. $m_{2}^{\prime b_{2}}:r_{2}\to g_{2}$) such that $g^{\prime}_{1}=\overline{g}_{1}$ (respect. $g^{\prime}_{2}=\overline{g}_{2}$). Moreover, since, by definition, $r^{env}$ is included in $l^{env}$ for any ESRR $l\to r$, we have $m_{1}^{\prime b_{1}}(r_{1}^{env})=m_{1}^{b_{1}}(r_{1}^{env})$ (respect. $m_{2}^{\prime b_{2}}(r_{2}^{env})=m_{2}^{b_{2}}(r_{2}^{env})$), where $m_{i}^{\prime b_{i}}$, for $i\in\{1,2\}$, are defined as follows:

for n\in{\cal N}_{r_{i}},{m^{\prime}}^{b_{i}}_{i}(n)=\left\{\begin{array}[]{l}m^{b_{i}}_{i}(n)\;if\;n\in{\cal N}_{r_{i}}^{env}\\ n\;otherwise(n\in{\cal N}_{r_{i}}^{new})\end{array}\right.

for p\in{\cal P}_{r_{i}},{m^{\prime}}^{b_{i}}_{i}(p)=\left\{\begin{array}[]{l}m^{b_{i}}_{i}(p)\;if\;p\in{\cal P}_{r_{i}}^{env}\\ p\;otherwise(p\in{\cal P}_{r_{i}}^{new})\end{array}\right.

Now, let us define the isomorphism $h^{\prime\prime d}:g_{1}\to g_{2}$ with $d(x)=$ if $x\in b_{1}(A_{1})$ then $b_{2}\circ c_{v}\circ b_{1}^{-1}(x)$ else $x$. Let us consider $x$ such that $x$ is an element of $r^{env}$ (port or node). We have $m_{1}^{b_{1}}(v_{1}^{c_{1}}(x))=m_{2}^{b_{2}}(v_{2}^{c_{2}}(h^{a}(x)))$ is an element of $g$. Moreover $m_{1}^{\prime b_{1}}(v_{1}^{\prime c_{1}}(x))\in g_{1}$ and $m_{2}^{\prime b_{2}}(v_{2}^{\prime c_{2}}({h^{\prime}}^{a}(x))\in g_{2}$. Let us denote $y=m_{1}^{b_{1}}(v_{1}^{c_{1}}(x))$. By construction $m_{1}^{\prime b_{1}}(v_{1}^{\prime c_{1}}(x))=m_{1}^{b_{1}}(v_{1}^{c_{1}}(x))=y$ because $x\in r^{env}$. From the hypothesis we have $h^{a}(x)={h^{\prime}}^{a}(x)$. Thus $m_{2}^{\prime b_{2}}(v_{2}^{\prime c_{2}}({h^{\prime}}^{a}(x))=m_{2}^{\prime b_{2}}(v_{2}^{\prime c_{2}}(h^{a}(x))$ and then we have $m_{2}^{\prime b_{2}}(v_{2}^{\prime c_{2}}({h^{\prime}}^{a}(x))=m_{2}^{b_{2}}(v_{2}^{c_{2}}(h^{a}(x))=y$. Then, for all elements $z$ of the non-modified part of $g$ which is $g-m_{1}^{b_{1}}(v_{1}^{c_{1}}(l))$ ($z$ can be a port or a node if $y$ is not a node) such that $(z,y)\in g$, we have that $(z,y)\in g_{1}$ and $(z,y)\in g_{2}$ and ${h^{\prime\prime}}^{d}=Id^{d}$ on $g_{1}-m_{1}^{\prime b_{1}}(v_{1}^{\prime c_{1}}(r))$. Finally the definition of $h^{\prime\prime d}$ is :

For y\in{\cal N}_{g_{1}}\cup{\cal P}_{g_{1}},h^{\prime\prime d}(y)=\left\{\begin{array}[]{l}m_{2}^{\prime b_{2}}(h_{v}^{\prime c_{v}}((m_{1}^{\prime b_{1}})^{-1}(y)))\;if\;y\in m_{1}^{\prime b_{1}}(r_{1})\\ y\;otherwise\end{array}\right.

For all types of existing connections $(y,z)$ of $g_{1}$ where $y$ and $z$ in ${\cal N}_{g_{1}}\cup{\cal P}_{g_{1}}$, $h^{\prime\prime d}(y,z)=(h^{\prime\prime d}(y),h^{\prime\prime d}(z))$ is in $g_{2}$. By construction, the homomorphism conditions on attributes are fulfilled by $h^{\prime\prime d}$. Thus, $h^{\prime\prime d}:g_{1}\to g_{2}$ is a pregraph homomorphism. In addition, $h^{\prime\prime d}$ is bijective by construction. From $h^{\prime\prime d}$ and Proposition 6, we infer the isomorphism $h^{(3)d}:g^{\prime}_{1}\to g^{\prime}_{2}$.

∎

Definition 18** (Symmetry Condition).**

An ESRR $l\rightarrow r$ verifies the symmetry condition  iff $\forall h^{a}\in H(l),\;\exists\;h^{\prime a}\in H(r),\;\mbox{such that}\;\forall x\in r^{env},h^{a}(x)=h^{\prime a}(x)$

The reader can check that the rule $R_{T}$ verifies the symmetry condition.

Definition 19** (Matches up to automorphism, $\sim^{l}$).**

Let $l\to r$ be an ESRR satisfying the symmetry condition. Let $l_{1}\to r_{1}$ and $l_{2}\to r_{2}$ be two different variants of the rule $l\to r$. Let $v^{c_{1}}_{1}:l\to l_{1}$ and $v^{c_{2}}_{2}:l\to l_{2}$ be the isomorphisms that reflect the variant status of $l_{1}$ and $l_{2}$ of $l$. Let $m^{b_{1}}_{1}:l_{1}\to g$ and $m^{b_{2}}_{2}:l_{2}\to g$ be two matches such that $m^{b_{1}}_{1}(l_{1})=m^{b_{2}}_{2}(l_{2})$. We say that matches $m^{b_{1}}_{1}$ and $m^{b_{2}}_{2}$ are equal up to ($l$-)automorphism and write $m^{b_{1}}_{1}\sim^{l}m^{b_{2}}_{2}$ iff there exists an automorphism $h^{a}:l\to l$ such that $m^{b_{1}}_{1}=m^{b_{2}}_{2}\circ v^{c_{2}}_{2}\circ h^{a}\circ{v^{c_{1}}_{1}}^{-1}$.

Definition 20** (Rewriting up to automorphisms).**

Let $\mathcal{R}$ be a conflict free environment sensitive graph rewrite system whose rules satisfy the symmetry condition and $g$ a graph. Let $M(\mathcal{R},g)^{auto}=\{m^{a_{i}}_{i}:l_{i}\to g\;|\;l_{i}\mbox{ is the left-hand side of a variant of a }\mbox{rule }l\to r\mbox{ in }\mathcal{R}\mbox{ and }m^{a_{i}}_{i}\\ \mbox{is a match up to automorphism}\}$. We define the rewrite relation $\displaystyle\rightrightarrows_{auto}$ which rewrites graph $g$ by considering only matches up to automorphisms. I.e., the set of matches $M$ of Definition 14 is $M(\mathcal{R},g)^{auto}$.

Remark 4**.**

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

Theorem 3**.**

Let $\mathcal{R}$ be a conflict free environment sensitive graph rewrite system whose rules satisfy the symmetry condition. Then $\displaystyle\rightrightarrows_{auto}$ is deterministic. That is, for all graphs $g$, ($g\displaystyle\rightrightarrows_{auto}g^{\prime}_{1}$ and $g\displaystyle\rightrightarrows_{auto}g^{\prime}_{2}$) implies that $g^{\prime}_{1}$ and $g^{\prime}_{2}$ are isomorphic.

Sketch.

Let $M_{1}$ (resp. $M_{2}$) be the set of matches used in the rewrite step $g\displaystyle\rightrightarrows_{auto}g^{\prime}_{1}$ (resp. $g\displaystyle\rightrightarrows_{auto}g^{\prime}_{2}$). Let us assume that $M_{1}\not=M_{2}$. By definition of sets $M_{1}$ and $M_{2}$, for all matches $m_{i}^{b_{i}}:l_{i}\to g$ in $M_{1}$, there exits a match $m_{i}^{\prime b_{i}^{\prime}}:l^{\prime}_{i}\to g$ in $M_{2}$ such that $l_{i}$ and $l_{i}^{\prime}$ are the left-hand sides of two variants $l_{i}\to r_{i}$ and $l^{\prime}_{i}\to r^{\prime}_{i}$ of a rule $l\to r$ in $\mathcal{R}$ such that $m_{i}^{b_{i}}(l_{i})=m_{i}^{\prime b_{i}^{\prime}}(l^{\prime}_{i})$. That is to say, there exist four isomorphisms reflecting the variant status of these two rules, say $v_{i}^{c_{i}}:l\to l_{i}$, $v_{i}^{\prime c_{i}}:r\to r_{i}$, $w_{i}^{d_{i}}:l\to l^{\prime}_{i}$ and $w_{i}^{\prime d_{i}}:r\to r^{\prime}_{i}$ such that $l_{i}=v_{i}^{c_{i}}(l)$, $r_{i}=v_{i}^{\prime c_{i}}(r)$, $l^{\prime}_{i}=w_{i}^{d_{i}}(l)$, $r^{\prime}_{i}=w_{i}^{\prime d_{i}}(r)$, $\forall x\in r_{i}^{env},\,v_{i}^{c_{i}}(x)=v_{i}^{\prime c_{i}}(x)$ and $\forall x\in r_{i}^{{}^{\prime}env},\,w_{i}^{d_{i}}(x)=w_{i}^{\prime d_{i}}(x)$.

From the hypotheses, there exist two automorphisms $h_{i}^{a_{i}}:l_{i}\to l_{i}$ and $h_{i}^{\prime a_{i}}:r_{i}\to r_{i}$ and two isomorphisms ${h_{v}}_{i}^{e_{i}}:l_{i}\to l^{\prime}_{i}$ and ${h^{\prime}_{v}}_{i}^{e_{i}}:r_{i}\to r^{\prime}_{i}$ such that ${h_{v}}_{i}^{e_{i}}=w_{i}^{d_{i}}\circ h_{i}^{a_{i}}\circ(v_{i}^{c_{i}})^{-1}$ and ${h^{\prime}_{v}}_{i}^{e_{i}}=w_{i}^{\prime e_{i}}\circ h_{i}^{\prime a_{i}}\circ(v_{i}^{{}^{\prime}c_{i}})^{-1}$.

By following the same reasoning as in Proposition 11, we can build $h^{\prime\prime f}:g_{1}\to g_{2}$ defined as follows, where $\mu_{i}^{t_{i}}:r_{i}\to g_{1}$ and $\mu_{i}^{\prime t_{i}}:r^{\prime}_{i}\to g_{2}$ are induced by definition of rewrite steps ($\mu_{i}^{t_{i}}$ and $\mu_{i}^{\prime t_{i}}$ play the same role, for every two rules, as $m_{1}^{\prime b_{1}}$ and $m_{2}^{\prime b_{2}}$ in the proof of Proposition 11).

for n\in{\cal N}_{g_{1}},h^{\prime\prime f}(n)=\left\{\begin{array}[]{l}\mu_{i}^{\prime t_{i}}({h^{\prime}_{v}}_{i}^{e_{i}}((\mu_{i}^{t_{i}})^{-1}(n)))\;if\;n\in\mu_{i}^{t_{i}}(r_{i})\\ n\;otherwise\end{array}\right.

for p\in{\cal P}_{g_{1}},h^{\prime\prime f}(p)=\left\{\begin{array}[]{l}\mu_{i}^{\prime t_{i}}({h^{\prime}_{v}}_{i}^{e_{i}}((\mu_{i}^{t_{i}})^{-1}(p)))\;if\;p\in\mu_{i}^{t_{i}}(r_{i})\\ p\;otherwise\end{array}\right.

for $(p,n)\in{\cal N}_{g_{1}},h^{\prime\prime f}(p,n)=(h^{\prime\prime f}(p),h^{\prime\prime f}(n))$

for $(p,p^{\prime})\in{\cal N}_{g_{1}},h^{\prime\prime f}(p,p^{\prime})=(h^{\prime\prime f}(p),h^{\prime\prime f}(p^{\prime}))$

Clearly $h^{\prime\prime f}$ is an isomorphism between pregraphs $g_{1}$ and $g_{2}$. Therefore, by Proposition 6, $g^{\prime}_{1}$ (which equals $\overline{g}_{1}$) is isomorphic to $g^{\prime}_{2}$ (which equal $\overline{g}_{2}$).

∎

0.5 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.

0.5.1 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 $\nu(k)$ is the set of the neighbors of cell $k$: $x_{k}(t+1)=f(x_{k}(t),x_{n}(t),n\in\nu(k))$ In the case of a graph $g$, the neighbors of a cell (node) $k$, $\nu(k)$, is defined by : $l\in\nu(k)$ iff $\exists p_{1},\exists p_{2},(p_{1},k)\in{\cal PN}_{g}\wedge(p_{2},l)\in{{\cal PN}_{g}}\wedge(p_{1},p_{2})\in{{\cal PP}_{g}}$. Usually, the grid is oriented such that any cell of $\nu(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 [9] on a 2-dimensional grid. This neighborhood of radius 1 is composed of 8 neighbors. The distinguishing attributes on ports belong to the set ${\cal 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=({{\cal N}_{g}},{{\cal P}_{g}},{{\cal PN}_{g}},{\cal PP}_{g},{\cal A}_{g},\lambda_{g})$ such that :

• •

${\cal N}_{g}=\{m_{i,j}\}_{i\in I,j\in J}$, where intervals $I$ and $J$ are defined as $I=[-N,N]\cap\mathbb{Z}$ and $J=[-N^{\prime},N^{\prime}]\cap\mathbb{Z}$ for some natural numbers $N$ and $N^{\prime}$.

• •

${{\cal 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\in I,j\in J\}$,

• •

${{\cal 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\in I,j\in J\}$,

• •

${{\cal 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\in I,j\in J\}$,

• •

$\forall i\in I,\forall j\in J$, ${\lambda_{g}}(m_{i,j})\subseteq{\cal A}_{g}$,

• •

$\forall i\in I,\forall j\in J$, ${\lambda_{g}}(e_{i,j})=\{e\}$, ${\lambda_{g}}(w_{i,j})=\{w\}$,${\lambda_{g}}(s_{i,j})=\{s\}$, ${\lambda_{g}}(n_{i,j})=\{n\}$, ${\lambda_{g}}(ne_{i,j})=\{ne$, ${\lambda_{g}}(nw_{i,j})=\{nw\}$, ${\lambda_{g}}(se_{i,j})=\{se\}$, ${\lambda_{g}}(sw_{i,j})=\{sw\}$.

The attributes of the nodes correspond to states of the cells. They belong to a set ${\cal A}$. To implement the dynamics of the automaton one needs only one rewrite rule $\{\rho=l\to 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 12), 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 12 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)=((\sum_{l\in\nu(i)}x_{l}(t))=?=3)+((x_{i}(t)=?=1)$ $\times(\sum_{l\in\sigma(i)}x_{l}(t))=?=2))$

where (x=?=y)\Leftrightarrow\left\{\begin{array}[]{l}1\;if\;x=y\\ 0\;otherwise\end{array}\right.

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 $\displaystyle\rightrightarrows_{auto}$ is applied on the rewrite system ${\cal R}=\{\rho=l\to r\}$ reduced to one rule depicted in Figure 12. More precisely the graphs of the rule as defined as follows:

$l=({\cal N}_{l},{\cal P}_{l},{\cal PN}_{l},{\cal PP}_{l},{\cal A}_{l},\lambda_{l})$ with

• •

${\cal N}_{l}={\cal N}_{l}^{env}=\{i,a,b,c,d,e,f,g,h\}$,

• •

${\cal P}_{l}={\cal P}_{l}^{env}=\{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}\}$,

• •

${\cal PN}_{l}={\cal PN}_{l}^{env}=\{(a_{1},a),(b_{1},b),(c_{1},c),(d_{1},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)\}$,

• •

${\cal PP}_{l}={\cal PP}_{l}^{env}=\{(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})\}$.

• •

${\cal A}_{l}=\{0,1,x_{i}\}\cup\{y_{q}\;|\;q\in\{a,b,c,d,e,f,g,h\}\}$ and $\lambda_{l}=\lambda_{l}^{env}\cup\lambda_{l}^{cut}$ with $\lambda_{l}^{cut}:\{i\}\to{\cal A}_{l}$ such that $\lambda_{l}^{cut}(i)=\{x_{i}\}$ ; and $\lambda_{l}^{env}:\{a,b,c,d,e,f,g,h\}\to{\cal A}_{l}$ such that $\lambda_{l}^{env}(q)=\{y_{q}\}$

$r=({\cal N}_{r},{\cal P}_{r},{\cal PN}_{r},{\cal PP}_{r},{\cal A}_{r},\lambda_{r})$ with

• •

${\cal N}_{r}={\cal N}_{r}^{env}=\{i\}$,

• •

${\cal P}_{r}=\emptyset$, ${\cal PN}_{r}=\emptyset$, ${\cal PP}_{r}=\emptyset$.

• •

${\cal A}_{r}={\cal A}_{l}$

• •

Moreover, on nodes, $\lambda_{r}=\lambda_{r}^{new}$ ($\lambda_{r}^{env}$ being empty) with $\lambda_{r}^{new}:\{i\}\to Att_{r}$ and $\lambda_{r}^{new}(i)=\{((y_{a}+y_{b}+y_{c}+y_{d}+y_{e}+y_{f}+y_{g}+y_{h})=?=3)+((x_{i}=?=1)\times((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 13(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 14(a) yields Figure 14(b) as a fixed point. Here we observe that the indeterminacy concerns at most 4 cells over time.

0.5.2 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=({{\cal N}}_{g},{\cal P}_{g},{\cal PN}_{g},{\cal PP}_{g},{\cal A}_{g},\lambda_{g})$ with ${\cal N}_{g}=\{1,2,3\}$ , ${\cal P}_{g}=\{p_{1},q_{1},p_{2},q_{2},p_{3},q_{3}\}$, ${\cal PN}_{g}=\{(p_{1},1),(q_{1},1),(p_{2},2),(q_{2},2),(p_{3},3),(q_{3},3)\}$ , ${\cal PP}_{g}=\{(p_{1},q_{2}),(p_{2},q_{3}),(p_{3},q_{1})\}$.

\lambda_{g}(1)=\left(\begin{array}[]{c}-1\\ 0\end{array}\right), \lambda_{g}(2)=\left(\begin{array}[]{c}0\\ \sqrt{2}\end{array}\right), \lambda_{g}(3)=\left(\begin{array}[]{c}1\\ 0\end{array}\right), $\lambda_{g}(p_{1})=\lambda_{g}(p_{2})=\lambda_{g}(p_{3})=\{-\}$, $\lambda_{g}(q_{1})=\lambda_{g}(q_{2})=\lambda_{g}(q_{3})=\{+\}$.

The attributes of ports are distinguishing attributes. The attributes of nodes are the $\mathbb{R}^{2}$ positions of the nodes. Every node got one attribute in $\mathbb{R}^{2}$, thus by abuse of notation, we get rid of the set notation of attributes and use a functional one. The implementation of both relations $\displaystyle\rightrightarrows$ and $\displaystyle\rightrightarrows_{auto}$ using the rule depicted in Figure 15 provide the expected pictures of flakes as in Figures 16.

Let us denote \lambda_{l}(a)=\left(\begin{array}[]{c}x_{a}\\ y_{a}\end{array}\right) and \lambda_{l}(b)=\left(\begin{array}[]{c}x_{b}\\ y_{b}\end{array}\right). In this example, the attributes of nodes $i,j$ and $k$ are defined as follows: $\lambda_{r}(i)=\frac{2}{3}\lambda_{l}(a)+\frac{1}{3}$       \lambda_{l}(b)=\left(\begin{array}[]{c}\frac{2}{3}x_{a}+\frac{1}{3}x_{b}\\ \frac{2}{3}y_{a}+\frac{1}{3}y_{b}\end{array}\right),

\lambda_{r}(j)=\frac{1}{2}(\lambda_{l}(a)+\lambda_{l}(b))+\frac{\sqrt{3}}{6}(\lambda_{l}(a)^{T}+\lambda_{l}(b)^{T})=\left(\begin{array}[]{c}\frac{1}{2}(x_{a}+x_{b})+\frac{\sqrt{3}}{6}(y_{a}-y_{b})\\ \frac{1}{2}(y_{a}+y_{b})+\frac{\sqrt{3}}{6}(-x_{a}+x_{b})\end{array}\right), and \lambda_{r}(k)=\frac{1}{3}\lambda_{l}(a)+\frac{2}{3}\lambda_{l}(b)=\left(\begin{array}[]{c}\frac{1}{3}x_{a}+\frac{2}{3}x_{b}\\ \frac{1}{3}y_{a}+\frac{2}{3}y_{b}\end{array}\right)

0.5.3 Mesh refinement

Mesh refinement consists in creating iteratively new partitions of the considered space. The initial mesh $g$ we consider is depicted Figure 18. Distinguishing attributes are given on ports. Attributes on nodes are omitted but we can easily consider coordinates. Triangle refinements are given in Figure 17. The three rules verify the symmetry condition and we apply the $\displaystyle\rightrightarrows_{auto}$ relation on $g$ to obtain the graph $g^{\prime}$ described in Figure 18. Iteratively, the rewrite system can be applied again on $g^{\prime}$ and so forth.

0.6 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 [23] or (extensions of) L-systems [19]. 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 [15] or hyperedge replacement [10]. These approaches do not consider overlapping matches but act as context free grammars. However, in [8] 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 [22]. Amalgamation, see e.g.[13], 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 [14]. 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.