Rachid Echahed

Nicolas Peltier

Priority-Independent Rewrite Systems for Pointer-based Data-Structures

We define a syntactic class of graphs and graph rewrite systems for which the normal forms are independent from the order in which the nodes are reduced. This result, that is not covered by existing approaches in graph rewriting, allows us to devise simple confluence criteria and efficient normalization algorithms. It is based on a static analysis of the rewrite system, including a thorough analysis of the shape of the graphs generated during the rewriting process. The considered graphs naturally encode pointer-based data structures that are commonly used in practical programming and the rewrite rules can simulate any elementary transformation on these data structures (edge redirection, node relabeling etc.).

1 i.e. by redirecting existing edges instead of created new cells.

1 between the nodes (thus removing any computational overcost) and relies instead on a static analysis of the rewrite system. More precisely, we devise an algorithm that, given a graph rewrite system R and a graph t, effectively detects that the normal forms of t w.r.t. R do not depend on the order of reduction of the nodes (not only the nodes occurring in t, but also those introduced during rewriting). The graphs and rules for which the order of reduction is relevant are called clash-reducible. The algorithm runs in polynomial time w.r.t. the size of R and t. Furthermore, the most important part of the computation may be performed once and for all for a given graph rewrite system (see Section 5).

This result has many important applications that are of great interest in the context of declarative programming. Firstly, confluence criteria are easy to define for non clash-reducible graphs: it suffices to check that two distinct rules cannot be applied on the same node 2 . Secondly, efficient evaluation strategies can be defined, without any computational overcost w.r.t. the usual approaches in term rewriting (the computation of the dependency schemata which was required in [6] is avoided). Furthermore, it makes possible to use the narrowing algorithm of [4] to solve goals and synthesize complex data-structures. This last point is interesting because this narrowing algorithm is not compatible with priorities 3 .

Determining whether a graph rewrite system is clash-reducible or not is an undecidable problem. Thus the class of systems that are accepted by our algorithm, that are called well-defined, is strictly contained into the class of non clash-reducible systems. Roughly speaking, our algorithm checks that if two distinct defined functions f and g operate on the same node (or edge) γ in the reduced graph, then neither f nor g can physically affect γ and -more importantly -that this property is preserved during the rewriting process. This is done by automatically analyzing the shape of the graphs occurring in the derivation in order to find decidable approximations of the graph obtained after rewriting. It is worth to mention that well-defined graph rewrite systems may have non joinable critical pairs in the sense that there exist graphs on which two distinct rules apply, yielding non joinable results. Thus confluence cannot be proven by traditional approaches. Our automated analysis ensures that those graphs will never occur in the derivation (if the initial graph and the rewrite rules are well-defined).

As illustrated by the examples in Sections 1.3 and 4, the class of well-defined graph rewrite systems is comprehensive enough to express many interesting graph transformation algorithms. If a graph rewrite system is not well-defined, then it is usually easy to construct a well-defined system that computes the same normal forms (in the worst case this may be done by composing graph transformations in a purely sequential way). Well-defined graph rewrite systems may be a good candidate for defining efficient declarative programming languages operating on graphs and offering similar features than the languages based on term rewriting such as Haskell or Curry: efficient (or even optimal) lazy evaluation strategies, etc. The use of well-defined graph rewrite systems would significantly increase the expressiveness of declarative languages. As far as we are aware, no existing approach in graph rewriting offers comparable features (in particular, the confluence criteria are much less general).

The rest of the paper is structured as follows. In Section 1 we introduce the basic terminology on graphs and graph rewrite rules. In Section 2 we introduce a semantic criterion ensuring that the results of the derivations do not depend on the reduction ordering. We define simple confluence criteria for such graphs and efficient reduction strategies. In Section 3, we introduce a syntactic class of graphs called well-defined, that satisfy the condition above. Section 4 provides examples of well-defined graph rewrite systems. All these systems are confluent on well-defined graphs, although they have non joinable critical pairs (modulo isomorphism). Section 5 discusses the possible use of the results and concludes the paper.

Graph Rewriting

 because we restrict ourselves to injective mappings.

Basic Definitions

We assume that the following sets of symbols are given: a set of sorts S (denoted by s, nat, bool, . . .) a set of nodes N (denoted by Greek letters) and a set of function symbols Σ (denoted by f, g, . . .). Σ is divided into two disjoint sets of symbols: a set of defined symbols D and a set of constructors C. Every node α is mapped to a unique sort sort(α) and every function symbol f is mapped to a unique profile of the form s 1 × . . . × s n → s. n is called the arity of f and denoted by ar(f ).

Rewriting is a central paradigm in declarative programming. Most algorithms can be conveniently specified as sets of oriented equations, interpreted as rewrite rules. Efficient reduction strategies have been designed for computing the normal forms and narrowing algorithms can be used to solve goals. Unfortunately, some algorithms (e.g. the Schorr-Waite algorithm [START_REF] Schorr | An Efficient Machine Independent Procedure for Garbage Collection in Various List Structures[END_REF] or in-situ algorithms for sorting or reversing a list) are difficult (or even impossible) to specify by term rewrite rules (except by using inefficient encodings) because they strongly rely on the use of complex pointer-based data-structures and pointer redirections. The most natural way to specify these algorithms is to use rewrite rules operating on graphs, that are a very convenient and precise formalism for denoting the data-structures used in everyday programming. Numerous approaches exist in graph rewriting, with various kinds of graphs and rewrite systems. Most of them use algebraic formalisms based on category theory (using single or double push-outs). Many implementations have been developed and used for solving practical problems: GraphSynth, AGG, PROGRES,. . . We refer to [START_REF]Handbook of graph grammars and computing by graph transformation[END_REF][START_REF] Heckel | Graph transformation in a nutshell[END_REF][START_REF] Ehrig | Fundamentals of Algebraic Graph Transformation[END_REF] for overviews of this research domain and additional references.

A drawback of graph rewrite systems is that confluence is very hard to satisfy [START_REF] Plump | Confluence of graph transformation revisited[END_REF][START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF]. Confluence is an essential property, especially when rewrite rules are used to define functions, because it ensures that the normal forms are unique and enables more efficient reduction algorithms. Unfortunately, graph rewrite systems are seldom confluent, because two distinct defined functions may operate on the same nodes or edges. Even a rewrite system as simple as f (x) → x, g(x) → x turns out to be non confluent when applied on the cyclic term-graph α = f (g(α)) (even modulo isomorphism). This is even more obvious if the defined functions affect their arguments (e.g. by redirecting edges). Almost all non trivial graph rewrite systems have non joinable critical pairs. Assume for instance that one defines a function rev that physically 1 reverses a list and a function length returning the length of a list. Then the normal form of the graph (DAG) f (length(γ)), rev(γ)) where γ = [START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF][START_REF] Barendregt | Term Graph Rewriting[END_REF] obviously depends on the order on which the arguments of f are evaluated. If length(γ) is evaluated first we get f (2, [START_REF] Barendregt | Term Graph Rewriting[END_REF][START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF]). But if rev(γ) is evaluated first we get f (1, [START_REF] Barendregt | Term Graph Rewriting[END_REF][START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF]) since after the evaluation of rev( [START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF][START_REF] Barendregt | Term Graph Rewriting[END_REF]) the argument of length (i.e. the cell containing 1) becomes the last cell of the list.

In [START_REF] Echahed | Non Strict Confluent Rewrite Systems for Data-Structures with Pointers[END_REF] we have proposed to overcome this problem by ordering the nodes of the graphs. In this approach, a priority ordering must be provided by the programmer to specify the order in which the nodes are to be reduced, thereby ensuring the uniqueness of the normal form (for orthogonal rewrite systems). The drawback is that a set of relations, called the dependency schema, needs to be computed during the reduction of the graphs, in order to handle the dependencies between the defined functions operating on the same edges and nodes. This entails some computational overcost which may be unacceptable for applications in which efficiency is critical and/or for which the considered graphs are very large. This paper proposes another solution to the confluence problem in graph rewriting, which completely avoids the use of any priority ordering Definition 1 A term-graph (or simply a graph) t is defined by:

• A set of nodes N (t) ⊆ N .

• A node root(t) ⊆ N (t) called the root of t.

• A partial function (also denoted by t) mapping node α ∈ N (t) to a term of the form f (β 1 , . . . , β n ) s.t. f is of profile s 1 ×. . .×s n → s, β 1 , . . . , β n ∈ N (t)∪{⊥}, sort(α) = s and ∀i ∈ [1..n],

β i = ⊥ ⇒ sort(β i ) = s i .
The symbol ⊥ is used to denote undefined arguments. The set of nodes α s.t. t(α) is undefined is the set of variables, denoted by var(t). If t(α) = f (β 1 , . . . , β n ) then f is called the label of the node α and denoted by l t (α).

A position is a sequence of natural numbers. "." denotes the concatenation operator and ǫ denotes the empty sequence. If p is a position then p t (α) denotes the node reachable from α following the position p:

p t (α) def =    α if p is empty q t (β i ) if p = i.q, t(α) = f (β 1 , . . . , β n ), i ∈ [1.
.n] and β i = ⊥ undefined otherwise

In particular, if i is a natural number, then i t (α) is the i-th argument of t(α). The set of positions p s.t. p t (α) is defined is written pos t (α). If i is a natural number and if i t (α) = β then we say that t contains an edge from α to β, labeled by i. By definition, given a node α and a label i, there can be at most one edge starting from α and labeled by i and this edge points to i t (α).

Two graphs t, s are disjoint iff they share no nodes: N (t) ∩ N (s) = ∅. We write t ⊆ s iff N (t) ⊆ N (s) and ∀i ∈ N ∪ {l}, i t (α) = ⊥ ⇒ i s (α) = i t (α).

t, s are compatible iff there exists a graph containing both t and s, i.e. if the following property holds: ∀α ∈ N (t) ∩ N (s), ∀i ∈ N ∪ {l}, (i t (α) = ⊥ ∧ i s (α) = ⊥) ⇒ i t (α) = i s (α).

A path in a graph t from a node α to β is a sequence of nodes γ 1 , . . . , γ n s.t. γ 1 = α, γ n = β and for every i ∈ [1..n -1], t contains an edge from γ i to γ i+1 . If moreover every node in γ 1 , . . . , γ n is labeled by a constructor then γ 1 , . . . , γ n is a constructor path. We write α → t β (resp. α C → t β) if there exists a path (resp. a constructor path) from α to β. Obviously, α → t β iff β = t p (α) for some position p. → t is reflexive but not C → t ( C → t is reflexive only on nodes labeled by constructors). α, β are joinable (written α ↓ t β) if there exists a node γ s.t. α → t γ and β → t γ. If moreover sort(γ) = s, then we write α ↓ s t β.

Denoting graphs by labeled terms

For the sake of conciseness and readability, we use a linear notation for denoting graphs. The term α:f (t 1 , . . . , t n ) will be used as an abbreviation for denoting a graph t of root α, containing t 1 , . . . , t n and s.t. t(α) = f (root(t 1 ), . . . , root(t n )). We assume that t 1 , . . . , t n are compatible and that α is a non variable node in t 1 , . . . , t n . The node α can be left unspecified, and in this case it is simply replaced by an arbitrary node not occurring elsewhere. A term α ∈ N denotes a graph with a unique node α and no edge (i.e. a variable).

Some Basic Operations on Graphs

Union

If t, s are two graphs, we denote by t; s the graph u defined as follows:

• N (u) def = N (t) ∪ N (s) and root(u) def = root(t). • ∀α ∈ N (u), ∀i ∈ N ∪ {l}: i t (β) def =    i s (β) if i s (β) is defined. i t (β)
if i s (β) is undefined and i t (β) is defined. undefined if both i s (β) and i t (β) are undefined Informally, t; s is the union of t and s, where the labels/edges in s "overwrite" those in t. Notice that ";" is commutative iff t and s are compatible and have the same root.

Replacement

If t is a graph, we denote by t| α the subgraph s of t of root α, formally defined as follows:

• N (s) def = {β | α → t β}. • root(s) def = α. • ∀β ∈ N (s), s(α) def = t(α).
This notation extends naturally to positions: t| p denotes the graph t| α where α = p t (root(t)). If t is a graph and α, β are two nodes s.t. sort(α) = sort(β), we denote by t β/α the graph s obtained by redirecting every edge pointing to α to the node β, formally defined as follows:

• N (s) def = (N (t) \ {α}) ∪ {β}, root(s) def = root(t) if α = root(t) β if α = root(t) • ∀γ ∈ N (s), l s (γ) def = l t (γ) and ∀i ∈ N, i s (γ) def = β if i s (γ) = α. i t (γ) otherwise Then t[s] α denotes the graph: t[s] α def = t root(s)/α ; s.

Renamings

A renaming σ is a partial injective4 function from N to N . As usual, σ is extended into an homomorphism on the terms built on Σ ∪ N ∪ {⊥}. If σ is a renaming and t is a graph, σ(t) denotes the graph s defined as follows:

• N (s) def = {σ(α) | α ∈ N (t)}. • root(s) def = σ(root(t)). • s(σ(α)) def = σ(t(α)).
Notice that s is necessarily well-defined since σ is injective. We write t ≡ s if s = σ(t) for some renaming σ.

Graph Rewrite Rules

Definition 2 (Rewrite Rule) A graph rewrite rule is an expression of the form L → R where L, R are graphs s.t. sort(root(L)) = sort(root(R)). A graph rewrite system (GRS for short) is a set of rewrite rules.

Our definition is close to the ones in [START_REF] Barendregt | Term Graph Rewriting[END_REF][START_REF] Echahed | Admissible graph rewriting and narrowing[END_REF]. However, L and R are not necessarily compatible: the nodes in L can be redefined (as in the rule: f (α:0) → α:s(0)). Thanks to the use of injective mappings, this definition is simpler, more condensed and much more natural than the one used in [START_REF] Echahed | A needed rewriting strategy for data-structures with pointers[END_REF]. It is also very close to term rewriting rules. In [START_REF] Echahed | A needed rewriting strategy for data-structures with pointers[END_REF], node constraints were attached to the rule and the right-hand side R was defined as a sequence of elementary actions, operating on the left-hand side L. This is needed if non injective mappings are considered because in this case the image of the right-hand side is not necessarily a graph (the same node may have two incompatible definitions, for instance if the rule f (α:a, β:a) → f (α:a, β:b) is applied on f (α:a, α)).

N (ρ) def = N (L) ∪ N (R) denotes the set of nodes occurring in ρ. CN (ρ) def = N (R) \ N (L) denotes the set of nodes occurring in R but not in L, i.e. the nodes that are created by the rewrite rule. Finally, RN (ρ) is the set of nodes α ∈ N (L) s.t. either α = root(L) or R(α) = L(α). The nodes in RN (ρ) are affected by ρ in the sense that either α is relabeled or an edge starting from α is redirected (R stands for "redirected").

A rule ρ = L → R is: • Connex iff for every node α ∈ N (L), root(L) → L α. Every node occurring in the left-hand side must be reachable from the root.

• Constructor-based iff l L (α) ∈ D ⇔ α = root(L).
The root is the only node that is labeled by a non constructor symbol. This condition is usual in constructor-based rewrite systems. • Safe iff:

• For every node α, if L(α) is defined then R(α) is defined. • root(L) does not occur in R. • If l R (α) ∈ D
then α is a created node (only the created nodes may be labeled by a defined symbol).

These last three conditions are technically convenient and obviously non restrictive. From now on, we assume that all the rules are connex, constructor-based and safe. Definition 3 Let ρ : L → R be a rule. A ρ-matcher for a graph t at a node α ∈ N (t) is a renaming σ satisfying the following conditions.

1. σ(L) ⊆ t (i.e. σ(L) must be a subgraph of t).

α = σ(root(L)).

3. If β is a node in σ(L) distinct from α, then l t (β) ∈ D.

ρ-matchers can be easily computed using standard matching algorithms for graphs. Conditions 1 and 2 are very natural: they ensure that the left-hand side of ρ matches the subgraph of t at root α. Condition 3 may seem rather restrictive but it is needed to delay the application of a rule until its left-hand side is fully known. We will come back to this problem later (see Example 1). Condition 3 does not prevent the use of lazy evaluation strategies. It merely ensures that the names of the nodes are known before applying the graph-rewrite rules, which is rather natural since the rule may depend on these names (this is not the case of term rewrite systems).

Let

ρ = L → R, we write t → ρ,σ s if s = t[σ(R)] α ,
where σ is a ρ-matcher for t at α. We write t → ρ s if t → ρ,σ s for some renaming σ and t → R s iff there exists a rule ρ ∈ R s.

i ∈ [1..n -1] t i → R t i+1 .
If s is obtained from a t by applying a rule at a node α, and if β is a node in s then β -denotes the "ancestor" of the node β:

β -def = β if β is a node in t and β -def = α otherwise.

Examples of Graph Rewrite Systems

The following rules define a function physically appending two (distinct) lists. We use the constructor cons and nil to denote lists (we also use Prolog notations: cons(

append(nil, α) → α ζ:append(α:cons(β, γ), δ) → α:cons(β, append(γ, δ))
The definition is almost identical to the usual one, except that we reuse the node α in the right-hand side of the second rule instead of creating a new node.

The following rules define an in-situ reverse function:

rev(α) → rev ′ (α, nil) rev ′ (nil, α) → α rev ′ (α:cons(β, γ), δ) → rev ′ (γ, α:cons(β, δ))
The following function replaces the leaves c, d, h in a binary tree by new constant symbols ♣, ♦, ♥ respectively. The trees are represented by g(α, β), where α, β are the two children. No stack is used and the algorithm works by redirecting the edges in the graph (so that no additional memory is needed). We use a constant symbol dummy and two constructors g ′ , g ′′ to mark the nodes in the tree s.t. the first (resp. second) child has already been handled.

inc(α) → inc ′ (α, dummy) inc ′ (α:dummy, β) → β inc ′ (α:x, β) → inc ′ (β, α:⋆) where x, ⋆ ∈ {(c, ♣), (d, ♦), (h, ♥)} inc ′ (α:g(β, γ), δ) → inc ′ (β, α:g ′ (δ, γ)) inc ′ (α:g ′ (β, γ), δ) → inc ′ (γ, α:g ′′ (δ, β)) inc ′ (α:g ′′ (β, γ), δ) → inc ′ (γ, α:g(β, δ))
Notice that if a straightforward algorithm is used then in the worst case o(n) additional nodes would be created, where n is the size of the graph. Our algorithm uses only 1 additional node (this is obvious since the only rule that contains a created node distinct from the root of the right-hand side is the first one, which applies only once).

For instance we have the derivation:

inc(g(g(c, d), h)) → inc ′ (g(g(c, d), h), dummy) → inc ′ (g(c, d), g ′ (dummy, h)) → inc ′ (c, g ′ (g ′ (dummy, h), d)) → inc ′ (g ′ (g ′ (dummy, h), d), ♣) → inc ′ (d, g ′′ (♣, g ′ (dummy, h))) → inc ′ (g ′′ (♣, g ′ (dummy, h)), ♦) → inc ′ (g ′ (dummy, h), g(♣, ♦)) → inc ′ (h, g ′′ (g(♣, ♦), dummy)) → inc ′ (g ′′ (g(aaaa, ♦), dummy), ♥) → inc ′ (dummy, g(g(♣, ♦), ♥)) → g(g(♣, ♦), ♥)
The following example shows the importance of Condition 3 in Definition 3:

Example 1 Consider the rules e(α, β) → false, e(α, α) → true, g(α) → α and the graph: t = e(γ:g(λ), δ:g(λ)). If Condition 3 is not taken into account then t is reduced to false by the first rule. However, by applying the third rule on the nodes γ and δ both the nodes γ and δ are redirected to λ, thus the second rule applies and yields true. Condition 3 avoids this behavior by preventing the application of the first rule until both α and β are labeled by constructor symbols. This condition was omitted in [START_REF] Echahed | A needed rewriting strategy for data-structures with pointers[END_REF] because it was handled by the dependency schema (it is obvious that the use of node constraints does not solve this problem).

2 Clash-Reducible Graphs

Definition

Our goal is to ensure that the normal forms of a graph do not depend on the order in which the nodes are reduced. Intuitively, the reduction ordering matters when a function affects a node γ that is used by another function, as for instance in the term f (β:length(γ: [START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF][START_REF] Barendregt | Term Graph Rewriting[END_REF]), α:rev(γ)). In this case the result of the function depends on the order in which the nodes α and β are reduced 5 . This kind of configuration (which we want to avoid) will be called a clash. In order to formally define this notion, we need to introduce some additional terminology. The constructor shape of a graph t is the graph obtained from t by removing every variable and every node labeled by a defined symbol, except the root of the graph.

Formally, it is the graph s defined as follows:

• N (s) def = {root(t)} ∪ {β ∈ N (t) | l t (β) ∈ C}. • root(s) def = root(t).
• ∀α ∈ N (s), s(α)

def = f (γ 1 , . . . , γ n ) iff t(α) = f (λ 1 , . . . , λ n ) and ∀i ∈ [1..n], γ i def = λ i if λ i ∈ N (s) and γ i def = ⊥ otherwise. Let ρ = L → R be a rule.
A renaming σ is a potential ρ-matcher for a graph t at a node α iff σ(root(L)) = α and σ(L) is compatible with the constructor shape of t| α . Intuitively, σ is a renaming that may be extended into a matcher after some rewriting steps.

We write α ⊐ ρ t β iff β occurs both in σ(L) and in the constructor shape of t| α and α ⊐ R t β iff ∃ρ ∈ R, α ⊐ ρ t β. A node γ is demanded for α w.r.t. ρ if there exists a potential ρ-matcher σ and a node β s.t. α ⊐ ρ t β and γ = i σ(L) (β). Let ρ : f (cons(α, β), α) → true and t = γ:f (cons(g(δ), λ:nil), h(δ)), where g, h denote defined functions. The constructor shape of t is γ:f (cons(⊥, λ:nil), ⊥). This graph is compatible with the left-hand side of ρ and we have γ ⊐ ρ t γ, λ. The nodes of g(δ) and h(δ) are demanded (but δ is not).

Definition 4 Let R be a GRS. A clash for a graph t is a pair of distinct nodes α, β satisfying the following conditions:

1. There exist a rule ρ = L → R in R and a ρ-matcher σ at α.

2. There exists a node γ ∈ RN (σ(ρ)) s.t.:

(a) Either β = γ and root(t)

C → t β (b) or β ⊐ R t γ. Proposition 1 Let ρ = L → R
and π = G → D be two rules, let σ be a renaming, and let t, s be two graphs s.t. t → ρ,σ s. Let α be a node in t, distinct from root(σ(L)).

If θ is a π-matcher for s at α, then one of the following conditions hold: • t contains a clash.

• root(σ(L)) is demanded for α.

• θ is a π-matcher for t and π at α.

Proof Assume that θ is not a π-matcher for t. This means that θ(L) ⊆ t. Since θ(L) ⊆ s, a node β = p t (α) where p is a position in G must be affected by ρ. Assume that p is the minimal position having this property. By definition, t and s coincide on every node q t (α) where q is a proper prefix of p. Since π is constructorbased, every node in the path from α to β, except α and β, is labeled by a constructor. Thus this path occurs in the constructor shape of t| α , and β is demanded for α. If β = root(σ(L)) then the proof is completed. Otherwise, β must occur in σ(L) thus must be labeled by a constructor symbol and in this case we have α ⊐ π t β. By Condition 2b in Definition 4 t contains a clash.

The following lemma states that two rules applicable on distinct nodes of a given graph containing no clash necessarily commute.

Lemma 1 Let t be a graph containing no clash. Let ρ = L → R, π = G → D be two rules. Let s, u be two graphs s.t. t → ρ,σ s, t → π,θ u. Assume that s, u share no nodes except those occurring in t. Let

α = σ(root(L)), β = θ(root(G)). If α = β then there exists a graph v s.t. s → π,θ v, u → ρ,σ v. Proof If RN (σ(R))∩N (θ(G)
) contains a node γ then it is easy to check that all the conditions in Definition 4 are satisfied (in particular Condition 2b) thus α, β is a clash in t.

Therefore RN (σ(R)) ∩ N (θ(G)) = N (σ(L)) ∩ RN (θ(D)) = ∅ (by symmetry).
We have θ(G) ⊆ t. Since RN (σ(R)) ∩ N (θ(G)) = ∅ no node occurring in θ(G) may be directed by σ(R) (neither globally nor locally, hence no edge in θ(G) can be redirected). Thus θ(G) ⊆ s. Since the created nodes in σ, θ are distinct, this implies that θ is a π-matcher for s. By symmetry, σ is a ρ-matcher for u.

Let α ′ , β ′ be the roots of σ(R) and θ(D) respectively. We have seen that RN (θ(D)) ∩ N (σ(L)) = ∅. This implies in particular that α ′ = β. Similarly, β ′ = α. Since the non created nodes in θ(D) (except β) are labeled by constructors, α ′ cannot occur in θ(D) and similarly, β ′ cannot occur in σ(R). This implies that α ′ = β ′ . Moreover, the graphs σ(R) and θ(D) must be compatible. Indeed, the created nodes must be mapped to distinct nodes (since s, u share no nodes other than those in s). Furthermore, since RN (σ(R))∩N (θ(G)) = N (σ(L))∩RN (θ(D)) = ∅, the nodes that are affected by σ(R) (resp. θ(L)) cannot occur in θ(G) (resp. σ(L)). Therefore the nodes that are defined both in σ(R) and θ(D) must have the same definition as in t. Thus we have:

t[σ(R)] α [θ(D)] β = (t α ′ /α ; σ(R)) β ′ /β ; θ(D) = t α ′ /α β ′ /β ; σ(R); θ(D) = t β ′ /β α ′ /α ; θ(D); σ(R) = t[θ(D)] β [σ(R)] α .
A graph t is clash-reducible (w.r.t. a GRS R) iff there exists a graph s s.t. t → * R s and s contains a clash. We now establish interesting properties of non clash-reducible graphs.

A Confluence Criterion

A GRS R is orthogonal iff it contains no pair of distinct rules L → R, G → D ∈ R (up
to a renaming of the nodes) s.t. there exists a renaming σ s.t. σ(root(L)) = σ(root(G)) and σ(L) and σ(G) are compatible.

Theorem 1 Let R be an orthogonal GRS. → R is confluent on non clash-reducible graphs.

Proof As well-known, it suffices to prove that the relation → R , restricted to non clash-reducible graphs, is strongly confluent. Let t be a graph s.t. t → R s and t → R s ′ . There exists two rules ρ and π, a ρ-matcher σ at a node α and a π-matcher θ at a node β s.t. t → ρ,σ s and t → π,θ s ′ . If α = β then we have ρ = π (since R is orthogonal). Thus s, s ′ are identical up to a renaming of created nodes. If α = β the proof follows by Lemma 1.

A Needed Reduction Strategy

We now define a demand-driven reduction strategy for non clash-reducible graphs. Let ≺ be an arbitrary chosen total ordering on positions, containing the prefix ordering. The set of demanded nodes in a graph t is the least set s.t.:

• If p is the minimal position (w.r.t. ≺) s.t. p t (root(t)) is labeled by a defined symbol then p t (root(t)) is demanded. • If α is demanded and p is the minimal position s.t. p t (α) is demanded for α then p t (α) is demanded.

We write t → n R s if s is obtained from t by applying a rule in R on a demanded node in t. Notice that this strategy is much simpler than the more general one defined in [START_REF] Echahed | A needed rewriting strategy for data-structures with pointers[END_REF] (in the sense that the set of demanded nodes is much easier to compute). Theorem 2 shows that the above strategy is normalizing for every graph t that is not clash-reducible.

We need the following results:

Lemma 2 Let R be a GRS and let ρ = L → R. If t → ρ,σ s and if α = σ(root(L)) is not demanded, then any node that is demanded in s is also demanded in t.
Proof The proof is by induction on the set of demanded nodes. Let β be a demanded node in s.

Assume that root(s) is labeled by a constructor and that β = p s (root(s)) where p is the minimal position in s s.t. p s (root(s)) is labeled by a defined symbol. By definition there exists a node β ′ s.t. root(s)

C → s β ′ and β = i s (β ′ ), for some i ∈ N. If RN (σ(ρ)) contains a node γ s.t. root(t) C
→ t γ then according to Condition 2a in Definition 4, α, γ is a clash, which is impossible (notice that γ must be distinct from α since α is labeled by a defined symbol). Thus the nodes γ s.t. root(t)

C → t γ are not affected by ρ. Since root(s) C → s β ′ this implies that root(t) C → t β ′ and that p t (root(t)) = i t (β ′ ). Moreover, if i t (β ′
) is distinct from β then this means that i t (β ′ ) must have been redirected, thus this node must be α. Let q be the minimal position s.t. q t (root(t)) is labeled by a defined symbol. Since α is not demanded, this node cannot be α hence it cannot be redirected by ρ. Furthermore, we have seen that the nodes occurring at a position lower than q cannot be affected by ρ. Thus q s (root(s)) = q t (root(t)), hence q p (by definition p is the minimal position in s s.t. p s (root(s)) is labeled by a defined symbol).

We have seen that if p t (root(t)) = β then we have α = p t (root(t)). Thus in any case p t (root(t)) is labeled by a defined symbol, hence p q and p = q. Since α is not demanded we cannot have α = p t (root(t)), therefore p t (root(t)) = β, hence β is demanded in t.

Now assume that there exists a demanded node γ in s, a rule π in R and a position p s.t. p s (γ) is demanded for γ in s w.r.t. π and β = p s (γ). By the induction hypothesis we know that γ is demanded in t. If RN (σ(ρ)) contains a node λ s.t. γ ⊐ π λ then according to Condition 2b, α, γ is a clash, which is impossible. Otherwise, we prove, by using exactly the same reasoning as above (since the node γ cannot be redirected nor created by ρ) than β is demanded for γ in t and that β = p t (γ). Thus β is demanded in t.

A value is a graph that contains no node reachable from the root and labeled by a defined symbol.

Proposition 2 Let R be a GRS and let ρ = L → R. Let s be a value. If t → ρ,σ s and if σ(root(L)) is not demanded, then t is a value.
Proof Assume that t is not a value. Then t contains a demanded node β. We have root(t)

C → t β ′ and i t (β ′ ) = β.
By the same reasoning as in the proof of Lemma 2, we prove that ρ cannot affect any node along the path from root(t) to β ′ . Thus we have root(s) C → s β ′ and i t (β ′ ) = β. Furthermore, the label of β must be a defined symbol and s cannot be a value.

Theorem 2 Let R be a GRS. Let t 1 be a graph that is not clash-reducible. If there exists a derivation

t 1 → R . . . → R t n s.t. t n is a value, then there exists a derivation s 1 → n R . . . → n R s m s.t. t 1 = s 1 and a renaming σ s.t. s m | ǫ = σ(t n | ǫ ). Moreover m ≤ n and every node that is reduced in s 1 → n R . . . → n R s m is also reduced in t 1 → R . . . → R t n .
Notice that by the previous definitions, t| ǫ denotes the graph obtained from t by removing all nodes not reachable from the root.

Proof We reason by induction on n. If n = 1 the proof is obvious. Otherwise, since t 1 is not clash-reducible, t 2 cannot be clash-reducible, thus by the induction hypothesis we may assume that

t 2 → n R . . . → n R t n . There exist ρ = L → R and σ s.t. t 1 → ρ,σ t 2 . Let α = σ(root(L)). If α is demanded then t 1 → n R t 2 thus the proof is completed.
Thus we assume that α is not demanded. If n = 2, then by definition t 2 must be a value and we get the desired result by Proposition 2. Assume that n > 2. Then there exist π = G → D and θ s.t. t 2 → π,θ t 3 . Let β = θ(root(G)). We must have β = α (since α cannot occur in t 2 ). By Lemma 2, β is demanded in t 1 . By Proposition 1, θ is a matcher for t 1 and π. By Lemma 1, we have

t 1 → π,θ t ′ 1 → ρ,σ t 3 . Thus t 1 → n R t ′ 1 → t 3 → n R . . . → n R t k .
By reapplying the induction hypothesis on the derivation from t ′ 1 to t k , we get the desired result.

We now define a class of GRS for which the previous strategy is optimal (in the sense that the selected nodes are reduced in every derivation).

If t is a graph and p is a position, we denote by t| ≺p the graph s obtained from t by removing every node α s.t. ∀q ≺ p, α = q t (root(t)). A GRS R is ≺-sequential iff for every pair of rules ρ = L → R and π = G → D in R, either L ≡ G or there exists a position p ∈ pos L (root(L)) ∩ pos G (root(G)) s.t. L| ≺p ≡ G| ≺p and L| ≺p.1 ≡ G| ≺p.1 . Checking whether a given GRS is ≺-sequential or not is straightforward. All the GRS in this paper are ≺-sequential. Every inductively/strongly sequential GRS [START_REF] Huet | Computations in orthogonal rewriting systems[END_REF][START_REF] Klop | Sequentiality in orthogonal term rewriting systems[END_REF][START_REF] Hanus | Strongly sequential and inductively sequential term rewriting systems[END_REF] and every elementary GRS [START_REF] Echahed | A needed rewriting strategy for data-structures with pointers[END_REF] are ≺-sequential.

Proposition 3 Let t be a graph and let R be a ≺-sequential GRS. There exists at most one node in t that is both demanded and reducible.

Proof We consider the definition of demanded nodes. This definition is inductive. We denote by N 0 the set of nodes that are generated by the base case and by N i the nodes that are generated from the node i-1 j=0 N j at step i. We show that for every i ∈ N, N i contains at most one element and that if the node in N i is reducible then N i+1 is empty. These properties immediately entail the desired result.

By definition N 0 contains exactly one element (since ≺ is total). Assume that N i contains only one element α. Let β, β ′ be two nodes generated at step i + 1. By definition there exist two positions p, p ′ s.t. β = p t (γ) and β ′ = p ′ t (γ ′ ) are demanded for γ and γ ′ respectively. Furthermore, we must have γ ′ = γ = α, otherwise the node β and/or β ′ would have been generated before step i + 1.

α must be labeled by a defined symbol and there exist two rules ρ = L → R, ρ ′ = L ′ → R ′ s.t. p, p ′ are the minimal positions in pos L (root(L)) and pos L ′ (root(L ′ )) s.t. p t (α), p ′ t (α) are labeled by defined symbols. Since R is ≺-sequential, we have either L ≡ L ′ or there exists a position q s.t. L| ≺q ≡ L ′ | ≺q and L| ≺q.1 ≡ L ′ | ≺q.1 . If L ≡ L ′ then p = p ′ (since the set of demanded nodes depends only on t and on the left-hand side of the rule). Otherwise, by definition since L| ≺q ≡ L ′ | ≺q then if p = p ′ we must have p, p ′ q, furthermore, since

L| ≺q.1 ≡ L ′ | ≺q.1 , we have p = p ′ = q. Thus β = β ′ .
Moreover, if α is reducible then by definition there exists a rule π = G → D that is applicable on t at α. But then either L and G are identical (up to a renaming) hence ρ is applicable (which is impossible since p is a position in pos L (root(L)) and p t (α) is labeled by a defined symbol) or L| ≺r.1 ≡ L| ≺r.1 for some position r ∈ pos L (root(L)) ∩ pos G (root(G)) which is also impossible: indeed, there exists a renaming θ s.t. θ(G) ⊆ t hence the graph t ′ obtained from t by removing every node distinct from α and not labeled by a defined symbol contains θ(G). Since σ(L) and θ(G) are not compatible, t ′ and σ(L) cannot be compatible, thus there is no potential ρ-matcher for t at α. Lemma 3 Let R be a ≺-sequential GRS. Let t be a non clash-reducible graph. If α is demanded in t and reducible, then for every derivation

t 1 → ρ1,σ1 . . . → ρn,σn t n s.t. ρ 1 , . . . , ρ n ∈ R, t 1 = t and t n is a value, there exists i ∈ [1..n] s.t. α = σ i (root(L i )), where ρ i = L i → R i .
Proof By Theorem 2, we assume that t 1 → n ρ1,σ1 . . . → n ρn,σn t n . By Proposition 3 t 1 contains only one reducible demanded node, thus α = σ 1 (root(R 1 )).

A Decidable Criterion Ensuring Clash-Irreducibility

The results in the previous section demonstrate that non clash-reducible graphs have very interesting computational properties. Therefore restricting oneself to non clash-reducible graphs is a very natural idea. Unfortunately, clash-reducibility is a semantic property: there is no algorithm to check whether a graph is clash-reducible or not (it is easy to see that this problem is undecidable). Notice that it is not sufficient to check that a graph contains no clash (which is trivially decidable): we must ensure that no clash is generated during the rewriting process. Consequently, we need to define a decidable criterion, that is strong enough to ensure non clash-reducibility but that is weak enough to capture the systems arising naturally in practical programming. This is the goal of the present section.

Our approach can be summarized as follows. In Section 3.1, we introduce a notion of potential clashes that is weaker than the notion of clashes but that has the advantage of being invariant by rewriting: if a clash appears during the reduction of a graph t between two nodes α, β in t then there must be a potential clash between α and β (or their ancestors) already in t. This is unfortunately not sufficient to dismiss every clash-reducible graph, because the rewrite rules themselves may introduce clashes. Section 3.2 imposes additional conditions to forbid rewrite rules creating new clashes. To ensure this property, we need to impose additional conditions on the form of the graphs that may occur in the left-hand side of the rule. These conditions are called shape relations, because they describe the shape of the considered data-structures. We show how to determine automatically such shape relations and how to exploit them to define conditions that are comprehensive enough to capture many rewrite systems occurring in practice but in the same time sufficiently strong to prevent the rules to prevent clashes. This is done in Section 3.3, and Section 3.4 shows the soundness of the whole algorithm.

Potential Clashes

We need to detect "potential" clashes, i.e. clashes that do not occur in the initial graph, but that are introduced by rewriting. The first step is to control the side-effects performed by the defined functions.

Approximating the Effects of a Defined Function

We associate to each function symbol f of arity [1..n] a side-effect profile which is composed by three sets

w f , in f , out f ⊆ [1.
.n] × S. These sets will be used to approximate the effects of a defined function f on the graphs on which it is applied. Intuitively, the intended interpretation of these sets is the following: • (i, s) ∈ w f iff f may affect a node α of sort s occurring in its i-th argument (by relabeling α or by redirecting some edges starting from α). • (i, s) ∈ in f iff f may access to a node α of sort s occuring in its i-th argument.

• (i, s) ∈ out f iff the value returned by f may contain a node α of sort s initially occurring in its i-th argument.

Example 2 Consider the function append defined in Section 1.3. Assume that cons and append have profile nat × list → list and list × list → list respectively. append affects it first argument but not the second, thus w append = {(1, list)}. append accesses to the first element of the first list (of sort nat), to the tail of the second list and to the second list (both of sort list), thus in append = {(1, nat), (1, list), (2, list)}. Finally, out append = {(1, nat), (2, nat), (1, list), (2, list)} (both the first argument and the second are reachable from the result). Now, consider the function copy that returns a copy of a list, defined as follows: copy(nil) → nil, copy(cons(α, β)) → cons(α, copy(β)). We have w copy = ∅ (no side-effects), in copy = {(1, list), (1, nat)} and out f = {(1, nat)} (the initial list is not reachable from the result returned by copy but its elements are).

Let inc be a function (physically) incrementing every element occurring in a list (without affecting the list itself ). Then we would have

(1, nat) ∈ w inc , but (1, list) ∈ w inc .
Finally, let length be a function computing the length of a list, defined as usual. Then we have w length = ∅ (length produces no side effect) and out length = ∅ (the result is a created node, thus no node occurring in the list occurs in the result). Furthermore, in length = {(1, list)}. Definition 6 will formalize this and will show how to compute these relations. In particular, the set out f allows one to compute from a graph t, an approximation of the graph s obtained after some reduction steps, and more precisely of the reachability relation C → s . This is the goal of the next section.

Approximating the Reachability Relation

Being able to determine in advance whether a node α will be reachable or not from a node β after some rewrite steps is essential for detecting side-effects. Consider for instance the graph t = f (rev(α), rev(id(α))) where rev is a function physically reversing its argument and id is the identity function. Is t clash-reducible? This depends on the function id. The answer is clearly "no" if id returns a copy of its argument. In this case t is not clash-reducible because the two occurrences of rev operate on (physically) distinct lists: there is no physical connection between the result of the function id and its argument, that belongs to a different data space. However if id is simply defined as id(α) → α then there exists a clash because id merely redirects the argument of the second occurrence of rev to the node α, thus the two occurrences of rev actually operate on the same node (after reducing id, the graph becomes f (rev(α), rev(α)) with an obvious clash). To approximate the reachability relation obtained after some rewrite steps we define a family of relations ⊲ Γ t (where Γ ⊆ N (t)) on the nodes in t. α ⊲ Γ t β indicates that a constructor path possibly exists from α to β after reducing the nodes in Γ. More formally: Definition 5 Let t be a graph and let Γ ⊆ N (t). We denote by ⊲ Γ t the smallest relation (implicitly parameterized by out f ) on N (t) × N (t) s.t.the following conditions hold:

• If α ∈ Γ or if l t (α) ∈ C then α ⊲ Γ t α. • β = i t (α), l t (α) ∈ C and either β ∈ Γ or l t (β) ∈ C then α ⊲ Γ t β. • If α ⊲ Γ t β and β ⊲ Γ t γ then α ⊲ Γ t γ. • If i t (α) ⊲ Γ t β, l t (α) = f ∈ Dα, (i, sort(β)) ∈ out f and α ∈ Γ then α ⊲ Γ t β.
Using an obvious fixpoint algorithm, ⊲ Γ t may be computed in time |N (t)| 5 (if out f and Γ are given). There are at most |N (t)| 2 steps (the maximal cardinality of the computed relation) and at each step we need to check every triple of nodes in the graph. ⊲ Γ t may be seen as an approximation of the relation C → s , where s denotes a graph obtained from t by reducing all the nodes in Γ (and their descendants). The "ideal" reachability relation could be obtained, from a theoretical point of view, by reducing all the nodes in Γ, but this is of course infeasible in practice. The second item in the definition handles the edges in t. The third item states that the relation is transitive, and the last item covers the case in which the reduction of a node γ ∈ Γ (labeled by a defined symbol f ) creates a constructor path from α to β. Let t = α:append(β:cons(γ:0, λ:nil), ζ:copy(δ:cons(ǫ:0, λ))). We have:

⊲ ∅ t = {(β, β), (β, γ), (β, λ), (δ, δ), (δ, ǫ), (δ, λ), (ǫ, ǫ), (γ, γ), (λ, λ)}. ⊲ {α} t = ⊲ ∅ t ∪ {(α, α), (α, β), (α, γ), (α, λ)}. ⊲ {α,ζ} t = ⊲ {α} t ∪ {(ζ, ζ), (ζ, ǫ), (α, ζ), (α, ǫ)}.
Notice that we do not have α ⊲ {α,ζ} t δ. This indicates that a function operating on t cannot access to δ (since δ is not reachable from α, after the evaluation of append and copy).

We do not have either β ⊲ {α,ζ} ǫ, which may be seem surprising, since append creates a path from β to ǫ. However, we only consider non clash-reducible graphs, thus the only functions that access to β will actually operate on α. Since we have α ⊲ {α,ζ} t ǫ, the path from α to ǫ does not need to be considered.

Automatically Computing

w f , in f , out f
We now provide an algorithm to compute automatically the side-effect profile from a given GRS. We write s ≥ s ′ iff there exists a constructor graph whose root is of sort s containing a node of sort s ′ (≥ is obviously decidable). A node α accesses to a node β in t (resp. affects a node β in t) iff α is labeled by a defined symbol f and there exists i s.t. (i, sort(β)) ∈ in f (resp. (i, sort(β)) ∈ w f ) and i t (α) ⊲ N t β where Γ = N (t) \ {α}. If f, g are two defined functions, we write (f, i) > (g, j) iff there exist an f -rule L → R, a node α ∈ N (L| i ) s.t. sort(α) ≥ s and a node β in R labeled by g s.t. j R (β) ⊲ N R α. The following definition expresses the conditions that must be satisfied by w f , in f and out f (following the informal definition in Section 3.1.1). Definition 6 A side-effect profile (w f , in f , out f ) f ∈D is adequate for a GRS R if the three following conditions hold:

• (i, s) ∈ w f if there exist an f -rule L → R ∈ R and a node α ∈ N (L| i ) s.t. α ∈ RN (ρ) and sort(α) = s. This condition corresponds to the case in which an f -rule affects a node α reachable from the i-th argument of f .

• (i, s) ∈ in f if there exists an f -rule L → R ∈ R and a node α ∈ N (L| i ) s.t. α is of sort s. • If (f, i) > s (g, j) and (j, s) ∈ w g then (i, s) ∈ w f . • If (f, i) > s (g, j) and (j, s) ∈ in g then (i, s) ∈ in f . • (i, s) ∈ out f if there exist an f -rule L → R ∈ R and a node α ∈ N (L| i ) s.t. root(R)⊲ N R α and sort(α) ≥ s.
Example 4 Let f : nat × nat → nat and g : list → nat. We consider the following GRS:

f (α:0, β) → β; α:s(0) g(cons(α, β)) → f (α, α)
The node α is affected by the first rule. Moreover, this node is reachable from the first argument of f . Thus, by the first item in Definition 6, we have (1, nat) ∈ w f . Similarly by the second item we have (1, nat) ∈ in f and (2, nat) ∈ in f . β is reachable from the root of the right-hand side of the first rule, thus (2, nat) ∈ out f .

Consider the second rule. By the first item we have (1, nat), (1, list) ∈ in g . It is easy to check that (g, 1) > nat (f, 1), (g, 1) (since g calls the function f on α, α). Thus by the third item in Definition 6, we deduce (1, nat) ∈ w g and (1, nat) ∈ w g . Finally, by the last item we have (1, nat) ∈ out g .

Notice that we have (1, list) ∈ w g ∪ out g . This means that for instance if we consider the graph α:g(β:cons(0, nil)), we know that (i) β is not affected by α and (ii) β is not reachable from the image of g.

It is easy to compute a minimal family of side-effect profiles for a given GRS, using a standard fixpoint algorithm. This algorithm runs in polynomial time w.r.t. the size of the GRS. There are at most 3×a×|S|×|D| steps, where a is the maximal arity of the function symbols. At each step one must compute the relation ⊲ N R for each rule ρ = L → R and then check that the conditions of Definition 6 are satisfied. The maximal complexity is thus 3 × n 5 × a × |S| × |D| × m, where n denotes the maximal size of the rules in R and m the maximal number of rules corresponding to the same defined function. Notice that in practice, |D|, m and |S| may be high, but n, a are usually small.

In the rest of the section, we assume that (w f , in f , out f ) is the minimal side-effect profile that is adequate for the considered GRS. ⊲ Γ t denotes the corresponding approximation of the reachability relation.

Identifying Potential Clashes

Building on the previous results, we can weaken the definition of clashes: Definition 7 A potential clash for a graph t is a pair of distinct nodes α, β satisfying the following conditions:

• α is labeled by a defined symbol f .

• There exist a node γ and i ∈ [1..ar(f )] s.t. (i, sort(γ)) ∈ w f and i t (α) ⊲ Γ t γ where Γ def = N (t) \ {α, β}.

• Either β = γ and root(t) C → t β or β is labeled by a defined symbol g and there exists j ∈ [1..ar(g)] s.t. (j, sort(γ)) ∈ in g and j t (α) ⊲ Γ t γ. A graph t is clash-free if the graph t contains no potential clash.

Intuitively, α affects the node γ and either there exists a constructor path from the root of t to γ or there exists a defined node β that accesses to γ.

For instance the graph t = β:append(α:rev(γ:[1, 2]), γ) contains a potential clash between α and β, since

1 t (α) ⊲ ∅ t γ, 2 t (β) ⊲ ∅ t γ, ( 1
, list) ∈ w rev and (2, list) ∈ in append . Notice that t contains no clash. The graph s = [1|β: [START_REF] Barendregt | Term Graph Rewriting[END_REF][START_REF] Echahed | Admissible graph rewriting and narrowing[END_REF]]; α:rev(β) also contains a potential clash, since 1 t (α) ⊲ ∅ t β and β is reachable from the root of t.

Proposition 4 Every clash is a potential clash.

Proof Assume that t contains a clash. According to Definition 4, there exists a pair of nodes α, β satisfying the following conditions:

• α = β.

• There exist a rule ρ = L → R in R and a ρ-matcher σ at α. → s γ, thus j s (δ) ⊲ ∅ s γ. Moreover, by the second item in Definition 6, we have (j, sort(γ)) ∈ in g . Therefore, the conditions of Definition 14 are satisfied and s contains a potential clash.

Describing Data-Structures by Shape Relations

Since all clashes are also potential clashes, a clash-free graph cannot contain clashes. In order to get the desired result (namely ensuring clash-irreducibility), it remains to check that the class of clash-free graphs is closed under rewriting. Unfortunately this property does not hold in general and we need to infer additional information on the shape of the reduced graphs. Consider for instance the rule: ar(α, β) → a(rev(α), rev(β)), where a denotes the usual function appending two lists (with no side effects) and rev denotes a function that physically reverses its argument. Can this rule introduce a clash in the reduced graph ? Clearly this is possible, if α, β share some nodes. For instance, the normal form of the graph ar(cons(1, α: [START_REF] Barendregt | Term Graph Rewriting[END_REF][START_REF] Echahed | Admissible graph rewriting and narrowing[END_REF]), α) depends on the order in which the two occurrences of rev are evaluated. The reader can easily check that depending on the strategy, we could obtain the lists [3, 2, 1, 2] or [2, 1, 3, 2, 1]. However, if α and β denote distinct lists, belonging to different data spaces (i.e. sharing no nodes), then there is no clash. The assertion "α and β belong to different data spaces" can be seen as a "precondition" of the defined function ar. These preconditions should be compared to the connective * in separation logic (see e.g. [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]).

We introduce some relations which allow one to restrict the form (or shape) of a graph. The idea is to specify, for every function symbol f , which are the features (or arguments) of f that can be joinable (from a programming point of view this means that they belong to the same data-space), and which are the ones that may loop to the node of f itself (this implies that there is a cycle in the graph, containing the node of f ). We assume the following relations and sets are given, for every function symbol f of arity n in Σ:

• A symmetric and reflexive relation ∼ f ⊆ [1..n] × [1..n]. • A set f ⊆ [1..n].
These relations will be used to impose additional constraints on the considered graphs. i ∼ f j indicates that the arguments i and j of the function f cannot share nodes and i ∈ f states that the argument i of f does not contain the node of f itself (i.e. if t = α:f (β 1 :t 1 , . . . , β n :t n ) then there is no path from β i to α, i.e. t i is is a proper subgraph of t). This is formalized by Definition 8. We denote by N D (t) the set of nodes reachable from a defined node in t, i.e. N D (t)

def = {α | ∃β ∈ N (t), β → t α, l t (β) ∈ D}.
Definition 8 A node α is well-formed in a graph t iff either α is a variable or α is a node labeled by f and the two following conditions hold:

• If there exists a node γ and i, j ∈ [1..ar(f )] s.t. i t (α)

C → t γ and j t (α) C → t γ then i ∼ f j. • If there exists i ∈ [1..ar(f )] s.t. i t (α) C → t α then i ∈ f . A graph t is well-formed iff every node in N D (t) is well-formed.
Assume for instance that we have

∼ f = {(1, 2), (2, 1), (1, 1), (2, 2)}.
Then f (s(0), 0, s(s(0))) or f (s(α:0), s(α), 0) are well-formed, but not f (0, s(α:0), α).

If f = {2, 3} then α:f (α, 1, 2) is not well-formed, but α:f (β:1, α, 2) is well-formed.
If the constructor symbol cons is intended to denote non looping lists (without sharing) then we should have 1 ∼ cons 2 (the first element is non joinable with the tail of the list) and 1, 2 ∈ cons (the list cannot occur in the first element nor in the tail). If the elements can be (physically) repeated, as in the list [α, α], we should have 1 ∼ cons 2. On the other hand, if the list are looping then we should have cons = {2}. If moreover, the list may occur in itself then we should have cons = {1, 2} (notice in this case cons must have the profile: list × list → list).

Although we assume in this section that these relations are given, in practice they do not need to be provided by the programmer: as explained in Section 5 they can be automatically inferred from the given GRS (by interpreting Definitions 8 and 15 as fixpoint operators on shape relations). To ensure that wellformedness is preserved by rewriting, we use the approximation of the reachability relation to strengthen the condition on the graphs: Definition 9 A node α is ⊲-well-formed in a graph t iff either α is a variable or α is a node labeled by f and the two following conditions hold:

• If there exists a node γ and i, j ∈ [1..ar(f )] s.t. i t (α) ⊲ N t γ and j t (α)

⊲ N t γ then i ∼ f j. • If there exists i ∈ [1..ar(f )] s.t. i t (α) ⊲ N t α then i ∈ f . A graph t is ⊲-well-formed iff every node in N (t) is ⊲-well-formed.
If a graph t is ⊲-well-formed, then not only it is known to be well-formed (since ⊲ N t contains C → t ) but also it is ensured that every graph s that can be derived from t is well-formed.

Proposition 5 Let t, s be two graphs. Assume that ⊲ N t contains ⊲ N s and that i t (α) = i s (α) for every node α ∈ N (s) and for every i ∈ N ∪ {l}. If t is ⊲-well-formed then so is s.

Proof This follows straightforwardly from the definition (since the condition on a node α only depend on i t (α) (where i ∈ N ∪ {l}) and on the relation

⊲ N t ).
We denote by WG (resp. WG s ) the set of ⊲-well-formed graphs (resp. of ⊲-well-formed graphs of sort s). We write s ′ ≻ s if there exists t ∈ WG s ′ and a node α of sort s s.t. root(t) → t α.

Proposition 6 There exists an algorithm to check whether WG s is empty. Furthermore, ≻ is decidable.

Proof A graph is minimal iff for every pair of nodes α, β of sort s, if α → t β then α = β. This means that along every position in the graph, one can find at most one node of each sort. By the pigeonhole argument this implies that the length of the position is bounded, thus there are finitely many minimal graphs (up to a renaming). We now show that if WG s = ∅ then WG s contains a minimal graph. This obviously ensures that the test "WG s = ∅?" is decidable: it suffices to enumerate the set of minimal graphs and check whether it contains a ⊲-well-formed one. Assume that t is a non minimal ⊲-well-formed graph. W.l.o.g. we assume that the number of nodes in t is minimal. By definition, t contains two distinct nodes α, β of the same sort s.t. α → t β. Let s = t β/α . By definition, the edges in s are either edges in t or edges from nodes γ s.t. i t (γ) = α to β. For each of those nodes we have γ

C → t α, hence γ C → t β.
Consequently, → t contains → s . Furthermore, for every node λ ∈ N (s), we have λ ∈ N (t) and l t (λ) = l s (λ). By Proposition 5, since t is ⊲-well-formed, s must be also ⊲-well-formed.

By using the same principle, we can decide whether s ≻ s ′ : it suffices to enumerate the set of minimal graphs in WG s and check for each of them whether there exists a node of sort s ′ reachable from the root.

Exploiting Shape Relations

If we assume that all the graphs occurring in a derivation are well-formed, we can infer some interesting information about the variables occurring in the left-hand side of the rules that are applied along the derivation. For instance, if we know that 1 ∼ f 2 and if the left-hand side of a rule ρ contains the term f (α, β) then α and β cannot be joinable (in particular no path can exist from β to α nor from β to α). More precisely, if σ is a ρ-matcher for a well-formed term t then since σ(f (α, β)) ⊆ t we must have by Definition 8, σ(β) ↓ t σ(α). This information allows one to discard many potential clashes. Assume for instance that ρ is of the form f (α, β) → g(h(α), h ′ (β)), where f, g, h, h ′ denote defined symbols. Assume that h physically affects its argument. α, β denotes variables that may be instantiated arbitrarily thus the nodes α and β can be joinable and there is a potential clash between h(α) and h ′ (β) in the right-hand side. Assume for instance that h physically increments its arguments and that h ′ returns true iff its argument is 0. If the GRS is applied on the term f ([β:0], β) the result can be g([s(0)], true) or g([s(0)], false) depending on the strategy. Now, assume that we know that 1 ∼ f 2. Then, since the term in the left-hand side is matched to a well-formed term, α, β cannot be joinable and the previous case can be discarded. The term f (h(α), h ′ (β)) contains no clash.

Knowing that the reduced graph is well-formed allows us to restrict the paths that may occur "outside" the left-hand side of a rule. This is important in practice because those paths are not known at the time the static analysis is performed (only the left-hand sides of the rules are known). During the static analysis, we must take into account all the possible paths, except those that are explicitly forbidden by the shape relations. In order to capture the paths that may exist in the reduced node, but outside the left-hand side, we consider expressions of the form α → β or α ↓ s β and we introduce an algorithm to check whether these expressions are compatible with a given a graph, i.e. intuitively hold in at least one extension of t.

Definition 10 We consider expressions of the form α → β or α ↓ s β, where s ∈ S. An expression φ is compatible with a graph t if there exists a ⊲-well-formed graph s containing t s.t.:

• Either φ is of the form α → β, α ∈ var(t), β ∈ N (t) and α ⊲ N s β. • Or φ is of the form α ↓ s β, α, β ∈ var(t) and there exists a node γ of sort s s.t. α ⊲ N s γ and β ⊲ N s γ. We use the approximation of the reachability relation ⊲ N s and not the reachability relation itself because this allows us to discard some paths: for instance if t = f (α, β:copy(α)) then α, β are not joinable.

The next lemma states that the previous conditions can be decided effectively.

Lemma 4 There exists an algorithm deciding, for every expression φ and for every graph t, whether φ is compatible or not with t. This algorithm runs in polynomial time w.r.t. the size of t and φ.

Proof We only provide the proof for expressions of the form α → β (the case φ = (α ↓ s β) is similar). s, s ′ be the sorts of α, β respectively. If s ≻ s ′ then by definition there is no well-formed graph s containing a path from α to β. Thus α → β cannot be compatible with t. Now assume that s ≻ s ′ . In this case, there exists a graph w and two nodes α ′ , β ′ of sort s and s ′ respectively and s.t. α ′ = root(w), α ′ → w β ′ . By using appropriate renaming we assume that α = α ′ , β = β ′ and that the nodes in w that are distinct from α, β does not occur in t. We also assume that:

• For every subgraph γ:f (w 1 , . . . , w n ) occurring in w, w 1 , . . . , w n are disjoint. Moreover if w i contains γ then it must contain β. If this property does not hold then we simply replace one of the arguments w i of f by a disjoint copy of w i . In order to ensure that β = β ′ , we cannot rename the subgraph w i that contains β, which explains the restriction in the second condition. • β ∈ var(w). This condition is obviously not restrictive (if needed it suffices to replace β by a new variable of type s ′ ). • Let α 1 , . . . , α k be the path from α to β. For every i ∈ [1..k -1] there exists j s.t. j w (α i ) = α i+1 . We assume that j ∈ g , if it is possible (i.e. if a graph satisfying this condition exists).

In order to check that the conditions of Definition 10 hold we consider the graph u def = t; w. If u is ⊲-wellformed, then α → β is compatible with t, by definition. Now assume that that there exists a ⊲-well-formed graph s containing t and s.t. α → s β. We show that u is ⊲-well-formed.

Let Λ be the set of nodes in w that are distinct from α, β. W.l.o.g. we assume that s does not contain the nodes in

Λ. Let Γ ⊆ N . ⊲ Γ s contains ⊲ Γ t ∪ {(α, β)}. Let δ ∈ Λ.
The only node λ in t s.t. δ → w λ is the node β. Thus ⊲ Γ s contains the restriction of ⊲ Γ u to the nodes in t. Assume that u is not ⊲-well-formed. Then there exists a node λ ∈ N (u) that is non ⊲-well-formed. Let g = l u (λ). By definition, one of the two following conditions holds:

1. There exist i, j ∈ [1..ar(g)] s.t. i ∼ g j and i u (λ)

≥ N u • ≤ N u j u (λ)
. By definition of w, λ cannot occur in w (since the arguments of the node in w are disjoint). Thus λ and i u (λ) both occur in t and we have i s (λ) ≥ N s • ≤ N s j s (λ) which is impossible since s is ⊲-well-formed. 2. There exists i ∈ g s.t. i u (λ) ⊲ Γ u λ. If λ does not occur in w the proof is similar to the previous one. Otherwise, by definition of w this means λ occurs along the path from α to β in w and that the path from α to β in u contains an edge labeled by i from a node labeled by a function h s.t. i ∈ h . Then this node cannot be ⊲-well-formed in s, which is impossible.

The (approximated) reachability relation ⊲ Γ

t is now extended to rewrite rules: Definition 11 For any rule ρ = L → R, ⊲ Γ ρ denotes the smallest transitive relation containing ⊲ Γ R and every pair (α, β) s.t. α → β is compatible with L.

Intuitively, α ⊲ Γ ρ β if there exists a ⊲-well-formed graph t on which ρ is applicable and such that α ⊲ Γ s β, where t → ρ s (i.e. the graph obtained from t by applying ρ and reducing the nodes in Γ may contain a constructor path from α to β). The first point captures the paths that already exist in the left-hand side or that are created by the rule and the second one handles paths that exist in the reduced graph, but outside L. Let ρ be the rule α:f (β, γ) → β. Assume that ∼ f = {(1, 1), (1, 2), (2, 1), (2, 2)} and that f = ∅. We have α ⊲ β ρ ⊲ γ ρ and γ⊲ β ρ (since both β → γ and γ → β are compatible with L) but β ⊲ α ρ (since γ, β → α are not compatible with L). ⊲ Γ ρ can be computed in polynomial time since this is the case for ⊲ Γ R and for the set of compatible inequations.

Definition 8 can be adapted to apply it on rewrite rules instead of graphs:

Definition 12 A node α occurring in a rule L → R is well-formed iff either α ∈ var(R) or l R (α) = f and the two following conditions hold:

• If there exist two nodes β, γ s.t. either β = γ or β ↓ s γ is compatible with L (for some s ∈ S), and two indices i, j ∈ [1..ar(f )] s.t. i R (α) ⊲ N ρ β and j R (α) ⊲ N ρ γ then i ∼ f j. • If there exists an index i ∈ [1..ar(f )] s.t. i R (α) ⊲ N ρ α then i ∈ f . A rule ρ is well-formed iff every node in N (R) is well-formed.

Well-defined Graphs

Definition 13 A graph is well-defined if it is both ⊲-well-formed and clash-free.

This definition is then extended to GRS by replacing the reachability relation ⊲ Γ t by the (weaker) relation ⊲ Γ

ρ . As we have seen, this is necessary to take into account the paths that may exist in the reduced graph but outside the left-hand side.

Definition 14 A potential clash for a rule ρ = L → R is a pair of distinct nodes α, β labeled by defined functions f, g respectively and satisfying the following conditions:

• There exist i, j ∈ N and γ, δ ∈ N s.t. i t (α) ⊲ Γ ρ γ, j t (β) ⊲ Γ ρ δ, where Γ def = N (t) \ {α, β}. • Either γ = δ and sort(γ) = s, or γ ↓ s δ is compatible with L. • (i, s) ∈ w f and (j, s) ∈ in g .
A graph t containing no potential clash for ρ is ρ-clash-free. Notice that every ρ-clash-free graph is also clash-free.

We now provide the most important definition, namely the condition that must be fulfilled by the GRS. We assume that D contains a special symbol ⊤ of arity 1 (not occurring in the GRS) s.t. for every sort s:

(1, s) ∈ w ⊤ ∩ in ⊤ . A sort s is restricted if there exists a function symbol f of profile s 1 × . . . × s n → s s.t. either f = [1.
.n] or i ∼ f j for some i = j. A rule ρ = α:f (L 1 , . . . , L n ) → R is shape-preserving if for every node β of sort s in RN (ρ) for every node γ of sort s ′ in α:f (L 1 , . . . , L n ) if there exists a restricted sort s ′′ s.t. s ′ ≻ s ′′ ≻ s then γ → β is not compatible with L.

Definition 15 A rule ρ = L → R is clash-free if the graph ⊤(R) is ρ-clash-free. It is well-defined if it is shape-preserving, ⊲-well-formed and clash-free.

A GRS is well-defined if every rule in it is well-defined.

⊤ is a generic function symbol intended to represent all the defined symbols operating on the root of ρ. It is not sufficient to check that R is well-formed and clash-free because clashes may appear between a defined function occurring in R and a defined function (possibly performing side-effects) "outside" L. For instance, consider the rule f (s(α)) → s(f (α)). The term s(f (α)) is obviously clash-free (since it contains only one defined node). However, if f is applied on a cyclic term then a clash can appear, e.g. the term g(f (α:s(α))) (that is clash-free) can be transformed into g(α:s(f (α))) which contains a clash since g and f operate on the same node α. In order to check that a graph or GRS is well-formed or clash-free, one has to compute the relations ⊲ Γ t and ⊲ Γ ρ . This can be done in polynomial time w.r.t. the size of t, ρ (if the relations ∼ f and f are fixed). According to Definitions 14 and 9 we do not have to compute these relations for every possible set of nodes Γ (which would be very inefficient since there are exponentially many different sets), but only for sets of the form Γ = N or Γ = N (t) \ {α, β}, where α, β are nodes in t.

Invariance

In this section we show that the class of well-defined graphs is closed by rewriting (if the rules are welldefined), which ensures that well-defined graphs cannot be clash-reducible. This shows the soundness of the static analysis as defined by the previous definitions.

We first state an important property of the relation ⊲ Γ t . In the whole section, R denotes a well-defined GRS and (w f , in f , out f ) f ∈D denotes a side-effect profile adequate for R.

Lemma 5 Let ρ = L → R be a rule in R and let t be a clash-free graph. Let σ be a ρ-matcher for t at a node α. Let s be a graph s.t. t → ρ,σ s and let β, γ ∈ N (s). Let Γ be a set of nodes in s. Assume that there exists a node λ = α labeled by a defined symbol f s.t. i t (λ) ⊲ ∅ t β, where (i, sort(β))

∈ in f . If β ⊲ Γ s γ then β ⊲ Γ ′ t γ -, where Γ ′ = Γ -∪ {α}.
Proof We reason by induction on the relations ⊲ Γ s . Let f = l t (α). • If β = γ, then we must have β ∈ Γ, hence β -= β ∈ Γ ′ and the proof is immediate.

• Assume that σ(R) contains a ⊲ Γ t -path from β to γ. If σ(L) already contains a path from β to γ then obviously this path is in t, thus β ⊲ Γ ′ t γ (the only non constructor node along this path is α). Otherwise, this means that σ(R) affects a node β ′ such that β ⊲ ∅ t β ′ . Since i t (λ) ⊲ ∅ t β, we have i t (λ) ⊲ ∅ t β ′ . Since the graph t contains no potential clash, we must have β ′ = α and α is redirected to a node γ ′ s.t. γ ′ ⊲ Γ σ(R) γ. If γ is a created node then the proof is completed. Otherwise, γ must occur in σ(L) thus there exist i s.t. i σ(L) (α) → t γ hence i t (α) ⊲ ∅ t β. By definition of out f , i ∈ out f , thus we have α ⊲ Γ ′ t γ, and the proof is completed.

• Assume that we have β ⊲ Γ s δ and δ ⊲ Γ s γ. We assume that δ is not a created node, since this case is already covered by the previous item (the path from β to δ is inside σ(R)). Then by the induction hypothesis, we have β ⊲ Γ ′ t δ and δ ⊲ Γ ′ t γ. Thus β ⊲ Γ s γ, by transitivity. We have the following:

Proposition 7 Let ρ = L → R
Γ R λ. Furthermore, if β ∈ N (R) then λ ⊲ Γ R β, otherwise there exists γ ∈ var(R) s.t. λ ⊲ Γ ρ γ and λ ⊲ Γ t β.
By transitivity of ⊲ Γ ρ , we deduce that in the former case α ⊲ Γ R β and in the latter α ⊲ Γ ρ γ. Thus the proof is completed. Now, assume that λ is not in R. In this case we may assume, w.l.o.g. that no node in the path from λ to β is in R, thus λ ⊲ Γ t β. By the induction hypothesis, there exists a node γ ∈ var(R) s.t. α ⊲ Γ ρ γ and γ ⊲ Γ t λ and by transitivity γ ⊲ Γ t β. The lemmata 6 and 7 below state that the classes of ⊲-well-formed and clash-free graphs are stable by rewriting.

Lemma 6 Let ρ = L → R be a well-formed rewrite rule and let t, s be two graphs s.t. t → ρ s. If t is well-defined then s is ⊲-well-formed.

Proof We only consider the case where t → ρ,id s (it suffices to rename the nodes in ρ). Assume that s is not ⊲-well-formed. There exists a node α in N D (s) labeled by function symbol f s.t. one of the following conditions hold:

1. Either i ∼ f j and i s (α) ≥ N s • ≤ N s j s (α). 2. Or i ∈ f and i s (α) ⊲ N s α. Since α ∈ N D (s)
, there exists a node λ, labeled by a defined symbol g, s.t. λ ≫ i s α, where (i, sort(α)) ∈ in g . Assume that λ does not occur in t, i.e. that it is a created node. This implies that there exists a variable

λ ′ in t s.t. λ ≫ i R λ ′ , λ ′ C → t α. Hence sort(λ ′ ) ≻ sort(α).
If a node α ′ occurring in a path from α is affected by ρ, then α ′ must occur in RN (ρ) and we must have α ⊲ N t α ′ , thus sort(α) ≻ sort(α ′ ). But since ρ is shape-preserving, this implies that either sort(α) is unrestricted, which contradicts the assumptions 1 and 2 above, or that λ ′ → α ′ is not compatible with R. But this last condition cannot hold since by definition λ ′ ⊲ N t α ⊲ N t α ′ and t is a ⊲-well-formed graph containing R. Now, assume that λ occurs in t. If ρ redirects an edge starting from a node in this path, then t contains a clash between α and β. Thus we have λ ≫ i t α. Let h be the label of the root L. Assume that α occurs in t. Note that we have α = β since β does not occur in s. ρ cannot redirect c s (α) for any feature c since otherwise there would be a potential clash between λ and β. We distinguish the two cases above.

1. i ∼ f j and i s (α) ≥ N s • ≤ N s j s (α). There exists a node γ s.t. i s (α) ⊲ N s γ and j s (α) ⊲ N s γ. By Lemma 5 we have i s (α) -⊲ N t γ -and j s (α) -⊲ N t γ -, i.e. (since i t (α) and j t (α) cannot be redirected): i t (α) ⊲ N t γ -and j t (α) ⊲ N t γ -. Thus t is not ⊲-well-formed, which is impossible.

2. In the second case, we have similarly a t (α) ⊲ N s α -= α, hence t is not ⊲-well-formed.

Consequently, α cannot occur in t, hence is created by ρ. Then α occurs in R, as the nodes j s (α), for every j ∈ [1..ar(f )]. Once again, we consider each case separately.

1. There exists a node γ s.t. i s (α) ⊲ N s γ and j s (α) ⊲ N s γ. By Proposition 7 we have i s (α) ⊲ Γ ρ γ ′ and j s (α) ⊲ Γ ρ γ ′′ where γ ′ , γ ′′ ⊲ N t γ. But then γ ′ ↓ sort(γ) γ ′′ is compatible with L, thus the rule is not well-formed, a contradiction.

2. If i s (α)⊲ N s α, then by Proposition 7, we have i s (α)⊲ N ρ α, hence ρ is not well-formed, which is impossible.

Lemma 7 Let ρ = L → R be a clash-free rewrite rule and let t, s be two graphs s.t. t → ρ s. If t is well-defined then s is clash-free.

Proof As usual, we assume that t → ρ,id s. We denote by λ the root of the left-end side of ρ. Assume that s contains a potential clash. There exist two nodes α = β, labeled by defined symbols f and g respectively, two natural numbers i, j and a node γ of sort s s.t

. i s (α) ⊲ Γ s γ, j s (β) ⊲ Γ s γ, where Γ = N (s) \ {α, β}, (i, s) ∈ w f , (j, s) ∈ w g .
Assume that both α and β occurs in t. Then since the nodes labeled by defined symbols cannot be redirected (and since the arguments of these nodes cannot be redirected, otherwise the graph t would contain a potential clash), we have l s (α) = l t (α) = f , l s (β) = l t (β) = g, i s (α) = i t (α) and j s (β) = j t (β). By Lemma 5 we deduce

i t (α) ⊲ Γ -∪{λ} t γ -, j t (β) ⊲ Γ -∪{λ} t γ -.
Thus t contains a clash, which is impossible. Assume that α is in t but not β. We have i t (α) ⊲ Γ -∪{λ} t γ -. Let γ ′ be the last node in the path from j s (β) to γ s.t. γ ′-occurs in L (this node necessarily exists, because b s (β) -must be in σ(L) since β is created by ρ). There exists k s.t. k t (λ) → L γ ′-(since ρ is connex). Moreover, if (j, s) ∈ in f then we must have (k, sort(γ ′-)) ∈ in lt(λ) . Consequently, there must be a clash in t between λ and α. The proof is similar if β is in t but not α.

Thus both α and β are created. By Proposition 7, there exist two nodes α

′ , β ′ ∈ var(R) s.t. α ′ ⊲ Γ t γ, β ′ ⊲ Γ t γ, α ⊲ Γ ρ α ′ , β ⊲ Γ ρ β ′ . Then α ′ ↓ sort(γ)
β ′ is compatible with L and ρ contains a potential clash which is impossible.

The next theorem states the main result of our paper.

Theorem 3 Let R be a well-defined GRS. There is no clash-reducible well-defined graph.

Proof This is an easy consequence of Theorem 1, Lemmata 6 and 7 and Proposition 4.

Examples

We provide examples of well-defined and non well-defined GRS. It is worth mentioning that every standard term rewrite system is well-defined, as well as any GRS that does not perform any side-effect. Obviously this is also the case if the "defined part" of every graph in the right-hand side has a tree structure (with non joinable leaves).

Example 5

The GRS defining the in-situ reverse in Section 1.3 is well-defined (for any family of relation ∼ f , f ). Notice that this system has a non joinable critical pair, e.g. rev ′ (α:cons(β, γ), λ); rev ′ (α, λ ′ ), where λ, λ ′ denote distinct lists (obviously this is also the case if other graph rewriting formalisms are used, e.g. algebraic approaches). This shows the interest of our analysis, which guarantees that no such graph will be generated during the rewriting process (if the initial graph is well-defined).

The graph rev(α: [START_REF] Ariola | Bisimilarity in term graph rewriting[END_REF][START_REF] Barendregt | Term Graph Rewriting[END_REF]); rev(α) is not well-defined (since the two occurrences of rev affect the same graph α). rev(rev(α)) is well-defined (since the path from the first occurrence of rev to α necessarily contains the second occurrence of rev, there is no potential clash).

Let eq be a function comparing two lists and let copy be a function returning a copy of its argument, defined as in Example 2. eq(nil, nil) → true eq(cons(α, β), cons(α, γ)) → eq(β, γ) eq(cons(α, ⊥), cons(δ, ⊥)) → false palindrom(α) → eq(α, rev(copy(α))

The above GRS is well-defined. We assume that the constructors cons, nil have the profiles nat × list → list and list, where nat denotes (for instance) natural numbers. If instead, cons has profile list × list → list, then the above GRS is not well-defined. Indeed, in the last rule the arguments of rev and eq occur in the same data space since copy(α) and α share the elements of the list. If these elements are of type nat then they cannot be affected by rev (which only affects nodes of sort list) thus there is no potential clash, but if the elements are also of sort list then a clash is possible.

Example 6

The GRS defining the function inc in Section 1.3 is well-defined for every shape relation (this is obvious since the right-hand sides of the rules contain only one defined symbol, occurring at root position). However the GRS defining the function append (more precisely the third rule) is not well-defined in general. Consider for instance the graph length(append(α:[0, 1|alpha], nil)). After one reduction step we get: length(α:[0|append([1|α], nil))). The term obviously contains a potential clash since append may affect α. If we assume that 2 ∈ cons (non looping rules are considered) and that 1 ∼ append 2 (this is necessary to ensure that the rules are shape-preserving) then the GRS becomes well-defined.

Example 7

The following rules specify an in-situ insertion sort. sort(nil) → nil sort(λ:cons(α, β)) → insert(sort(β), λ:cons(α, nil)) insert(nil, λ:cons(α, nil)) → λ insert(δ:cons(β, γ), λ:cons(α, nil)) → if α ≤ β then λ:cons(α, δ) else δ:cons(β, insert(γ, λ))

The rules for if . . . then . . . else . . . and ≤ are defined as usual. One can check that the above rules are well-defined if we have 1, 2 ∈ cons (i.e. there is no cyclic list). This GRS is not well-defined. For instance in the rule to the right, α may be reachable from δ, which entails that a potential clash exists between c ′ (in the right-hand side) and a defined function operating on α. Fortunately, one can easily specify the same function in such a way that the GRS becomes well-defined, it suffices to return the result only when the end of the list is reached, so that no other function can be applied on the list before the evaluation of c is completed: c(α) → c ′ (α, α) c ′ (α:cons(β, γ), δ) → c ′ (γ, δ) c ′ (α:cons(β, γ), γ) → γ; α:cons(β, nil)

Discussion

We have identified a syntactic class of graphs and graph rewrite systems, called well-defined, for which the normal forms do not depend on the reduction ordering among the nodes. This result (that is not covered by traditional approaches in graph rewriting) allowed us to devise very general confluence criteria and efficient evaluation strategies for the considered class of graphs. The previous property is ensured by automatically analyzing the shape of the reduced graphs as well as the side-effects performed by the defined symbols. Examples showed that well-defined systems are expressive enough to denote many algorithms useful in practical programming.

The class is parameterized by the shape relations ∼ f and f . The above results can be used in at least three ways. First, ∼ f and f can be provided by the programmer. Then it is easy to check automatically that the graphs and rules are well-defined (in polynomial time w.r.t. the size of the graphs and GRS). Alternatively, one can check for every set of rules R and for every graph t whether there exist shape relations s.t. t and R are well-defined. To this purpose, it suffices to use a fixpoint algorithm, starting with the minimal relations i ∼ f j ⇔ i = j and f = ∅ (for every function symbol f ) and weakening iteratively these relations in such a way that the conditions of Definition 15 are satisfied (until a fixpoint is reached). According to Definition 8, one can always ensure that the conditions hold by adding elements in ∼ f and f . This has the advantage that the process is fully automatic. However, the complexity of the computation is much higher (it increases by a factor n × m 2 where m is the number of features and n the number of function symbols). This may be unacceptable in practice, in particular if one has to evaluate many distinct terms t using the same GRS, since the shape relations must be recomputed for each term. Therefore, a good compromise could be to compute automatically, for a given GRS, a maximal pair of relations (∼ f , f ) such that R is well-defined. Then it is easy to check whether the terms are well-defined w.r.t. these relations. This is easy to automatize, and the advantage is that the computation is performed once and for all for a given GRS (it does not need to be computed again each time a graph is evaluated). A drawback is that there exist in general many maximal relations.

The previous results suggest that well-defined graph rewrite systems may provide a convenient highlevel framework for handling complex pointer-based data-structures and algorithms operating on them. An important aspect is how to handle "rejected" GRS, i.e. GRS that are not well-defined. In this case one should provide the programmer a clear and intuitive explanation of why the GRS is to be rejected (e.g. an example showing the ambiguity of the rewrite relation). The programmer could react either by correcting the GRS or by providing additional information (e.g. refined shape relations) ensuring that the GRS becomes well-defined. This point obviously deserves further investigations. Algorithms "compiling" non well-defined GRS into (equivalent) well-defined ones could also be defined.

Example 8

 8 The following function (physically) transforms a cyclic list into a standard one:c(α) → c ′ (α, α) c ′ (α:cons(β, γ), δ) → α; c ′ (γ, δ) c ′ (α:cons(β, γ), γ) → α:cons(β, nil)

  t. t → ρ s. As usual, → * denotes the reflexive and transitive closure of the relation →. A derivation from a graph t 1 in a GRS R is a sequence of graphs t 1 , . . . , t n s.t. for every

  We remark that according to Definition 5, the relation ⊲ ∅ t contains . Therefore we have i t (α) ⊲ ∅ t γ. Moreover, by the first item in Definition 6, we have (i, sort(γ)) ∈ w f . If β = γ and root(t) β the proof is completed. Otherwise, if β ⊐ R t γ, then there exists j s.t. j s (β)

	C

• There exist a node γ ∈ RN (σ(ρ)) s.t. either β = γ and root(t)

C → t β or β ⊐ R t γ. Since γ ∈ RN (σ(ρ)), γ occurs in σ(L). Since ρ is connex, we have i σ(L) (α) C → σ(L) γ, for some i ∈ [1..ar(f )] hence i t (α) C → t γ. C → t C → t

  be a rewrite rule and let t, s be two graphs s.t. t → ρ,id s. If α ⊲ Γ s β where α is a node in R then:• Either β is a node in R and α ⊲ Γ R β. • Or β ∈ N (R) and there exists a node γ ∈ var(R) s.t. α ⊲ Γ ρ γ and γ ⊲ Γ t β.Proof The proof is by induction of ⊲ Γ R . Assume that β = i s (α). If β is not in R then the edge from α to β necessarily occurs in t, furthermore α, β cannot be relabeled, thus α ⊲ Γ t β. Assume that α ⊲ Γ s λ ⊲ Γ s β. Assume that λ occurs in R. By the induction hypothesis, we deduce that α ⊲

This (obviously decidable) condition is not sufficient in general.

Defining efficient narrowing algorithms handling node ordering is a very difficult problem.

In this paper we only consider injective mappings in contrast to what is done in[START_REF] Echahed | Non Strict Confluent Rewrite Systems for Data-Structures with Pointers[END_REF][START_REF] Echahed | A needed rewriting strategy for data-structures with pointers[END_REF] in which explicit equational constraints were attached to the graphs. The use of injective mappings is very convenient from a theoretical point of view and is well-known to be non restrictive, although it should be avoided in practice because it may exponentially increase the size of the graphs.

After the execution of rev, γ becomes the last cell of the list.