The termination issue that we tackle is rooted in Natural Language Processing where computations are performed by graph rewriting systems (GRS) that may contain a large number of rules, often in the order of thousands. This asks for algorithmic procedures to verify the termination of such systems. The notion of graph rewriting that we consider does not make any assumption on the structure of graphs (they are not “term graphs”, “port graphs” nor “drags”). This lack of algebraic structure led us to proposing two orders on graphs inspired from language theory: the matrix multiset-path order and the rational embedding order. We show that both are stable by context, which we then use to obtain the main contribution of the paper: under a suitable notion of “interpretation”, a GRS is terminating if and only if it is compatible with an interpretation.
Computer linguists rediscovered a few years ago that graph rewriting is a good model of computation for rule-based
systems. They used traditionally terms, see for instance Chomsky’s Syntagmatic Structures [
Following the tracks of term rewriting, for which the definition is essentially fixed by the algebraic structure of terms,
many approaches to graph rewriting emerged in past years. Some definitions (here meaning semantics) are based on a
categorical framework, e.g., the double pushout (DPO) and the single pushout (SPO) models, see [
Another line of research follows from the seminal work by Lafont [
Let us come back to the initial problem: termination of graph rewriting systems in the context of natural language processing. We already mentioned that rule sets are large, which makes manual inspection impossible. Moreover, empirical studies fail to observe some of the underlying hypotheses of the previous frameworks. For instance, there is no clear bound on tree-width: even if input data such as dependency graphs are almost like trees, the property is not preserved along computations. Also, constraints on node degrees are also problematic: graphs are usually sparse, but some nodes may be highly connected. To illustrate, consider the sentence “The woman, the man, the child and the dog eat together”. The verb “eat” is related to four subjects and there is no a priori limit on this phenomenon. Typed versions (those with fixed arity) are also problematic: a verb may be transitive or not. Moreover, rewriting systems may be intrinsically nondeterministic. For instance, if one computes the semantics of a sentence out of its grammatical analysis, it is quite common there are multiple solutions. To further illustrate nondeterminism consider the well known phrasal construction “He saw a man with a telescope” with two clear readings.
Some hypotheses are rather unusual for standard computations, e.g., fixed number of nodes. Indeed, nodes are usually
related to words or concepts (which are themselves closely related to words). A paraphrase may be a little bit longer
than its original version, but its length can be easily bounded by the length of the original sentence up to some linear
factor. In GREW, node creations are restricted. To take into account the rare cases for which one needs extra nodes, a
“reserve” is allocated at the beginning of the computation. All additional nodes are taken from the reserve. Doing so has
some efficiency advantages, but that goes beyond the scope of the paper. Also, node and edge labels, despite being
large, remain finite sets: they are usually related to some lexicons. These facts together have an important impact on the
termination problem: since there are only finitely many graphs of a given size, rewriting only leads to finitely many
outcomes. Thus, deciding termination for a particular input graph is decidable. However, our problem is to address
termination in the class of all graphs. The latter problem is often referred to as uniform termination, whereas the former
is refereed to as non-uniform. For word rewriting, uniform termination of non increasing systems constituted a well
known problem, and was shown to be undecidable by Sénizergues in [
This paper proposes a novel approach for termination of graph rewriting. In a former paper [
One of our graph orderings will involve matrices, and orderings on matrices. Nonetheless, as far as we see, there is no
relationship with matrix interpretations as defined by Endrullis, Waldmann and Zantema [
The paper is organized as follows. In Section 2 we recall the basic background on graphs and graph rewriting systems (GRS) that we will need throughout the paper, and introduce an example that motivated our work. In Section 3 we consider a language theory approach to the termination of GRSs. In particular, we present the language matrix, and the matrix multiset path order (Subsection 3.4) and the rational embedding order (Subsection 3.5). We also propose the notion of stability by context (Subsection 3.6) and show that both orderings are stable under this condition (Subsection 3.7). In Section 4 we propose notion of graph interpretability and show one of our main results, namely, that a GRS is terminating if and only if it is compatible with interpretations.
Main contributions: The two main contributions of the paper are the following.
1. We propose two orders on graphs inspired from language theory, and we show that both are monotonic and stable by context. 2. We propose a notion of graph interpretation, and show that GRSs that are terminating are exactly those that are compatible with such interpretations.
Notation and Graph Rewriting In this section we recall some general definitions and notation. Given an alphabet ⌃ , the set of words (finite sequences of elements of ⌃ ) is denoted by ⌃ ⇤ . The concatenation of two words v and w is denoted by v · w. The empty word, being the neutral element for concatenation, is denoted by 1⌃ or, when clear from the context, simply by 1. Note that h⌃ ⇤ , 1, ·i constitutes a monoid.
A language on ⌃ is some subset L ✓ ⌃ ⇤ . The set of all languages on ⌃ is P(⌃ ⇤ ). The addition of two languages L, L0 ✓ ⌃ ⇤ is defined by L + L0 = {w | w 2 L _ w 2 L0}. The empty language is denoted by 0 and hP(⌃ ⇤ ), +, 0i is also a (commutative) monoid. Given some word w 2 ⌃ ⇤ , we will also denote by w the language made of the singleton {w} 2 P(⌃ ⇤ ). Given two languages L, L0 ✓ ⌃ ⇤ , their concatenation is defined by L · L0 = {w · w0 | w 2 L ^ w0 2 L0}. In this way, hP(⌃ ⇤ ), 1, ·i is also a monoid. Given the distributivity of ⇥ with respect to +, the 5-tuple hP(⌃ ⇤ ), +, 0, 1, ·i forms a semiring.
A preorder on a set X is a binary relation ✓ X2 that is reflexive (x x, for all x 2 X) and transitive (if x y and
y z, then x z, for all x, y, z 2 X). A preorder is a partial order if it is anti-symmetric (if x y and y x, then
x = y, for all x, y 2 X). An equivalence relation is a preorder that is symmetric (x y ) y x) . Observe that each
preorder induces an equivalence relation ⇠ : a ⇠ b if a b and b a. The strict part of is then the relation: x y
if and only if x y and ¬(x ⇠ y). We also mention the “dual” preorder ⌫ of defined by: x ⌫ y if and only if y x.
A preorder is said to be well-founded if there is no infinite chain · · · x2 x1 or, equivalently, x1 x2 · · · .
The remainder of this section may be found in [
Given a graph G, we denote by NG, EG and `G respectively its sets of nodes, edges and labeling function. We we will also (abusively) use the notation m 2 G and m !e n 2 G instead of m 2 NG and m !e n 2 EG when the context is clear. Furthermore, in | A ~ , a, b are nodes, | , ~ are the respective node labels and A is the edge label (here a b between a and b).
The set of graphs on node labels ⌃ N and edge labels ⌃ E is denoted by G⌃ N,⌃ E or G in short. Two graphs G and G0 are said to share their nodes when NG = NG0 . Given two graphs G and G0 such that NG ✓ N G0 , set G J G0 = hNG0 , EG [ E G0 , `i with `(n) = `G(n) if n 2 NG and `(n) = `G0 (n), otherwise.
A graph morphism µ between a source graph G and a target graph H is a function µ : NG ! N H that preserves edges and labelings, that is, for all m !e n 2 G, µ(m) !e µ(n) 2 H holds, and for any node n 2 G: `G(n) = `H (µ(n)). A basic pattern is a graph, and a basic pattern matching is an injective morphism from a basic pattern P to some graph G. Given such a morphism µ : G ! G0, we define µ(G) to be the sub-graph of G0 made of the nodes {µ(n) | n 2 NG}, of the edges {µ(m) !e µ(n) | m !e n 2 G} and node labels µ(n) 7! `G(n).
A pattern is a pair P = hP0, ~⌫i made of a basic pattern P0 and a sequence of injective morphisms ⌫ i : P0 ! Ni, called negative conditions. The basic pattern describes what must be present in the target graph G, whereas negative conditions say what must be absent in the target graph. Given a pattern P = hP0, ~⌫i and a graph G, a pattern morphism is an injective morphism µ : P0 ! G for which there is no morphism ⇠ i such that µ = ⇠ i ⌫ i.
| b0
A ~ b1 µ
A ~ C E | B g1 A | g0 D g2 A | ~ that we hope is self-explanatory. b0 ⇥ B b1 The pattern P = hP0, [⌫ ]i with ⌫ defined by | A ~ ⌫ | ~ prevents the application of the morphism above.
b0 b1 b0 B b1 Indeed, ⇠ = b0 7! g0, b1 7! g1 is such that ⇠ ⌫ = µ. When there is only one negative condition, we represent the pattern by crossing nodes and edges which are not within the basic pattern. For instance, the pattern P above looks like
A In this paper we think of graph transformations as sequences of “basic commands”.
Definition 1 (The command language). There are three basic commands: label(p, ↵ ) for node renaming, del_edge(p, e, q) for edge deletion and add_edge(p, e, q) for edge creation. In these basic commands, p and q are nodes, ↵ is some node label and e is some edge label. A pattern hP0, ~⌫i is compatible with a command whenever all nodes that it involves belong to P0.
Definition 2 (Operational semantics). Given a pattern P = hP0, ~⌫i compatible with some command c, and some
pattern matching µ : P ! G where G is the graph on which the transformation is applied, we have the following
possible cases: c = label(p, ↵ ) turns the label of µ(p) into ↵ , c = del_edge(p, e, q) removes µ(p) !e µ(q) if it
exists, otherwise does nothing, and c = add_edge(p, e, q) adds the edge µ(p) !e µ(q) if it does not exist, otherwise
does nothing. The graph obtained after such an application is denoted by G ·µ c. Given a sequence of commands
~c = (c1, . . . , cn), let G ·µ ~c be the resulting graph, i.e., G ·µ ~c = (· · · ((G ·µ c1) ·µ c2) ·µ · · · cn).
Remark 1. We took a slightly simplified version of patterns. Actually, in [
Definition 3. A rule is a pair R = hP, ~ci made of a pattern and a (compatible) sequence of commands. Such a rule R applies to a graph G via a pattern morphism µ : P ! G. Let G0 = G ·µ ~c, then we write G ! R,µ G0. We define G ! G0 whenever there is a rule R and a pattern morphism µ such that G ! R,µ G0. 2.1
The main example Let ⌃ N = {A} and ⌃ E = {↵, , T }. For the discussion, we suppose that T is a working label, that is not present in the initial graphs. We want to add a new edge between node n and node 1 each time we find a maximal chain: A ↵ A ↵ A ↵ ··· ↵ A within a graph G. Consider the basic pattern Pinit = A ↵ A together with its two 1 2 3 n p q negative conditions ⌫ 1 = A ⇥ ↵
A ↵ p
A and ⌫ 2 = A ⇥ q
A ↵ p
q Init: hhPinit, [⌫ 1, ⌫ 2]i, (add_edge(p, T, q))i which fires the transitive closure.
p End: h A p
T
A ↵ q T Aq ⇥ ↵
A , (add_edge(p, T, r), del_edge(p, T, q))i which follows the chain.
r
A , (del_edge(p, T, q), add_edge(q, , p ))i which stops the procedure.
To prevent all pathological cases (e.g., when the edge is misplaced, when two chains are crossing, and so on), we could introduce more sophisticated patterns. But, since that does not change issues around termination, we avoid obscuring rules with such technicalities.
Example 2. Consider the graph G = A ↵
1 as: A ↵ 1
A ↵ 2
A ! 3
↵ A A ↵ 1 T 2
A ! 3
A ↵ 2 A 1 2.2
Three technical facts about Graph Rewriting
3 ↵ 2
A ↵ T
A ! 3
A 1 ↵ 2
A ↵
A 3 It is well known that the main issue with graph rewriting definitions is the way the context is related to the pattern image and its rewritten part. We shall tackle this issue with Proposition 1.
Self-application Let R = hP, ~ci be the rule made of a pattern P = hP0, ~⌫i and a sequence of commands ~c. There is the identity morphism 1P0 : P0 ! P0, and thus we can apply rule R on P0 itself, that is, P0 ! R,1P0 P00 = P0 ·1P0 ~c. We call this latter graph the self-application of R.
Rule node renaming To avoid heavy notation, we will use the following trick. Suppose that we are given a rule
R = hP, ~ci, a graph G and a pattern morphism µ : P ! G. Let P = hP0, ~⌫i. We define Rµ to be the rule obtained
by renaming nodes p in P0 to µ(p) (and their references within ~c). For instance, the rule ’Follow’ can be rewritten as
F ollowµ = h A T A ↵ A , (add_edge(1, T, 3), del_edge(1, T, 2))i where µ denotes the pattern morphism used
1 2 3
to apply ’Follow’ in the derivation. Observe that: (i) the basic pattern of Rµ is actually µ(P0), which is a subgraph of
G, (ii) ◆ : µ(P0) ! G mapping n 7! n is a pattern matching, and (iii) applying rule Rµ with ◆ is equivalent to applying
rule R with µ. In other words, G ! R,µ G0 if (and only if) G ! Rµ,◆ G0. To sum up, we can always rewrite a rule so
that its basic pattern is actually a subgraph of G.
↵ ↵
Uniform rules Let us consider rule ’Init’ above. It applies on: A T A , and the result is the graph itself: A T A .
p q p q
Indeed, we cannot add an already present edge (relative to a label) within a graph. Thus, depending on the graph, the
rule will or will not append an edge. Such an unpredictable behavior can be easily avoided by modifying the pattern of
↵
’Init’ to: A T A . The same issue may come from edge deletions. A uniform rule is one for which commands apply
p ⇥ q
(that is, modify the graph) for each rule application. Since this is not the scope of the paper, we refer the reader to [
First, any rule can be replaced by a finite set of uniform rules (using negative conditions as above) that operate identically. Thus, we can always suppose that rules are uniform.
Second, the following property holds for uniform rules (see [
Proposition 1. Suppose that G ! R,◆ G0 with R = hP, ~ci and P = hP0, ~⌫i (the basic pattern P0 being a subgraph of G). Let C be the graph obtained from G by deleting the edges in P0. Then G = P0 J C and G0 = P00 J C with P00 being the self-application of the rule. Moreover, EC \ E P0 = ;and EC \ E P00 = ;.
Throughout the remainder of the paper we assume that all rules are uniform. 3
Termination of Graph Rewriting Systems By a graph rewriting system (GRS) we simply mean a set of graph rewriting rules (see Section 2). A GRS R is said to be terminating if there is no infinite sequence G1 ! G2 ! · · · . Such sequences, whether finite or not, are called derivations.
Since there is no node creation (neither node deletion) in our notion of rewriting, any derivation starting from a graph G will lead to graphs whose size is the size of G. Since there are only finitely many such graphs, we can decide the termination for this particular graph G. However, the question we address here is the uniform termination problem (see Section 1).
Remark 2. Suppose that we are given a strict partial order , not necessarily well founded. If G ! G0 implies G G0 for all graphs G and G0, then the system is terminating. Indeed, suppose it is not the case, let G1 ! G2 ! · · · be an infinite reduction sequence. Since there are only finitely many graphs of size of G1, it means that there are two indices i and j such that Gi ! · · · ! Gj with Gi = Gj . But then, since Gi Gi+1 · · · Gj , we have that Gi Gj = Gi which is a contradiction.
A similar argument was exhibited by Dershowitz in [
Let us try to prove the termination of our main example (see Subsection 2.1). Rules such as ’Init’ and ’End’ are “simple”: we put a weight on edge labels ! : ⌃ E ! R and we say that the weight of a graph is the sum of the weights of its edges labels. Set ! (↵ ) = 0, ! ( ) = 2 and ! (T ) = 1. Then, rules ’Init’ and ’End’ decrease the weight by 1 and, since rule ’Follow’ keeps the weight constant, it means the two former rules can be applied only finitely many times. Observe that negative weights are no problem with respect to Remark 2.
But how do we handle rule ’Follow’? No weights as above can work. 3.1
A language point of view Let G ! G0 be a rule application. The set of nodes stays constant. Let us think of graphs as automata, and let us forget about node labeling for the time being. Let ⌃ E be the set of edge labels. Consider a pair of states (nodes), choose one to be the initial state and one to be the final state. Thus the automaton (graph) defines some regular language on ⌃ E. In fact, the automaton describes n2 languages (one for each pair of states).
Now, let us consider the effect of graph rewriting in terms of languages. Consider an application of the ’Follow’ rule:
G0. Any word to state r that goes through the transitions p !T q !↵ r can be mapped to a shorter one in G0 via
G !
the transition p !T r. The languages corresponding to state r contain shorter words. The remainder of this section is
devoted to formalizing this intuition into proper orders on graphs. For that, we will need to count the number of paths
between any two states. Hence, we shall introduce N-rational expressions, that is, rational expression with multiplicity.
See, e.g., Sakarovitch’s book [
Given a series s, let s k be its restriction to words of length less or equal to k, i.e., s k(w) = 0 whenever |w| > k and s k(w) = s(w), otherwise.
An N-rational expression on an alphabet ⌃ is built upon the grammar [
E ::= a 2 ⌃ | n 2 N | (E + E) | (E · E) | (E⇤ ).
Thus, given the constructions mentioned in the previous paragraph, any N-rational expression E 2 E denotes some formal series. To each N-rational expression corresponds an N-automaton, which is a standard automaton with transitions labeled by a non empty linear combination Pi k niai with ni 2 N and ai 2 ⌃ for all i k. 3.3
The language matrix Let us suppose given an edge label set ⌃ E. Let E denote the N-rational expressions over ⌃ E. A matrix M of dimension P ⇥ P for some (finite) set P is an array (Mi,j )i2 P,j2 P whose entries are in E. Let ME be the set of such matrices. Given a graph G, we define the matrix MG of dimension NG ⇥ N G as follows: MGi,j = T1 + · · · + T` with T1, . . . , T` the set of labels on the transitions between state i and j if such transitions exist, otherwise 0.
Let 1P be the unit matrix of dimension P ⇥ P , that is (1P )i,j = 0 if i 6= j else 1. From now on, we abbreviate the notation from 1P to 1 if the context is clear. Then, let M G⇤ = 1 + MG + M G2 + · · · . Each entry of M G⇤ is actually an N-regular expression (see Sakarovitch Ch. III, §4 for instance). The (infinite) sum is correctly defined since for all i, j, we have the equality (MG)i,j = T1 + · · · + T`. Thus, 1 62 (MG)i,j .
The question about termination can be reformulated in terms of matrices whose entries are languages (with words counted with their multiplicity). To prove the termination of the rewriting system, it is then sufficient to exhibit some order > on matrices such that for any two graphs G ! G0, we have M G⇤ > M G⇤0 . To prove such a property in the infinite class of finite graphs, we will use the notion of “stable orders”.
Recall the ’Follow’ rule and consider the corresponding basic pattern L and its self-application R. Their respective matrices are: Observe that (MR)13 > (ML)13. This matrix deals with edges/transitions. In order to consider paths, we need to compute M L⇤ and M R⇤ that are given by:
Any word within M R⇤’s entries is a sub-word of the corresponding entry in M L⇤.
Example 3. Consider now a variation of ’Follow’ made of the pattern h A T A ↵ A and commands p q r (add_edge(p, T, r), del_edge(p, T, q))i. By setting L0 as its pattern and R0 as its self-application, we get the following
(T ↵ )⇤ M L⇤0 = ↵ (T ↵ )⇤ (T ↵ )⇤
T (↵T (↵T T (↵T )⇤ )⇤ )⇤
T ↵ (T ↵ )⇤ ! ↵ (T ↵ )⇤ (T ↵ )⇤
(T )⇤ M R⇤0 = ↵ (T )⇤ (T )⇤ 0 T (T )⇤ ! 1 ↵ (T )⇤ 0 (T )⇤ .
Again, words within M R⇤0 are sub-words of the corresponding ones in M L⇤0 . 3.4
The matrix multiset path order
The order we shall introduce in this section is inspired by the notion of multiset path ordering within the context of term
rewriting (see for instance [
Let E be the word embedding on ⌃ ⇤ , that is, the smallest partial order such that 1 E w, and if u E v, then (u · w E v · w
and w · u E w · v, for all u, v, w 2 ⌃ ⇤ . This order E can be extended to formal series, that is, the multiset-path ordering,
see Dershowitz and Manna [
Definition 4 (Multiset path order). The multiset path order is the smallest partial order on finite series such that • if there is w 2 t such that for all v 2 s, v / w, then s E t, and • if r E s and t E u, then r + t E s + u.
We write s / t when s E t and s 6= t.
Proposition 2. Addition and product are monotonic with respect to the multiset-path order. Moreover, addition is strictly monotonic with respect to E, and if r / s, then r · t / s · t and t · r / t · s, whenever t 6= 0 (otherwise, we have equality).
Proof. Addition is monotonic by definition. Actually, we prove now that it is strictly monotonic. Suppose that r / s. We prove that r + t / s + t, by induction (see Definition 4). Suppose that there is w 2 s such that for all v 2 r we have v / w, then r / s. Since r(w) = 0, then (r + t)(w) = t(w) < s(w) + t(w) = (s + t)(w), and we are done. Otherwise, r = r0 + r1 and s = s0 + s1 with r0 E s0 and r1 E s1. One of the two inequalities must be strict (otherwise r = s). Suppose r0 / s0. By definition, observe that r1 + t E s1 + t. But then, r + t = r0 + (r1 + t) and s = s0 + (s1 + t) and we apply induction on (r0, s0). As addition is commutative, the result holds.
For the product, suppose that r E s and let t be some series. We prove r · t E s · t; the other inequality t · r E t · s is similar. Again, we proceed by induction on Definition 4: • Suppose there is w 2 s such that for all v 2 r, v / w. By induction on t, if t = 0, r · t = 0 E 0 = s · t.
Otherwise, t = t0 + v0 for a word v0. Observe that r · v0 = Pv2 r r(v)v · v0. Since for all v 2 r, v · v0 / w · v0, we have r · v0 / w · v0 E s · v0. Now, r · t = r · (t0 + v0) = r · t0 + r · v0 and s · t = s · t0 + s · v0. By induction, r · t0 E s · t0 and since r · v0 E s · v0, the result holds. • Otherwise, r = r0 + r1. In this case, s · r = s · r0 + s · r1 and t · r = t · r0 + t · r1. The result then follows by induction.
To show strict monotonicity, suppose r / s and again proceed by case analysis. Suppose that there is some w 2 s such that for all v 2 r, v / w. Since t 6= 0, it contains at least one word v0 such that t = t0 + v0. By r / s, r · v0 = Pv2 r r(v)v·v0 /Pv2 s s(v)v·v0 = s·v0. Now, r·t0 E s·t0 by monotonicity. Thus r·t = r·t0 +r·v0 /s·t0 +s·v0 = s·t where the strict inequality is due to strict monotonicity of addition.
|P | and for all (i, j) 2 P ⇥ P , we have M i,jk E Mi0,j k.
Definition 5 (Matrix multiset-path order). Let M and M 0 be two matrices with dimension P ⇥ P . Write M E M 0 if for all k Corollary 1. The addition and the multiplication are monotonic with respect to the matrix multiset-path order. Proof. It follows from Proposition 2 since addition and product of matrices are defined as addition and product of their entries.
Proposition 3. Let [⌧ ] : L !
assertions hold.
Let ⌃ be some fixed alphabet. A finite state transducer is a finite state automaton whose transitions are decorated by
pairs (a, w), a 2 ⌃ , w 2 ⌃ ⇤ . We refer the reader to the book of Sakarovitch [
• such that |f (w)| | w|, for every w 2 L0. Such functions (and the corresponding transducers) are said to be
decreasing (in [
We say that a transition of a transducer is deleting when it is of the form a | 1 for some a 2 ⌃ . A transducer whose transitions are of the form X | Y , with |Y | | X|, is itself decreasing. If a path corresponding to an input w passes through a deleting transition, then |⌧ (w)| < |w|.
In the sequel we will make use of the following results that are direct consequences of Nivat’s Theorem [
L0 be computed by a transducer ⌧ , and let L00 be a regular language. Then the following 1. The restriction ⌧ |L00 : L00 \ L !
L0 \ L00 mapping w 7! ⌧ (w) if ⌧ (w) 2 L00 and otherwise undefined, is 2. The co-restriction ⌧ |L00 : L !
computable by a transducer. 3. The function ⌧ 0 : L ! transducer.
L0 defined by ⌧ 0(w) = ⌧ (w) if w 2 L00 and otherwise undefined, is computable by a Observe that the identity on ⌃ ⇤ is computed by a transducer (made of a unique initial/final state with transitions a | a for all a 2 ⌃ ). Then, the identity on L is obtained by Proposition 3(1,2). Thus we have that . is reflexive. Also, it is well known that both transducers and injective functions can be composed. Hence, we also have that . is transitive. Thus, . is a preorder.
However, we do not have anti-reflexivity in general. For instance, we have
L1 = A · (A + B)⇤ . L2 = B · (A + B)⇤ . L1.
To see this, consider the following transducer (whose initial state is indicated by an in-arrow, whereas the final one by
B | A an out-arrow): q0 A | B q1
. This shows that L1 . L2. Swap ’A’ and ’B’, to see that the reversed relation also holds.
A | B It is worth noting that there is a simple criterion to ensure a strict inequality.
transition, then the relation is strict.
Proof. As before, set L1 < L2 whenever L1 . L2 but not L2 . L1. Ad absurdum, suppose L1 . L2 . L1 with a transducer ✓ : L1 ! L2 and ⌧ as above. Then ✓ ⌧ (the composition of the two transducers) defines an injective function. Let w be the smallest input word from the initial state to a final state through the transition a | 1 in ⌧ . Define the set
M <|w| = {u 2 L2 | |u| < |w|}. For any word u, we have |✓ ⌧ (u)| | u|. Thus ✓ ⌧ (M <w) ✓ M <w. Since M <w is a finite set and ✓ ⌧ is injective, it is actually bijective when restricted to M <w. However, |✓ ⌧ (w)| | ⌧ (w)| < w implies ✓ ⌧ (w) 2 M <w. By the Pigeon-hole Principle, there is one word in M <w that has two pre-images via ✓ ⌧ . Thus, ✓ ⌧ cannot be injective, which yields a contradiction.
Remark 3. From Proposition 3 it follows that if two regular languages L and L0 are such that L ✓ L0, then L . L0. Definition 7. The rational embedding order extends to matrices by pointwise ordering: Let M and N with dimension P ⇥ P , and write M . N if for every i, j 2 P ⇥ P , we have Mi,j . Ni,j .
Recall the modified version of ’Follow’ (Example 3). The following transducers show that all entries strictly decrease. In the following, to compare two graphs by means of the rational embedding order, we transform graphs into matrices as follows. Given a graph G, let M G0 be the matrix of dimension NG ⇥ N G such that (M G0)i,j = T1i,j + T2i,j + · · · T`i,j with T1, . . . , T` the labels of the edges from i to j. In other words, we “decorate” the labels with the source and target nodes. Then, G . G0 whenever M G0 . M G00 . 3.6 Stable orders on matrices A matrix on E is said to be finite whenever all its entries are finite. Two matrices M and M 0 (of same dimension) on E are said to be disjoint if for every i, j, Mi,j · Mi0,j = 0.
matrix M " G defined by:
(M " G)i,j = ⇢ Mi,j if i, j 2 P 0 otherwise The notation M " G is shortened to M " when G is clear from the context. Fact 1. Let M be a matrix of dimension P ⇥ P , with P ✓ Definition 9. We say that a partial order on E is stable by context if for every P ✓ dimension P ⇥ P , and every C of dimension G ⇥ G, the following assertions hold. G. Then (M " G)⇤ = (M ⇤ )" G. 1. If L, R, C are finite, L being disjoint from C, R being disjoint from C and R⇤ (L + C)⇤ ;
L, then R" G
L" G.
Lemma 1. Let be a partial order stable by context and consider finite matrices L, R of dimension P ⇥ P and let C be a finite matrix of dimension G ⇥ G with P ✓ G. Then, R⇤ L⇤ implies (R" + C)⇤ (L" + C)⇤ . Proof. If R⇤ L⇤ , then we have (R⇤ )" (L⇤ )" by Definition 9.2. By Lemma 1, it follows that (R" )⇤ Clearly, R" and L" are finite, and from Definition 9.1, we have (R" + C)⇤ (L" + C)⇤ (L" )⇤ .
Theorem 1. Let be a partial order stable by context. Suppose that for every rule R = hP, ~ci with P = hP0, ~⌫i and P00 the self-application of R, we have (P00)⇤ (P0)⇤ . Then the corresponding GRS is terminating. Proof. Let be a partial order on graphs and consider the corresponding order on matrices: G G0 if and only if M G⇤ M G⇤0 . We show that for every rule, we have G ! G0 implies G0 G. So let R be a graph rewriting rule and let µ be a morphism such that G ! R,µ G0. By the discussion in the beginning of Section 3, without loss of generality, we | ↵ | 1 q0 | q1 T | T q2 ↵ | 1 1 C C C C C C C C C C C C C C A can suppose that µ is actually the inclusion of pattern P0 in G. Now, let P0 and P00 be respectively the basic pattern and the self-application of R. Define C to be the graph made of the nodes of G without edges in P0. By Proposition 1, MG = M P"0 + MC and MG0 = M P" 0 + MC . Moreover, MP0 , MP 0 and MC are finite, MP0 is disjoint from MC , and 0 0 MP00 is disjoint from MC . From Lemma 1 it thus follows that M G⇤0 = (M P" 0 + MC )⇤ (M P"0 + MC )⇤ = M G⇤. 0 3.7 Stability of the orderings
Proof. We first verify that condition 2 of Definition 9 holds. Suppose that R / L with R, L of dimension P ⇥ P . Then, for all (i, j) 62 P ⇥ P , Ri",Gj = 0 E 0 = L"i,Gj. Now, for all k |G| |P | and for all (i, j) 2 P ⇥ P , we have (R" G)i,jk = Ri,jk E Li,jk = (L" G)i,jk. To verify that condition 1 also holds, let G ⇥ G be the dimension of L, R and C. Take k |G|. On the one side we have and on the other side (R + C)⇤ k = (L + C)⇤ k = where Ai{R result follows.
X
X (A1,...,A`)2{ R,C}⇤ , ` k i ` (A1,...,A`)2{ R,C}⇤ |` k i `
Y Ai Y Ai{R
L},
L} = L if Ai = R, and C otherwise. As the product and the addition are (strictly) monotonic, the
Proof. Since we use a component-wise ordering, it is easy to verify that condition 2 of Definition 9 holds. To verify that condition 1 also holds, let P ⇥ P be the shared dimension of L, R and C of dimension G ⇥ G with P ✓ G. Since R < L, there are decreasing transducers ⌧ i,j : Li,j ! Ri,j with at least one of them deleting. We build the family of transducers (✓ p,q)p,q2 G⇥ G as follows. The family of transducers will share the major part of the construction. They only differ by their initial and terminal states. First, we make a copy of all transducers (⌧ i,j )i,j . Then, we add as states T i,j|T i,j ! all the elements of G outside P . Given a non null entry T = Ci,j , we set a transition i j. That is the transducer T i,j|T i,j "copies" the paths within C. For a an entry T = Ci,j with i 62 P, j 2 P , we set the transitions: i ! qn for all qn initial state of the transducer ⌧ j,n, n 2 P . Similarly, for any entry T = Ci,j with i 2 P, j 62 P , we set the transitions:
T i,j|T i,j rn ! j for each terminal state rn of the transducer ⌧ n,i, n 2 P . This construction can be represented as follows: j
U j,i | U j,i
V i,k | V i,k i T i,j | T i,j
W i,` | W i,` p q ⌧ k,m · · · · · · · · · ⌧ `,n r s
Xm,i | Xm,i Y n,i | Y n,i where U, T, W, X, Y range over the edge labels. Take k, ` 62 P . Any path from state k to state ` describes a path in C + L on the input side and a path in C + R on the output side. Indeed, transitions within C are simply copied and the transducers ⌧ i,j transform paths in L into paths in R.
It remains to specify initial and final states of ✓ p,q with (p, q) 2 G ⇥ G. Given some entry p, q 2 G, if p 62 P , we set the initial state to be p. Otherwise, we introduce a new state ◆ which is set to be initial, and we add a transition ◆ 1!|1 i for any state i initial in ⌧ p,r for some r. If q 62 P , then, q is the final state. Otherwise, any state j within some ⌧ r,q, r 2 P , is final.
Consider some pair p, q 2 G. We prove that the transducer ✓ p,q is injective. Consider a path w in C + L. It can be decomposed as follows: w = w1`1 · · · wk`k where the `i’s are the sub-words within L (that is the wi’s have the shape viai where ai is a transition from C to L). Consider a second word w0 = w10`01 · · · wk00 `0k0 such that the transducer ✓ p,q(w) = ✓ p,q(w0) = u. Given the construction of ✓ p,q, consider the word u = u1r1 · · · ukrk with r1, . . . , rk some path within R. Indeed, only a letter within L can produce a letter within R. Consider the case where rk is non empty. When the transducer reaches the first letter in `k, it is in a state ⌧ k,m for some m. Actually, m = q since only ⌧ k,q contains a final state. Thus, the path is fixed within ⌧ k,p and then the injectivity of ⌧ k,p applies. So, `0k0 = `k. We can go back within wk. On this part of the word, the transitions have the shape T i,j | T i,j . Thus, wk = wk00 . We can continue this process up to the beginning of w and w0. Up to here, rewriting did not involve node creation. In this subsection, we will adress this issue informally, and we leave for future work the definitive formalization.
So consider a new command add_node(↵ ) with ↵ a label. This command adds a new node to the graph with label ↵ . As in standard settings, this node is not related to others at creation time.
Actually, we see node creation as follows. Let us consider a fixed denumerable set U of nodes. For any finite graph, one may suppose without loss of generality that its nodes belong to U . More precisely, we see graphs as having U as an underlying node set, among which only finitely many are “under focus”. The nodes in this finite set have a label within the set ⌃ N and they may be related via edges to some other nodes, all the others are isolated and their label is ? , a trash label. In other words, there is never some node creation, but some may be added to the focus. Notice that at each step, only finitely many nodes may be added to a graph via rewriting. In finitely many steps, starting from a finite graph, the denumerable set U is a sufficiently large container.
If we come back to our termination issue, there are a few changes. In the one hand, matrices have infinite dimension, that is, U ⇥ U . But on the other hand, at each step of computation, only finitely many entries are non null. Thus, all established results still apply to this more general framework and the method is still correct.
As a consequence, if we still find some ordering on language matrices, termination will follow. However, there is one important point that must be discussed in detail. We said that the ordering on matrices did not need to be well founded to show termination. And for that, we needed the fact that all graphs met during computation have a fixed size (so that there are only finitely many of them). In the present context, this hypothesis is not reasonable in general. We thus propose two ways of overcoming this apparent limitation.
First, if the ordering on matrices is well-founded, there are no more issues. Termination will hold directly. Second, if
the ordering is not well-founded, then we will need an additional ingredient. Let us suppose that the ordering is stable
by edge contraction: that is, if G0 is obtained from G by contracting some edge e 2 G, then MG0 MG. Suppose
furthermore that for any steps, G ! G0, we have MG0 MG, then the system is terminating. Indeed, due to Robertson
and Seymour’s Theorem (see [
Interpretation methods are well known in the context of term rewriting, see for instance Dershowitz and Jouannaud’s
survey on rewriting [
Definition 10. A graph interpretation is a triple hX, , i where hX, i is a partially ordered set and : G ! X is such that given two graphs P and P 0 having the same set of nodes and C disjoint of P and P 0, if (P ) (P 0), then (P + C) (P 0 + C).
An interpretation ⌦ = hX, , i is compatible with a rule R if (P00) (P0) where P0 is the basic pattern of R and P00 its self-application. Similarly, an interpretation is compatible with a GRS if it is compatible with all of its rules. Theorem 2. Every GRS compatible with an interpretation ⌦ is terminating.
The theorem being a more abstract form of Theorem 1, its proof follows exactly the same steps. Proof. Suppose that G G0 if and only if (G) (G0). We prove that for each rule R of the GRS, G ! G0 implies G0 G. Indeed, suppose that G ! R,µ G0. Let P0 and P00 be respectively the basic pattern and the self-application of R. Then, there is a graph C such that G = P0 + C, G0 = P00 + C, such that P0 and P00 are disjoint from C. Since (P00) (P ), we then have (G0) (G).
Example 4. The triple hM, E, (M( ))⇤ i is an interpretation for ’Follow’.
1, ! ( ) =
Example 5. Let us come back to the weight analysis. Define ! (G) = Pp! e q2 G ! (e) with ! (↵ ) = 0, ! (T ) = Example 6. Let hX1, 1, 1i be an interpretation for a set of rules R1, and let hX2, 2, 2i be an interpretation for a set of rules R2. Suppose that for every rule R in R2, G ! R,µ G0 implies G0 1 G (that is without strict inequality). Then the lexicographic ordering on X1 ⇥ X2 defined by (x1, x2) 1,2 (y1, y2) if and only if x1 1 y1, or x1 1 y1 and x2 2 y2, constitutes an interpretation hX1 ⇥ X2, 1,2, 1 ⇥ 2i for R1 [ R 2.
Thus, combining Example 4 and Example 5, we have a proof of the termination of the Main Example (Subsection 2.1).
Example 7. Let R be a terminating GRS. Then there is an interpretation that “justifies” this fact. Indeed, take hG, , 1G i with defined to be the transitive closure of the rewriting relation ! . The termination property ensures that the closure leads to an irreflexive relation. The compatibility of with respect to 1G is immediate.
Corollary 3. A GRS is terminating if and only if it is compatible with some interpretation. 5
Conclusion
We proposed a new approach based on the theory of regular languages to decide the termination of graph rewriting
systems, which does not account for node additions but settles the uniform termination problem for these GRS. We
think that there is room to reconsider some old results of this theory under the new light. In particular, we think of
profinite topology [
As the next natural step, we intend to explore more systematically graph rewriting with node creations and that take into account node labels. Moreover, in the experiments mentioned in the introduction about natural language processing, in principle, these two orders should still be sufficient to ensure termination. However, we need to implement these new results for an extensive and complete evaluation.
Acknowledgment. The authors are thankful to the anonymous reviewers for their careful reading of our manuscript and for the constructive remarks and useful suggestions, that were of great help when revising this manuscript.