Guillaume Bonfante

Bruno Guillaume

Non-size increasing Graph Rewriting for Natural Language Processing

) in general, we define termination criterions based on weight, we prove the termination of weighted rewriting systems and we give complexity bounds on derivation lengths for these rewriting systems. Contents 1 Introduction 2 Linguistic motivations 2.1 Node preservation property 2.2 Edge shifting 2.3 Negative conditions 2.4 Long distance dependencies 3 Graph Rewriting for NLP 3.1 Graphs 3.2 Graph decomposition 3.3 Rules 13 3.4 Graph Rewriting System 15 4 Big step semantics 15 4.1 Rules normalization 15 4.2 Big step modification 17 5 Termination 19 5.1 Termination by weight analysis 19 5.2 Termination by lexicographic weight 21 6 Properties of weighted GRS 25 6.1 The synthesis of weights 26 6.2 The derivation height of weighted GRS 26 6.3 The derivation height of lexicographically weighted GRS 28 6.4 A characterization of polynomial time 30 7 Conclusion 32 References 32 Appendix A Proof details 34 I see that Mike begins to work SUBJ SUBJ AUX CPL COMP COMP

The second linguistic model of syntax is based on the notion of constituents (mainly promoted by Chomsky) in which words are grouped in a hierarchy of typed constituents.

and a rule application

Definition 4.3 (Crown image). Let R = P, c a node-preserving rule and G → R,µ G a rule application. Let N G = P µ ⊕ K µ ⊕ C µ the decomposition given by Lemma 4.3. The crown image is the set of edges of G which links the pattern nodes to the crown nodes:

Proof. By induction on the length of the sequence of commands c. Corollary 4.1. If a rule does not contain any shift command, K µ = K µ . Lemma 4.5. Given the notations of the preceding lemma, given an edge label e ∈ Σ E , we have |K µ | e ≤ |K µ | e . Proof. The preceding lemma induces a function : T : n e -→ p ∈ K µ → n e -→ p ∈ K µ and p e -→ n ∈ K µ → p e -→ n ∈ K µ . Let us verify that the function T is injective which is a sufficient condition to prove the lemma. Suppose that n 1 e -→ p 1 = n 2 e -→ p 2 ∈ K µ (the case p 1 e -→ n 1 = p 2 e -→ n 2 is similar, the cases p 1 e -→ n 1 = n 2 e -→ p 2 are trivial since n 1 and p 2 are not in the same set). Let T (n 1 e -→ p 1 ) = n 1 e -→ p 1 and T (n 2 e -→ p 2 ) = n 2 e -→ p 2 . The inequality p 1 e -→ n 1 = n 2 e -→ p 2 means that either p 1 = p 2 or that n 1 = n 2 . If p 1 = p 2 , trivially n 1 e

Introduction

Linguists introduce different levels to describe a natural language sentence. Starting from a sentence given as a sequence of sounds or as a sequence of words; among the linguistic levels, two are deeply considered in literature: the syntactic level (a grammatical analysis of the sentence) and the semantic level (a representation of the meaning of the sentence). These two representations involve mathematical structures such as logical formulae, λterms, trees and graphs.

Linguistic theories of syntax split in two main branches. The firsts are based on the notion of dependency structure, the seconds on constituents. Dependency structures already appeared in the Ancient History, for instance in the Sanskrit grammar of Pān . ini; it is also used by Arabic grammarians of the Middle Age; a modern presentation of dependency structures is due to Tesnière [START_REF] Tesnière | Eléments de syntaxe structurale[END_REF]. A dependency structure is an ordered sequence of words, together with some relations between these words. Let us consider the English sentence "I see that Mike begins to work". This sentence has a dependency structure like the one below: Our approach would fit both representations. For the sake of clarity, in this contribution, we will present the examples with dependency structure which we think are a little bit more intuitive.

There is a large debate in the literature about the mathematical nature of the structures needed for natural language syntax: do we have to consider trees or graphs? Many linguistic theories argue for the tree nature of these structures which are simpler both from theoretical and practical views. However, as we shall see, it is clearly insufficient. Usually, linguists add some external structure to deal with problematic cases (they identify nodes by means of coreferences or path equations). Working directly with graphs avoids these encodings. We think that this is the best way to obtain a simple, tractable and natural computational model. Let us illustrate the limitations of tree-representations with some linguistic examples. Consider for instance the sentence "Bill expects Mary to come", the node "Mary" is shared, being the subject of "come" and the object of "expects": Many examples with coordination induces sharing of some nodes: in the sentence "Nicolas gave a book and Helen lent a newspaper about economy to Peter yesterday", the two verbs "gave" and "lent" shared their subject "Nicolas", and the two prepositional phrases "to Peter" and "yesterday".

The situation can be even worse: cycles may appear such as in the sentence below where edges in the cycle are drawn with dashed line. For the semantic representation of natural language sentences, first order logic formulae are widely used. But, natural language can be highly ambiguous; this is mainly due to the fact that scope of quantifiers are not given explicitly in sentence. To avoid to produce many formulae for a given sentence, new representations of semantic were introduced (they are know as underspecified semantic representations). As an example, one of the underspecified semantic representations is the DMRS (Dependency Minimal Recursion Semantics) presented in [START_REF] Copestake | Invited Talk: Slacker Semantics: Why Superficiality, Dependency and Avoidance of Commitment can be the Right Way to Go[END_REF]. The structure for the sentence "The Dog whose toy the cat bit barked" is given in Figure 1. In DMRS structure, three kind of relations are described: first, relations ARG1, ARG2 link predicate to their semantic arguments; second relation RSTR described the quantifier restrictions; the unoriented relation EQ describes scope constraints. The UNL project [START_REF] Uchida | UNL: Universal Networking Language[END_REF] is another example of a framework where graphs are used to encode deep linguistic information as an intermediate structure in a multilingual communication system.

bytev theq catn R S T R theq dogn R S T R barkv A R G 1 possv A R G 2 toyn A R G 1 A R G 1 A R G 2 E Q E Q defq R S T R
At the syntax level, considering the fixed order of the words of the sentence, it may be possible to use some edge inversion and the transform our graphs into DAGs. However, at the semantic level there is no more fixed ordering between nodes and so there is no canonical way to turn graphs into DAGs.

To describe transformations (in both ways) between flat structures and syntactic structures or between syntactic structures and semantics structures, computational linguists have invented a lot of solutions based on many computational models. To cite some of them, we note those using finite state automata (with Markov Models, see for instance (Roche and Schabes, 1997)), those based on λ-calculus [START_REF] Montague | Universal grammar[END_REF][START_REF] Montague | The proper treatment of quantification in ordinary english[END_REF], or Natural Language Processing (NLP) specific solutions (unifications based systems like HPSG [START_REF] Pollard | Head-Driven Phrase Structure Grammar[END_REF], LFG [START_REF] Kaplan | Lexical-functional grammar: A formal system for grammatical representation[END_REF] or Tree Adjoining Grammars [START_REF] Vijay-Shanker | Feature structures based tree adjoining grammars[END_REF]).

It is somewhat surprising that Graph Rewriting Systems (GRS) have been hardly considered so far. Not so far from being extensive, we mention [START_REF] Hyvönen | Semantic Parsing as Graph Language Transformation -a Multidimensional Approach to Parsing Highly Inflectional Languages[END_REF][START_REF] Bohnet | On using a parallel graph rewriting formalism in generation[END_REF][START_REF] Crouch | Packed Rewriting for Mapping Semantics to KR[END_REF][START_REF] Jijkoun | Learning to transform linguistic graphs[END_REF][START_REF] Bédaride | Semantic Normalisation : a Framework and an Experiment[END_REF][START_REF] Chaumartin | Une approche paresseuse de l'analyse sémantique ou comment construire une interface syntaxe-sémantique à partir d'exemples[END_REF]. To explain that, GRS implementations are usually considered to be too inefficient to justify their extra-generality. For instance, pattern matching does not take linear time where linear time is usually seen as an upper limit for fast treatment.

However, if one drops for a while the issue of efficiency, the use of GRS is promising. Indeed, linguistic considerations can be most of the time expressed by some relations between a few words. Thus, they are easily translated into rules. To illustrate this point, in [START_REF] Bonfante | Modular graph rewriting to compute semantics[END_REF], we proposed a syntax to semantics translator based on GRSs: given the syntax of a sentence, it outputs the different meaning associated to this syntax. In [START_REF] Guillaume | Annotation sémantique du French Treebank à l'aide de la réécriture modulaire de graphes[END_REF], the system was applied to a large corpus (the French Treebank).

In the two earlier mentioned studies, we tried to delineate what are the key features of graph rewriting in the context of Natural Language Processing. We come back to it in the next section. Roughly speaking, node creation are strictly restricted, edges may be shifted from one node to another and there is a need for negative patterns. Based on this analysis, we define here a suitable framework for NLP (see Section 3). As a matter of facts, our application performs very common transformations in NLP, which, in other words, means that the features provided by our framework can be seen as the minimal requirements in terms of expressivity of an NLP oriented Graph Rewriting Semantics.

Indeed, compared to term rewriting, the semantics of graph rewriting is problematic: different choices can be made in the way the context is glued to the rule application [START_REF] Rozenberg | Handbook of Graph Grammars and Computing by Graph Transformations[END_REF]. As far as we see, our notion does not fit properly the DPO approach due to unguarded node deletion nor the SPO approach due to the shift command, as we shall see. Thus we will provide a complete description of our notion. We have chosen to present it in an operational way and we leave for future work a categorial semantics. We also leave as future work the comparison of our definition with other algorithmic approaches to graph rewriting like [START_REF] Janssens | Graph grammars with neighbourhood-controlled embedding[END_REF] and [START_REF] Schürr | Programmed graph replacement systems[END_REF].

One of the main issues we have been faced with is to control globally computations by rewriting. Indeed, since each step of computation is fired by some local condition in the whole graph, one has no/few grip on the sequence of rewriting steps. Thus, the more rules, the more interactions between rules, and the consistency of the whole system becomes difficult to maintain. Moreover, some rules are not written by hand. Indeed, to take into account the particular behavior of some words, some rules are directly synthesized from some linguistic resources. For instance, a verb may have an intransitive form, a transitive form or both forms. This property can be extracted from syntactic lexicons which describes the sub-categorization frames for each verbs. The role of the NLP programmer is then to define the shape of the rules depending on the lexicon. To give an idea of the size of programs, our application involves 571 rules among which 379 have been produced out of the French verb valency lexicon Dicovalence (Van den [START_REF] Van Den Eynde | La valence : l'approche pronominale et son application au lexique verbal[END_REF]. To keep the general coherence, to ease the development and the maintenance of the system, we have organized rules in modules (applied sequentially). A module is a set of rules that is linguistically consistent and represents a particular step of the transformation. As an illustration, in our system, one of them turns a sentence in passive form to its active form. Another module resolves the anaphoric links which are internal to the sentence and determined by the syntax. In our proposal, there are 34 modules.

Generally speaking, the ambiguity of the meaning of a sentence is a very common phenomenon which cannot be avoided. Technically, this implies that the relation between the syntax of sentences to their semantics is not functional, which implies that the graph rewriting systems themselves are not confluent. Anyway, some modules are confluent. In that case, since we can restrict computations to only one normal form, the process is much more efficient. In our system, only 8 of the 34 modules are not confluent.

The large amount of rules, the fact that they are not written by hand and the large number of modules justify to have some tools to verify some properties of modules. In Section 5, we provide two termination methods based on a weight analysis. There are two reasons we have been interested by the property of termination. First, there is a direct motivation: in our NLP application, any computations should terminate. If it is not the case, it means that the rules where not correctly drawn. Then, termination ensures partly the correctness of the transformation. There is also an indirect reason to consider termination: one way of establishing confluence is through Newman's Lemma [START_REF] Newman | On theories with a combinatorial definition of "equivalence[END_REF] which requires termination.

In Section 6, we consider two properties of the above mentioned termination methods. First, we show that they are decidable, that is the existence of weights can be computed statically from the rules, and thus we have a fully automatic tool to verify termination. Obviously, it is not complete. In a second step, we evaluate the strength of the two methods. To do that, we consider what restrictions they impose on the length of computations. We get quadratic time for the first method, polynomial time for the second.

Linguistic motivations

Without any linguistic exhaustivity, we highlight in this section some crucial points of the kind of linguistic transformation we are interested in and hence the relative features of rewriting we have to consider. These examples below explain and justify the main technical choices we have made in our Graph Rewriting definition.

Node preservation property

As linguistic examples above suggest, the goal of linguistic analysis is mainly to describe different kinds of relations between elements that are present in the input structure. As a consequence, the set of nodes in the output structure is directly predictable from the input and only a very restrictive notion on node creation is needed. For instance, we have to add a subject node for each infinitive verb; we also have to split some well-known words which produces several semantics items (like "whose" in Figure 1 and the two corresponding items in the DMRS structure poss v and def q ).

In practice, these node creations can be anticipated in some enriched input structure on which the whole transformation can be described as a non-size increasing process.

This property of node preservation is also present in many widely-used formalism. For instance, in TAG [START_REF] Vijay-Shanker | Feature structures based tree adjoining grammars[END_REF]Joshi, 1988), in Minimalist Grammars (Stabler, 1997) or in Abstract Categorial Grammars (de Groote, 2001), input structures are lexicalized (i.e. are directly linked to words of the language) and the operations used during the analysis process are non-size increasing: substitution and adjunction for TAG, merge and move for Minimalist Grammars and linear β-reduction for Abstract Categorial Grammars.

Edge shifting

Recall the dependency structure of the sentence "I see that Mike begins to work": In a more general setting, our transformations may have to specify the fact that all incident edges of some node X must be transported to some other node Y . We call this operation shift.

I
To describe our graph rewriting rules, we introduce a system of commands (like in [START_REF] Echahed | Inductively sequential term-graph rewrite systems[END_REF]) which expresses step by step the modifications applied on the input graph. The transformation described above is performed in our setting as follows:

Negative conditions

In some situation, rules must be aware of the context of the pattern to avoid unwanted ambiguities. When computing semantics out of syntax, one has to deal with passive sentence; the two sentences below show that the agent is optional. In order to switch to the corresponding active form, two different linguistic transformations have to be defined for these two sentence; but, clearly, the first graph is a subgraph of the second one. We don't want the transformation for the short passive on the left to apply on the long passive on the right. we need to express a negative condition like "there is no out edge labeled by AGT out of the main verb" to prevent the unwanted transformation to occur.

Long distance dependencies

Most of the linguistic transformation can be expressed with successive local transformation like the one above. Nevertheless, there are some cases where more global rewriting is required; consider the sentence "The women whom John seems to love", for which we consider the syntactic structure above:

OBJ

One of the steps in the semantic construction of this sentence requires to compute the antecedent of the relative pronoun "whom" (the noun "woman" in our example). The subgraph we have to search in our graph is depicted as a non-local pattern on the left and the graph modification to perform is given on the right.

X PRO_REL Y Z T OBJ (OBJ|COMP)* MOD_REL add edge(X,ANT,T)
The number of OBJ or COMP relations to consider (in the relation depicted as (OBJ|COMP)* in the figure above) is unbounded (in linguistics, this phenomenon is called long distance dependencies); it is possible to construct grammatical sentences with an arbitrary large number of relations.

As we want to stay in the well-known framework of local rewriting, we implement such non local rules with sets of local transformations. The first rule (on the left) creates an edge TMP which serves as a pointer. The second rules updates the pointer to find the end of the chain made of COMP and OBJ labels.

X PRO_REL Y OBJ add edge(X,TMP,Y) X Y Z TMP COMP
del edge(X,TMP,Y) add edge(X,TMP,Z)

X Y Z TMP OBJ
del edge(X,TMP,Y) add edge(X,TMP,Z)

When the TMP pointer reaches the end of the chain, we can update the link between the PRO REL and its target. In the end, we remove the temporary link TMP.

X Z T

TMP MOD_REL add edge(X,ANT,T) del edge(X,TMP,Z)

Graph Rewriting for NLP

Before we enter into the technical sections, let us define some useful notations. First, we use the notation c to denote sequences. The empty sequence is written ∅. The length of a sequence is denoted by | c |. We use the same notation for sets: the empty set is denoted ∅ and the cardinality of a set S is written |S|. The context will make clear whether we are talking about sequences or sets. Given a function f : X → Y and some sets X ⊆ X and Y ⊆ Y , we define f (X )

{f (x) | x ∈ X } and f -1 (Y ) {x ∈ X | f (x) ∈ Y }; the restriction of the function f to the domain X is f | X : x ∈ X → f (x ). The function c X : x ∈ X → c ∈ Y is the constant function on X.
The identity function is written 1. Finally, given a function f : X → Y and (x, y) ∈ X × Y , the function f [x → y] maps t = x to f (t) and x to y.

The set of natural numbers is N, integers are denoted by Z. Given two integers a, b, we define [a, b] = {x ∈ Z | a ≤ x ≤ b}.

Graphs

The graphs we consider are directed graphs with both labels on nodes and labels on edges. We restrict the edge set: given some edge label e, there is at most one edge labeled e between two given nodes n and m. This restriction reflects the fact that, in NLP application, our edges are used to encode linguistic information which are relations. We make no other explicit hypothesis on graphs: in particular, graphs may be disconnected, or have loops.

All along this paper, we suppose given two finite sets Σ E of edge labels, Σ N of node labels and an enumerable set U called universe, where graph nodes live.

Definition 3.1 (Graph). A graph G is defined as a triple (N , , E) where -N is a finite set of nodes: N ⊂ U; -is a labeling function: : N → Σ N ; -E is a set of edges: E ⊆ N × Σ E × N .
Let n, m ∈ N and e ∈ Σ E . When there is an edge from n to m labelled e (i.e. (n, e, m) ∈ E), we write

n e -→ m or n -→ m if the edge label is not relevant. If G denotes some graph (N , , E), then N G , G , E G denote respectively N , and E. The number of nodes of a graph G is written |G|. Given a graph G, two nodes n, m ∈ N G and e ∈ Σ E , let G + {n e -→ m} N G , G , E G ∪ {n e -→ m} . We use the + notation to stress the fact that n e -→ m is not intended to be in G. Example 3.1. Let Σ E = {A, B, C, D, E}, Σ N = {♣, ♥} and G 0 = ({g 0 , g 1 , g 2 },
, {(g 0 , A, g 1 ), (g 2 , A, g 1 ), (g 0 , B, g 1 ), (g 1 , C, g 2 ), (g 0 , D, g 2 ), (g 0 , E, g 0 )}) with (g 0 ) = (g 2 ) = ♣ and (g 1 ) = ♥. It is pictured as follows:

♣ g 0 ♥ g 1 ♣ g 2 A B D C A E Definition 3.2 (Graph morphism). A graph morphism µ from the graph G = (N , , E) to the graph G = (N , , E ) is a function from N to N such that: -for all n ∈ N , (µ(n)) = (n); -for all n, m ∈ N and e ∈ Σ E , if n e -→ m ∈ E then µ(n) e -→ µ(m) ∈ E . A graph morphism µ is said to be injective if µ(n) = µ(m) implies n = m.
We make the following abuse of notation: given some graph morphism µ : G → G , and a set In a pattern P = B, ν , the positive pattern B plays a central role. Thus, we use in the sequel N P for N B , E P for E B and so on. We do as if the pattern were a graph, that is its positive pattern. The notations should not be ambiguous. The empty sequence is () and thus, P = (B, ()) denotes a pattern with an empty set of negative conditions. Definition 3.5 (Matching). Given a pattern P = B, ν defined as above and a graph G, a matching from P to G is a positive matching µ : B → G such that there is no index 1 ≤ i ≤ k, for which there is an injective morphism ξ i with

E ⊆ E G , we let µ(E) = {µ(n) e -→ µ(m) | n e -→ m ∈ E}. A subgraph G of G is a graph such that N G ⊆ N G , E G ⊆ E G and G = G | N G . The graph G is said to be full in G whenever it is a subgraph and E G = E G ∩(N G ×Σ E ×N G ). Given a subgraph G of G , we denote by 1 G,G : n ∈ G → n ∈ G . It is an injective morphism from G to G .
ξ i • ν i = µ : B B i G ν i µ × ξ i
Negative conditions remove "bad matchings". To see them in action, let us come back to the graph of Example 3.1 and consider the two matchings µ 0 , µ 1 :

B 0 → G 0 . ♣ b 0 ♥ b 1 A µ 0 ♣ g 0 ♥ g 1 ♣ g 2 A B D C A E µ 1 ♣ g 0 ♥ g 1 ♣ g 2 A B D C A E
The two morphisms µ 0 and µ 1 are matchings for the pattern B 0 , () . Let us consider now the morphism ν 0 : B 0 → B 0 defined by:

♣ b 0 ♥ b 1 A ν 0 ♣ b 0 ♥ b 1 A B
The morphism µ 0 is not a matching for the pattern B 0 , (ν 0 ) . Indeed, there is a morphism

ξ 0 = [b 0 → g 0 , b 1 → g 1 ] such that ξ 0 • ν 0 = µ 0 .
Let us consider the case of the morphism ν 1 defined as follows:

♣ b 0 ♥ b 1 A ν 1 ♣ b 2 ♣ b 0 ♥ b 1 A D
The morphism µ 1 is not a matching for the pattern B 0 , (ν 1 ) . Indeed, the morphism

ξ 1 = [b 0 → g 2 , b 1 → g 1 , b 2 → g 0 ] verifies ξ 1 • ν 1 = µ 1 .
To describe one negative condition ν : B → B , we use the following convention. We "show" the graph B , crossing parts of it that are not in the image of ν(B). For the morphism ν 0 , we get:

♣ b0 ♥ b1 A B ×
. For the negative condition ν 1 , we have:

♣ b 2 ♣ b 0 ♥ b 1 A D × .
Let us end the section with the following observation. Given a pattern P = B, ν , suppose that there is a negative condition ν i among ν which is an isomorphism. Then, there is no matchings for P . Indeed, let us suppose a positive matching µ : B → G. Let ν i : B → B i be the incriminated isomorphism, there exists thus a morphism η i such that

η i • ν i = 1 B . Set ξ i = µ • η i . It is injective (as the composition of two injective morphisms). But ξ i • ν i = µ • η i • ν i = µ • 1 B = µ.
And thus µ is not a matching. In other words, as long as there is an isomorphism within negative conditions, there is no more matchings. Such patterns become dubious and we suppose from now on that negative conditions are never isomorphisms.

Once the condition on negative conditions is set, we can observe that the identity is a matching: given a pattern P, ν , 1 : P → P is a matching from P to P .

Graph decomposition

The proper description of actions of a rule on some graph G requires first the definition of two partitions: one on nodes and the other on edges. They are both relative to the matching of some pattern P into G.

For technical reasons, we will have to consider the decomposition of some other graphs (for instance obtained after a subpart of the global transformation). To capture these cases, we need a more general definition. Let µ be an injective matching µ : P → H; as N H ⊂ U, we can see µ as an injective function µ : N P → U and define the decomposition of a graph G with respect to µ as follows.

Definition 3.6 (Nodes decomposition: pattern image, crown and context). Let µ : P → H a matching from the pattern P into a graph H. Let G a graph (N G , G , E G ). Nodes of G can be split in a partition of three sets

N G = P µ ⊕ K µ ⊕ C µ :
the pattern image is P µ = µ(N P ) ∩ N G ; the crown contains nodes outside the pattern image which are directly connected to the pattern image:

K µ = {n ∈ N G \ P µ | ∃p ∈ P µ such that n -→ p or p -→ n}; -the context contains nodes not linked to the pattern image: C µ = N G \ (P µ ∪ K µ ).
Definition 3.7 (Edges decomposition: pattern edges, crown edges, context edges and pattern-glued edges). Let µ : P → H a matching from the pattern

P into a graph H. Let G a graph (N G , G , E G ). Edges of G can be split in a partition of four sets E G = P µ ⊕ K µ ⊕ C µ ⊕ H µ :
the pattern edges set is P µ = µ(E P ) ∩ E G ; the crown edges set contains edges which links a pattern image node to a crown node:

K µ = {n -→ m ∈ E G | n ∈ P µ ∧ m ∈ K µ } ∪ {n -→ m ∈ E G | n ∈ K µ ∧ m ∈ P µ };
the context edges set contains edges which connect two nodes that are not in the pattern image:

C µ = {n -→ m ∈ E G | n / ∈ P µ ∧ m / ∈ P µ }.
the pattern-glued edges set contains edges which are not pattern edges but which connect two nodes that are in the pattern image:

H µ = {n -→ m ∈ E \ µ(E P ) | n ∈ P µ ∧ m ∈ P µ }.
In Figure 2, for the particular case where H = G we draw a pattern, a matching of this pattern in a larger graph as an illustration of the nodes and edges decomposition (see the legend in the figure).

Rules

In our graph rewriting framework, the transformation of the graph is described through some atomic commands (like in [START_REF] Echahed | Inductively sequential term-graph rewrite systems[END_REF]). Commands definition refer to some pattern P and pattern nodes N P are used as identifiers. The five kinds of commands are described below (where a, b ∈ N P , α ∈ Σ N and e ∈ Σ E ):

-change label(a, α) -del edge(a, e, b) -add edge(a, e, b) -del node(a) -shift(a, b)
Their names speak for themselves, however, we will come back to their precise meaning below.

Definition 3.8 (Rule). A rule R is a pair R = P, c of a pattern P and a sequence of commands c. A rule R is said to be node-preserving if it does not contain any del node command.

Let G a graph, R = P, c a rule and µ : P → G a matching. The application of the sequence c on G is a new graph which is written G • µ c (shortened G • c when µ is clear from the context) and is defined by induction on the length k of c. The commands change label, del edge and add edge are called local commands: they modify only the edges and the nodes described in the image of the pattern. The commands del node and shift are non-local, they can modify edges outside the pattern: pattern-glued edges and crown edges.

If k = 0, G • () = G. If k > 0, let G = (N , , E )
In a sequence of commands, there may be some commands without any effects, whatever is the graph to which the sequence is applied. First, if a command is a del node(a), all following commands refering to a has no effect. Second, if some sequence of commands contains two change label commands which refer to the same node, the first one can be removed without changing the effect of the whole sequence. Third, if a sequence contains two commands add edge or del edge referring to the same triplet (a, e, b), the first one can be removed without changing the behavior of the rule. The definition below describes sequences without these spurious commands. Definition 3.9 (Consistent sequence of commands). A sequence of commands c 1 , . . . , c n is called consistent if it verifies the following conditions:

if c i = del node(a) then for all j such that i < j ≤ n the command c j does not refer to the node a;

if c i = change label(a, α) then for all j such that i < j ≤ n the command c j = change label(a, α ); if c i = del edge(p, e, q) or c i = add edge(p, e, q) then for all j such that i < j ≤ n the command c j = del edge(p, e, q) and c j = add edge(p, e, q). Lemma 3.1. Any non consistent sequence c of commands can be replaced by a shorter consistent sequence c which as the same effect:

G → P, c G iff G → P, c G Proof.
From a non consistent sequence c, we built a new sequence with the procedure:

if 1 ≤ i < j ≤ n, c i = del node(a) and c j refers to a, the command c j is removed from the sequence; if 1 ≤ i < j ≤ n, c i = change label(a, α) and c j = change label(a, α ), the command c i is removed from the sequence; if 1 ≤ i < j ≤ n, c i = del edge(p, e, q) or c i = add edge(p, e, q) and c j = del edge(p, e, q)

or c j = add edge(p, e, q), the command c i is removed from the sequence.

It is easy to verify that each step of the procedure build a strictly smaller sequence with the same effet. The procedure can be iterated until a consistent sequence c is reached.

Graph Rewriting System

Definition 3.10 (Rewrite step). Let G a graph, R = P, c a rule and µ : P → G a matching. Let G = G • µ c, then we say that G rewrites to G with respect to the rule R and the matching µ. We write it

G → R,µ G or G → R G or even simply G → G .
We will also use the usual notation → * for the transitive and reflexive closure of the relation →. Given some GRS G, a graph G is a normal form with respect to G if there is no

H such that G → G H. Finally, if H is a normal form such that G → * H, we write G → ! H.
Let us recall that the identity is always a matching. Thus, one may apply a rule R = P, c on itself. That is 1 P : P → P is a matching, and thus we can compute P • 1 P c. This is the auto-application of a rule, and we will shorten the notation to P • c in the sequel.

Definition 3.11 (Graph Rewriting System). A Graph Rewriting System G is a finite set of rules. Definition 3.12. A GRS G induces a relation G from graphs to graphs defined as follows:

(G, H) ∈ G ⇐⇒ G → ! H Conversely, a relation R on graphs is computed by a GRS G iff G = R.
In our application, the translation of the syntax to semantics splits into several independent levels of transformation driven by linguistic consideration (such as translation of passive forms to active ones, computation of the deep subject of infinites). Rules are then grouped in subsets called modules and modules apply sequentially; each module being used as a graph rewriting system on the outputs of the previous module.

Big step semantics

The previous section described semantics of rules step by step. To assert global properties of rewriting like termination, we need a big step semantics to observe the full effect of some rule rather than the effect of individual commands.

Rules normalization

Recall the decomposition of nodes and edges as given by Definitions 3.6 and 3.7. Node deletion modifies nodes in P µ , edges in µ(E P ), K µ and H µ . Shifting modifies edges in the crown K µ . Edge addition and edge deletion modify edges in the pattern image µ(E P ) or in the pattern-glued edges H µ and renaming modify P µ . Apart from the node deletion command which has a more global scope, the three sets {change label}, {add edge, del edge} and {shift} operate respectively on the three distinct sets P µ , µ(E P ) ⊕ H µ and K µ . Thus, if one supposes that there is no node deletion, commands may be separated according to the three sets above, and the global transformation can be computed independently.

Even with the consistent sequences (Def. 3.9), a command like change label, add edge or del edge may be ineffective. Consider, for instance, the graph G = g : α h : α E . Given the pattern P = b : α , it may be applied on G via the morphism µ g : b → g or via the morphism µ h : b → h. In the first case, the command c = del edge(b, E, b) does not modify G. Whereas, in the second case, the command c removes the loop in H µ h within G. A similar remark holds for the command add edge. Uniform rules avoid such an unpredictable behavior.

Definition 4.1 (Uniform rule). We say that a rule B, ν , c is uniform if:

1 if there is an index i such that c i = change label(p, α), then B (p) = α; 2 if there is an index i such that c i = add edge(p, e, q), then 1 B,B+{p e -→q} ∈ ν; 3 if there is an index i such that c i = del edge(p, e, q), then p e -→ q ∈ B.

Lemma 4.1. Given an uniform rule

R = P, c . If G → R,µ G then H µ is left unchanged in G .
Proof. By induction on the length of the sequence c.

The non-predictable behavior of add edge and del edge commands definitely compromises a static analysis of GRSs, and, in particular their termination property. In uniform rules, add edge and del edge commands have a predictable behavior. Actually, sticking to uniform rules is not restrictive: we show that any set of rules can be replaced by an equivalent set of uniform rules.

Lemma 4.2 (Uniformisation). Let R a rule, there is a finite set of uniform rules S(R)

such that G → R G iff G → S(R) G .
The idea of the proof is to replace a rule with an add edge or del edge command which may be ineffective by a couple of rules: one for the effective case, one for the other possibility. Ineffective change label commands are simply removed.

Let us introduce some notations. For a rule R = P, c , if it is not uniform we write γ(R) the index of the first command that makes it non uniform: i.e the smallest index i such that P, (c 1 , . . . , c i-1 ) is uniform but P, (c 1 , . . . , c i ) is not. For a rule R = P, c , we define δ(R) to be 0 if R is uniform and

| c | -γ(R) else. Note that in any case, δ(R) ≤ | c |. We write c -j = (c 1 , . . . , c j-1 , c j+1 , . . . , c | c | ).
Proof. We will give below a procedure which construct from a non-uniform rule R a set R of at most 2 rules such that:

-for all R ∈ R, we have δ(R ) < δ(R) -for any G, G ∪ {R} = G ∪ R .
This procedure can be iterated to replace in a GRS any rule R = P, c by a subset of at most 2 | c | uniform rules without changing the relation induced.

Let us now describe the procedure. Let R = P, c be a rule such that δ(R) > 0. We consider the command c j with j = γ(R) (i.e. the first non-uniform command). We are necessarily in one of the 3 following cases:

1 c j = change label(p, α) and B (p) = α, let R = {R 1 } with R 1 = P, c -j 2 c j = add edge(p, e, q), and 1 B,B+{p e -→q} / ∈ ν, let R = {R 1 , R 2 } with (a)R 1 = B ∪ {p e -→ q}, ν , c -j (b)R 2 = B, ν ∪ 1 B,B+{p e
-→q} , c 3 c j = del edge(p, e, q), and

p e -→ q / ∈ B, let R = {R 1 , R 2 } with (a)R 1 = B, ν ∪ 1 B,B+{p e -→q} , c -j (b)R 2 = B ∪ {p e -→ q}, ν , c
In cases 2(b) and 3(b), the pattern was changed in such a way that γ(R 2 ) > γ(R) and as the length of the sequence of commands is the same δ(R 2 ) < δ(R). In the 3 other cases, the sequence was not changed until index j -1, and so γ(R 1 ) ≥ γ(R); but the length strictly decreases and we can conclude δ(R 1 ) < δ(R).

Big step modification

To describe the effect of a sequence of shift commands, we define a global function Φ which sums up in a single step the composition of the commands in the sequence. Definition 4.2. Let P a pattern and a sequence c of commands. We define inductively the big step shift-edges function Φ c : N P → N P :

-Φ ∅ = 1 -Φ c,shift(m,n) = 1[m → n] • Φ c -Φ c,c = Φ c if c is not a shift command
Using definition 3.6, the following lemma describes node decomposition with respect to a rule application: Lemma 4.3 (Graph node decomposition). Given a graph G and a rule R = P, c

-→ p 1 = n 2 e -→ p 2 . If n 1 = n 2 , then Φ -1 c (n 1 ) ∩ Φ -1 c (n 2 ) = ∅. Thus n 1 ∈ Φ -1 c (n 1 ) is different to n 2 ∈ Φ -1 c (n 2 ).
With the definition above, we can state how the graph decomposition is modified by a rule application.

Theorem 4.1 (Big step semantics). Given R = P, c a node-preserving and uniform rule and a rule application G → R,µ G . Let K µ the crown image and E G = µ(E P ) ⊕ K µ ⊕ C µ ⊕H µ the decomposition of E G with respect to µ (Definition 3.7). Then, with P = P • 1 c, edges of G can be described as follows:

E G = µ(E P ) ⊕ K µ ⊕ C µ ⊕ H µ .
With the previous theorem, we have completely described a rewriting step when no node deletion is involved. The theorem could be generalized to node deletion, but at the price of clarity. In any case the extra-generality is not needed in the following.

The following lemma states that a rule with some node deletions modifies at most a linear number (with respect to the number of nodes in the graph) of edges. Given a rewriting step G → R,µ G , we can consider a less fine-grained decomposition of edges of

G into E G = C µ ⊕ Q µ where, of course, Q µ = µ(E P ) ⊕ K µ ⊕ H µ .
By definition of the context, edges in C µ are unchanged during the reduction and edges of G can also be split in two sets:

E G = C µ ⊕ Q µ .
Lemma 4.6 (Linear modification). Given a GRS G, there is a constant C > 0 such that, for any rewriting step G → R,µ G the two canonical corresponding edge decompositions

E G = C µ ⊕ Q µ and E G = C µ ⊕ Q µ satisfy: |Q µ | ≤ C × (|G| + 1) and |Q µ | ≤ C × (|G| + 1) Proof. Let C = max{2 × |P | 2 × |Σ E | | P, c ∈ G}. Both in G

Termination

We recall that a GRS is said to be (strongly) terminating whenever there is no infinite sequence G 1 → G 2 → • • • . Actually, for non-size increasing GRS as presented above, we have immediately the decidability of non-uniform termination. That is, given some GRS G and some graph G, one may decide whether there is an infinite sequence

G 1 → G 2 → G 3 → • • • .
Indeed, one may observe that for such sequence, for all i ∈ N, |G i | ≤ |G|. Thus, the G i 's range in the finite set G ≤|G| of graphs of size less or equal to |G|. Consequently, either the system terminates or there is some j ≤ |G ≤|G| | and some k ≤ j such that G j = G k . To conclude, to decide non-uniform termination, it is sufficient to compute all the (finitely many) possibilities of rewriting G in less than |G ≤|G| | steps and to verify the existence of such a j and k above. Finally, since |G ≤|G| | ≤ 2 O(|G| 2 ) , the procedure as described above takes exponential time.

Uniform termination-given a GRS, is it terminating on all inputs?-is undecidable [START_REF] Plump | Termination of graph rewriting is undecidable[END_REF]. For the particular case of non-size increasing graph rewriting, the problem remains open.

There is a need to define some termination method pertaining to non-size increasing GRS. Compared to standard work in termination [START_REF] Plump | On termination of graph rewriting[END_REF][START_REF] Godard | Termination detection of distributed algorithms by graph relabelling systems[END_REF], there are two difficulties: first, our graphs may be cyclic, thus forbidding methods developed for DAGs such as term-graphs. Second, using term rewriting terminology, our method should operate for some non-simplifying GRS, that is GRS for which the output may be "bigger" than the input. Indeed, the NLP programmer sometimes wants to compute some new relations, so that the input graph is a strict subgraph of the resulting graph.

Termination by weight analysis

In the context of term-rewriting systems, the use of weights is very common to prove termination. There are many examples of such orderings, Knuth-Bendix Ordering [START_REF] Knuth | Simple word problems in universal algebras[END_REF] to cite one of them. We recall that all graphs we consider are defined relatively to two signatures Σ E of edge labels and Σ N of node labels.

Definition 5.1 (Edge weight, node weight). An edge weight is a mapping w : Σ E → Z. Given some subset E of edges of G, the weight of E is w(E) = n e -→m∈E w(e). The edge weight of a graph G is w

(G) = w(E G ). A node weight is a mapping η : Σ N → Z. For a graph G = (N G , G , E G ), we define η(G) = n∈N G η( G (n)).
Let us make some observations. Let |G| e denote the number of edges in G which have the label e, then w(G) = e∈Σ E w(e) × |G| e . Second, for a pattern matching µ : P → G, w(µ(P )) = w(P ).

The weight of a graph may be negative. This is not standard, but it is useful here to cope with non-simplifying rules, that is rules which add new edges. Since a graph G has at most |Σ E | × |G| 2 edges, the following lemma is immediate.

Lemma 5.1. Given an edge weight w and a node weight η, let

K w = max e∈Σ E (|w(e)|), K E = |Σ E | × K w , K η = max α∈Σ N (|η(α)|), then (a) for each subset of edges E ⊂ E G of some graph G, we have w(E) ≤ K w × |E|. (b) for each graph G, we have -K E × |G| 2 ≤ w(G) ≤ K E × |G| 2 ; (c) for each graph G, we have |η(G)| ≤ K η × |G|.
Definition 5.2 (Weight compatibility). A weight ω is said to be compatible with a rule R = P, c whenever c contains a node deletion command or when c preserves nodes and the three following conditions hold:

1 R is uniform, 2 ω(P • c ) < ω(P ), 3 for all e ∈ Σ E such that w(e) < 0, for all n ∈ Φ c (N P ), let M n = Φ -1 c (n); then for all α ∈ Σ N , for all but possibly one element q in M n , the set of negative condition contains α m P (q) q e × ∈ ν and for all α ∈ Σ N , for all but possibly one element p in M n , the set of negative conditions contains

α m P (q) q e × ∈ ν.
A weight is said to be compatible with a GRS G when it is compatible with all its rules. In that case, we say that G has a compatible weight. A weighted GRS is a pair (G, w) of a GRS and a compatible weight.

Hypothesis (1) will serve to manage glued edges in the pattern images, Hypothesis (2) will serve edges in the pattern image and Hypothesis (3) for the crown edges. One may note that when there is no shift commands in the rule, the Hypothesis (3) holds whatever ω is. Indeed, in that case, Φ is the identity function and all the sets M n are singletons. Theorem 5.1. For any weighted GRS (G, w), G is strongly terminating.

Proof. Let be the lexicographic ordering on

N × Z, that is (n, v) (n , v ) iff n > n or n = n and v > v . The ordering is well-founded on any subset N × I with I a finite subset of Z. We define ω(G) = (|G|, w(G)). Lemma 5.2 shows that G → G implies that ω(G) ω(G ). Consider a sequence G 1 → G 2 → • • • . Since the system is non-size increasing, |G i | ≤ |G 1 | and consequently K E × |G i | 2 ≤ K E × |G 1 | 2 . But, by lemma 5.1(b), -K E × |G i | 2 ≤ w(G i ) ≤ K E × |G i |, the weights w(G i ) range actually in the set [-K E × |G 1 | 2 , . . . , K E × |G 1 | 2 ]. Then, (ω(G i )) i is a decreasing sequence on N × [-K E × |G 1 | 2 , . . . , K E × |G 1 | 2 ],
thus finite.

Condition (3) of Definition 5.2 is necessary. Here is a counter-example of a nonterminating system with a compatible weight up to this condition. We define the GRS defined by the rules

R 1 = (Q 1 , ()), c 1 and R 2 = (Q 2 , ()), c 2 . Set w(A) = w(B) = 1 and w(C) = -2. Then, one may observe that w(Q 1 • 1 c 1 ) = 1 < 2 = w(Q 1 ) and w(Q 2 • c 2 ) = -2 < -1 = w(Q 2 ). However, there is an infinite sequence G 1 → R1 G 2 → R2 G 1 → R1 G 2 → • • • with

Termination by lexicographic weight

In our experiments, in most cases, the weight analysis of the preceding section was sufficient. The main counter-example is however systems composed of rules as given in Section 2.4. In a first step, we prove that such systems are strongly terminating but have no compatible weight. In a second step, we provide a conciliable extension of this termination proof method. With a little abstraction, the linguistic example of Section 2.4 about long distance dependencies looks like R nl :

R nl = b 0 :P b 1 :X b 2 :X O O A × b 0 :X b 1 :X O b 2 :X M A × add edge(b 0 , A, b 2 )
For k ∈ N, let us consider the two graphs G k (on the left) and G k (on the right):

p 0 :P p 1 :X q 0 :X O O q k :X p 2 :X O p 3 :X M p 0 :P p 1 :X q 0 :X O O q k :X p 2 :X O p 3 :X M A Let us suppose that a GRS G implements the graph rewriting form G k to G k . It is clear that the shortest derivation G k → H 1 → . . . → H d k = G k has length d k ≥ Ω(k).
Let us observe that it is impossible to find a weight compatible with all rules of G. Ad absurdum, suppose that w is such a weight. Then, as there is no node deletion, by Lemma 5.2, for all k > 0,

w(G k ) ≤ w(G k ) -d k . Since w(G k ) -w(G k ) = w(A), d k ≤ -w(A)
. This means that the derivation height is bounded by a constant and this is contradictory with d k ≥ Ω(k).

In Figure 3, we propose a GRS G nl with 4 rules which implements the non-local rule R nl . With this GRS, we have:

G k → Init → k Rec → Stop → k+1 Clean G k .
To prove termination of this GRS, we have to use the notion of contextual weight defined below.

Σ E × Σ N → Z.
As for weights, for some graph G = (N , , E) it extends to any set E ⊆ E by: ω(E) = n e -→m∈E ω( (n), e, (m)). And the weight of a graph is ω(G) = ω(E). A contextual weight is a pair π = (ω, η) with ω an edge contextual weight and η a node weight. We define π(G) = ω(G) + η(G).

An edge contextual weight is called (α,α )-decreasing if We say that a rule R is label-compatible with a context weight ω if ω is (α, α )decreasing whenever R contains a rule change label(α, α ).

∀e ∈ Σ E , ∀β ∈ Σ N , ω (
Lemma 5.3 (Contextual closure). Given a contextual weight π = (ω, η), a rule R = P, c which is (a) uniform, (b) contains no shift and (c) is label-compatible with ω, consider a rule application G → R G . Then π(P ) > π(P ) implies π(G) > π(G ) where

P = P • 1 c. If π(P ) ≥ π(P ), then π(G) ≥ π(G ).
Proof. We do the proof for the strict inequality, the other one is analogous. To stress that the node labeling functions, in G and in G , may differ, we write

ω (E) = n e -→m∈E ω( (n), e, (m)) for E in G and ω (E) = n e -→m∈E ω( (n), e, (m)) for E in G . We recall that E G = P µ ⊕ K µ ⊕ C µ ⊕ H µ and E G = P µ ⊕ K µ ⊕ C µ ⊕ H µ . Since R contains no shift K µ = K µ by Corollary 4.1. Since R is w-compatible, ω (K µ ) = n e -→m∈K µ ω( (n), e, (m)) ≥ n e -→m∈K µ ω( (n), e, (m)) = ω (K µ ) (1)
Since R is uniform, by Lemma 4.1, H µ = H µ ; again, by label-compatibility:

ω (H µ ) ≥ ω (H µ ) (2) Now, π(G) = π(P ) + ω (K µ ) + ω (C µ ) + ω (H µ ) + η(K µ ) + η(C µ ) > π(P ) + ω (K µ ) + ω (C µ ) + ω (H µ ) + η(K µ ) + η(C µ ) by hypothesis > π(P ) + ω (K µ ) + ω (C µ ) + ω (H µ ) + η(K µ ) + η(C µ )
by ( 1) and ( 2)

> π(G )
where the last inequality is due to the fact that the labeling functions and are equal on K µ and C µ .

Definition 5.4 (lexicographical weight). Given an edge weight w 0 : Σ E → Z, given k contextual weights π 1 = (ω 1 , η 1 ), . . . , π k = (ω k , η k ) and a rule R = P, c , we write P = P • 1 c. We say that R is compatible with (w 0 , π 1 , . . . , π k ) iff: either c contains a del node command or R is a node-preserving rule such that: 1 R is uniform and 2 either (i) w 0 (P ) < w 0 (P ) and

(ii) for all e ∈ Σ E such that w(e) < 0, for all n ∈ Φ c (N P ), let M n = Φ -1 c (n); then for all but possibly one element q in M n , the set of negative condition contains α m P (q) q e × ∈ ν and for all but possibly one element p in M n , the set of negative conditions contains α m P (q) q e × ∈ ν.

3 or ∃j ≤ k such that (i) w 0 (P ) = w 0 (P ) and (ii) ∀i < j, π i (P ) = π i (P ) and (iii) π j (P ) < π j (P ) and (iv) ∀i ≤ j, R is label-compatible with w i and (v) c does not contain any shift commands.

When a weight w 0 and k contextual weights π 1 , . . . , π k are compatible with all the rules of some GRS G, we say that G is lexicographically weighted by (w 0 , π 1 , . . . , π k ). Observe that Definition 5.2 corresponds to the current definition with k = 0. Clauses (1) and (2.a) of Definition 5.4 play the role of clauses ( 1) and (2) in Definition 5.2.

Example 5.2. Let us come back to Figure 3, we define

w 0 = 0 Σ E [A → -1], and ω = 0 Σ N ×Σ E ×Σ N [(P, E, X) → 1, (P , E, X) → -1]. Consider the contextual weight π = (ω, 0 Σ N ).
Rule Stop decreases by (2.a); rules Init and Rec decrease by (2.b): there is one more edge labeled E starting from P and rule Clean decrease by (2.b): one edge labeled E starting from P disappears.

Theorem 5.2. Whenever a program G is lexicographically weighted by (w 0 , π 1 , . . . , π k ), it is strongly terminating.

Proof. Given 1 ≤ i ≤ k, let π i = (ω i , η i ), define K ωi = max (α,e,β)∈Σ N ×Σ E ×Σ N |ω i (α, e, β)| K ηi = max α∈Σ N |η i (α)| K πi = |Σ E | × K ωi + K ηi
Then, adapting Lemma 5.1(b) to the present context, we can state that

|ω i (G)| ≤ K ωi × |Σ E | × |G| 2 . With Lemma 5.1(c), we have |η i (G)| ≤ K ηi × |G| and finally |π i (G)| ≤ K ωi × |Σ E | × |G| 2 + K ηi × |G| ≤ K πi × |G| 2 Let K 0 = max i∈[1,k] (K πi )
. Finally, let K E be the constant as given by Lemma 5.1 for w 0 , we define K = max(K 0 , K E ). Then, for all i ≤ k, we have: 3) and ( 4), any element of the sequence

|π i (G)| ≤ K × |G| 2 (3) |w 0 (G)| ≤ K × |G| 2 (4) Consider a sequence G 1 → G 2 → • • • , let I = {1, 2, . . .} be the set of indices of this sequence. Since for all n ∈ I, |G n | ≤ |G 1 |, due to Equations (
(|G n |, w 0 (G n ), π 1 (G n ), . . . , π k (G n )) n∈I is ranging in L = [0, |G 1 |] × [-K × |G 1 | 2 , K × |G 1 | 2 ] k+1
. On the set L, the lexicographic ordering is well-founded. Thus, to prove the finiteness of the sequence

G 1 → G 2 → • • • , it is sufficient to prove that the se- quence (|G n |, w 0 (G n ), π 1 (G n ), . . . , π k (G n ))
n∈I is strictly decreasing for the lexicographic ordering.

Consider a step G → R,µ G of the sequence. The rule R is compatible with the weights, so that we work by case on Definition 5.4. The Lemma 5.2 deals with case (1) and case (2.a) of the definition. It remains to look at case (2.b). So, the commands are neither node deletion nor shifts. Let edges

E G = µ(E P )⊕K µ ⊕C µ ⊕H µ and E G = µ(E P )⊕K µ ⊕C µ ⊕H µ .
Since there is no shift commands (Hyp. (2.b.v)), K µ = K µ , by Corollary 4.1. Since the rule is uniform, H µ = H µ (by Lemma 4.1). Thus, w 0 (G i ) = w 0 (K µ ) + w 0 (C µ ) + w 0 (H µ ) + w 0 (µ(P )) = w 0 (K µ ) + w 0 (C µ ) + w 0 (H µ ) + w 0 (µ(P )) = w 0 (G i+1 ) where the second equality is due to Hypothesis (2.b.i).

Now, let us consider j ∈ N given by definition (2.b). If i ≤ j, applying Lemma 5.3 (with Hyp (2.b.ii) and (2.b.iv)), we get π i (G) ≥ π i (G ) . With Hyp (2.b.iii) and (2.b.iv), the same lemma leads to π j (G) > π j (G ).

Properties of weighted GRS

We consider two properties of weighted GRS. First, we show that we can decide whether or not a GRS has a compatible weight. Second, we give a precise bound on the length of derivation of weighted GRS.

The synthesis of weights

The problem of the synthesis is the following. Given a GRS G, is there a weight w compatible with G? The next theorem gives an answer to this question. Theorem 6.1. Given a GRS G, one may decide whether or not it has a compatible weight.

The remaining of the section is devoted to the proof of the Theorem. To sum up, we have to compute a weight that is compatible with all rules. First we can verify that either the rule preserves node or not. Since this is a syntactical question, it can be checked within the rules. If a rule is node preserving, we have to check its uniformity. Again, this is a syntactical problem. The remaining is to find a weight that respects conditions (2) and (3) for node preserving rules. Let R 1 , . . . , R n be the set of node preserving rules.

Without loss of generality, we suppose Σ E = {e 1 , . . . , e k }. Given some node-preserving rule R = P, ν , c , let P = P • c, finally let the Equation E(R) on variables x 1 , . . . , x k be:

(|P | e1 -|P | e1 ) × x 1 + • • • + (|P | e k -|P | e k ) × x k > 0 E(R).
A weight w verifies Hypothesis (2) of Definition 5.2 iff (x i → w(e i )) i≤k is a solution to Equation E(R) for each R. In other words, to get Hypothesis (2), we have to check the existence of x 1 , . . . , x k such that W (x 1 , . . .

x k ) E(R 1 ) ∧ E(R 2 ) ∧ • • • ∧ E(R n ). Hypothesis (3) is verified as follows. Given e i ∈ Σ E , let H ei ∀R ∈ R 1 , . . . , R k : ∀n ∈ N P : ∀α ∈ Σ N : ∀p, q : (Φ c (p) = Φ c (q) ∧ p = q) ⇒ [( α m P (p) p ei × ∈ ν ∧ α m P (q) q ei × ∈ ν) ∨ ( α m P (p) p ei × ∈ ν ∧ α m P (q) q ei × ∈ ν)]
where in the formula, N P refers to the nodes of the positive pattern of R, c to its commands and ν to the negative conditions of its pattern. As we can see, this formula is actually purely syntactic and its validity can be checked. The Hypothesis (3) is equivalent to U (x 1 , . . . , x k ) ∀i ≤ k :

x i < 0 ⇒ H ei .
So, a weight is compatible with R 1 , . . . , R n whenever ∃x 1 , . . . , x k : W (x 1 , . . . , x k ) ∧ U (x 1 , . . . , x k ) is satisfiable. One may observe that this formula is actually defined in Presburger's arithmetic. Thus, the existence of a weight is decidable. It is clear that the proof, although tedious, can be extended to contextual weights. Thus, Theorem 6.2. Given a GRS G, one may decide whether or not it has a compatible lexicographic weight. 6.2. The derivation height of weighted GRS Definition 6.1. Given a strongly terminating GRS G and a graph G, the derivation height for G, next denoted h G (G), is the length of the longest derivation

G → G 1 → • • • → G k starting from G. The derivation height of G, next denoted h G (n), is defined by: h G (n) = max{h G (G) | |G| ≤ n}.
The proof of Theorem 5.1 actually suggests a cubic upper bound on derivation height.

We establish in this section that the exact-both an upper and a lower-bound on derivation height is quadratic. Theorem 6.3. Given a weighted GRS (G, w), then the derivation height of G is at most quadratic. Furthermore, this quadratic bound is a lower bound, that is there is a GRS G with a compatible weight such that h G (n) ≥ Ω(n 2 ). We prove now the upper bound, that is given a GRS G and a compatible weight w, then h G (n) ≤ O(n 2 ). Let C be the constant as defined by Lemma 4.6, let K = max(1, K w ) (we recall that K w = max e∈Σ E (|w(e)|)). Finally, let H = max{n | (P, c 1 , . . . , c n ) ∈ G}. Let A = 2 × K × C × (H + 1) + 1. Let Ω be the 'energy function' defined on graphs Ω(G) = w(G)

+ A × |G| 2 .
Suppose that G → R,µ G , we prove that Ω(G) > Ω(G ). First, if there is no node deletion, then, w(G) > w(G ), |G| = |G | and the result follows. Suppose now the there is a node deletion command. From the definition of H and the fact that there is a del node command, it is clear that

|G | < |G| ≤ |G | + H. (5)
From Lemma 4.6, we have the decompositions

E G = C µ ⊕ Q µ and E G = C µ ⊕ Q µ . Then w(G) = w(E G ) = w(C µ ) + w(Q µ ) and w(G ) = w(E G ) = w(C µ ) + w(Q µ ). w(G ) -w(G) = w(Q µ ) -w(Q µ ). ( 6
)
Due to Lemma 4.6, both inequality

|Q µ | ≤ C × (|G| + 1) and |Q µ | ≤ C × (|G| + 1) hold. According to Lemma 5.1(a), w(Q µ ) ≤ K w × |Q µ | ≤ K × C × (|G| + 1) and w(Q µ ) ≤ K w × |Q µ | ≤ K × C × (|G| + 1) and so w(Q µ ) -w(Q µ ) ≤ 2 × K × C × (|G| + 1).
Injecting the inequality in Equation 6, we get:

w(G ) -w(G) ≤ 2 × K × C × (|G| + 1) (7) ≤ 2 × K × C × |G | + 2 × K × C × (H + 1) due to Eq 5 (8) < 2 × A × |G | + A (9)
To conclude, if there is a deletion rule,

Ω(G) = w(G) + A × |G| 2 ≥ w(G) + A × (|G | + 1) 2 due to Eq 5 ≥ w(G ) + A × |G | 2 + A × (2 × |G | + 1) + w(G) -w(G ) ≥ Ω(G ) + 2 × A × |G | + A + w(G) -w(G )
> Ω(G ) due to Eq 9.

Now, for all graph G, due to Lemma 5.1, we have:

-K × |Σ E | × |G| 2 ≤ w(G) ≤ K × |Σ E | × |G| 2 and then (A -K × |Σ E |) × |G| 2 ≤ Ω(G) ≤ (A + K × |Σ E |) × |G| 2 .
Since Ω(G) > Ω(G ) for all G → G , given some derivation

G 0 → G 1 → • • • → G k , we can state that k ≤ Ω(G 0 ) -Ω(G k ). After injection of the inequations above, we get k ≤ (K × |Σ E | + A) × |G 0 | 2 + (K × |Σ E | -A) × |G k | 2 . But, |G k | ≤ |G 0 | implies k ≤ 2 × K × |Σ E | × |G 0 |
2 which itself establishes the quadratic bound.

The derivation height of lexicographically weighted GRS

We prove the following theorem:

Theorem 6.4. If a program G is compatible with the lexicographic weight (w 0 , π 1 , . . . , π k ), then its derivation height is at most polynomial. The bound is tight, that is for all k > 0, there is a GRS whose derivation height is O(n k ).

In the proof of the termination of lexicographically weighted programs, we have seen that any sequence k+1 which is a polynomial with respect to |G 1 |. The upper bound follows. Contrarily to the previous section, the bound given here is not precise, but sufficient with respect to the theorem statement.

G 1 → • • • → G n is such that (|G i |, w 0 (G i ), π 1 (G i ), . . . , π k (G i )) i∈[1,n] range in L = [0, |G 1 |] × [-K × |G 1 | 2 , K × |G 1 | 2 ] k+1 . Thus, n ≤ |L| = (|G 1 | + 1) × (2 × |G 1 | 2 + 1)
For the lower bound, we build a graph rewriting system which simulates a k-counters machine. In the graphs we consider, edges are used to encode a k digits representation in base n. The starting graph correponds to the representation (n -1)

• (n -1) • • • (n -1)
k and rules are drawn to decrease the given encoding one by one downto 0 • • • 0 k ; this ensures that the rewriting process uses at least n k steps. All graphs we will consider are built from the skeleton graph (below) by adding edges going from node x to one of the nodes {y 1 , . . . , y n-1 } and labeled by an integer between 1 and k. This drives us to the definitions below (where F stands for "first", S for "successor" and "L" for last). Let Σ E = {1, . . . , k, F, S, L}, let Σ N = {e, e 0 , . . . , e k-1 }. There are four kinds of rules intended to implement the predecessor operation. That is, in terms of counters, to transform the graph corresponding to

a k • • • a l • 0 • • • 0 into a k • • • (a l -1) • (n -1) • • • (n -1), one applies rules: D l , F l-1 , (S l-1 ) n-2 , L l-1 , F l-2 , (S l-2 ) n-2 , L l-2 , . . . , F 1 , (S 1 ) n-2 , L 1
D l decreases by one digit l while the further rules update digits 1 . . . (l -1) from 0 to n -1. More precisely, rules F j , S j increase by one counter number j and L j gives hand to the update of the lower bit.

-For all l such that 1 ≤ l ≤ k, the rule D l (given below) removes a l-edge provided there is no edge with a smaller label starting from x. The node label of x is changed to enforce the construction of the full set of edges with labels 1, . . . , l -1.

x:e 0 y:e -The F -edge of the pattern ensures that y 1 is the first node to receive an l-edge. For all l such that 1 ≤ l ≤ k -1, the rule F l is given by:

x:e l y:e -For all l such that 1 ≤ l ≤ k -1, the rule S l is given by:

x:e l y:e y :e l l × S add edge(x, l, y )

-For all l such that 1 ≤ l ≤ k -1, the rule L l is given by:

x:e l y:e l L change label(x, e l-1 )

The graph rewriting system is lexicographically weighted by (0, π k , . . . , π 1 ), the contextual weights π j being defined by π j = (ω j , η j ) with ω j = 0 Σ N ×Σ E ×Σ N [(e j , j, e) → -2, (e j-1 , j, e), → 2, . . . , (e 0 , j, e) → 2]; -

η j = 0 Σ E [e j-1 → 1].
The verification of the compatibily of the weights with the graph rewriting system is given in the appendix.

A characterization of polynomial time

We have defined in Section 3, Definition 3.12 a notion of semantics, that is which relations are computed by our notion of rewriting. To evaluate the strength of the lexicographic order, we propose to describe the set of relations computed by such GRS through (implicit) computational complexity. To make the relation between computations on graphs and functions on words (as done in complexity theory), we introduce the following notion of computation. Given an alphabet Σ, a word w = a 1 , . . . , a k in Σ * is encoded as a graph G w :

b 1 :a 1 b 2 :a 2 b n-1 :a n b n :nil suc suc suc suc
on the vertex labels Σ ∪ {nil}, the latter label serves as an endmarker. The edge label is suc. It is clear that the function w → G w is injective, thus, given such a graph G, we can define G to be the unique (if it exists) word w such that G = G w . One may observe that G w = w for all words in Σ * . Consider for a while a GRS G working on the set W = {G w | w ∈ Σ * }. Suppose that (G w , G u ) ∈ G . Due to the non-size increasing property of our notion of rewriting, the size |u| of u is smaller than the size |w| of w. This notion of computation-though interesting-restricts to non-size increasing relation. Such relations arise quite usually in complexity theory. Maybe the most remarkable result comes from Hofmann in the context of linear logic [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF] where he describes non-size increasing functions computable in polynomial time. In some way, with the size restriction, the best we can offer is a characterization of functions computable within linear space. However, a machine working in linear space may take exponential time, so that a direct simulation would involve exponential derivation height. Since we have a polynomial derivation length on GRS with lexicographic weight, there is no hope for such a simulation.

To decouple size issues from time issues, we propose a little bit more liberal notion of computation, by padding inputs by a polynomial number of blank symbols. Let us extend the alphabet Σ by an extra blank letter . Let F be a vertex label. Given some word w, F [w] denote the unique graph made of one node F pointing to G w : We state that: Theorem 6.5. Functions computed by a polynomial-time Turing Machine are exactly functions computed up to padding by GRS compatible with a lexicographical weight.

Proof. First, we prove that any function computed (up to padding) by a GRS is computable in polynomial time. So, let us suppose w ∈ Σ * has size n. The initial graph F [w] has size Q(n) = P (n)+n+2 where P is the padding polynomial. Thus, all graphs along a computation have size bounded by Q(n), that is are polynomially bounded with respect to the size of the input word w. By Theorem 6.4, we can state that the derivation height of G on F [w] is bounded by R(P (n) + n + 2) for some polynomial R.

Since the GRS is supposed to be confluent, to compute the normal form of F [w], it is sufficient to simulate the rewriting process. Finding a redex in a graph takes polynomial time (this is the sub-isomorphism problem for some fixed patterns) in the size of the current graph. The graph transformations take linear time (each command taking linear time) in the size of the current graph. Now, we conclude: we apply polynomially many steps with respect to n, each of which takes polynomial time with respect to a the size of a graph which itself has polynomial size with respect to the input words. Thus, the process takes polynomial time.

In the other direction, the key idea is to use the GRS of the preceding section as clocks to simulate the computation of a Turing Machine.

First, without loss of generality, we may suppose that a Turing Machine working in polynomial time uses only a right-lateral tape. That is, it never goes to the left of its input (see for instance the book [START_REF] Jones | Computability and complexity: from a programming perspective[END_REF]). Consider such a machine M working in polynomial time for some polynomial P . If the letter corresponds to the blank symbol of the Turing Machines, we can suppose that a run of M on the initial tape w pad = w • P (|w|) never reaches the last symbol of w pad . In other words, such a machine runs in constant space on its initial configuration.

This being said, any step of computation of a Turing Machine M = Q, Σ, q 0 , F, δ may be simulated by a graph rule. For instance, consider the transition δ(q, a) = (q , a , Right), that is in state q, if the current letter is an 'a', rewrite it by a b, go to the right, and update state to q . This is expressed by the rules: with b ∈ Σ. With the precaution we took at the beginning on the size of inputs, such a step by step simulation will eventually output the result of the computation of the Turing Machine after at most P (|w|) steps. Moreover, for any node weight being constant on Σ ∪ Q, for any edge weight contant on {reads, suc}, for any edge contextual weight constant on Q × {reads, suc} × Σ, the weight of the left hand side of these rules equals their right hand side. Moreover, these rules do not contain any shift commands. It remains to glue clock rules (which will be lexicographically ordered) to the preceding ones to get both:

the termination of the system in time P (|w|) by a lexicographic weight, the simulation of the Turing Machine.

Conclusion

We have implemented a software -called grew (grew.loria.fr)-based on the Graph Rewriting definition presented in this article. In [START_REF] Guillaume | Annotation sémantique du French Treebank à l'aide de la réécriture modulaire de graphes[END_REF], the software was used to produce a semantically annotated version of the French Treebank; in this experiment, the system contains 34 modules and 571 rules and the corpus is constituted of 12 000 sentences of length up to 100 words. This experiment is a large scale application which shows that the proposed approach can be used in real-size applications.

As said earlier, despite the global non-confluence of the system, we can isolate subsets of rules that are confluent and use our system of modules to benefit from this confluence in implementation. In our last experiment, 26 of our 34 modules are confluent, but confluence proofs are tedious. We leave for further work the study of the local confluence of terminating GRS and the general study of confluence of Graph Rewriting Systems. There is no change label in F l and so (2.b.iv) is necessarily verified.

-Rule S l : the clause (2.b) is verified with j = l. We have to check that π l (S l ) < π l (S l ) and that for i > l, π i (S l ) = π i (S l ). The different cases are given in the table below and so, (2.b.ii) and (2.b.iii) are verified for rule S l .

(2.b.ii) (2.b.iii) i > l + 1 i = l + 1 i = l ω i η i ω i η i ω i η i

x There is no change label in S l and so (2.b.iv) is necessarily verified.

-Rule L l : the clause (2.b) is verified with j = l + 1. We have to check that π l+1 (L l ) < π l+1 (S l ) and that for i > l + 1, π i (L l ) = π i (S l ). The different cases are given in the table below and so, (2.b.ii) and (2.b.iii) are verified for rule L l .

(2.b.ii) (2.b.iii) i > l + 1 i = l + 1 ω i η i ω i η i

x:e l y:e l L 0 0 0 1

x:e l y:e l L 0 0 0 0

For the clause (2.b.iv), we have to check that for all i ≥ l + 1, w i is (e l , e l-1 )decreasing. The only case where a crown-edge changes of weight during the operation change label(e l , e l-1 ) is the case of an edge (e l , m, e) which becomes (e l-1 , m, e). Now, if m = i, w i (e l , m, e) = 2 = w i (e l-1 , m, e) and if m = i, w i (e l , m, e) = 0 = w i (e l-1 , m, e).

This achieves to prove the Theorem 6.4.

Fig. 1 .

 1 Fig. 1. DMRS structure for the sentence "The Dog whose toy the cat bit barked"

  Definition 3.3 (Positive pattern and positive matching). A positive pattern B is a graph. A positive matching µ of the positive pattern B in the graph G is an injective graph morphism (written µ : B → G). As shown in Section 2, negative conditions on the subgraph to match naturally arise in NLP. The positive patterns describes what must be present in the image, not what is absent. Negative conditions fulfill the gap. Definition 3.4 (Pattern). A pattern is a pair P = B, ν made of a positive pattern B and a sequence of injective morphisms ν = (ν 1 : B → B 1 , . . . , ν k : B → B k ) that share the graph B. The morphisms ν i within ν are the negative conditions.

  Fig. 2. A pattern, a matching and its decomposition

  be the graph obtained by application of the sequence c 1 , . . . , c k-1 ; then we consider each command in turn: Change label: If µ(a) ∈ N , the command c k = change label(a, α) changes the label of the node µ(a) of the graph G and G • c = (N , , E ) with = [µ(a) → α]. If µ(a) ∈ N then G • c = G . Delete edge: If µ(a) ∈ N , µ(b) ∈ N and µ(a) e -→ µ(b) ∈ E , the command c k = del edge(a, e, b) deletes the edge from µ(a) to µ(b) labelled with e and G • c = (N , , E ) with E = E \ {µ(a) e -→ µ(b)}. Note that, in all other cases (µ(a) ∈ N , µ(b) ∈ N or if no edge µ(a) e -→ µ(b) exists in the graph), then G •del edge(a, e, b) = G , which implies G • c = G . Add edge: If µ(a) ∈ N , µ(b) ∈ N and µ(a) e -→ µ(b) ∈ E , the command c k = add edge(a, e, b) adds an edge from µ(a) to µ(b) labelled with e and G• c = (N , , E ) with E = E ∪ {µ(a) e -→ µ(b)}. Note that, in all other cases (for instance if such an edge already exists in the graph), then G • add edge(a, e, b) = G which implies G • c = G . Delete node: If µ(a) ∈ N , the command c k = del node(a) removes the node µ(a) of the graph G ; G • c = (N , , E ) with N = N \ {µ(a)}, = | N and E = E ∩ {N × Σ E × N }. Shift edges: If µ(a) ∈ N or µ(b) ∈ N , the command c k = shift(a, b) does not change the graph and G • c = G . Else, µ(a) ∈ N and µ(b) ∈ N , the command c k = shift(a, b) changes in-edges of n = µ(a) starting from the crown to in-edges of m = µ(b) and all out-edges of n going to the crown to out-edges of m. We consider the decompositon of nodes of G : N = P µ ⊕ K µ ⊕ C µ . Formally, G • c = (N , , E ) with the set E defined by, for all e ∈ Σ E : for all p ∈ K µ , m e -→ p ∈ E iff m e -→ p ∈ E or n e -→ p ∈ E ; for all p ∈ K µ , p e -→ m ∈ E iff p e -→ m ∈ E or p e -→ n ∈ E ; for all p, q such that {p, q} ∩ {n, m} = ∅, p e -→ q ∈ E iff p e -→ q ∈ E .

P

  Lemma 5.2 (weight context closure). Let (G, w) be a weighted GRS. Suppose that G → G is a rewrite step of G, either |G| > |G | or |G| = |G | and w(G) > w(G ).Proof. The property holds for the pattern, we prove that it is close by context. If the rule applied on G contains a del node command, then, |G| > |G | and the result holds. We suppose now that the rule contains no del node command. Then |G| = |G |. We prove that ω(G) > ω(G ). By Definition 3.7, E G = P µ ⊕ K µ ⊕ C µ ⊕ H µ . Since the rule is uniform (Hyp. (1)), by Theorem 4.1, we can state that edges ofG are E G = µ(P • 1 c ) ⊕ K µ ⊕ C µ ⊕ H µ . As ω(P • c ) < ω(P ) (Hyp.(2) in the definition), we only have to prove that the weight of the crown edges decrease:w(K µ ) ≤ w(K µ ). Since w(K µ ) = e∈Σ E ω(e) × |K µ | e and w(K µ ) = e∈Σ E ω(e) × |K µ | e , it is enough to prove that, for each e ∈ Σ E , that ω(e) × |K µ | e ≤ ω(e) × |K µ | e .For a label e such that ω(e) ≥ 0, this follows from Lemma 4.5. Now let e such that ω(e) < 0, we show that|K µ | e = |K µ | e .Ad absurdum, suppose |K µ | e < |K µ | e , this implies that there are two edges in K µ with the same image in K µ . Suppose that these two edges are oriented from crown nodes to pattern nodes (the other case is similar): m e -→ p ∈ K µ and m e -→ q ∈ K µ such that r = Φ(p) = Φ(q). But this is not possible since either α m thus, one of the two edges cannot exist.

  [add edge(3, A, 4); add edge(5, C, 3)]

  Fig. 3. Local implementation of the non-local rule

  α, e, β) ≥ ω(α , e, β) and ω(β, e, α) ≥ ω(β, e, α )

Proof.

  We begin to show the lower bound. Let Σ E = {E}, Σ N = {e}. Consider the two rules GRS G defined by the two positive patterns: ( P 0 , () , [del edge(0, E, 1)]) and ( P , () , [del edge(2, E, 2)]). Then, since the clique C n of size n has n 2 edges, the derivation height h G (C n ) = n 2 . The lower bound follows from the definition.

  encodes a k digits representation in base n in the following way: the digit of rank j is the number of edges labelled j in the graph. The skeleton graph corresponds to the encoding of 0 • • • 0. The graph encoding (n -1) • • • (n -1) is obtained by adding to the skeleton graph the edges (x -→ y m ) for all 1 ≤ ≤ k and 1 ≤ m ≤ n -1.

  A function φ : Σ * → Σ * is computed up to padding by a confluent GRS G iff there is a polynomial P such that for all words w ∈ Σ * :F [G w• P (|w|) ] → ! G φ(w) .

  c, reads, b 1 ) add edge(c, reads, b 2 ) change label(c, q ) change label(b 1 , a ).

not the right structure. Indeed, the transformation should shift what the linguists call the head of the phrase "Mike begins to work" from the word "begins" to the word "work" with all relative edges. In that case, the transformation should produce the next structure:

  In this case, the verb "begins" is called a raising verb and we know that "Mike" is the deep subject of the verb "work"; "begins" being considered as a modifier of the verb. To recover this deep subject, one may imagine a local transformation of the graph which turns the first graph below into the second one.

					COMP
					CPL			COMP
			SUBJ		SUBJ			AUX
			see	that	Mike	begins	to	work
								SUBJ
				COMP					MOD
	SUBJ	AUX					AUX
	X	Y begins	Z to	T	X	Y begins	Z to	T
	Of course, this kind of transformation can be expressed in any graph rewriting frame-
	work. However, in our example above, a direct application of the transformation leads
	to the structure below:
							SUBJ
				COMP			MOD
			SUBJ		CPL				AUX
		I	see	that	Mike	begins	to	work
	which actually is I	see SUBJ	that	Mike	begins SUBJ CPL COMP	to MOD	AUX	work

  and G , edges that are not in the context are either between two pattern nodes or between a pattern node and a crown node. The total number of edges of the first kind (either pattern edges or glued-pattern edges) is bounded by |P | 2 × |Σ E |. For each pattern node, the number of edges which connect this node to some non-pattern node is bounded by 2 × |G| × |Σ E | and so the total number of edges which link some pattern node to some non-pattern node is bounded by 2 × |G| × |Σ

E | × |P |. Putting everything together, |Q µ | ≤ C × (|G| + 1) and |Q µ | ≤ C × (|G| + 1).

Acknowledgement. The authors thank the referees for their helpful comments. Some of them lead to substantial improvements.

Appendix A. Proof details

We give here the details of the end of the proof of the theorem 6.4. We have to prove that the graph rewriting system described in the proof is lexicographically weighted by (0, π k , . . . , π 1 ), the contextual weights π j being defined by π j = (ω j , η j ) with ω j = 0 Σ N ×Σ E ×Σ N [(e j , j, e) → -2, (e j-1 , j, e), → 2, . . . , (e 0 , j, e) → 2];

It is suffisant to prove that each rule is compatible (definition 5.1) with (0, π k , . . . , π 1 ). No rule contains a del node command and the node weight is 0, so none of the hypothesis (1) and (2.a) apply. Les us prove that all rules verify hypothesis (2.b). As node weight is 0, (2.b.i) is verified for all rules; as there is no shift commands, (2.b.v) is also verified for all rules. It remains to check clauses (2.b.ii), (2.b.iii) and (2.b.iv). Let us consider each rule in turn.

-Rule D l : the clause (2.b) is verified with j = l. We have to check that π l (D l ) < π l (D l ) and that for i > l, π i (D l ) = π i (D l ). The different cases are given in the table below and so, (2.b.ii) and (2.b.iii) are verified for rule D l .

(

For the clause (2.b.iv), we have to check that for all i ≥ l > 1, w i is (e 0 , e l-1 )decreasing. The only case where a crown-edge changes of weight during the operation change label(e 0 , e l-1 ) is the case of an edge (e 0 , m, e) which becomes (e l-1 , m, e). In this case, w i (e 0 , m, e) = 2 and w i (e 0 , m, e) ≥ w i (e l-1 , m, e) because 2 is the maximal weight value.

-Rule F l : the clause (2.b) is verified with j = l. We have to check that π l (F l ) < π l (F l ) and that for i > l, π i (F l ) = π i (F l ). The different cases are given in the table below and so, (2.b.ii) and (2.b.iii) are verified for rule F l .