Hubert Comon
email: hubert.comon@lsv.ens-cachan.fr

Florent Jacquemard
email: florent.jacquemard@inria.fr

Ground Reducibility is EXPTIME-complete

We prove that ground reducibility is EXPTIME-complete in the general case. EXP-TIME-hardness is proved by encoding the emptiness problem for the intersection of recognizable tree languages. It is more difficult to show that ground reducibility belongs to DEXPTIME. We associate first an automaton with disequality constraints AR,t to a rewrite system R and a term t. This automaton is deterministic and accepts at least one term iff t is not ground reducible by R. The number of states of AR,t is O(2 R t ) and the size of its constraints is polynomial in the size of R, t. Then we prove some new pumping lemmas, using a total ordering on the computations of the automaton. Thanks to these lemmas, we can show that emptiness for an automaton with disequality constraints can be decided in a time which is polynomial in the number of states and exponential in the size of the constraints. Altogether, we get a simply exponential time deterministic algorithm for ground reducibility decision.

Introduction

Ground reducibility of a term t w.r.t. a term rewriting system R expresses that all ground instances (instances without variables) of t are reducible by R. This property is fundamental in automating inductive proofs in equational theories without constructors [START_REF] Jouannaud | Automatic proofs by induction in theories without constructors[END_REF]. It is also related to sufficient completeness in algebraic specifications (see e.g. [START_REF] Kapur | On sufficient completeness and related properties of term rewriting systems[END_REF]). Roughly, it expresses that all cases have been covered by R and that t will be reducible for any inputs. Many papers have been devoted to decision of ground reducibility. Let us report a brief history of the milestones, starting only in 1985 with the general case.

Ground reducibility was first shown decidable by D. Plaisted [START_REF] Plaisted | Semantic confluence tests and completion methods[END_REF]. The algorithm is however quite complex: a tower of 9 exponentials though there is no explicit complexity analysis in the paper. D. Kapur et al. [START_REF] Kapur | On sufficient completeness and related properties of term rewriting systems[END_REF] gave another decidability proof which is conceptually simpler, though still very complicated, and whose complexity is a tower of 7 exponentials in the size of R, t. More precisely, they show that checking the reducibility of all ground instances of t can be reduced to checking the reducibility of all ground instances of t of depth smaller than N (R) where N (R) is a tower of 5 exponentials in the size of R. A third proof was proposed by E. Kounalis [START_REF] Kounalis | Testing for the ground (co)-reducibility in term rewriting systems[END_REF]. The result is generalized to co-ground reducibility and the expected complexity is 5 exponentials, though there is no explicit complexity analysis in the paper. These three algorithms use combinatorial arguments and some "pumping property": if there is a deep enough irreducible instance of t, then there is also a smaller instance which is also irreducible. This yielded the idea of making explicit the pumping argument as a pumping lemma in some tree language. In support of this idea, when both t and the left members of R are linear, i.e. each variable appears only once, then the set of reducible instances of t is accepted by a finite tree automaton [START_REF] Gallier | Reductions in tree replacement systems[END_REF]. Hence the set of irreducible ground instances is also accepted by a tree automaton, by complement. This easily gives a simply exponential algorithm in the linear case. (As we will see this algorithm is optimal). H. Comon expressed first the problem of ground reducibility as an emptiness problem for some tree language [START_REF] Comon | An effective method for handling initial algebras[END_REF]. He also gave a decision proof whose complexity is even worse than the former ones. A.-C Caron, J.-L. Coquid and M. Dauchet [2,[START_REF] Dauchet | Automata for reduction properties solving[END_REF] proved a very beautiful result in 1993, enlighting the pumping properties and their difficulty. They actually show a more general result: the first-order theory of unary encompassment predicates is decidable. And it turns out that ground reducibility can be expressed as a simple formula in this logic. Their technique consists in associating an automaton with each formula, in the spirit of Buchi's and Rabin's method. The kind of automata which is appropriate here is what they call reduction automata, a particular case of automata with constraints introduced by M. Dauchet in 1981. Such tree automata have the ability to check for equality or disequality of some subtrees before applying a transition rule. In general, emptiness of languages recognized by such automata is undecidable. However, when we only allow a fixed number of equality tests on each computation branch, then emptiness becomes decidable. Unfortunately, their result does not give any information about possible efficient algorithms. The complexity which results from their proof is not better than Plaisted's bound. We tried to specialize the tree automata technique for ground reducibility and we got in this way a triple exponential bound [4]. This is better than previous methods, but still far from the lower bound.

The problem in all works about ground reducibility is that they give a bound on the depth of a minimal irreducible instance of t (or a minimal term accepted by the automaton). However, after establishing carefully such an upper bound, they use a brute-force algorithm, checking the reducibility of all terms of depth smaller than the bound, which increases the complexity by a double exponential.

We use here a different approach. We still rely on automata with disequality constraints. However, we do not try to give a bound on the depth of an accepted term. Rather, we show a stronger result: with an appropriate notion of minimality, a minimal term accepted by the automaton contains at most an exponential number of distinct subterms. To prove this, we use a generalization of pumping to arbitrary replacements for which the term is decreasing according to some well chosen well founded ordering. With a few more ingredients, this yields an algorithm for deciding the emptiness of an automaton with disequality constraints which runs in polynomial time w.r.t. the number of states and in exponential time w.r.t. the size of the constraints. On the other hand, we show that ground reducibility of t w.r.t. R can be reduced to the emptiness problem for an automaton A with disequality constraints whose number of states is an exponential in the size of R and t and whose constraints are polynomial in size. Altogether, we have a simply exponential algorithm for ground reducibility.

This result is optimal since ground reducibility is EXPTIME-hard, already for linear rewrite systems and linear t. A O(2 n log n ) lower bound was proved by Kapur et al [START_REF] Kapur | Sufficient completeness, ground reducibility and their complexity[END_REF]. We give here a simple proof of EXPTIME-hardness. It is known that the emptiness problem for the intersection of n recognizable languages is EXPTIME-complete, see [START_REF] Frühwirth | Logic programs as types for logic programs[END_REF][START_REF] Seidl | Haskell overloading is dexptime-complete[END_REF]. We show here that this problem is reducible to ground reducibility in polynomial time.

In section 2, we recall the definition of automata with disequality constraints. In section 3, we show how to construct an automaton with disequality constraints whose emptiness is equivalent to the ground reducibility of t w.r.t. R and we analyze carefully the complexity of such a construction, and the size of the automaton. Section 4 is devoted to to pumping lemmas for automata with disequality constraints. These lemmas are applied in section 5 to derive an optimal algorithm which checks the emptiness of the (language recognized by) an automaton with disequality constraints. Finally, we study the lower bound of ground reducibility in section 6.

Automata with disequality constraints

F will always be a fixed finite set of function symbols (together with their arity), and X a set of variables. The set of terms built on F is written T (F, X ) and its subset of ground terms is written T (F). A position is a string of positive integers. The concatenation of two positions p and p is denoted pp and Λ is the empty string. The length of a string p is |p|. Positions are ordered according the prefix ordering: p ≺ p iff there is a string p such that pp = p . The position p, p are called parallel, p p , iff p p and p p. As usual, a finite term t can be viewed as a mapping from its set of positions We assume the reader familiar with (constrained) term rewriting systems (see [START_REF] Dershowitz | Rewrite systems[END_REF] for a survey). Let us only recall that a term t is ground reducible by a rewrite system R iff all the ground instances of t are reducible by R. The rewriting relation associated to a rewrite system R is denoted -→ R and its reflexive transitive closure is denoted -→ * R . A term t is ground reducible by a rewrite system R iff all the ground instances of t are reducible by R.

Pos(t) into F. For instance, if t = f (g(a), b), Pos(t) = {Λ,
We use the subsumption quasi-ordering on terms: s • t if there is a substitution σ such that sσ = t. Two terms are similar if s • t and t • s. The set of variables occurring in a term t is denoted Var (t). Finally, the size of a term t, which is denoted by t , is the cardinal |Pos(t)| of its positions set, and the size of a rewrite system R, which is denoted R , is the sum of the sizes of its left members1 . Definition 1. An automaton with disequality constraints (or ADC for short) is a tuple (Q, Q f , ∆) where Q is a finite set of states, Q f is the subset of Q of final states and ∆ is a finite set of transition rules of the form: f (q 1 , . . . , q n ) -→ c q where f ∈ F has arity n, q 1 , . . . , q n , q ∈ Q and c is a boolean combination without negation of constraints π = π where π, π are positions.

The empty conjunction is written . The state q is called target state of the rule f (q 1 , . . . , q n ) -→ c q. A ground term t ∈ T (F) satisfies a constraint π = π (which we write t |= π = π ) if both π and π are positions of t and t| π = t| π . This notion of satisfaction is extended to conjunctions and disjunctions as expected. (In particular t |= for every t).

Definition 2. A run of the automaton

A = (Q, Q f , ∆) on a term t is a mapping ρ from P os(t) into ∆ such that, for every p ∈ P os(t), if t(p) = f with arity n then ρ(p) is a rule f (q 1 , . . . , q n ) -→ c q and 1. for every 1 ≤ i ≤ n, ρ(p • i) is a rule whose target is q i 2. t| p |= c.
If only the first condition is met by ρ, ρ will be called a weak run.

Runs of A can also be seen as ground terms over the alphabet ∆ (terms of T (∆)), the arity of a "symbol" f (q 1 , . . . , q n ) -→ c q in ∆ being n, the arity of the symbol f in F.

A term t ∈ T (F) is accepted by A. there is a run ρ of A on t such that ρ(Λ) is a rule whose target is a final state of Q f . In this case, ρ is called an accepting run. The language L(A) of A is the subset of T (F) of its accepted terms. Equivalently, L(A) is the set of all terms t ∈ T (F) which can be reduced to a final state q ∈ Q f by the constrained rewrite system ∆:

L(A) = {t ∈ T (F) | ∃q ∈ Q f , t-→ *
∆ q} A regular language is a language of some standard tree automata, i.e. of an ADC all the constraints of which are .

Example 1. Let F = {f, a, b} and Q = {q} = Q f , ∆ = {r 1 : a → q r 2 : b → q r 3 : f (q, q) --→ 1 =2 q}.
This defines an automaton (which accepts the terms irreducible by the rule f (x, x) → a). The term f (a, b) is accepted since ρ = r 3 (r 1 , r 2 ) is a run on t such that r 3 yields a final state. The term f (a, a) is not accepted by A: there is a weak run r 3 (r 1 , r 1 ) on f (a, a) but the disequality of r 3 is not satisfied.

Note that in general ADC can be non-deterministic (more than one run on a term) or not completely specified (no run on some term). However, given a run ρ, there is a unique term [ρ] ∈ T (F) associated to ρ.

Definition 3. Let

A = (Q, Q f , ∆
) be an ADC and ρ a weak run of A on t. An equality of ρ is a triple of positions (p, π, π ) such that p, pπ, pπ ∈ P os(t), π = π is in the constraint of ρ(p) and t| pπ = t| pπ .

In particular, a weak run without any equality is a run. The equalities in a run are also classified according to a particular position p 0 ∈ P os(t):

-(p, π, π ) is close to p 0 iff p p 0 ≺ pπ or p p 0 ≺ pπ -(p, π, π ) is far (or remote) from p 0 if pπ p 0 or pπ p 0
These two possible situations are depicted in figure 1.

Reducing ground reducibility to an emptiness problem for ADC

In this section, we show how to construct an ADC whose emptiness is equivalent to the ground reducibility problem and we show precisely the size of such an automaton. We start with an ADC accepting the set of irreducible ground terms (normal forms).

Normal forms ADC

Let L be the set of left hand sides of a given rewrite system R. Let L 1 be the subset of the linear terms in L, let L 2 be its complement in L and let L 3 be the set of linearized versions of terms in L 2 (i.e. terms obtained by replacing in some t ∈ L 2 each occurrence of a variable by a new variable, yielding a linear term). The initial set of states Q 0 consists in all strict subterms of elements in L 1 ∪ L 3 plus two special states: a single variable x which will accept all terms, and q r which will accept only reducible terms of R (hence is a failure state). We assume that all terms are considered up to variable renaming (in particular any two terms are assumed to share no variables in what follows).

The set of states Q NF(R) of the normal forms automaton consists in all unifiable subsets of Q 0 \ {q r } plus the state q r . Each element of Q NF(R) is denoted q u where u is the most general unifier (mgu) of the state -if it is not the special symbol "r".

The transition rules set, denoted ∆ NF(R) , is the set of rules of the form:

f (q u 1 , . . . , q un ) -→ c q u with:

1. if one of the q u i 's is q r or if f (u 1 , . . . , u n ) is an instance of some s ∈ L 1 , then q u = q r and c = 2. if f (u 1 , . . . , u n ) is not an instance of any term in L 1 , then u is the mgu of all terms v ∈ Q 0 \ {q r } (including the variable x) such that f (u 1 , . . . , u n ) is an instance of v 3. when q u = q r , the constraint c is defined by:

∈L 2 u, are unifiable x is a var. of |π= | π =x π ≡π (π = π )
Note that the unifier in the second condition always exists because one of the states of Q 0 is q x , x ∈ X . The final states of the normal forms automaton are all states, except q r .

Q f NF(R) := Q NF(R) \ {q r }
The normal forms automaton A NF(R) is defined by the above constructed sets:

A NF(R) := (Q NF(R) , Q f NF(R) , ∆ NF(R) )
This automaton A NF(R) is not necessary complete (the automaton may have no run on terms that are reducible by a non-left linear rule). It is however deterministic.

Example 2. The normal forms automaton A in Example 1 is the normal form automaton A NF(R) where R = {f (x, x) → a}. Note that A is indeed deterministic but that there exists no run of A on e.g. the reducible term f (a, a). Proposition 1. The automaton A NF(R) accepts the set of terms of T (F) that are irreducible by R. Its number of states is an exponential in the size of R. Each constraint occurring in a rule of A NF(R) has a size bounded by O( R 3 ).

Proof. The constraints in the rules of ∆ NF(R) are conjunctions of disjunctions of disequality atoms. The size of each of these constraints can be bounded according to the respective sizes of conjunctions, disjunctions and atoms.

# of ∧ # of ∨ size ≤ ∈L 2 π,π ∈Pos( ) (|π| + |π |) ≤ →r∈R π∈Pos( ) |π| + π ∈Pos ( ) |π | ≤ →r∈R π∈Pos( ) (|π| + 2 ) ≤ →r∈R ( 3 + 2 ) ≤ R 3
Concerning the number of states, if is sufficient to remark that it is of the same magnitude as the cardinal of the closure of Q 0 \ {q r } by mgu. We prove the first part of Proposition 1 in the two following paragraphs.

Correctness. Lemmas 1 and 2 show that A NF(R) recognises normal forms of R only.

Lemma 1. Let s ∈ T (F). If s -----→ * ∆ NF(R) q u for some q u ∈ Q f NF(R) , then s is an instance of u and u = sup{v | q v ∈ Q NF(R) and s is an instance of v} (sup is considered w.r.t. • ).

Proof. By induction on the length of the derivation s

-----→ * ∆ NF(R) q u . Lemma 2. Let s ∈ T (F). If s -----→ * ∆ NF(R) q u for some q u ∈ Q f NF(R) , then s is a normal form of R.
Proof. By induction on the length of the derivation s -----→ * ∆ NF(R) q u . If the length is 1, s is a constant of F. In that case there exists a rule s → q u ∈ ∆ NF(R) and thus s / ∈ L 1 by the first construction condition, which means that s is a normal form. Assume s -----→ * ∆ NF(R)

f (q u 1 , . . . , q un ) -→ c q u ∈ Q f NF(R) , and let s = f (s 1 , . . . , s n ). For each 1 ≤ i ≤ n, we have s i -----→ * ∆ NF(R)
q u i and q u i = q r by the first condition of the construction. Thus each s i is a normal form by induction hypothesis. Assume now that s is reducible by R. This means that it must be an instance of some term in L, say f (l 1 , . . . , l n ). We have two cases for f (l 1 , . . . , l n ):

1. if f (l 1 , . . . , l n ) ∈ L 1 , for each 1 ≤ i ≤ n, s i is an instance of l i . By Lemma 1, this implies that for each 1 ≤ i ≤ n, u i is also an instance of l i , thus f (u 1 , . . . , u n ) is an instance of f (l 1 , . . . , l n ) ∈ L 1
which contradicts the existence of the rule f (q u 1 , . . . , q un ) -→ c q u (q u = q r ) in ∆ NF(R) , by the first construction condition 2. if f (l 1 , . . . , l n ) ∈ L 2 , s is an instance of f (l 1 , . . . , l n ) = l iff s is an instance of the linearised version of l, and, for every distinct positions π, π of l such that l| π ≡ l| π , we have s| π ≡ s| π . This last condition implies s |= ¬c by construction of c. Hence s |= c, which of course contradicts the application of the rule f (q u 1 , . . . , q un ) -→ c q u in the last step of the derivation s -----→ * ∆ NF(R)

q u .
(end of proof of Lemma 2)

Completeness. A NF(R) recognises every ground normal forms of R.

Lemma 3. Let s be a term of T (F) which is a normal form of R. There exists

q u ∈ Q f NF(R) such that s -----→ * ∆ NF(R)
q u and s is an instance of u.

Proof. By induction on s.

If s is a constant, then it is not (an instance of) any term in L 1 thus we have s → q x ∈ ∆ NF(R) by construction.

For the induction step, let s = f (s 1 , . . . , s n ). The subterms s 1 , . . . , s n are normal forms of R.

Thus by induction hypothesis, we have states q u 1 , . . . ,

q un ∈ Q f NF(R) = Q NF(R) \{q r } such that s i -----→ * ∆ NF(R)
q u i and s i is an instance of u i for all i ≤ n. Thus s is an instance of f (u 1 , . . . , u n ).

We proceed by contradiction. Assume that no rule in ∆ NF(R) with a target in Q f NF(R) is applicable to f (q u 1 , . . . , q un ). Then we are in one of the following cases.

One of the q u

i 's is q r or f (u 1 , . . . , u n ) is an instance of some term in L 1 (first condition in the construction of ∆ NF(R)
). This would contradict respectively the induction hypothesis and the irreducibility of s by Lemma 1. 2. There exists f (q u 1 , . . . , q un ) -→ c q u in ∆ NF(R) for some c and t = r but s |= c. This contradicts the irreducibility of s again, by construction of the constraint c.

Hence, there exists a term u, such that s -----→ * ∆ NF(R)

q u . Moreover, by construction, u is the most general unifier of the terms v ∈ Q 0 \ {q r } such that f (u 1 , . . . , u n ) is an instance of v. Thus s is an instance of u.
(end of proof of Proposition 1)

Ground reducibility and ADC

If t is a linear term, then its ground reducibility is equivalent to the emptiness of the intersection of L(A NF(R) ) with the (regular) set of instances of t. Since the class ADC is closed by intersection with a regular language (it can be computed in time the product of the sizes of both automata), deciding ground reducibility amounts to decide emptiness of an ADC whose number of states is O(2 R × t ) and constraints have a size O( R 3 ).

It is a bit more difficult when t is not linear since, in such a situation, the set of irreducible instances of t is not necessarily recognized by an ADC. For this reason, we have to compute directly an automaton whose language is empty iff t is ground reducible by R. This ADC is denoted:

A NF(R),t = (Q NF(R),t , Q f NF(R),t , ∆ NF(R),t )
We start with the above normal forms ADC constructed in section 3.1:

A NF(R) := (Q NF(R) , Q f NF(R) , ∆ NF(R) ). Let S t = {tσ| p | p ∈ Pos(t)}
where σ ranges over substitutions whose domain is the set of of variables occurring at least twice in t into Q f NF(R) . The cardinal of S t is thus exponential in the size t of t.

1. Q NF(R),t := S t × Q NF(R) 2. the final states set Q f NF(R),t := {[u, q] | q ∈ Q NF(R) , u is an instance of t} 3. For all f (q 1 , . . . , q n ) -→ c q n+1 ∈ ∆ NF(R) and all u 1 , . . . , u n ∈ S t , ∆ NF(R),t contains the fol- lowing rules: (a) f ([u 1 , q 1 ], . . . , [u n , q n ]) --→ c∧c [f (u 1 , . . . , u n ), q n+1 ] if f (u 1 , . . . , u n ) is an instance of t and c is defined below. (b) f ([u 1 , q 1 ], . . . , [u n , q n ]) -→ c [f (u 1 , . . . , u n ), q n+1 ] if [f (u 1 , . . . , u n ), q n+1 ] ∈ Q NF(R)
,t and we are not in the first case.

(c) f ([u 1 , q 1 ], . . . , [u n , q n ]) -→ c [q n+1 , q n+1 ] in all other cases. Remark that [q n+1 , q n+1 ] is indeed one of the states of Q NF(R),t
The constraint c is constructed in three steps.

Lifting. First, all disequality constraints which are checked "in the t part" of f (u 1 , . . . , u n ) = tσ, are "lifted" to the root position; this is explained in the following construction. From f (u 1 , . . . , u n ) we can retrieve the rules of A NF (R) which are applied at any position p ∈ Pos(t) in a run on f (u 1 , . . . , u n ) (A NF (R) is deterministic). Let c p be the constraint of the rule applied at position p. We write p • c the constraint defined by induction on c as below and let c 1 be

p∈Pos(t) p • c p . p • := , p • ⊥ := ⊥ p • (c 1 ∧ c 2 ) := p • c 1 ∧ p • c 2 p • (π = π ) := pπ = pπ p • (c 1 ∨ c 2 ) := p • c 1 ∨ p • c 2
Extension. The second step consists in ensuring that all disequality constraints are "deep enough", i.e. below the positions of t: for each constraint p = p in c 1 , such that p or p is a strict prefix of some position of t, we apply the following rule. We get then a constraint c 2 .

p = p → pπ ∈ Posl (t) ∧ p π / ∈ Pos (t) or p π ∈ Posl (t) ∧ pπ / ∈ Pos (t) pπ = p π
Variables. After this preparation, we take into account non-linearities of t: they imply equality constraints at the root, hence, by equational deduction, new disequality constraints can be inferred: We let c be the constraints obtained by saturation of c 2 using the following deduction rule for each distinct positions p 1 and p 2 in Pos(t) such that t| p 1 ≡ t| p 2 is a variable:

p 1 π = p p 2 π = p Example 3. Let F = {f, a, b}, t = f (x, f (x, y)) and R = f (x, x) → a}. The automaton A NF(R) is (see Examples 1 and 2): A NF(R) = {q}, {q}, {a → q; b → q; f (q, q) --→ 1 =2 q}
Then the automaton A NF(R),t will contain additionally the rule f ([q q , q], [q f (q,q) , q]) ------→ 1 =2∧1 =22 q.

Proposition 2. The term t is ground reducible by R iff the language accepted by A NF(R),t is empty. The number of states of this automaton is O(2 c× t × R ) where c is a constant. The global size of the constraints of transition rules is O(

t 4 × R 3 ).
Moreover, the number of rules of the automaton is O(2 c× t × R ×α × |F|) where α is the maximal arity of a function symbol of F and |F| is the number of function symbols.

Proof. To bound |Q NF(R),t |, let us recall that Q NF(R),t := S t × Q NF(R) , and that |Q NF(R) | = 2 d× R where d is a constraint. Moreover by construction, |S t | ≤ |Q f NF(R) | t = O(2 d× R × t ) which give upper bound O(2 c× t × R ) for the number of states of A NF(R),t .
The constraints in the rules of ∆ NF(R),t are constraints of ∆ NF(R) or are conjunction of such constraints and a c constructed as above. The c 's are conjunctions of disjunctions of conjunctions of disequality atoms and there size after each construction step is bounded below.

Lifting.

p∈Pos(t) →r∈R π,π ∈Pos( ) (|π| + |π | + 2|p|)
Extension.

p∈Pos(t) →r∈R π,π ∈Pos( ) p ∈Pos(t) (|π| + |π | + 2 t ) Variables. t × →r∈R π,π ∈Pos( ) t × 2 t × (|π| + |π | + 2 t ) ≤ 2 t 3 × →r∈R π,π ∈Pos ( ) (|π| + |π | + 2 t ) ≤ 2 t 3 × R 3 + 2 t 3 × 2 t × R 2 ≤ 2 t 3 × R 3 + 4 t 4 × R 2
The if direction of the first part of Proposition 2 follows from the following lemma.

Lemma 4. Every ground instance of t which is irreducible by R is accepted by

A NF(R),t
Proof. Let τ be a substitution from the set of variables of t to the ground terms of T (F) such that tτ is irreducible by

R. t ∈ L(A NF(R),t
) is a consequence of the following fact, proved by multiset induction.

Lemma 5. Let τ be a substitution such that tτ is ground and irreducible by R. For all multiset {{u 1 , . . . , u m }} of subterms of t, there exists: a substitution σ from the variables of t to Q NF(R) and final states

q f 1 , . . . , q f m ∈ Q f NF(R) such that for all 1 ≤ i ≤ m, u i τ is reduced by ∆ R,t into the state [u i σ, q f i ].
Note that the substitution σ is the same for every u i .

Proof. Let {{x 1 , . . . , x m }} be a multiset of variables of t. By hypothesis, for all 1

≤ i ≤ m, x i τ is a normal form of R. Thus, x i τ ∈ L(A NF(R)
) by Proposition 1. This means that there exists final states

q f 1 , . . . , q f m ∈ Q f NF(R) such that for each i ≤ m, x i τ -----→ * ∆ NF(R) q f i Thus each x i τ is reduced by ∆ NF(R),t into the state [q f i , q f i ]. We can moreover assume that for all 1 ≤ i 1 , i 2 ≤ m such that x i 1 = x i 2 , we have q f i 1 = q f i 2 .
This give the substitution σ from {x 1 , . . . , x m } to {q f 1 , . . . , q f m }. Let {{u 1 , . . . , u m }} be a multiset of subterms of t, such that one u j (1 ≤ j ≤ m) at least is not a variable. We let u j = f (v 1 , . . . , v n ). By induction hypothesis for the multiset:

{{u 1 , . . . , u j-1 , v 1 , . . . , v n , u j+1 , . . . , u m }} there exists final states q f 1 , . . . , q f m+n-1 ∈ Q f NF(R)
and a substitution τ from the set of variable of t to Q NF(R) such that for all 1 ≤ i < j and all j < i ≤ m, u i τ is reduced by A NF(R),t into the state [u i σ, q f i ]. Moreover, by hypothesis, u j τ is irreducible by R, thus accepted by A NF(R) which is deterministic (see Proposition 1). Thus, ∆ NF(R) contains a transition rule of the form: f (q f j , . . . , q f j+n-1 ) -→ c q f with q f ∈ Q f NF(R) and u j τ |= c. And ∆ NF(R),t contains a transition rule:

f ([v 1 σ, q f j ], . . . , [v n σ, q f j+n-1 ]) -→ c [f (v 1 , . . . , v n )σ, q f ] where c = c ∧ c if f (v 1 , . . . , v n )σ is an instance of t and c = c otherwise.
This gives the final states: q f 1 , . . . , q f i-1 , q f , q f i+1 , . . . , q f m and the substitution σ we wanted for the multiset {{u 1 , . . . , u i-1 , u i , u i+1 , . . . , u m }} The only if direction of the first part of Proposition 2 is now proved with the help of three intermediate lemmas. The automaton A NF(R),t does not recognise only irreducible ground instances of t. However, we are going to show that if u is accepted then we can construct a term u which is an irreducible instance of t and which is still accepted (u is thus a witness for non ground reducibility of t by R).

Lemma 6. Each term of L(A

NF(R),t ) is a normal form of R.
Proof. By construction, if we transform A NF(R) with a projection on the first component of the states of Q NF(R),t , we obtain exactly the normal form ADC A NF(R) of Proposition 1.

Lemma 7. Each term of L(A NF(R),t ) is a ground instance of the linearised version of t.

Proof. We may show by induction the more general fact that each term of T (F) recognized by A NF(R),t in the state [uσ, q] ∈ Q NF(R),t (uσ ∈ S t and u = t| p for some p ∈ Pos(t)) is a ground instance of the linearised version of u, by induction on u.

(p ) = q ∈ Q NF(R) , then the target state of ρ(pp ) is [q , q ].
Proof. by induction on ρ. Now, we can terminate the proof of the only if direction of the first part of Proposition 2. Assume we have s ∈ L(A NF(R),t ). Let ρ be a run of A NF(R),t on this s. By Lemma 7, s is a ground instance of the linearised version of t. It could happen though that s is a actually not an instance of t itself, because we have in s two distinct subterms at positions p 1 , p 2 ∈ Pos(t) corresponding to the same variable in t (t(p 1 ) = t(p 2 ) ∈ X ). The idea is then to construct s , a ground instance of t by replacing s| p 1 with s| p 2 in s. Lets associate to each variable x ∈ Var (t) the set occ t (x) of positions of x in t,

occ t (x) := {p ∈ Pos(t) | t(p) = x}
And let [tσ, q] be the (final) target state of ρ(Λ). For each variable x in t, we note q x := xσ, which is by construction a state of Q NF(R) . From Lemma 8, for each p ∈ occ t (x), the target state of ρ(p) is [q x , q x ].

We then construct a weak run ρ as follows: for each x ∈ Var (t), if |occ t (x)| ≥ 1, we choose p ∈ occ t (x) and do the replacement ρ[ρ| p ] p for all other p ∈ occ t (x) \ {p}. To show that ρ is indeed a run of A NF(R),t , we have to check that the constraints in ρ are still valid after the replacements, in other words, that ρ contains no equalities. This follows from the fact that the constraint of ρ(Λ) is satisfied by s, in particular the subconstraint c constructed as above. We shall first remark that c contains every constraints which are valid in ρ and may not be valid in ρ , because of the first part, lifting, of the construction of c . There are only two kind of equalities which may occur in ρ (see Lemma 9 in section 4):

1. (p, π, π ) such that there is α such that pπα ∈ occ t (x) for some variable x, we performed the replacement ρ[ρ| pπα ] β (for some other β ∈ occ t (x)), and s| pπ α = s| β , which is the cause of the equality s| pπ = s| pπ . This situation is not possible because of the transformations performed in the part extension in the construction of c . 2. (p, απ, π ) such that pα ∈ occ t (x) for some variable x, we performed the replacement ρ[ρ| pα ] β (for some other β ∈ occ t (x)), and s| pπ = s| βπ . This situation is made impossible by the completion in the part called variables in the construction of c .

The term s is the term of T (F) associated to ρ and it is a ground instance of t. Moreover, by Lemma 6, s is irreducible by R.

(end of proof of Proposition 2)

Generalised pumping lemmas

This is the crux part of our proof. We assume here a given ADC A = (Q, Q f , ∆) and a well founded ordering , total on runs Hence, in the following, we may refer to close and far equalities in pumpings, forgetting the position p. Given a large enough run ρ, we will successively show how to construct a weak run by pumping which does not contain any close equality (this uses combinatorial arguments only) then we show how to remove far equalities by further successive pumpings.

Pumping without creating close equalities

Given an ADC A = (Q, Q f , ∆) and an integer k, we let:

g(A, k) := (e × k + 1) × |Q| × 2 c(A) × c(A)!
where e is the exponential basis (e := +∞ n=0 1 n! ) and c(A) is the number of distinct suffixes of positions π, π in an atom π = π occurring in a constraint of transition rules of A. Then we have a pumping lemma which generalises those of [START_REF] Dauchet | Automata for reduction properties solving[END_REF]4]. Lemma 10. Let k be an integer. If ρ is a run of A and p 1 , . . . , p g(A,k) are positions of ρ such that ρ| p 1 . . . ρ| p g(A,k) then there are indices i 0 < i 1 < . . . < i k such that the pumping ρ[ρ| p i j ] p i 0 does not contain any close equality. Example 4. This example illustrates the principle of the proof of Lemma 10. Let F contain a ternary symbol f and let the ADC A contain the following transition rule:

r : f (q 1 , q 2 , q 3 ) -------→ 1 =31∧1 =32 q
Consider moreover the following run (which is also depicted on figure 2): We show that ρ is large enough so as to be able to find a pumping which does not create any close equality. Assume first that the replacement of the subtree at position 3 in ρ by any other subtree rooted by r (except ρ itself) creates a close equality. This means that, for all i = 2, . . . , 6, u i = u 0 or v i = v 0 . Then it is possible to extract a subsequence of three indices

ρ = r(u 0 , v 0 , r(u 1 , v 1 , r(u 2 , v 2 , r(u 3 , v 3 , r(u 4 , v 4 , r(u 5 , v 5 , r(u 6 , v 6 , v)))))))
i 1 , i 2 , i 3 such that (u 0 = u i 1 = u i 2 = u i 3 ) ∨ (v 0 = v i 1 = v i 2 = v i 3
). Assume we are in the first case of the disjunction and that, for instance u 0 = u 2 = u 4 = u 6 . Now, we try to replace the subterm r(u 2 , v 2 , . . .) with r(u 4 , v 4 , . . .) and r(u 6 , v 6 , v) respectively. Since u 2 = u 4 = u 6 = u 1 , if each of these replacements creates a close equality, we must have v 1 = v 4 = v 6 . Finally, replacing r(u 4 , v 4 , . . .) by r(u 6 , v 6 , v), we cannot create a close equality since u 6 = u 4 = u 3 and v 6 = v 4 = v 3 .

Proof. (Lemma 10) We can first extract from p 1 . . . p g(A,k) a subsequence p l 0 . . . p l k 1 such that ρ(p l 0 ) . . . ρ(p l k 1 ) have all the same target state, with:

k 1 := g(A, k) |Q| = (e × k + 1) × 2 c(A) × c(A)!
Let us define u 0 := p l 0 , . . . ,u k 1 := p l k 1 To extract a second subsequence we use a function test(p) defined on the positions of Pos(ρ) and such that for all p ∈ Pos(ρ): We see that for all p ∈ Pos(ρ), cr(p) is included in the set of suffixes of positions π and π such that (π = π ) is a atomic constraint occurring in one of the rules of ∆. Thus the number of distinct sets cr(p) for p ∈ Pos(ρ) is smaller than 2 c(A) . We can extract a subsequence u l 0 . . . u l k 2 of positions from u 0 . . . u k 1 such that cr(u l 0 ) = . . . = cr(u l k 2 ), with:

test(p) = (p , π) | p ≺ p p π | ∃π s.t. (π = π ) or (π = π)
k 2 := k 1 2 c(A) = (e × k + 1) × c(A)! We note v 0 := u l 0 , . . . ,v k 2 := u l k 2
. Then we are going to show that we can finally extract from v 0 . . . v k 2 another subsequence corresponding to the one in Lemma 10. This is a consequence of the following intermediate Lemma 11. Some additional definitions and notations are used in this Lemma 11. The dependency degree of a subsequence

v i 0 . . . v im of v 0 . . . v k 2 is: dep(v i 0 . . . v im ) := |{β ∈ cr(v 0 ) | t| v i 0 β = . . . = t| v im β }|
where t ∈ T (F) is the term associated3 to ρ. Let f (n) be an integer function recursively defined on the interval [0 . . . c(A)] by:

f (c(A)) = k f (n) = (c(A) -n) × (f (n + 1) + 1) + k -1 for n < c(A) Lemma 11. If for all 0 ≤ j ≤ k 2 , the cardinal of the set {j | k 2 ≥ j > j, ρ[ρ| v j ] v j has no close equality} is smaller than k then for all 0 ≤ n ≤ c(A), there exists a subsequence v i 0 . . . v i f (n) of v 0 . . . v k 2 such that dep(v i 0 . . . v i f (n) ) ≥ n.
Proof. We assume that the hypothesis of Lemma 11 is true and we prove the conclusion by induction on n.

For n = 0, by definition of the function dep, for every subsequence

v i 0 . . . v im of v 0 . . . v k 2 , we have dep(v i 0 . . . v im ) ≥ 0. Thus on this case, it is sufficient to show that f (0) ≤ k 2 . Let F (n) = f (c(A) -n) for all 0 ≤ n ≤ c(A). F (0) = k F (n) = n(F (n -1) + 1) + k -1 for 1 ≤ n ≤ c(A)
Developing,

F (n) = n! × (F (0) + 1) + k × n! n i=1 1 i! -1 ≤ k × n! + n! + k × n! × (e -1) -1 ≤ n! × (k × e + 1)
Thus,

f (0) = F (c(A)) ≤ c(A)! × (k × e + 1) ≤ (e × k + 1) × c(A)! ≤ k 2
For n + 1, assume that the property is true for n < c(A). By induction hypothesis, we have a subsequence

v i 0 . . . v i f (n) extracted from v 0 . . . v k 2 such that dep(v i 0 . . . v i f (n) ) ≥ n.
Moreover, by the hypothesis of Lemma 11, for at least

f (n) -(k -1) = (c(A) -n) × (f (n + 1) + 1) positions w among v i 1 . . . v i f (n) , ρ[ρ| w ] v i 0
has a close equality. We let:

k 3 = (c(A) -n) × (f (n + 1) + 1)
and we let w 1 . . . w k 3 be the above positions w, assuming that w 1 . . .

w k 3 is a subsequence of v i 1 . . . v i f (n)
. By definition of close equalities, for all j such that 1 ≤ j ≤ k 3 , there exists β j ∈ cr(v i 0 ) = cr(v 0 ), there exists v ≺ v i 0 and (π = π ) an atomic constraint in ρ(v) such that (we only consider one case because of the symmetry):

v i 0 β j = vπ (1)
t| v i 0 β j = t| vπ (2) t| w j β j = t| vπ (3)
Lets recall that t ∈ T (F) is the term associated to the run ρ. The construction of β j is depicted on figure 4.

By definition of dep(v

i 0 . . . v i f (n) ) ≥ n, there exists a subset E ⊆ cr(v 0 ) = cr(v i 0 ) such that: |E| = n (4) for all β ∈ E, t| v i 0 β = . . . = t| v i f (n) β (5)
In particular, for all β ∈ E, t| Let us recall that by definition of E, β / ∈ E, hence:

v i 0 β = t| w 1 β . . . = t| w k 3 β . Hence, {β 1 . . . β k 3 } ∩ E = ∅ by (2) and (3)
dep(w j 0 . . . w j f (n+1) ) > dep(v i 0 . . . v i f (n) ) ≥ n
This completes the proof of Lemma 11 because w j 0 . . .

w j f (n+1) is a subsequence of v 0 . . . v k 2 .
(end of the proof of Lemma 11)

Now, we have to finish the proof of Lemma 10. We will show that the hypothesis of Lemma 11 cannot be true. Assume it is true. Thus, for n = c(A) and f (n) = k, there exists a subsequence

v i 0 . . . v i k of v 0 . . . v k 2 such that dep(v i 0 . . . v i k ) ≥ c(A). But, by the above fact, |cr(v 0 )| ≤ c(A), thus by definition of dep(v i 0 . . . v i k ) we have: for all β ∈ cr(v 0 ), t| v i 0 β = . . . = t| v i k β
Assume now that one of the pumping ρ[ρ| v i j ] v i 0 for 1 ≤ j ≤ k has a close equality. This means that there exists v ≺ v i 0 and (π = π ), an atomic constraint in ρ(v) such that, v ≺ v i 0 vπ and t| vπ = t| v i j β . The position β := (vπ )/v i 0 ∈ cr(v i 0 ) is such that t| vπ = t| v i 0 β and with t| vπ = t| v i j β this contradicts t| v i 0 β = t| v i j β (see figure 5).

Thus for all 1 ≤ j ≤ k, the pumping ρ[ρ| v i j ] v 0 does not have any close equality. This completes the proof of Lemma 10.

Pumping without creating equalities

Definition 5. M is the predicate (defined relatively to an ADC A and an ordering ) which holds true on a run ρ of A, a position p of ρ and an integer k iff there exists k runs ρ| p ρ k . . . ρ 1 such that ρ(p), ρ 1 (Λ), . . . , ρ k (Λ) have the same target state and for every 1 ≤ i ≤ k the pumping ρ[ρ i ] p does not contain any close equality.

We list without proof two obvious consequences of Definition 5.

Lemma 12. If k ≥ k then M(ρ, p, k) implies M(ρ, p, k ).

Lemma 13. If a run ρ is such that M(ρ, Λ, k) for some k ≥ 1, then there exists a run ρ ρ such that the target states of ρ (Λ) and ρ(Λ) are the same.

Let h(A, k) = (d(A) + 1) × n(A) × k + g(A, k + 2d(A) × n(A))

where n(A) is the maximal number of atomic constraints occurring in a rule of A and d(A) is the maximal length |π| or |π | among every atomic constraints π = π in the transitions rule of A.

The following propagation lemma is the crux part of our proof. (It is also very technical to prove). It explains how to get rid of far equalities, if we have enough pumpings which do not create close equalities. The underlying intuitive idea behind Lemma 14 is the following. If we assume h(A, k) pumpings below p, which do not create close equalities (it will be possible to construct such pumpings thanks to Lemma 10), either one of them yields a run, and we completed our goal, or each of them contains a far equality. However, all these far equalities give us some information on the structure of the original run, and we are going to take advantage of this to design new other pumpings, which, combined with the original ones, ensure again h(A, k) pumpings below p < p each of them not containing equalities below p . This allows to prime an induction: we can construct pumpings such that ρ| p [ρ i ] is a run, provided that ρ| p [ρ j ] is a run. Eventually, we will have p = Λ and hence a pumping which is a run.

Lemma 14 (Propagation lemma). Let ρ be a run of A, p ∈ P os(ρ) and k be an integer such that k 2 ≥ h(A, k). If M(ρ, p, h(A, k)) is true, then one of the following properties holds:

1. there is a run ρ such that ρ| p ρ and ρ[ρ ] p is a run 2. there exists a position p such that |p | < |p| and M(ρ, p , h(A, k)) is true.

We shall show below (page 20) that such an integer k exists, and depends on A.

Proof. Assume M(ρ, p, h(A, k)) is true. This means that we have h(A, k) runs ρ 1 , . . . , ρ h(A,k) ∈ T (∆) such that ρ| p ρ i and ρ[ρ i ] p does not create a close equality, for 1 ≤ i ≤ h(A, k), following Definition 5 of M(). If we are not in the first case of the lemma, then for each

1 ≤ i ≤ h(A, k), ρ[ρ i ] p contains far equalities.
For each index j ≤ h(A, k), let γ j be a maximal position w.r.t. prefix ordering such that (γ j , π, π ) is a (far) equality of ρ[ρ j ] p , see figure 6. Let E be the set of triples (γ j , π, π ). We have |E| = h(A, k). Indeed, having two identical far equalities (γ j , π, π ) = (γ j , π, π ) for two distinct pumpings ρ[ρ j ] p and ρ[ρ j ] p would mean an equality of two different terms to the same subterm. Moreover, the number of distinct first components of elements of E is:

|{γ | ∃π, π (γ, π, π ) ∈ E}| ≥ |E| n(A) ≥ (d(A) + 1) × k + g(A, k + 2d(A) × n(A)) (6)
Note that every position γ j is a prefix of p (since ρ and ρ i are runs) hence the set of first components of E can be totally ordered by the prefix ordering.

Let u i , 1 ≤ i ≤ (d(A) + 1) × [k + g(A, k + 2d(A) × n(A))
], be a strictly decreasing sequence (w.r.t. the prefix ordering) of first components of elements in E.

We are going to show that M(ρ, u i , k 2 ) is true for some i, which implies the second case of Lemma 14 by hypothesis and by Lemma 12. First, we extract from the sequence (u i ) a subsequence (p i ) of length k 1 := k + g(A, k + 2d(A) × n(A)) defined by:

p i = u (d(A)+1)×i for all 1 ≤ i ≤ k 1 (7)
This ensures that two positions p i and p j are distant enough. To each integer 1 ≤ i ≤ k 1 , we can associate a unique index ν(i) ≤ h(A, k) defined by p i = γ ν(i) . By construction, for every equality (γ, π, π ) of the pumping ρ[ρ ν(i) ] p one has γ p i (p i is itself one of these γ which has been chosen to be maximal).

Now, we consider any given pumping

ρ[ρ ν(m) ] p for k 1 -k + 1 ≤ m ≤ k 1 (i.e
. p m is one of the k smallest positions p i ) and we show that there is one position p i m,0 , i m,0 ≤ k 1k, and k other pumpings on ρ[ρ ν(m) ] p whose equalities are far from p i m,0 . For sake of simplicity, we note ρ m := ρ[ρ ν(m) ] p . Note that, by construction, for each k

1 -k + 1 ≤ m ≤ k 1 , ρ m | p k 1 -k is a run.
We shall apply Lemma 10 to these runs in order to find appropriate pumpings. To each 1 ≤ i ≤ k 1 we can associate some positions π i and π i such that (p i , π i , π i ) ∈ E (i.e. it is a far equality of some ρ[ρ ν(i) ] p ). Moreover, with this construction, by definition of far equalities, for each i, we have either p i π i ≺ p or p i π i ≺ p (p is from the hypotheses of Lemma 14). By symmetry, we assume that we are in the first case for all i. Note that by construction of (p i ), and by definition of d(A), we have:

p 1 π 1 p 1 p 2 π 2 p 2 . . . p m ( 8
)
The situation is depicted in figure 7. The equality (p i , π i , π i ) is a far equality, hence, for every i, p i , p i π i and p i π i are indeed positions of ρ i and

p k 1 pm p k 1 -k p k 1 -k π k 1 -k p k 1 -k π k 1 -k p2 p2π 2 p2π2
ρ i | p i π i = ρ| p i π i . Following (8), ρ| p l π l is a subterm of ρ i | p i π i for l > i.
It follows that the terms ρ| p i π i are pairwise distinct. Hence, we can apply Lemma 10 to the run

ρ m | p k 1 -k and the positions p 1 π 1 , . . . , p k 1 -k π k 1 -k (of ρ). Note in particular that k 1 -k = g(A, k + 2d(A) × n(A)) and that ρ m | p k 1 -k π k 1 -k . . . ρ m | p 1 π 1 . This yields a subsequence (p i m,j π i m,j ), with 0 ≤ j ≤ k + 2d(A) × n(A), such that every pumping ρ m,j := ρ m [ρ m | p i m,j π i m,j
] p i m,0 π i m,0 does not contain close equalities (note that these pumpings ρ m,j are pairwise distinct). The pumpings ρ m,j may though contain some far equalities. In the following table, we give (upper bounds for) the number of these far equalities, w.r.t. the positions p i m,0 and p i m,0 π i m,0 . See also figure 8 for a picture of the three situations.

Equalities

Max. number (γ, π, π ) far from p i m,0 π i m,0 and

p i m,0 ≺ γ d(A) × n(A) (γ, π, π ) far from p i m,0 π i m,0 and close to p i m,0 d(A) × n(A) (γ, π, π ) far from p i m,0 π i m,0 and far from p i m,0 |p i m,0 | × n(A)
For the first two lines of this table, there are at most d(A) possible positions for γ and at most n(A) possible equalities for each of these positions. For the last line, the maximal number of positions is |p i m,0 |. Note that every equality in one of the pumpings ρ m [ρ m | p i m,j π i m,j ] p i m,0 π i m,0 is registered in this array. Thus, there exists at least k pumpings of the form

ρ m [ρ m | p i m,j π i m,j ] p i m,0 π i m,0
every equality of which is far from p i m,0 . Every equality in ρ m itself is also far from p i m,0 since:

pi m,0 ≺ γ (γ, π, π ) close to pi m,0 pi m,0 γ γπ pi m,0 π i m,0 γπ pi m,0 πi m,0 pi m,j pi m,j π i m,j pi m,j πi m,j γ pi m,0 γπ pi m,0 π i m,0 pi m,0 πi m,0 pi m,j pi m,j π i m,j pi m,j πi m,j γπ (γ, π, π ) far from pi m,0 γ γπ γπ pi m,0 pi m,0 π i m,0 pi m,0 πi m,0 pi m,j pi m,j π i m,j pi m,j πi m,j
1. the first component of such each an equality is one of

p k 1 -k+1 ,. . . , p k 1 2. p k 1 ≺ p k 1 -k+1 ≺ p i m,0 3. the distance between p k 1 and p i m,0 is at least d(A) + 1 (|p i m,0 | -|p k 1 | ≤ d(A) + 1).
To summarise, we have k possible pumpings ρ m ρ and for each of them we have k other pumpings ρ m,j ρ m (j ≤ k) such that every equality in a ρ m,j is far from some position p i m,0 ≺ p. By the remarks above, the ρ m,j are pairwise distinct. Let p be the largest of the above p i m,0 . With the remark that all of these pumping are only replacement at some positions bigger than p , we proved M(ρ, p , k 2 ) thus M(ρ, p , h(A, k)), by Lemma 12. (end of proof of Lemma 14) We initiate the process with Lemma 10 and use the propagation lemma 14 to push the position under which no equality is created, up to the root of the tree. With simple sufficient conditions for the inequality k 2 ≥ h(A, k), this yields the following lemma 15, where cs(A) is the global size of constraints in the transition rules of A.

Lemma 15. Let A = (Q, Q f , ∆) be an ADC . There exists two constants γ and δ independent from A such that if M ρ, p, γ × |Q| 2 × 2 δ.cs(A) 2 . ln(cs(A)) is true for some position p of a run ρ of A then there is a run of A ρ ρ such that ρ(Λ) and ρ (Λ) have the same target state.

Proof. We shall use Lemma 14. Hence, we need an integer k such that:

k 2 ≥ h(A, k) ( 9 )
For sake of simplicity, we write c, n and d respectively for c(A), n(A) and d(A). We assume that d, n ≥ 1. One can check that for (9), it is sufficient to have k = m + dn. Therefore,

h(A, k) ≤ (d + 1).n × [k + g(A, k + 2dn)] ≤ (d + 1).n × [k + |Q|.2 c .c! × (ek + 2edn + 1)] ≤ (d +
h(A, k) = h(A, m + dn) = m 2 + 2mdn = α 2 .|Q| 2 .2 2β.c. ln(c) .d 2 n 2 + 2α.|Q|.2 β.c. ln(c) .d 2 n 2 ≤ 2α 2 |Q| 2 .2 2β.c. ln(c) .d 2 n 2 ≤ 2α 2 |Q| 2 .2 2β.dn. ln(dn) .d 2 n 2 because c(A) ≤ d(A) × n(A) ≤ 2α 2 |Q| 2 .2 4β.cs(A) 2 . ln(cs(A)) .cs(A) 4 because d(A), n(A) ≤ cs(A) ≤ γ|Q| 2 × 2 δ×cs(A) 2 ×ln(cs(A)) with γ = 2α 2 and δ = 4β + 2
The rest follows by induction on the depth of ρ, using the propagation Lemma 14 and the Lemmas 12 and 13.

Emptiness Decision for ADC

In this section we present the following result:

Theorem 1. There is an algorithm which decides the emptiness of an ADC A = (Q, Q f , ∆) and which runs in time O (|Q| × |∆|) P (cs(A)) where P is a polynomial.

Algorithm

We use a marking algorithm in which each state is marked with some successful runs yielding the state. This generalises the usual marking algorithm for finite bottom-up tree automata: we do not keep only the information that a state is inhabited but also keep witnesses of this fact. The witnesses are used to check the disequality constraints higher up in the run. To choose the witnesses runs which mark the states and ensure the termination of the algorithm, we use a sufficient condition for the above M predicate. In the algorithm, we use the set C(A) of suffixes of positions π, π in an atom π = π occurring in a constraint of transition rule of A. Note that c(A) = |C(A)|. We use also a bound evaluated in the proof of Lemma 15:

b(A) := γ × |Q| 2 × 2 δ.cs(A) 2 . ln(cs(A)) (10)
We assume moreover that the constants γ and δ are such that:

b(A) > |Q| × |F| (11)

Emptiness decision algorithm.

Start with a mapping which associates each state q with an empty set E 0 q then saturate the states E 0 q using the rule:

{ρ 1 ,...,ρn}∈ S m i=0 S q∈Q E i q r(ρ 1 ,...,ρn)∈E m+1 q 0
under the conditions:

1. r(ρ 1 , . . . , ρ n ) is a run, 2. the target state of r is q 0 , 3. for every p ∈ Pos(ρ)\C(A), with |p| ≤ d(A)+ 1, there exists no sequence of length b(A) of runs of m i=0 q∈Q E i q , ρ| p ρ b(A) . . . ρ 1 such that ρ(p), ρ 1 (Λ), . . . , ρ b(A) (Λ)
have the same target state and for every 1 ≤ j ≤ b(A), the pumping ρ[ρ j ] p does not contain any close equality.

We consider only fair executions of the algorithm: we assume that for each runs ρ 1 , . . . , ρ n constructed and each r ∈ ∆, r(ρ 1 , . . . , ρ n ) is eventually checked. We also also assume some marking of the runs checked which prevents the algorithm to check the same run twice.

We have to prove on one hand that the saturated set E * := m≥0 q∈Q E m q contains an accepting run iff A accepts at least one tree (correctness, completeness) and on the other hand that E * is computed with the expected complexity.

Correctness and completeness Lemma 16 (Correctness). If E * contains an accepting run then L(A) is not empty.

Proof. Immediate by the condition "1. r(ρ 1 , . . . , ρ n ) is a run" in the emptiness decision algorithm.

Lemma 17 (Completeness). If E * does not contain any accepting run then L(A) is empty.

Proof. Assume that A accepts at least one ground term, and let ρ be an accepting run of A, minimal w.r.t. . We prove that ρ ∈ E * by contradiction.

Assume that ρ / ∈ E * , and let µ be a subterm of ρ, minimal w.r.t. the subterm ordering in the set of subterms of ρ which do not belong to E * . We can first show that have depth(µ) > 0. Indeed, if depth(µ) = 0, every run µ µ has the form c → q. By (11) the number of such runs is smaller that b(A), hence the condition 3 of the emptiness decision algorithm must be true for µ, and therefore µ ∈ E * , a contradiction.

Hence, let µ = r(µ 1 , . . . , µ n ). By minimality hypothesis, µ 1 , . . . , µ n ∈ E * . Since µ / ∈ E * , the condition 3 of the emptiness decision algorithm is not true, which means that there exists a position p ∈ Pos(µ) \ C(A), with |p| ≤ d(A) + 1, and a sequence µ| p µ b(A) . . . µ 1 of runs of E * such that µ(p), µ 1 (Λ), . . . , µ b(A) (Λ) have the same target state and for every 1 ≤ j ≤ b(A), the pumping µ[µ j ] p does not contain any close equality.

Let p ∈ Pos(ρ) be the position such that µ = ρ| p . Since p / ∈ C(A), and by definition of close equalities page 4, for all 1 ≤ j ≤ b(A), the pumping ρ[µ j ] p .p does not contain any close equality. By Lemma 15, this contradicts the minimality of ρ w.r.t. .

Termination and complexity

In order to show the termination of the emptiness decision algorithm and to give a complexity bound, we need an additional argument: a generalization of König's theorem for bipartite graphs to hypergraphs. Let us first define a notion of dependency in hypergraphs: Definition 6. Let S be a set and n, k be integers. The n-uples s 1 , . . . , s k of elements in S are independent iff there is a set I ⊆ {1, . . . , n} such that

-∀i ∈ I, s 1,i = . . . = s k,i -∀i / ∈ I, ∀j = j , s j,i = s j ,i
Now, we have the analogue of König's theorem:

Theorem 2 (B. Reed, private communication). Let S be a set and K, n be integers.

Let G ⊆ S n . If every subset G 1 ⊆ G of independent elements has a cardinal |G 1 | ≤ K, then |G| ≤ K n × n!
Proof. We prove the result by induction on n.

For n = 1, G itself is a set of independent elements, hence |G| ≤ K. Assume now that the property holds for n -1. Consider the graph H(G) whose vertices are the elements of G and such that there is an edge (g, g ) iff there is a component i ∈ [1.

.n] such that

g i = g i . Any stable subset G 1 of G is independent, hence |G 1 | ≤ K (a subset G 1 of G is stable if G 1 × G 1 contains no edge of H(G)).
Now, let V be the maximal number of edges sharing some vertex v 0 in H(G) (maximal neighbourhood). We construct a stable set G 1 whose cardinal is |G 1 | ≥ |G| V +1 as follows:

Initially, G 2 = G and G 1 = ∅.
Repeat the following: Choose a vertex v in G 2 and put it in G 1 remove v from G 2 as well as all vertices w such that (v, w) ∈ H(G) until G 2 is empty.

Since, at each step, we remove at most V + 1 elements from G 2 , we have at least |G| V +1 steps, and, at each step, we add an element in

G 1 . Hence |G 1 | ≥ |G| V +1 . Moreover, G 1 is stable, by construction. Now, K ≥ |G 1 | ≥ |G| V +1 , hence V ≥ |G| K -1. Assume, by contradiction, that |G| > K n × n!, then V > K n ×n! K -1 = K n-1 × n! -1. Now,
there are at least K n-1 × n! edges departing from v 0 in H(G). Hence there is an index j ∈ [1..n] such that, for at least

K n-1 × (n -1)! vertices v in H(G), v j 0 = v j . Let G = {(v 1 , ..., v j-1 , v j+1 , . . . , v n )|(v 1 , . . . , v j-1 , v j 0 , v j+1 , . . . , v n ) ∈ G} every subset G 1 of G of independent
elements has a cardinal smaller or equal to K and |G | ≥ K n-1 × (n -1)! + 1, which contradicts the induction hypothesis.

Independence of runs

Let us denote C(A) = {π 1 , . . . , π c(A) } and let ρ be a run of A. Then Check(ρ) is the tuple (t 1 , . . . , t c(A) ) ∈ (T (F) ∪ {⊥}) c(A) such that t i =⊥ if π i / ∈ Pos(ρ) and t i is the term of T (F) associated to ρ| π i otherwise. We say that the runs ρ 1 ,. . . , ρ k are independent if Check(ρ 1 ),. . . , Check(ρ k ) are independent.

-for each i ∈ I, for each j ≤ k, t j | π i = t| p.π i -for each i / ∈ I, for ever j = l ≤ k, t j | π i = t l | π i
Let J ⊆ {1, . . . , k} be the set of all indices j such that ρ[ρ j ] p contains a close equality. We associate with each j ∈ J:

a close equality (p j , α j , β j ) of ρ[ρ j ] p , -the integer i(j) such that C(A) π i(j) = p j α j \ p (by construction, p j α j p or p j β j p, by symmetry, we may assume that p j α j p)

We note p = p j .p j and α j = p j .π i(j) . The mapping j → (p j , α j , β j , i(j)) has an image of cardinality at most c(A) × cs(A) (for a fixed p). Indeed, π i(j) , α j , β j uniquely define p j , and p j , p determine p j ; and there are at most cs(A) possible values for i(j) and less than cs(A) possible values for (α j , β j ) By contradiction, assume that |J| ≥ c(A) × cs(A) + 1. By a pigeon hole principle, there are two indices j, j ∈ J such that p j = p j , α j = α j , β j = β j , and i(j) = i(j ). Hence,

t j | π i(j) = t| p j .β(j) = t| p j .β(j ) = t j | π i(j ) (12)
Hence, i(j) = i(j ) ∈ I, and by definition of I, it follows that t j | π i(j) = t| p.π i(j) . Therefore, by [START_REF] Kounalis | Testing for the ground (co)-reducibility in term rewriting systems[END_REF], t| p.π i(j) = ρ p j .β(j) , and, noting that t| p.π i(j) = t p j .α j , it means that ρ contains a close equality, which is a contradiction.

Bound on the number of steps. Let G * ⊆ E * be the subset of runs occurring as strict subterms of runs of E * at positions not in C(A).

G * := {ρ| p | ρ ∈ E * , p ∈ Pos(ρ) \ C(A)} Note that |E * | ≤ |∆| c(A) × |G * | c(A)×α ( 13
)
where α is the maximal arity of a function symbol of F. Indeed constructing a run ρ ∈ E * , we shall fix the labels at positions in C(A) ∩ Pos(ρ) (this can be done in at most |∆| c(A) ), and then choose at most |G * | c(A)×α subruns belonging to G * . According to the condition 3 of the emptiness decision algorithm and to Lemma 18, for each state q ∈ Q, the set G * ∩ m≥0 E m q cannot contain more than b(A) + c(A) × cs(A) + 1 independent runs. By Theorem 2, and by definition of independence of runs, this means that

|G * ∩ m≥0 E m q | ≤ (b(A) + c(A) × cs(A) + 1) c(A) × c(A)! Hence, with the remark that G * ⊆ E * , |G * | ≤ |Q| × (b(A) + c(A) × cs(A) + 1) c(A) × c(A)! ( 14
)
Every term considered by the emptiness decision algorithm, (and checked for conditions 1, 2 and 3) has the form r(ρ 1 , . . . , ρ n ) where r ∈ ∆ and ρ 1 , . . . , ρ n ∈ E * . This ensures the termination of the algorithm and together with ( 13) and ( 14), this gives the following bound for the number of steps for emptiness decision, for some polynomial P 1 :

# of steps ≤ |∆| × |E * | α ≤ |∆| c(A).α+1 × |G * | c(A).α 2 (13) ≤ |∆| c(A).α+1 × |Q| c(A).α 2 × (b(A) + c(A) × cs(A) + 1) c(A) 2 .α 2 × (c(A)!) c(A).α 2 (13) ≤ |∆| c(A).α+1 × |Q| c(A).α 2 × (γ × |Q| 2 × 2 δ.cs(A) 2 . ln(cs(A)) + c(A) × cs(A) + 1) c(A) 2 .α 2 × (c(A)!) c(A).α 2 (10) ≤ (|Q| × |∆|) P 1 (cs(A))
In the last step, we assume that |Q| × |∆| ≥ 2 and we use the inequality:

c(A) ≤ d(A) × n(A) ≤ cs(A) 2
Cost of one inference step. Now, we have to estimate the cost of each inference step. The choice of one transition rule r in the algorithm is done among the set ∆, thus this (deterministic) choice is performed in time at most |∆|. For each new candidate r(ρ 1 , . . . , ρ n ), the sons are already in the set E * . Hence, for checking that r(ρ 1 , . . . , ρ n ) is a run, it is sufficient to check that the disequality constraints of r are satisfied. Of course, we assume that identical subterms are shared, and therefore disequalities are checked in constant time. Hence, verifying the condition 1 of the algorithm is performed in time at most cs(A).

Finally, we need to estimate the cost of checking the condition 3 on a run ρ. The number of position p ∈ Pos(ρ) \ C(A) to consider is at most α d(A)+1 (we recall that α is the maximal arity of a function symbol of F). Let q be the target state of the rule ρ(p). To check the non existence of a sequence of runs ρ| p ρ b(A) . . . ρ 1 like in condition 3, we check all the possible ρ j individually. To bound the number of possible candidates for ρ j , j ≤ b(A), we add the additional requirement that is such that:

ρ ρ implies d(ρ) > d(ρ ) (15)
With the condition (15) above, only the runs which are already in n≥0 E n q , are possible candidates for ρ j , j ≤ b(A), which means that the number of runs to check is smaller than |E * |. For each pumping ρ[ρ j ] p , verifying whether or not it creates a close equality requires time at most d(A) × cs(A). Indeed, it is sufficient to check that for each position p p, p ∈ Pos(ρ[ρ j ] p ), at distance at most d(A) from p (i.e. such that |p| -|p | ≤ d(A)), and for each disequality π = π in the constraint of the rule at position p in ρ[ρ j ] p , with p ≺ p π or p ≺ p π , one has t[t j ] p | p π = t[t j ] p | p π , where t and t j are the terms associated respectively to ρ and ρ j . As above, we assume that the verification of the inequalities is performed in constant time.

Hence the condition 3 can be checked in time at most, for some polynomial P 2 :

α d(A)+1 × |E * | × d(A) × cs(A) ≤ (|Q| × |∆|) P 2 (cs(A))
where |E * | is bounded as above.

With the above remarks, the cost of one inference step is therefore smaller than, for some polynomial P 3 :

|∆| × cs(A) × (|Q| × |∆|) P 2 (cs(A)) ≤ (|Q| × |∆|) P 3 (cs(A))
Together with the bound on the number of steps, we get the complexity in Theorem 1.

Ordering

It still remains to exhibit an ordering which satisfies all our requirements:

Lemma 19. There is an ordering which is monotonic, well-founded, total on T (∆) and such that, if depth(ρ) > depth(ρ ) then ρ ρ .

Proof. Consider the following interpretation of a term t: I(t) is the triple (depth(t), M(t), t) where M (t) is the multiset of strict subterms of t.

Triples are ordered with the lexicographic composition of:

1. the ordering on natural numbers, 2. the multiset extension of , 3. a lexicographic path ordering extending a total precedence.

itself is defined as u t iff I(u) > I(t).

First, we should explain why the definition of the ordering itself is well-founded: is defined recursively, using its multiset extension. However, while defining on t, we use the multiset extension of on strict subterms of t and the subterm ordering is well-founded.

)) = d(ρ j ) + 1 if d(ρ j ) ≥ max(d(t k )) 1 + d(t k ) > d(ρ j ) for some k, otherwise In any case, d(δ(t 1 , . . . , t i , ρ 1 , t i+1 , . . . , t n )) ≥ d(δ(t 1 , . . . , t i , ρ 2 , t i+1 , . . . , t n )). I(ρ 1 ) > I(ρ 2 ) implies either d(ρ 1 ) > d(ρ 2 ) or M (ρ 1 ) ≥ M (ρ 2 ). Moreover, M (δ(t 1 , . . . , t i , ρ j , t i+1 , . . . , t n )) = n i=1 M (t i ) ∪ {{t 1 , . . . , t n }} ∪ {{ρ j }} ∪ M (ρ j ) If d(ρ 1 ) > d(ρ 2 )
, then there is a strict subterm ρ 3 of ρ 1 such that, for every strict subterm ρ 4 of ρ 2 , d(ρ 3 ) > d(ρ 4 ), which implies ρ 3 ρ 4 . Then, by definition of the multiset ordering, {{ρ 3 }} > M(ρ 2 ) and hence M (ρ 1 ) > M(ρ 2 ). It follows that, in any case,

ρ 1 ρ 2 ⇒ M (ρ 1 ) ≥ M (ρ 2 ) then M (δ(. . . , ρ 1 , . . .)) ≥ n i=1 M (t i ) ∪ M (ρ 2 ) ∪ {{t 1 , . . . , t n }} ∪ {{ρ 1 }} > n i=1 M (t i ) ∪ M (ρ 2 ) ∪ {{t 1 , . . . , t n }} ∪ {{ρ 2 }} = M (δ(. . . , ρ 2 , . . .))
This suffices to guarantee the monotonicity.

is well-founded. By structural induction on t, there is no infinite strictly decreasing sequence starting with t. If t is a constant, then I(t) = (1, ∅, t) and t is minimal. If this is true for the strict subterms of t, then let E be the set of terms smaller (w.r.t. ) than some strict subterm of t.

is well-founded on E by induction hypothesis. Then its multiset extension is well-founded on multisets whose elements are in E.

Then there is no infinite strictly decreasing sequence starting with t by well-foundedness of the lexicographic path ordering and since the lexicographic combination of well-founded orderings is itself well-founded. contains the strict superterm relation. Because of the first component of the interpretation. is total. That is the purpose of the last component of the interpretation: the lexicographic path ordering extending a total precedence is total on ground terms. Hence, for any distinct terms ρ 1 , ρ 2 , either I(ρ 1 ) I(ρ 2 ) or I(ρ 2 ) I(ρ 1 ).

As a consequence of Theorem 1 and Proposition 2, the decision of ground reducibility is in DEXPTIME. Theorem 3. Ground reducibility of a term t w.r.t. a rewrite system R can be decided in deterministic time O(2 P ( t , R ) ) where P is a polynomial.

Lower bound

Theorem 4. Ground reducibility is EXPTIME-hard, for linear rewrite systems R and linear terms t, with PTIME reductions.

The proof is a reduction of the emptiness problem for the intersection of (languages recognized by) k tree automata.The latter is know to be EXPTIME-complete ( [START_REF] Frühwirth | Logic programs as types for logic programs[END_REF][START_REF] Seidl | Haskell overloading is dexptime-complete[END_REF]). We encode several (parallel) computations (runs) of k given tree automata on the same ground term t ∈ T (F) as a term of s ∈ T (F ) where F is a new alphabet built from F and the tree automata. This encoding is polynomial. Then, we build a rewrite system R whose every ground normal form as the form g(s) where g is a new function symbol and s ∈ T (F ) represents successful runs of the k automata A 1 . . . A k . Thus, L(A 1 ∩ . . . ∩ A k ) is not empty iff the term g(x) (x ∈ X ) is not ground reducible w.r.t. R. Finally, we can conclude the proof of Theorem 4 by checking that the system R is built in polynomial time w.r.t. the size of the size of the tree automata.

An EXPTIME complete problem

The formal definition of the EXPTIME-hard problem we consider is the following: Proposition 3. T. Frühwirth et. al. [START_REF] Frühwirth | Logic programs as types for logic programs[END_REF], H. Seidl [START_REF] Seidl | Haskell overloading is dexptime-complete[END_REF] The following problem is EXPTIME hard: "given k tree automata A 1 , . . . , A k , is L(A 1 ) ∩ . . . ∩ L(A k ) empty ?"

Representation of runs

Let A 1 = (Q 1 , Q f 1 , ∆ 1 ) . . . A k = (Q k , Q f k , ∆ k ).
We can assume without loss of generality that the sets Q 1 . . . Q k are pairwise disjoint.

The alphabet F is defined as follows:

-F := F {g} Q 1 . . . Q k g / ∈ F and g is unary in F . -The arity (in F ) of each symbol of Q 1 . . . Q k is zero.

-The arity (in F ) of each symbol of f ∈ F is the arity of f in F plus k.

We distinguish a subset S ⊆ T (F ) which is recursively defined as follows:

-For each constant a in F, each states q 1 ∈ Q 1 , . . . , q k ∈ Q k , a(q 1 , . . . , q k ) ∈ S.

-For each symbol f ∈ F, f having arity n in F, each states q 1 ∈ Q 1 , . . . , q k ∈ Q k , and each t 1 , . . . , t n ∈ S, f (q 1 , . . . , q k , t 1 , . . . , t n ) ∈ S.

Note that the above a(q 1 , . . . , q k ) and f (q 1 , . . . , q k , t 1 , . . . , t n ) are indeed terms of T (F ). The terms of S will be used to represent parallel computations of A 1 , . . . , A k on a term t ∈ T (F).

The rewrite system R

The system R is expected to reduce any ground term t ∈ T (F ) which is not of the form t = g(s) where s represents successful runs of A 1 , . . . , A n on a term t ∈ T (F). There can be four (mutually exclusive) reasons for that: [ g cannot occur inside a term ] f (x 1 , . . . , x i-1 , g(x), x i+1 , . . . , x k+n ) → q such that:

f ∈ F and f as arity n in F x 1 , . . . , x i-1 , x, x i+1 , . . . , x k+n are distinct variables of X 2. Every rule of the second category has one of the forms:

(a) [ no state can occur after the first kth positions below an f ∈ F ] f (x 1 , . . . , x i-1 , q , x i+1 , . . . , x k+n ) → q such that:

f ∈ F and f as arity n in F x 1 , . . . , x i-1 , x i+1 , . . . , x k+n are distinct variables of X i > k q ∈ Q 1 . . . Q k (b) [ no symbol of the original signature F can occur in the first kth positions ] f (x 1 , . . . , x i-1 , f (y 1 , . . . , y k+n ), x i+1 , . . . , x k+n ) → q such that: -f, f ∈ F and their respective arity are n and n in F x 1 , . . . , x i-1 , x i+1 , . . . , x k+n , y 1 , . . . , y k+n are distinct variables of X i ≤ k (c) [ at position i, one must have a state of Q i ] f (x 1 , . . . , x i-1 , q , x i+1 , . . . , x k+n ) → q such that: -f ∈ F and its arity in F is n x 1 , . . . , x i-1 , x i+1 , . . . , x k+n are distinct variables of

X -i ≤ k -q ∈ Q 1 . . . Q i-1 Q i+1 . . . Q k 3.
The rules for this category are (see also figure 9):

[ the subterms must describe transitions of the automata ] f   

x 1 . . . x i-1 , q i , x i+1 . . . x k , f 1 (y 1 1 . . . y 1 i-1 , q 1 i , y 1 i+1 . . . y 1 k+a 1 ), . . . f n (y n 1 . . . y n i-1 , q n i , y n i+1 . . . y n k+an )    → q such that: -f, f 1 , . . . , f n ∈ F and their respective arities in F are n and a 1 ,. . . , a n x 1 , . . . , x i-1 , x i+1 , . . . , x k , y 1 1 , . . . , y 1 i-1 , y 1 i+1 , . . . , y 1 k+a 1 , y n 1 , . . . , y n i-1 , y n i+1 , . . . , y n k+an are distinct variables of X i ≤ k q i , q 1 i , . . . , q n i ∈ Q i

Fig. 1 .

 1 Fig. 1. An equality close to p0An equality far from p0.

Lemma 8 .

 8 Let ρ be a run of A NF(R),t and a position p ∈ Pos(ρ) such the target state of ρ(p) is [u, q]. Then for all position p ∈ Pos(u), if u

Fig. 2 .

 2 Fig. 2.A run with a possible pumping.

Fact 1 .Fig. 3 .

 13 Fig. 3. The bold branch is in cr(p).

Fig. 4 .

 4 Fig. 4. Definition of βj, proof of Lemma 11.

  . Moreover, according to the above fact 1, |cr(v 0 )| ≤ c(A). This implies that there are at most c(A)n distinct positions among β 1 . . . β k 3 . Thus there exists:1 ≤ j 0 < . . . < j f (n+1) ≤ k 3 such that β j 0 = . . . = β j f (n+1) , because k 3 c(A)-n = f (n + 1) + 1.Let β this unique position. By construction: t| w j 0 β = . . . = t| w j f (n+1) β

Fig. 5 .

 5 Fig. 5. Proof of Lemma 10.

Fig. 6 .

 6 Fig. 6. The far equality (γj, π, π ) in ρ[ρj]p.

Fig. 7 .

 7 Fig. 7. Proof of Lemma 14.

Fig. 8 .

 8 Fig. 8. (γ, π, π ) far from pi m,0 π i m,0 .

  1).n.(e.|Q|.2 c .c! + 1).k + (d + 1).n.|Q|.2 c .c! × (2edn + 1) ≤ α.|Q|.2 β.c. ln(c) .dn.k + α.|Q|.2 β.c. ln(c) .d 2 .n 2 where α and β are constants independent of A ≤ m.k + m.dn where m := α.|Q|.2 β.c. ln(c) .dn

Fig. 9 .

 9 Fig. 9. Rules of category 3 (left members).

  1, 11, 2} and e.g. t(1) = g. The subset of maximal position of t w.r.t. , also called subset of leaves positions is denoted Posl (t). If p ∈ Pos(t), we write t| p for the subterm of t at position p and t[s] p for the term obtained by replacing t| p by s (at position p) in t.

  Lemma 18. Let ρ be a run of the ADC A and p ∈ P os(ρ), let k > b(A) and be a total ordering. If there are k runs ρ 1 , . . . , ρ k such that ρ 1 . . . ρ k ρ| p , and ρ 1 (Λ), . . . , ρ k (Λ) and ρ(p) have the same target state, and ρ 1 ,. . . , ρ k , ρ| p are independent, then there are at least kc(A) × cs(A) different pumpings ρ[ρ i ] p (with i ≤ k) without close equalities. Proof. Let t, t 1 , . . . , t k be the terms associated to respectively ρ, ρ 1 , . . . , ρ k . By hypothesis, we have a subset I ⊆ {1, . . . , c(A)} such that:

	Note that the totality of	is sufficient for this lemma.

  , . . . , t i , ρ j , t i+1 , . . . , t n

	If d(ρ) > d(ρ ), then ρ	ρ , simply because d(ρ) is the first component of I(ρ).
	is monotonic. Assume ρ 1	ρ 2 i.e. I(ρ 1 ) > I(ρ 2 ). Then d(ρ 1 ) ≥ d(ρ 2 ) by definition of the
	lexicographic composition. Next,
	d(δ(t 1

This may be a non standard definition but the size of right hand sides of rules is not relevant for our purpose.

Let us recall that runs of A = (Q, Q f , ∆) can be seen as terms of T (∆).

the term associated to the run ρ is the term on which the ADC A makes the run ρ.

Acknowledgments

The authors wish to thank Bruce Reed for his proof of the theorem 2, and Denis Lugiez for his useful remarks and suggestions.

f (q 1 i , . . . , q n i ) → q i / ∈ ∆ i 4. Finally, in the last category, we have:

[ at the top of the term, we want final states ] g(f (x 1 , . . . , x i-1 , q , x i+1 , . . . , x k+n )) → q such that:

Size of R. First of all, note that the system R is linear. Now, we need to evaluate its size. It will be expressed in term of k, of the number of states of the automata A 1 , . . . , A k , of the initial number of function symbols |F| and finally of the maximal arity α of a function symbol in F:

The biggest rule of R belongs to the category 3 and its size is:

The number of rules in each category is summarised below:

Thus, the size of R is polynomial in the (sum of) sizes of the given tree automata.

On the other hand, it is clear that the construction of R does not require a time bigger than the size of this system. Altogether, this proves Theorem 4.

Conclusion

We proved that ground reducibility is EXPTIME-complete for both the linear and the nonlinear case. This closes a pending question. However, we do not claim that this result in itself gives any hint on how to implement a ground reducibility test. As we have seen, it is not tractable in general. A possible way to implement these techniques as efficiently as possible was suggested in [START_REF] Caron | Pumping, cleaning and symbolic constraints solving[END_REF]. In the average, some algorithms may behave well. In any case, we claim that tree automata help both in theory and in practice.


Student Member, IEEE Yuliya Tarabalka
email: yuliya.tarabalka@hyperinet.eu

Mathieu Fauvel
email: mathieu.fauvel@inrialpes.fr

Senior Member, IEEE Jocelyn Chanussot
email: jocelyn.chanussot@gipsa-lab.grenoble-inp.fr

Fellow, IEEE Jón Atli Benediktsson

SVM-and MRF-Based Method for Accurate Classification of Hyperspectral Images

Keywords: Classification, hyperspectral images, Markov random field (MRF), support vector machine (SVM)

The high number of spectral bands acquired by hyperspectral sensors increases the capability to distinguish physical materials and objects, presenting new challenges to image analysis and classification. This letter presents a novel method for accurate spectral-spatial classification of hyperspectral images. The proposed technique consists of two steps. In the first step, a probabilistic support vector machine pixelwise classification of the hyperspectral image is applied. In the second step, spatial contextual information is used for refining the classification results obtained in the first step. This is achieved by means of a Markov random field regularization. Experimental results are presented for three hyperspectral airborne images and compared with those obtained by recently proposed advanced spectral-spatial classification techniques. The proposed method improves classification accuracies when compared to other classification approaches.

I. INTRODUCTION

H YPERSPECTRAL imaging sensors measure the energy of the received light in tens or hundreds of narrow spectral bands in each spatial position in the image [START_REF] Chang | Hyperspectral Data Exploitation: Theory and Applications[END_REF]. Thus, every pixel can be represented as a high-dimensional vector across the wavelength dimension, called the spectrum of the material in this pixel. Since different substances exhibit different spectral signatures, hyperspectral imagery is a well-suited technology for accurate image classification, which is an important task in many application domains (monitoring and management of the environment, precision agriculture, etc.).

Most classification methods process each pixel independently without considering the correlations between spatially adjacent pixels (so-called pixelwise classifiers) [START_REF] Landgrebe | Signal Theory Methods in Multispectral Remote Sensing[END_REF], [START_REF] Camps-Valls | Kernel-based methods for hyperspectral image classification[END_REF]. In particular, support vector machines (SVMs) have shown good performances for classifying high-dimensional data when a limited number of training samples are available [START_REF] Camps-Valls | Kernel-based methods for hyperspectral image classification[END_REF], [START_REF] Vapnik | Statistical Learning Theory[END_REF]. Furthermore, spatial contextual information should help for an accurate scene interpretation. Therefore, it is very important to develop spectral-spatial classification techniques that are capable to consider spatial dependences between pixels [START_REF] Kettig | Classification of multispectral image data by extraction and classification of homogeneous objects[END_REF]- [START_REF] Tarabalka | Segmentation and classification of hyperspectral images using minimum spanning forest grown from automatically selected markers[END_REF].

In general, two categories of spectral-spatial classification methods can be distinguished. First, spatial contextual information is exploited in the classification stage. For instance, spectral and spatial information can be combined within a feature vector of each pixel, and then, a pixelwise classification technique can be applied to the obtained set of vectors [START_REF] Fauvel | Spectral and spatial classification of hyperspectral data using SVMs and morphological profiles[END_REF], [START_REF] Camps-Valls | Composite kernels for hyperspectral image classification[END_REF]. Another group of methods from this category first defines the objects within the image scene and then classifies each object [START_REF] Landgrebe | Signal Theory Methods in Multispectral Remote Sensing[END_REF], [START_REF] Kettig | Classification of multispectral image data by extraction and classification of homogeneous objects[END_REF]. Second, spatial dependences are considered in the decision rule [START_REF] Bovolo | A context-sensitive technique based on support vector machines for image classification[END_REF]. An example is a pixelwise classification followed by spatial regularization of the classification map.

Markov random fields (MRFs) are probabilistic models that are commonly used to integrate spatial context into image classification problems [START_REF] Farag | A unified framework for map estimation in remote sensing image segmentation[END_REF], [START_REF] Bovolo | A context-sensitive technique based on support vector machines for image classification[END_REF], [START_REF] Liu | A spatial-temporal approach to monitoring forest disease spread using multi-temporal high spatial resolution imagery[END_REF]. In the MRF framework, the maximum a posteriori (MAP) decision rule is typically formulated as the minimization of a suitable energy function [START_REF] Solberg | A Markov random field model for classification of multisource satellite imagery[END_REF]. An extensive literature is available on MRF-based image classification techniques. In particular, the research groups of Farag [START_REF] Farag | A unified framework for map estimation in remote sensing image segmentation[END_REF], Bruzzone [START_REF] Bovolo | A context-sensitive technique based on support vector machines for image classification[END_REF], and Gong [START_REF] Liu | A spatial-temporal approach to monitoring forest disease spread using multi-temporal high spatial resolution imagery[END_REF] have investigated the integration of the SVM technique within an MRF framework for accurate spectral-spatial classification of remote sensing images. All of them use SVMs to estimate class conditional probability density functions and MRFs to estimate contextbased class priors. Farag et al. [START_REF] Farag | A unified framework for map estimation in remote sensing image segmentation[END_REF] have applied the mean fieldbased SVM regression algorithm for density estimation, with the purpose of hyperspectral image classification. Good classification results are reported, although no comparison with other advanced spectral-spatial classification techniques is published.

This letter presents a novel SVM-and MRF-based (SVMMRF) method for spectral-spatial classification of hyperspectral images. In the first step of the proposed method, a probabilistic SVM pixelwise classification of the hyperspectral image is applied. In the second step, spatial contextual information is used for refining the classification results obtained in the first step. This is achieved by means of the MRF regularization. An important difference from previously proposed methods [START_REF] Farag | A unified framework for map estimation in remote sensing image segmentation[END_REF], [START_REF] Bovolo | A context-sensitive technique based on support vector machines for image classification[END_REF], [START_REF] Liu | A spatial-temporal approach to monitoring forest disease spread using multi-temporal high spatial resolution imagery[END_REF] consists in defining and integrating the "fuzzy no-edge/edge" function into the spatial energy function involved in MRFs, aiming at preserving edges while performing spatial regularization. The second contribution of this letter consists in the experimental comparison of the presented approach with other recently proposed advanced spectral-spatial classification techniques. Experimental results are demonstrated on three hyperspectral airborne images recorded by the Airborne Visible/Infrared Imaging Spectrometer (AVIRIS) and the Reflective Optics System Imaging Spectrometer (ROSIS).

The outline of this letter is as follows. In the next section, an SVMMRF classification scheme for hyperspectral images is presented. Experimental results are discussed in Section III. Finally, conclusions are drawn in Section IV.

II. SVMMRF CLASSIFICATION SCHEME

The flowchart of the proposed SVMMRF classification method is shown in Fig. 1. At the input, a B-band hyperspectral image is given, which can be considered as a set of n pixel vectors X = {x j ∈ R B , j = 1, 2, . . . , n}. Let Ω = {ω 1 , ω 2 , . . . , ω K } be a set of information classes in the scene. Classification consists in assigning each pixel to one of the K classes of interest.

A. Probabilistic SVM Classification

The first step of the proposed procedure consists in performing a probabilistic SVM pixelwise classification of the hyperspectral image [START_REF] Vapnik | Statistical Learning Theory[END_REF], [START_REF] Platt | Probabilities for support vector machines[END_REF]. Other probabilistic classifiers could be used. However, SVMs are extremely well suited to classify hyperspectral data [START_REF] Camps-Valls | Kernel-based methods for hyperspectral image classification[END_REF]. The standard SVMs do not provide probability estimates for the individual classes. In order to get these estimates, pairwise coupling of binary probabilistic estimates is applied [START_REF] Platt | Probabilities for support vector machines[END_REF], [START_REF] Wu | Probability estimates for multiclass classification by pairwise coupling[END_REF].

B. Computation of the Gradient

Independent of the previous step, a one-band gradient of the hyperspectral image is computed, which is further used for defining the fuzzy no-edge/edge function. Approaches for defining a one-band gradient from the B-band image are analyzed in [START_REF] Tarabalka | Segmentation and classification of hyperspectral images using watershed transformation[END_REF]. Here, we first compute horizontal, vertical, and two diagonal gradients (corresponding to the directions 0 • , 90 • , 45 • , and 135 • , respectively), using Sobel masks [START_REF] Gonzalez | Digital Image Processing[END_REF], where each of the gradients is computed as the sum of the gradients of every spectral channel. The resulting one-band gradient ∇(X) = {ρ j ∈ R, j = 1, 2, . . . , n} is found as the average of the four obtained directional gradients.

C. MRF-Based Regularization

In the final step, the regularization of the SVM classification map is performed, using the MAP-MRF framework. This framework is based on the interpixel class dependence assumption, which means that a pixel belonging to a class ω i is likely to have neighboring pixels belonging to the same class. In our work, an eight-neighborhood is assumed (let N i be the set of neighbors for a given pixel x i ).

We adopt the Metropolis algorithm, based on stochastic relaxation and annealing, for computing the MAP estimate of the true classification map given the initial (pixelwise) classification map [START_REF] Metropolis | Equations of state calculations by fast computing machines[END_REF], [START_REF] Geman | Stochastic relaxation, Gibbs distributions, and the Bayesian restoration of images[END_REF]. The considered method is based on the Bayesian approach and aims at minimizing the global energy in the image, by iterative minimization of local energies (defined hereafter) associated with randomly chosen image sites, i.e., pixels.

Let L = {L j , j = 1, 2, . . . , n} be a generic set of information class labels for the image X. We propose to compute the local energy of a given site associated with a pixel x i as

U (x i ) = U spectral (x i ) + U spatial (x i ) (1)
where U spectral (x i ) is the spectral energy function from the observed data and U spatial (x i ) is the spatial energy term computed over the local neighborhood N i . We define the spectral energy term as

U spectral (x i ) = -ln{P (x i |L i )} (2)
where P (x i |L i ) is estimated by pairwise coupling of probability estimates from "one-versus-one" SVM outputs [START_REF] Liu | A spatial-temporal approach to monitoring forest disease spread using multi-temporal high spatial resolution imagery[END_REF], [START_REF] Wu | Probability estimates for multiclass classification by pairwise coupling[END_REF].

For the spatial energy term, two different expressions are investigated. We first consider the standard spatial energy expression, used, for instance, in [START_REF] Bovolo | A context-sensitive technique based on support vector machines for image classification[END_REF], which is computed as

U NE spatial (x i ) = x j ∈N i β(1 -δ(L i , L j )) (3)
where andδ(a, b) = 0 otherwise) and β is a parameter that controls the importance of the spatial versus spectral energy terms. The superscript "NE" means that no edge information is taken into account. The term U NE spatial (x i ) is proportional to the number of neighboring pixels of x i assigned to one of the classes different from L i . This spatial energy term is particularly suitable for the images with large spatial structures. However, if a small one-pixel object is present in the image, this model will favor assigning this pixel to the class of the surrounding objects.

δ(•, •) is the Kronecker delta function (δ(a, b) = 1 if a = b,
In order to mitigate this drawback of the previous spatial term and to preserve small structures and edges in the classification map, we propose to integrate the edge information into the spatial energy function. The computation of an accurate edge map for hyperspectral images is a challenging task. For instance, it can be obtained by thresholding the gradient image {ρ j ∈ R, j = 1, 2, . . . , n}. For this purpose, an appropriate threshold must be chosen. Instead of computing the edge map, we propose to define the following "fuzzy no-edge/edge function":

ε (x j ) = 1 - ρ j α + ρ j ( 4
)
where α is a parameter controlling the approximate edge threshold. From here, the following spatial energy function is proposed:

U E spatial (x i ) = x j ∈N i βε(x j )(1 -δ(L i , L j )). (5)
The superscript "E" means that the edge information is taken into account. In the following, we thus refer to two different methods, namely, SVMMRF-NE and SVMMRF-E, when (3) and ( 5) are used for computing the spatial energy, respectively.

We briefly summarize the considered Metropolis algorithm for optimizing the energy function. In each iteration, an image site (i.e., a pixel x i ) is randomly chosen. The local energy of the given site U (x i ) is computed by [START_REF] Chang | Hyperspectral Data Exploitation: Theory and Applications[END_REF]. Then, a new class label L new i is randomly selected for the site x i , and a new local energy U new (x i ) is computed. If the variation of the energy ΔU = U new (x i ) -U (x i ) < 0, the new class label is assigned to x i : L i = L new i . Otherwise, the new class assignment is accepted with the probability p = exp(-ΔU/T ). Here, T is a global control parameter called "temperature" [START_REF] Geman | Stochastic relaxation, Gibbs distributions, and the Bayesian restoration of images[END_REF]. The optimization begins at a high temperature, which is gradually lowered as the relaxation procedure proceeds. This procedure avoids converging to local minima.

III. EXPERIMENTAL RESULTS AND DISCUSSION

We applied the proposed SVMMRF-NE and SVMMRF-E classification approaches to three hyperspectral airborne images described in the following: More information about the images can be found in [START_REF] Tarabalka | Segmentation and classification of hyperspectral images using minimum spanning forest grown from automatically selected markers[END_REF]. In all experiments, the probabilistic one-versus-one SVM classification with the Gaussian radial basis function (RBF) kernel was applied. The optimal parameters C (parameter that controls the amount of penalty during the SVM optimization [START_REF] Vapnik | Statistical Learning Theory[END_REF]) and γ (spread of the RBF kernel) were chosen by fivefold cross validation. The temperature T was varied during the Metropolis relaxation procedure [START_REF] Geman | Stochastic relaxation, Gibbs distributions, and the Bayesian restoration of images[END_REF]: The initial temperature was set to T 1 = 2 (a relatively low value of the initial temperature results in a faster execution of the algorithm). After every 10 6 (order of the number of pixels in an image) iterations, the temperature for the next iteration (k + 1) was recomputed as T k+1 = 0.98T k . The optimal value of the parameter α = 30 was experimentally derived (the same optimal value of α was obtained for the three considered data sets).

Furthermore, we have investigated the performances of the SVMMRF-NE and SVMMRF-E algorithms for different values of the context weight parameter β. Table I reports the SVMMRF-NE and SVMMRF-E overall (percentage of correctly classified pixels) and average (mean of the percentage of correctly classified pixels for each class) classification accuracies for the three considered data sets. It can be concluded that the optimal parameter is β ∈ [START_REF] Chang | Hyperspectral Data Exploitation: Theory and Applications[END_REF][START_REF] Landgrebe | Signal Theory Methods in Multispectral Remote Sensing[END_REF] for the SVMMRF-NE approach and β ∈ [START_REF] Landgrebe | Signal Theory Methods in Multispectral Remote Sensing[END_REF][START_REF] Vapnik | Statistical Learning Theory[END_REF] for the SVMMRF-E approach (for both methods, the corresponding overall accuracies are nonsignificantly different over the given range of values). Moreover, the methods are robust to the choice of β, and quite a wide range of values of β leads to high classification accuracies. 1Table II summarizes the global (overall average accuracies and kappa coefficient [START_REF] Tarabalka | Segmentation and classification of hyperspectral images using minimum spanning forest grown from automatically selected markers[END_REF]) and class-specific classification accuracies for the Indian Pines image. In order to compare the performances of the proposed method with other recently proposed advanced classification techniques, we have included results of the pixelwise SVM classifiers, the well-known ECHO (Extraction and Classification of Homogeneous Object) spatial classifier [START_REF] Kettig | Classification of multispectral image data by extraction and classification of homogeneous objects[END_REF], classification using majority vote within the adaptive neighborhoods defined by watershed segmentation (WH + MV) [START_REF] Tarabalka | Segmentation and classification of hyperspectral data using watershed[END_REF], as well as the results obtained using the construction of a minimum spanning forest from the probabilistic SVMderived markers followed by majority voting within connected regions (SVMMSF + MV) [START_REF] Tarabalka | Segmentation and classification of hyperspectral images using minimum spanning forest grown from automatically selected markers[END_REF]. Fig. 2 shows some of the corresponding classification maps. As can be seen from the table, all the spectral-spatial approaches yield higher classification accuracies when compared to the pixelwise method. The proposed SVMMRF-NE and SVMMRF-E techniques give the highest global and most of the best class-specific accuracies. Following the results of the McNemar's test, the SVMMRF-NE, SVMMRF-E, and SVMMSF + MV accuracies are not significantly different, using 5% level of significance. From Fig. 2, it can be seen that the corresponding three classification maps are comparable and contain more homogeneous regions, when compared to the SVM classification map. Since the considered image contains large spatial structures and reference data do not comprise region edges, the advantage of the SVMMRF-E method versus the SVMMRF-NE method is not obvious here. Table III gives the global classification accuracies for the Center of Pavia data, where the same techniques are used for comparison. The proposed SVMMRF-E method yields the best classification accuracies. This image of an urban area contains small spatial structures, such as shadows and trees. Therefore, the inclusion of the edge information in the context-based regularization improves the classification performances.

Table IV reports the global classification accuracies for the University of Pavia image. For this data set, the SVMMSF + MV classifier gives the best accuracies, and the SVMMRF-E method outperforms the SVMMRF-NE technique in terms of accuracies. According to the results of the McNemar's test, all the corresponding classification maps are significantly different, using 5% level of significance. From these results, the following conclusions can be derived: 1) the advantage of the edge-based SVMMRF-E method for the classification of urban images is confirmed, and 2) the MRF-based regularization includes the spatial context information from only the closest neighborhoods (in our case, eight neighborhoods) when classifying an image. Therefore, the proposed method is efficient only in the case if there is no large misclassified region in the initial pixelwise classification map (this assumption often holds). If such a region exists, the MRF-based method cannot reconstitute its true class label. This happens in the case of classification of the University of Pavia image, where some relatively large regions remain misclassified. The SVMMSF + MV method works differently: If there is a suspicion that a pixel might be misclassified, this pixel remains unclassified, and the classification decision is further taken by the region growing step. This appears to be a robust procedure for classifying large regions with uncertain spectral properties. Furthermore, the proposed SVMMRF-E method was applied and has shown the best classification (overall and average) accuracies at the Third HYPER-I-NET summer school on hyperspectral imaging student contest "Evaluation of an unknown hyperspectral data set and information extraction." The contest was organized by P. Gamba on September 10, 2009, in Pavia, Italy, where the students in teams were supposed to provide a classification map of the rural area acquired by the Compact Airborne Spectrographic Imager sensor.

When comparing the results of several classifiers, an important issue is the computational cost of each classifier. Here, we compare the computational times for classification of the University of Pavia image using different methods. We conducted experiments on an Intel Core 2 Duo 2.40-GHz processor with 3.5-GB RAM. The processing times in seconds were 3339 for the SVM method, 3353 for the WH + MV method, 3351 for the SVMMSF + MV method, 3444 for the SVMMRF-NE method, and 3450 for the SVMMRF-E method. None of the algorithms has been implemented in parallel (which would further speed up computational times). While the SVM classifier is a computationally demanding algorithm, other considered methods require at maximum 3% more time to be executed. In terms of duration, the proposed SVMMRF-NE method takes 93 s longer for the classification of the data than the SVMMSF + MV approach, and the SVMMRF-E method takes 6 s longer than the SVMMRF-NE method.

IV. CONCLUSION

A novel accurate SVMMRF method for spectral-spatial classification of hyperspectral images has been presented in this letter. The method consists in performing a probabilistic SVM pixelwise classification, followed by MRF-based regularization for incorporating spatial and edge information into classification. Experimental results have demonstrated that the proposed method yields accurate classification maps within a short time interval and is sufficiently robust for classifying different kinds of images.

Fig. 1 .

 1 Fig. 1. Flowchart of the proposed SVMMRF classification scheme.

1 )

 1 The Indian Pines image is of a vegetation area that was recorded by the AVIRIS sensor. The image is of 145 by 145 pixels, with a spatial resolution of 20 m/pixel and 200 spectral channels. A three-band false color image and the reference data are shown in Fig. 2. Sixteen classes of interest are considered, which are detailed in Table II, with a number of training and test samples for each class. Training samples have been randomly chosen from the reference data. 2) The Center of Pavia image was recorded by the ROSIS sensor over the urban area of Pavia, Italy. It is of 900 by 300 pixels, with a spatial resolution of 1.3 m/pixel and 102 spectral channels. The reference data contain nine thematic classes and 56 070 labeled pixels. Thirty samples for each class were randomly chosen from the reference data as training samples. 3) The University of Pavia image is of an urban area, acquired by the ROSIS sensor. It is of 610 by 340 pixels, with 103 spectral channels. The reference data contain nine classes of interest. The training and test sets are composed of 3921 and 40 002 pixels, respectively.

Fig. 2 .

 2 Fig. 2. Indian Pines image. (a) Three-band color composite. (b) Reference data. (c) SVM pixelwise classification map. (d) SVMMSF + MV classification map. (e) SVMMRF-NE classification map. (f) SVMMRF-E classification map.

TABLE I SVMMRF

 I -NE AND SVMMRF-E CLASSIFICATION ACCURACIES FOR DIFFERENT VALUES OF THE PARAMETER β TABLE II NUMBER OF LABELED SAMPLES (NUMBER OF SAMPLES) AND CLASSIFICATION ACCURACIES IN PERCENTAGE FOR THE INDIAN PINES IMAGE

TABLE III GLOBAL

 III CLASSIFICATION ACCURACIES IN PERCENTAGE FOR THE CENTER OF PAVIA IMAGE

TABLE IV GLOBAL

 IV CLASSIFICATION ACCURACIES IN PERCENTAGE FOR THE UNIVERSITY OF PAVIA IMAGE

A similar study has shown robustness of the SVMMRF-E method to the choice of the parameter α.

ACKNOWLEDGMENT

The authors would like to thank D. Landgrebe from Purdue University, and P. Gamba from the University of Pavia, for providing the hyperspectral data.

This work was supported in part by the Marie Curie Research Training Network "HYPER-I-NET." Y. Tarabalka is with the Grenoble