Guillem Godoy
email: ggodoy@lsi.upc.edu

Florent Jacquemard
email: florent.jacquemard@inria.fr

Unique Normalization for Shallow TRS

Computation with a term rewrite system (TRS) consists in the application of its rules from a given starting term until a normal form is reached, which is considered the result of the computation. The unique normalization (UN) property for a TRS R states that any starting term can reach at most one normal form when R is used, i.e. that the computation with R is unique. We study the decidability of this property for classes of TRS defined by syntactic restrictions such as linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have height at most one) and shallowness (variables occur at depth at most one in the rules). We prove that UN is decidable in polynomial time for shallow and linear TRS, using tree automata techniques. This result is very near to the limits of decidability, since this property is known undecidable even for very restricted classes like right-ground TRS, flat TRS and also right-flat and linear TRS. We also show that UN is even undecidable for flat and right-linear TRS. The latter result is in contrast with the fact that many other natural properties like reachability, termination, confluence, weak normalization, etc. are decidable for this class of TRS.

Introduction

Term rewriting is a Turing-complete model of computation. Computation with a TRS consists in the application of its rules from a given starting term until a normal form is reached, i.e. a term that cannot be rewritten any more, which is usually considered as the result of the computation.

The unique normalization (UN) property for a TRS R states that any starting term can reach at most one normal form when R is used, i.e. that the computation with R is unique. This property is hence very desirable when dealing with TRS as computation models, and therefore it is important to establish the borders of its decidability.

Other interesting and much studied properties of TRS are reachability (whether a given term can be derived with a given TRS from another given term), joinability (whether two given terms can be rewritten into one common term), termination (whether there are no infinite derivations from any starting term), confluence (whether every two terms derived from a common one can also be rewritten into another common term), weak normalization (whether every term can be rewritten into a normal form), uniqueness of normal forms (whether every term has at most one normal form equivalent to it modulo the equational theory induced by the TRS), etc. Note that a TRS may satisfy the unique normalization property and simultaneously unsatisfy the uniqueness of normal forms property. This is the case of R = {a → b, a → c, c → c, d → c, d → e}, where all terms can reach at most one normal form, but it holds that the normal forms b and c are equivalent.

In the recent years there has been much progress on determining decidability of these fundamental properties for several classes of TRS, which are defined by imposing certain syntactic restrictions on the rules. Some of the restrictions usually taken into consideration are groundness (no variable appears in the rules), linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have height at most one) and shallowness (variables occur at depth at most one in the rules). When these restrictions refer only to one side of the rules, then we talk about left-linearity, right-linearity, left-flatness, etc. Some of the strongest known decidability results are the following. Reachability and joinability are decidable for right-shallow right-linear TRS [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF], and even for weaker restrictions [START_REF] Takai | Right-linear finite path overlapping term rewriting systems effectively preserve recognizability[END_REF]. Termination is decidable for right-shallow rightlinear TRS [START_REF] Godoy | Termination of rewriting with right-flat rules[END_REF] and other variants of syntactic restrictions based on the form of the dependency pairs obtained from a TRS [START_REF] Wang | Decidability of termination for semi-constructor trss, leftlinear shallow TRSs and related systems[END_REF]. Confluence is decidable for shallow right-linear TRS [START_REF] Godoy | Confluence of shallow right-linear rewrite systems[END_REF], and for right-(ground or variable) TRS [START_REF] Godoy | Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure[END_REF]. The weak normalization problem is decidable for left-shallow left-linear TRS [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF], right-shallow linear TRS and shallow right-linear TRS [START_REF] Godoy | On the normalization and unique normalization properties of term rewrite systems[END_REF]. Uniqueness of normal forms is decidable in polynomial time for linear shallow TRS [START_REF] Verma | A polynomial-time algorithm for uniqueness of normal forms of linear shallow term rewrite systems[END_REF].

On the negative side, all of these properties have been proved undecidable for flat TRS [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF][START_REF] Mitsuhashi | The confluence problem for flat TRSs[END_REF][START_REF] Godoy | Termination of rewriting with right-flat rules[END_REF][START_REF] Godoy | Undecidable properties for flat term rewrite systems[END_REF].

The case of the UN property seems to be more difficult. In [START_REF] Verma | A new decidability technique for ground term rewriting systems[END_REF], a polynomial time algorithm is given for UN and TRS with ground rules. On the negative side, UN is undecidable for right-flat and linear TRS [START_REF] Godoy | On the normalization and unique normalization properties of term rewrite systems[END_REF], for right-ground TRS [START_REF] Verma | Complexity of normal form properties and reductions for rewriting problems[END_REF] and for flat TRS [START_REF] Godoy | Undecidable properties for flat term rewrite systems[END_REF]. UN has also been shown undecidable for TRS whose rules have at most height two and, moreover, they are left-flat, right-linear, noncollapsing, or linear and noncollapsing in [START_REF] Verma | New undecidability results for properies of term rewrite systems[END_REF]. In [START_REF] Godoy | On the normalization and unique normalization properties of term rewrite systems[END_REF] the decidability of this problem is left open for flat right-linear TRS.

In this paper, we provide a polynomial time algorithm for deciding UN for shallow and linear TRS (Section 2). We also prove (Section 3) undecidability of UN for flat and right-linear TRS. Our approach for decidability in polynomial time consists in giving a certain characterization of UN. We essentially show that UN is equivalent to the fact that certain regular sets of terms can reach at most one normal form. This characterization can be checked using tree automata techniques. The proof of undecidability is an adequate adaptation of the reductions appearing in [START_REF] Godoy | Termination of rewriting with right-flat rules[END_REF][START_REF] Godoy | Undecidable properties for flat term rewrite systems[END_REF].

Preliminaries

Terms Algebra. We use standard notation from the term rewriting literature [START_REF] Baader | Term rewriting and all that[END_REF]. A signature is a finite set Σ = max Σ i=0 Σ i of function symbols, with i being the arity of symbols in Σ i . Function symbols of arity 0 are called constants. Sometimes we denote a signature as {f 1 : a 1 , . . . , f n : a n } where each f i is a function symbol, and each a i is its corresponding arity. Let V be a set disjoint from Σ whose elements are called variables. The set T (Σ, V) of terms over Σ and V is defined to be the smallest set containing V and such that f (t 1 , . . . , t m ) ∈ T (Σ, V) whenever f ∈ Σ m and t 1 , . . . , t m ∈ T (Σ, V). Var (t) denotes the set of variables occurring in the term t.

The size t of a term t is the number of occurrences of variables and function symbols in t. The height of a term t, denoted as height (t), is 0 if t is a constant or a variable, and 1 + max {height (t 1 ), . . . , height (t m )} if t = f (t 1 , . . . , t m ). The positions of a term t, denoted p, q, are sequences of natural numbers that are used to identify the location of subterms of t. The set Pos(t) of positions of t is defined by Pos(t) = {ǫ} if t is a constant or a variable, and

Pos(t) = {ǫ} ∪ {1.p | p ∈ Pos(t 1 )} ∪. . .∪{m.p | p ∈ Pos(t m )} if t = f (t 1 , . . . , t m )
, where ǫ denotes the empty sequence and p.q denotes the concatenation of p and q. If t is a term and p ∈ Pos(t) a position, then t| p is the subterm of t at position p. More formally, t| ǫ = t and f (t 1 , . . . , t m )| i.p = t i | p . We denote by t[s] p (p ∈ Pos(t)) the term that is like t except that the subterm t| p is replaced by s. More formally, t[s] ǫ = s and f (t 1 , . . . , t m )[s] i.p = f (t 1 , . . . , t i-1 , t i [s] p , t i+1 , . . . , t m ). We can define a partial order ≤ on Pos(t) by p ≤ q if and only if p is a prefix of q, i.e there is a sequence p ′ such that q = p.p ′ . We say that two positions p and q are parallel, denoted p q, if they are incomparable with respect to ≤. Given a position p in a term s, the depth of the occurrence s| p in s is |p|. A substitution is a mapping V → T (Σ, V). Substitutions can also be applied to arbitrary terms by homomorphically extending its application to variables. The application of a substitution σ to a term t, denoted as σ(t), is defined as follows for nonvariable terms: σ(f (t 1 , . . . , t m )) = f (σ(t 1 ), . . . , σ(t m )). A variable renaming is a substitution from variables to variables.

Term Rewriting. An extended rewrite rule, denoted ℓ → r, is a pair of terms ℓ ∈ T (Σ, V) (the left-hand side) and r ∈ T (Σ, V) (the right-hand side). When ℓ is not a variable, and every variable occurring in r occurs also in ℓ, ℓ → r is called a rewrite rule. An extended term rewrite system (extended TRS) R is a finite set of extended rewrite rules. A term rewrite system (TRS) R is a finite set of rewrite rules. A term s rewrites to t in one step at position p (by an extended TRS R), denoted by s ---→ R,p t, if s| p = σ(ℓ) and t = s[σ(r)] p , for some ℓ → r ∈ R and substitution σ. In this case, s is said to be R-reducible. Otherwise s is called an R-normal form. The set of R-normal forms is denoted by NF R . Sometimes we write s --→ R t when p is not important, or s ----→ R,σ,p t, for making the used substitution explicit. The transitive closure, and symmetric and transitive closure of --→ R are denoted as --→ * R and ← --→ * R . When s --→ * R t we say that t is reachable from s, or that s reaches t. When s ← --→ * R t we say that s and t are equivalent. When there exists a term u reachable from s and t, we say that s and t are joinable. When there exists a term u reachable from every term in a set S we say that S is joinable. Given L ⊆ T (Σ), we denote

R * (L) = {t | ∃s ∈ L, s --→ * R t}. The size of R is R = ℓ→r∈R ( ℓ + r ).
A term is linear if no variable occurs more than once in it. A term is shallow if all variables occur at depth at most one. A term is flat if its height is at most one. A rewrite rule ℓ → r is flat (linear, shallow) if ℓ and r are. A rewrite rule ℓ → r is right-flat (right-linear, right-shallow) if r is. A rewrite rule ℓ → r is left-flat (left-linear, left-shallow) if ℓ is. A TRS is flat (linear, shallow) if all its rules are. A TRS is right-flat (right-linear, right-shallow, left-flat, left-linear, leftshallow) if all its rules are. A TRS is uniquely normalizing, or satisfies the unique normalization (UN) property, if for each term s and each two normal forms t 1 and t 2 reachable from s, t 1 = t 2 holds.

Tree Automata. A tree automaton (TA) A over a signature Σ is a tuple (Q, Q f , ∆) where Q is a finite set of nullary state symbols, disjoint from Σ, Q f ⊆ Q is the subset of final states and ∆ is a set of ground rewrite rules of the form: f (q 1 , . . . , q m ) → q, or q 1 → q (ε-transition) where f ∈ Σ m , and q 1 , . . . , q m , q ∈ Q (q is called the target state of the rule). The size of A is

A = f (q1,...,qm)→q∈∆ (m + 2) + q1→q∈∆ (2).
The language of ground terms accepted by a TA A on Σ in a state q is the set

L(A, q) := {t ∈ T (Σ) | t --→ * ∆ q}. The language of A is L(A) := q∈Q f L(A, q)
and a subset of T (Σ) is called regular if it is the language of a TA.

We shall use the following classical properties and problems of TA, see [START_REF] Comon | Tree automata techniques and applications[END_REF] for details.

Proposition 1. Given two TA A 1 and A 2 over the same signature Σ, one can construct in polynomial time two TA recognizing respectively L(A 1 ) ∪ L(A 2 ) and L(A 1 )∩L(A 2 ), whose sizes are respectively linear and quadratic in A 1 + A 2 .

We will consider the two following decision problems for TA:

Problem: Emptiness. Instance: a TA A; Question: L(A) = ∅? Problem: Singleton. Instance: a TA A; Question: |L(A)| = 1? Proposition 2. [2]
The emptiness problem is decidable in linear time. The singleton problem is decidable in polynomial time.

Decidability of UN for Shallow and Linear TRS

In this section we prove that UN is decidable in polynomial time for flat and linear TRS (Theorem 1), and this result is immediately extended to shallow and linear TRS (Theorem 2). ¿From now on, we assume a fixed signature Σ and consider the maximal arity max Σ of its function symbols as a constant. Hence, when analysing complexity of deciding the UN problem, this value is not considered as part of the input. This is a common approach when evaluating complexity for TRS problems (see e.g. the computation of a congruence closure for shallow equations [START_REF] Nieuwenhuis | Basic paramodulation and decidable theories (extended abstract)[END_REF], or the time complexity given for certain problems using tree automata techniques [START_REF] Comon | Tree automata techniques and applications[END_REF]) . This is because, in practice, non-constant function symbols are usually fixed and represent relations with small arity or functions with few parameters, while constants are not fixed and represent the input data of the problem.

After proving some technical lemmas about rewrite reduction with flat and linear TRS in Subsection 2.1, we identify in Subsection 2.2 some necessary and sufficient conditions for UN of such TRS. Finally, in Subsection 2.3 we show how the conditions can be decided by reduction to the above tree automata decision problems.

Preliminary Results

In this subsection, we first present some technical lemmas concerning the rewriting sequences with flat and linear TRS which will be useful in the proof of Theorem 1. They are based on the notion of the use of a position and a derivation which is roughly a form of the descendant of the position. Definition 1. Let R be a flat and linear TRS over Σ. Given a derivation s --→ * R t and a position p ∈ Pos(s), we define use(p, s --→ * R t) recursively on the length of s --→ * R t as follows:

-If s| p ∈ Σ 0 , then use(p, s --→ * R t) := s| p . -If s| p / ∈ Σ 0 and s --→ * R t has length 0, then use(p, s --→ * R t) is undefined. -If s| p / ∈ Σ 0 and s --→ * R t is of the form s ----→ p1,R s ′ --→ * R t for a position p 1 such that p 1 ≥ p or p 1 p then use(p, s --→ * R t) := use(p, s ′ --→ * R t). -If s| p / ∈ Σ 0 and s --→ * R t is of the form s -----→ p1,ℓ→r s ′ --→ * R t
, where p = p 1 .i.p 2 , and ℓ| i ∈ V, we consider two cases. If ℓ| i does not occur in r, then use(p, s --→ * R t) is undefined. Otherwise, if ℓ| i = r| q for some q ∈ Pos(r), then use(p, s --→ * R t) := use(p 1 .q.p 2 , s ′ --→ * R t). Note that all possible cases are considered since R is flat. Moreover, the last one is well (uniquely) defined since R is linear.

Example 1. Let us consider the following flat and linear TRS R 1 = {x + 0 → x, s(0) → c 1 , x + c 1 → s(x), x + y → y + x, s(c 1 ) → 0}, and the derivation:

ρ 1 := 0 + s(0) --→ R1 0 + c 1 --→ R1 s(0) --→ R1 c 1 ,

and let ρ ′

1 be its subderivation starting with 0 + c 1 . We have use(1, ρ 1 ) = 0 and use (2,

ρ 1 ) = use(2, ρ ′ 1 ) = c 1 . 3
The following three lemmas can be easily proved by induction on the length of the rewrite sequences. t, or there exists a position q ∈ Pos(t) such that s

[x] p --→ * R t[x] q and s| p --→ * R t| q .
Lemma 3. For any flat and linear TRS R, derivation s --→ * R t, position p ∈ Pos(s) such that s| p is a certain variable x, and all (new) variable w not occurring in s, either s[w] p --→ * R t or there exists a position q ∈ Pos(t) such that t| q = x and s

[w] p --→ * R t[w] q .
2.2 Necessary and sufficient conditions for UN Definition 2. Let R be a flat and linear TRS over Σ. A fork of R is a pair of terms f (s 1 , . . . , s n ), f (t 1 , . . . , t n ) , for a function symbol f ∈ Σ n (n ≥ 0), such that for all i ∈ {1, . . . , n}, either s i and t i are the same variable of V, or s i is a constant of Σ 0 and t

i --→ * R s i , or t i is a constant of Σ 0 and s i --→ * R t i . Example 2. x + (0 + s(0)), x + c 1 and c 1 + x, s(0) + x
′ , t ′ such that s --→ * R s ′ and t --→ * R t ′ , it holds s ′ = t ′ .
Proof. First, we show that the condition is necessary for unique normalization proceeding by contradiction. Assume that there exists a fork s, t and two different normal forms s ′ and t ′ such that s --→ * R s ′ and t --→ * R t ′ . It suffices to construct a term u reaching both s and t in order to prove that R is not uniquely normalizing. Let s and t be of the form f (s 1 , . . . , s n ) and f (t 1 , . . . , t n ), respectively. We construct u = f (u 1 , . . . , u n ) as follows. For every i in {1, . . . , n}, if s i and t i are the same variable, then we define u i := s i . Otherwise, if s i --→ * R t i then we define u i := s i . Otherwise, t i --→ * R s i holds, and we define u i := t i . It is clear from this construction that u --→ * R s and u --→ * R t hold, and this concludes the proof for the only if direction.

We prove that the condition is sufficient again by contradiction: we assume that R is not uniquely normalizing and then prove the existence of a fork not as in Proposition 3. We choose a term u minimal in size with two distinct normal forms v and w reachable from u. The term u cannot be a variable, since variables cannot be rewritten by R. Hence, u = f (u 1 , . . . , u n ) for some f ∈ Σ n with n ≥ 0. In order to conclude, it suffices to construct a fork s, t and two different normal forms s ′ and t ′ reachable from s and t, respectively.

For the construction of s, t, s ′ and t ′ we proceed iteratively as follows, by initializing them, and modifying them along n steps. The invariant is that s ′ and t ′ are always different normal forms reachable from s, and t, respectively, and that every s| i and t| i are either both the same variable, or both are u| i , or one of them is a constant reachable from u| i and the other is u| i , for i ∈ {1, . . . , n}. At the end of the process, s, t will be a fork.

First, we set s := u, t := u, s ′ := v and t ′ := w. After that, for each i in {1, . . . , n}, we modify the values of s, t, s ′ and t ′ depending on the (un-)definition of use

(i, s --→ * R s ′ ) and use(i, t --→ * R t ′ ). If use(i, s --→ * R s ′ ) is defined to be a constant c, then, by Lemma 1, s[c] i --→ * R s ′ and s| i --→ * R c.
In this case we just set s := s[c] i and leave s ′ , t and t ′ unchanged.

The case where use(i, s --→ * R s ′ ) is undefined but use(i, t --→ * R t ′ ) is defined to a constant is solved analogously to the previous one.

If both use(i, s --→ * R s ′ ) and use(i, t --→ * R t ′ ) are undefined, let x be a new variable not occurring in s nor t. By Lemma 2, either s[x] i --→ * R s ′ , or there exists a position q in Pos(s ′ ) such that s

[x] i --→ * R s ′ [x] q and s| i --→ * R s ′ | q .
(This is also analogously true for t and t ′ .) In any case we set s := s[x] i . In the first case we leave s ′ unchanged and in the second case we let s ′ := s ′ [x] q . We proceed analogously with t and t ′ . Note that both s| i and t| i are now the variable x, and that the new s ′ and t ′ are also normal forms reachable from s and t, respectively. But the preservation of the invariant stating that s ′ and t ′ are still different requires an explanation. They could only be equal if the same position q has been replaced to x in both terms, and in such a case, the old values s ′ | q and t ′ | q must be different. This would imply that the old s| i and t| i reach different normal forms, and hence, u| i can reach two different normal forms. But this is in contradiction with the fact that u is a minimal term in size reaching two different normal forms.

⊓ ⊔

We will use tree automata techniques for checking the condition provided by Proposition 3. But there is a difficulty: with tree automata, we can recognize just ground terms, or terms with variables chosen over a finite set of variables (seen as constants). Fortunately, the condition of Proposition 3 can be simplified by forcing the fork to contain at most two different variables. Proposition 4. Let x, y be two distinct variables. A flat and linear TRS R over Σ is not UN if and only if there exists a fork s, t of R with s, t ∈ T (Σ, {x, y})

and two different R-normal forms s ′ , t ′ such that s --→ * R s ′ and t --→ * R t ′ .
For proving Proposition 4 it suffices to apply some variable renaming to the given fork by making an adequate use of Lemma 3.

Checking the hypotheses of Proposition 4 requires to test an infinite number of forks. In order to obtain a decision procedure for UN based on the notion of forks, we need a finite representation of such infinite sets of forks. For this purpose, we generalize Definition 2 of forks with regular sets of terms (Definition 3 below), and generalize Proposition 4 into Proposition 5 accordingly. In the next definition, we write f (L 1 , . . . , L n ), where f ∈ Σ n and L 1 , . . . , L n ⊆ T (Σ, X) for the set {f (t 1 , . . . , t n ) | t 1 ∈ L 1 , . . . , t n ∈ L n }. Definition 3. Let x, y be two fixed different variables. A fork of languages with respect to a flat and linear TRS R over Σ is a pair L, L ′ of sets of terms of T (Σ, {x, y}) where L and L ′ have the form f (L 1 , . . . , L n ) and f (L ′ 1 , . . . , L ′ n ), respectively, and for every i ∈ {1, . . . , n}, either

L i = L ′ i = {x}, or L i = L ′ i = {y}, or L i = {c} and L ′ i = (R -1 ) * {c} ∩ T Σ, {x, y} , or L ′ i = {c} and L i = (R -1 ) * {c} ∩ T Σ, {x, y} , for some constant c.
Recall that R -1 is not necessarily a TRS, but it is an extended TRS. The following lemma is an immediate consequence of Definition 3 (following the assumption that the maximal arity of a function symbol in Σ is fixed). Lemma 4. The number of forks of languages with respect to a flat and linear TRS R is polynomial in the size of R.

Proof. A fork of languages is determined by choosing a function symbol in Σ n , and by iterating n times the election of either a constant in Σ 0 , placed in one of two component of the fork of languages, or the variable x or the variable y. Thus, there are at most |Σ| • (2|Σ| + 2) max Σ elections. If Σ (and not only max Σ ) is fixed then this is a constant. Otherwise, |Σ| can be assumed bounded by R , and hence, this is a polynomial on R .

⊓ ⊔ Proposition 5. A flat and linear TRS R over Σ is UN if and only if for all fork of languages L,

L ′ with respect to R, if R * (L)∩NF R = ∅ and R * (L ′ )∩NF R = ∅, then R * (L) ∩ NF R = R * (L ′ ) ∩ NF R = {t}, for some term t.
Proposition 5 is a direct consequence of Proposition 4.

Decision of UN

We show now how to decide the condition of Proposition 5, and thus, how to decide UN for flat and linear TRS, using tree automata techniques.

Lemma 5. Given a flat and linear TRS R over Σ ∪ {x, y}, there exists a TA A R on Σ, of size polynomial in the size of R, recognizing NF R ∩ T (Σ, {x, y}). Moreover, A can be computed in polynomial time.

Proof. We construct a TA

A R = (Q, Q f , ∆) where Q = Q f = {q α | α ∈ ((Σ 0 ∪ {x, y}) ∩ NF R )} ∪ {q}
, and ∆ contains one rule α → q α for every q α ∈ Q, and one rule f (q 1 , . . . , q n ) → q for all q 1 , . . . , q n ∈ Q such that the linear term associated to f (q 1 , . . . , q n ) by replacing every occurrence of q c by c, for each c ∈ Σ 0 , and all occurrences of q x , q y and q by distinct variables, is not reducible by R. The identity L(A R ) = NF R ∩ T (Σ, {x, y}) follows by induction on terms for both inclusions. The construction of A takes time proportional to its size, which is

O(|Σ| • (|Σ 0 | + 3) max Σ ). ⊓ ⊔
Note that linearity and flatness are both crucial for the above construction in the given complexity bounds. First, it is known that when R is not left-linear, then NF R is not necessarily a TA language. Second, NF R ∩ T (Σ, {x, y}) is a TA language as soon as R is left-linear, but when R is not flat, there is no polynomial time construction of a TA for NF R with a polynomial number of states. This is a consequence of the EXPTIME lower bound for the ground reducibility of a linear term wrt a linear TRS [START_REF] Comon | Ground reducibility is EXPTIME-complete[END_REF]. The following lemma can be proved using a construction in [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF] (Lemma 5.11). Lemma 6. Given a TA A over Σ ∪ {x, y} and an extended flat and linear TRS R over Σ, there exists a TA of size polynomial in R + A , recognizing R * L(A) ∩ T (Σ, {x, y}), which can be constructed in polynomial time.

There exists a TA construction for larger classes of extended TRS than flat and linear, like right-shallow and right-linear TRS [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF]. We focus on the flat and linear case here for complexity reasons. Nevertheless, as we shall see later, UN is undecidable for these larger classes of TRS.

Example 3. The TA A ′ 0 = {q 0 , q c1 }, {q 0 }, ∆ recognizes R -1 1 * ({0}) ∩
T (Σ, {x, y}), for the TRS R 1 of Example 1, where ∆ contains 0 → q 0 , c 1 → q c1 , s(q 0 ) → q c1 , s(q c1 ) → q 0 , q 0 + q 0 → q 0 , q c1 + q c1 → q 0 , q 0 + q c1 → q c1 and q c1 + q 0 → q c1 . 3

Now we shall use the above results for the decision of the sufficient condition for UN given in Proposition 5. The following lemma is a direct consequence of Lemma 6.

Lemma 7. Let R be a flat and linear TRS over Σ. For each fork of languages L, L ′ with respect to R, L and L ′ are recognized by two TA over Σ∪{x, y} whose respective sizes are polynomial in the size of R, and which can be constructed in polynomial time. Now, we have all the ingredients to prove the main result of the paper.

Theorem 1. UN is decidable in polynomial time for flat and linear TRS.

Proof. Let R be a flat and linear TRS over Σ. We construct first a TA A R over Σ ∪ {x, y} recognizing NF R ∩ T (Σ, {x, y}), and whose size A R is polynomial in the size of R, following Lemma 5. Now, for each fork of languages L, L ′ with respect to R, we perform the following test. Let A and A ′ be two TA of size polynomial in the size of R, recognizing respectively L and L ′ (constructed according to Lemma 7).

1. Construct two TA recognizing respectively R * (L) and R * (L ′ ). According to Lemma 6, their sizes are polynomial in the size of R. 2. Construct two TA recognizing respectively R * (L) ∩ NF R and R * (L ′ ) ∩ NF R , using the TA constructed at the above step and the above A R . According to Proposition 1, the sizes of these two TA are still polynomial in the size of R.

3. If one of the languages R * (L)∩NF R or R * (L ′ )∩NF R is empty (this emptiness test is performed in polynomial time, according to Proposition 2) then the test passes successfully. 4. Otherwise, check whether both languages R * (L) ∩ NF R and R * (L ′ ) ∩ NF R are singleton sets (this test is performed in polynomial time according to Proposition 2). If it is not the case, the test fails. Otherwise, we construct a TA recognizing their intersection and the test succeeds iff its language is not empty (the construction and emptiness test can still be performed in polynomial time).

According to Proposition 5, R is UN iff all fork of languages with respect to R pass the test. According to Lemma 4, there will be a polynomial number of such tests, and following the above evaluation, each test is performed in polynomial time. Altogether, the upper bound on the complexity of deciding UN is polynomial.

⊓ ⊔

This result can be immediately extended to shallow TRS thanks to the following proposition given in [START_REF] Verma | A polynomial-time algorithm for uniqueness of normal forms of linear shallow term rewrite systems[END_REF]. Proposition 6. Given a shallow and linear TRS R over Σ, there exists a flat and linear TRS R ′ on an extended signature Σ ′ ⊇ Σ such that R ′ is UN iff R is UN. Moreover, the size of R ′ is polynomial in the size of R, and can be computed in polynomial time.

As a consequence of Theorem 1 and Proposition 6 we conclude decidability of UN in polynomial time for shallow and linear TRS.

Theorem 2. UN is decidable in polynomial time for shallow and linear TRS.

3 Undecidability of UN for Flat and Right-Linear TRS Some undecidability results for UN have been recalled in the introduction. In particular, UN is undecidable for right-flat and linear TRS [START_REF] Godoy | On the normalization and unique normalization properties of term rewrite systems[END_REF]. Thus, the result of Theorem 1 is no longer valid if we relax the assumption on flatness for the left-hand sides of rules. In this section, we show that one can neither relax the assumption on linearity for left-hand sides of rules in Theorem 1. More precisely, we prove (Theorem 3 below) undecidability of UN for flat and right-linear TRS. This result is in contrast with other properties like reachability, joinability, confluence, termination and weak normalization which are all decidable for flat and right-linear TRS [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF][START_REF] Godoy | Confluence of shallow right-linear rewrite systems[END_REF][START_REF] Godoy | Termination of rewriting with right-flat rules[END_REF][START_REF] Godoy | On the normalization and unique normalization properties of term rewrite systems[END_REF] (and in some cases for weaker restrictions). The proof involves a reduction from the Post correspondence problem (PCP) restricted to nonempty strings over a fixed finite alphabet Γ .

Problem: restricted-PCP (rPCP). Instance: a sequence of pairs of words u 1 , v 1 . . . u n , v n , with ∀i ≤ n, u i , v i ∈ Γ * \ ǫ. Question: is there a non-empty sequence of indexes 1 ≤ i 1 , . . . , i k ≤ n such that u i1 . . .

u i k = v i1 . . . v i k ?
The rPCP is known to be undecidable [START_REF] Sipser | Introduction to the Theory of Computation[END_REF]. We call solution of a rPCP instance a non-empty sequence of indexes that gives a positive answer to the above question.

Example 4. The instance of rPCP ab, a , c, bc has a solution obtained by choosing the pairs 1 and 2 consecutively, obtaining abc at both sides. 3

In the proof of the undecidability theorem below, we assume a given instance u 1 , v 1 . . . u n , v n of rPCP that is, u i , v i are nonempty strings over the alphabet Γ . The j'th symbol of u i and v i , whenever they exist, are denoted by u ij and v ij respectively. For the sake of readability, we shall sometimes write terms made of symbols of arity 0 and 1 as words over the same symbols. Theorem 3. UN is undecidable for flat and right-linear TRS.

The additional symbols f , 0 and 1 are used in the next crux rewrite rules, which act as checkers for solutions, in order to ensure the correctness of the reduction. R f := {f (U, V, x, y, x, y, x, y) → 0, f (x, y, A, P, x, x, y, y) → 1} Finally, the last TRS R n will ensure that 0 and 1 are the only non variable terms in normal form.

R n := c → c | c ∈ Σ 0 \ {0, 1} ∪ {h(x) → h(x) | h ∈ Σ 1 } ∪ {f (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 ) → f (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 )}
To summarize, the TRS R on Σ is defined by:

R := R A ∪ R s ∪ R ′′ U ∪ R ′′ V ∪ R P ∪ R c ∪ R f ∪ R n .
Note that all the rules of R are flat, all the rules of R \ R f are linear, and the rules in R f are right-ground. Theorem 3 follows immediately from Lemmas 15 and 8 below, which ensure respectively the correctness and completeness of the reduction of the instance rPCP into the non-UN of R.

Lemma 8. If the given rPCP instance has a solution then R is not UN.

Proof. We assume a solution i 1 , . . . , i k of the rPCP instance, and show that there exists a term s ∈ T (Σ) such that 0 ← -- * R s --→ * R 1. It permits us to conclude since 0 and 1 are R-normal forms.

Let w = u i1 . . . u i k ⊥ = v i1 . . . v i k ⊥, and let (s U , s V ) be a carrier of the solution, and s ′′ U , s ′′ V , s P be copies defined as follows.

s U := U i11 . . . U i1L . . . U i k 1 . . . U i k L ⊥ s ′′ U := U ′′ i11 . . . U ′′ i1L . . . U ′′ i k 1 . . . U ′′ i k L ⊥ s P := P i11 . . . P i1L . . . P i k 1 . . . P i k L ⊥ s V := V i11 . . . V i1L . . . V i k 1 . . . V i k L ⊥ s ′′ V := V ′′ i11 . . . V ′′ i1L . . . V ′′ i k 1 . . . V ′′ i k L ⊥ s := f (U, V, A, P, s U , s U , s V , s V ) It is easy to verify U ---→ * R ′′ U s ′′ U ←-- * Rc s U and V ---→ * R ′′ V s ′′ V ←-- * Rc s V .
Moreover, A, s U and s V rewrite to w using R A and R s . Also, P , s U and s V rewrite to s P using R P and R c . Therefore, there exist derivations s --→ * R f (U, V, w, s P , w, s P , w, s

P ) ---→ R f 0 and s --→ * R f (s ′′ U , s ′′ V , A, P, s ′′ U , s ′′ U , s ′′ V , s ′′ V ) ---→ R f 1 and this concludes the proof. ⊓ ⊔
Lemma 15 is slightly more difficult and requires some additional definitions and intermediate lemmas for its proof. For space reasons, they are given below withour proof.

Given a word w, we define indexes(w) to be the word obtained by applying to w the morphism ϕ defined as ϕ(

U i1 ) = ϕ(U ′′ i1 ) = ϕ(V i1 ) = ϕ(V ′′ i1 ) = ϕ(P i1 ) = i and
ϕ(h) = ǫ for any other symbol h. Note that two copies of the same carrier will have the same indexes. We say that a word wα is a

generator if α is in {U, V, A, P, U ′ ij , V ′ ij , P ′ ij |i ∈ [1..n], j ∈ [1.
.L]}. Otherwise, if α is ⊥, we say that wα is a non-generator. We define Σ c as the subset of Σ 1 of the unary symbols h for which there exists a collapsing rule h(x) → x in R, i.e. Σ c contains all U ij such that j > |u i |, and all V ij such that j > |v i |. For any term t define clean(t) recursively as follows. If the top symbol h of t is in Σ c then we define clean(t) = clean(t| 1 ). Otherwise, we define clean(t) = t. In other words, clean(wα) removes from t the longest prefix of unary symbols with all them in Σ c . Lemma 12. Let w 1 ⊥ and w 2 ⊥ be two non-generator words. Let α be either U or V or P . If {w 1 ⊥, w 2 ⊥, α} is R-joinable, then indexes(w 1 ) = indexes(w 2 ). Lemma 13. Let w 1 ⊥ be a non-generator word joinable with U . Let w 2 ⊥ be a word reachable from w 1 ⊥ and such that w 2 ∈ Γ * . If i 1 , . . . , i k = indexes(w 1 ) then w 2 = u i1 . . . u i k .

The following lemma is the analogous to the previous lemma, but with V 's and v's instead of U 's and u's. Lemma 14. Let w 1 ⊥ be a non-generator word joinable with V . Let w 2 ⊥ be a word reachable from w 1 ⊥ and such that w 2 ∈ Γ * . If i 1 , . . . , i k = indexes(w 1 ) then w 2 = v i1 . . . v i k . Now, we have all the necessary ingredients for proving Lemma 15.

Lemma 15. If R is not UN then the given rPCP instance has a solution. Proof. Let s be a term in T (Σ, V), minimal in size, such that s ′ ← -- * R s --→ * R s ′′ where s ′ and s ′′ are two distinct R-normal forms. Note that only 0, 1 and variables are R-normal forms. The term s is not rooted by a symbol in Σ \ (Σ c ∪ {f, 0, 1}): otherwise it could not reach a R-normal form, because of the rules of R n and because such symbols cannot be removed.

Assume that s is rooted by a symbol h in Σ c . Thus, s is of the form h(s 1 ) for some term s 1 . Then in both derivations s --→ * R s ′ and s --→ * R s ′′ , the rule h(x) → x is applied at the root position. Hence, the term s 1 also reaches s ′ and s ′′ with R, contradicting the minimality of s.

Assume that s is rooted by 0 or 1 or a variable. It means that s is directly 0 or 1 or a variable. Any of these terms is a normal form, and this is in contradiction with the fact that s reaches two different R-normal forms.

From the above observations it follows that s is of the form f (s 1 , s 2 , s 3 , s 4 , s 5 , s 6 , s 7 , s 8 ) for some terms s 1 , . . . , s 8 . Since no variable is reachable from a term of this form (there is no collapsing rule in R with a f at the top of its left-hand side), we conclude that s ′ = 0 and s ′′ = 1, or vice-versa. Thus,

Lemma 1 .

 1 For any flat and linear TRS R, derivation s --→ * R t, position p ∈ Pos(s) and all constant c, if use(p, s --→ * R t) = c, then s[c] p --→ * R t and s| p --→ * R c. Lemma 2. For any flat and linear TRS R, derivation s --→ * R t, position p ∈ Pos(s) such that use(p, s --→ * R t) is undefined, and all variable x, either s[x] p --→ * R

Lemma 9 .

 9 Let s and t be terms satisfying s--→ * R t. Then clean(s) --→ * R clean(t). Lemma 10. If s --→ * R U then clean(s) = U ; if s --→ * R V then clean(s) = V ; if s --→ * R A then clean(s) = A; if s --→ * R P then clean(s) = P . Lemma 11.A word wα is necessarily a non-generator if both {wα, U } and {wα, A}, or both {wα, V } and {wα, A}, or both {wα, U } and {wα, P }, or both {wα, V } and {wα, P } are joinable.

  are forks of the TRS R 1 given in Example 1.

3 Proposition 3. A flat and linear TRS R over Σ is UN if and only if for each fork s, t of R and every R-normal forms s

The first author was supported by Spanish Min. of Educ. and Science by the FOR-MALISM project (TIN2007-66523) and by the LOGICTOOLS-2 project (TIN2007-68093-C02-01)

We shall define a TRS R such that the given rPCP instance has a solution iff R is not uniquely normalizing. The TRS R is defined as the union of several flat and right-linear TRS. The role of these sub-TRS is described below, as well as the signature they are based on.

We will represent the words of Γ * by string terms of T Σ A \ {A} where Σ A := {γ : 1 | γ ∈ Γ } ∪ {A : 0, ⊥ : 0}. These terms are generated by a regular tree grammar with a single non-terminal symbol (the constant A), and whose production rules are the rules of the TRS R A below.

Intuitively, we associate to a sequence i 1 , . . . , i k the pair made of the terms

which we call a carrier of the sequence. The following TRS permits to recover a solution (or more precisely the terms u i1 . . . u i k and v i1 . . . v i k that must be equal) from a carrier.

Let us now consider several copies of the terms in carriers of solutions, built over the following signatures:

The regular grammars generating copies of carriers, using the above (nullary) non-terminal symbols U , V and P , are called respectively R ′′ U , R ′′ V and R P .

The following TRS casts carrier of solutions into copies.

Let us now define the signature

the two rules of R f are applied at the root position in the derivations from s and we have the following rewrite sequences:

Note that only rewrite steps with f (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 ) → f (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 ) occur at the root position in the two above diagonal rewrite sequences. This implies that each subterm at depth 1 in f (s 1 , s 2 , s 3 , s 4 , s 5 , s 6 , s 7 , s 8 ) reaches the subterm at depth 1 in f (U, V, s 0 3 , s 0 4 , s 0 3 , s 0 4 , s 0 3 , s 0 4 ) located at the same position, and also the subterm at depth 1 in f (s 1 1 , s 1 2 , A, P, s

2 ) located at the same position. By Lemma 9, we can assume without loss of generality that any subterm t at depth 1 in any of those three terms satisfies clean(t) = t. Moreover, by Lemma 10, it follows s 1 = U , s 2 = V , s 3 = A and s 4 = P . This implies the following facts.

-U and s 5 are joinable, and s 5 and A are joinable, and hence, by Lemma 11, s 5 is a non-generator. Similarly, s 6 , s 7 and s 8 are non-generators. -{U, s 5 , s 6 } is joinable, and hence, by Lemma 12, indexes(s 5 ) = indexes(s 6 ).

Similarly, indexes(s 7 ) = indexes(s 8 ), and indexes(s 6 ) = indexes(s 8 ). Let i 1 , . . . , i k be indexes of any of them. -{U, s 5 } is joinable, and {A, s 5 } is joinable to a word s 0 3 of the form w⊥ such that w ∈ Γ * . Hence, by Lemma 13, w = u i1 . . . u i k . Similarly, {V, s 7 } is joinable, and {A, s 7 } is joinable to the same s 0 3 = w⊥. Hence, by Lemma 14, w = v i1 . . . v i k . Thus, u i1 . . . u i k = v i1 . . . v i k .

From the above facts, it follows that i 1 , . . . , i k is a solution of the given rPCP instance.

⊓ ⊔

Conclusion

We have shown that UN is decidable in polynomial time for shallow and linear TRS (Theorem 2), and is undecidable for flat and right-linear TRS (Theorem 3). With these results, the problem of decidability of UN for classes of TRS defined by syntactic restrictions like linearity, flatness or shallowness is essentially closed. Perhaps, one could still consider this problem for other variants of syntactic restrictions based on the form of the dependency pairs obtained from a TRS, like the ones given in [START_REF] Wang | Decidability of termination for semi-constructor trss, leftlinear shallow TRSs and related systems[END_REF].


Silvia Valero

Philippe Salembier

Jocelyn Chanussot

New hyperspectral data representation using binary partition tree

Keywords: Hyperspectral imaging, Binary Partition Tree, segmentation, classification

The optimal exploitation of the information provided by hyperspectral images requires the development of advanced image processing tools. This paper introduces a new hierarchical structure representation for such images using binary partition trees (BPT). Based on region merging techniques using statistical measures, this region-based representation reduces the number of elementary primitives and allows a more robust filtering, segmentation, classification or information retrieval. To demonstrate BPT capabilites, we first discuss the construction of BPT in the specific framework of hyperspectral data. We then propose a pruning strategy in order to perform a classification. Labelling each BPT node with SVM classifiers outputs, a pruning decision based on an impurity measure is addressed. Experimental results on two different hyperspectral data sets have demonstrated the good performances of a BPT-based representation

INTRODUCTION

Recent advances in remote sensing and geographic information has led the way for the development of hyperspectral sensors which produce a data cube of hundreds of contiguous waveband images. Therefore, each pixel is represented by a spectrum related to the light absorbing and/or scattering properties of the spatial region that it represents. Given the wide range of real-life applications, great deal of research is invested in the field of hyperspectral image segmentation. The segmentation of these images is a key step in their analysis. Unfortunately, hyperspectral image processing is still a difficult endeavor due to the huge amount of data involved. Consequently, most of the standard segmentation methods fail. In the literature, different segmentation algorithms based on morphological profiles [START_REF] Pesaresi | Classification and feature extraction for remote sensing[END_REF], endmember extraction [START_REF] Plaza | Advanced Processing of Hyperspectral Images[END_REF], Markov random fields [START_REF] Marroquin | Hidden Markov Measure Field Models for Image Segmentation[END_REF], Bayesian segmentation [START_REF] Li | Semi-supervised hyperspectral image segmentation[END_REF] and hierarchical segmentation [START_REF] Gualtieri | Hierarchical Segmentation of Hyperspectral Data[END_REF] have been proposed. The goal of segmentation (in particular for all the algorithms mentioned before) is to compute a partition from a pixel-based representation of the image. This approach has two drawbacks: 1) The segmentation cannot be generic and also reliable. In fact, it has to depend on the application. 2) The initial pixel-based representation is too low level which implies that the segmentation algorithm is quite complex or not very robust. To tackle these issues, we would like to define a new data representation which represents a first abstraction from the pixel-based representation and that is multiscale to be able to cover a wide range of applications. Binary Partition Tree (BPT) is one example of such representations. Having a rather generic construction (more or less application independent), they can be interpreted as a set of hierarchical regions stored in a tree structure. Note that from the tree representation, many partitions can be extracted for various applications. The processing of BPT will then involve an application dependant pruning strategy. Hence, we propose BPT as a new region-based hierarchical representation [START_REF] Salembier | Binary partition tree as an efficient representation for image processing, segmentation, and information retrieval[END_REF] for hyperspectral images. In the case of remote sensing hyperspectral data, different prunings can be suitable for filtering, classification and segmentation purposes. As a first instance, we present here a pruning strategy aiming at a classification of the image. The organization of this paper is given as follows: Section 2 gives a brief introduction on BPT, explaining the details of its construction. The BPT pruning for classification is discussed in section 3. Experimental results are shown in section 4. Finally, conclusions are drawn in section 5.

CONSTRUCTION OF THE BPT

Binary Partition Tree (BPT) is a hierarchical representation of a set of regions obtained from an initial partition. The tree leaves correspond the regions of the initial partition and the remaining tree nodes represent regions formed by the merging of two children regions.The root node represents the entire image support. The tree construction is performed by keeping track of merging steps of an iterative region merging algorithm (see Fig. 1). The creation of BPT implies two important notions. On one hand, the merging criterion O(Ri, Rj) between two adjacent regions Ri and Rj, on the other hand, the region model M Ri . The merging criterion defines the similarity of neighboring regions and hence determines the order in which regions are 80 978-1-4244-9566-5/10/$26.00 ©2010 IEEE IGARSS 2010

going to be merged. The region model specifies how regions are represented and how to model the union of two regions. Nevertheless, the definition of O(Ri, Rj) as a similarity measure between two hyperspectral regions nodes is not an easy issue. In the literature, some distances such as Spectral Angle Mapper or Spectral Information Divergence have been proposed to measure spectral similarity. However, their use as O(Ri, Rj) is not straightforward as each region is made of several pixels and therefore several spectra. To overcome this problem, past approaches [START_REF] Gualtieri | Hierarchical Segmentation of Hyperspectral Data[END_REF] have assumed that M Ri is a constant, representing the regions by their mean spectrum. With this approach, the interclass spectral variability induced by natural variations, noise and mixed pixels is overlooked. In order to take into account this spectral variability within regions, we propose to model each band of the region spectrum by its probability density function [START_REF] Calderero | General region merging approaches based on information theory statistical measures[END_REF].

Region Model

Working with N bands, the region model consists of N histograms representing for each band the empirical distribution of the pixels belonging to the region. Consequently, the region model M Ri is given by

M Ri = {P 1 Ri , P 2 Ri , ..., P N Ri } (1)
where P k Ri is the empirical distribution of the region Ri in the band k which is formed by

P k Ri = {P k Ri (a 1 )P k Ri (a 2 ), ....P k Ri (a |χ| )} (2)
being a i the possible values of the pixels in each band k. We must remark that this region model can also be defined when tree leaves are single pixels by exploiting the image self-similarity. Indeed, the probability density function for individual pixels can be estimated and the precise modeling of the pixels pdf is important in order to get very precise region contours [START_REF] Dimicolli | Hierarchical regionbased representation for segmentation and filtering with depth in single images[END_REF].

Merging criterion: Bhattacharyya coefficient

For each band k of each region R, the model P k R is an empirical discrete probability distribution. Accordingly, the Bhattacharyya coefficient [START_REF] Calderero | General region merging approaches based on information theory statistical measures[END_REF] can be used to measure the similarity between two adjacent regions R i and R j of a given band k. Theorically, this measure is defined by:

BC(P k Ri , P k Rj ) = -log( |χ| j=1 P Ri(k) (a j ) 1 2 P Rj(k) (a j ) 1 2 ) (3)
Existing a perfect overlap between both probability distributions, the Bhattacharyya coefficient will be 0. Consequently, a merging criterion of a pair of adjacent regions can be defined as the minimum sum of the N dissimilarity measures obtained for the different bands.

O(R i , R j ) = argmin Ri,Rj N -1 k=0 BC(P k Ri , P k Rj ) (4)
Experimentally, we have observed that the criterion of Eq. 4 does not assure that the areas of the regions tend to increase as the number of regions into the partition decreases. Then, in order to avoid small and meaningless regions into the generated partitions, the merging of very small regions has to be favored. To this goal we introduce a regularization term based on the size of the regions.

O(R i , R j ) = min( N Ri , N Rij )O(R i , R j ) (5)
Note that we propose to use the square root of the minimum area. To conclude this section, we must let us mention that the merging criterion defined by Eq. 4 simply adds the contribution of the various bands without exploiting their mutual information. Future works will analyze how this mutual information between bands can be used in the merging criterion.

BPT PRUNING

In this section, we discuss an example of tree processing for a classification application. The processing can be seen as a tree pruning step the goal of which is to remove subtrees composed of nodes belonging to the same class. To perform this task, we analyze the tree starting from the leaves and moving along the branches to select the nodes of largest area that involve pixels belonging to a unique class. As a first step, we measure a specific region descriptors for each node R i along the tree structure. These values are used to compute an increasing cost C associated to each BPT node. The increasingness of C along the branches guarantees that removing nodes having a cost lower than given threshold leads to a pruning. The choice of region descriptors is determined by the application. In our case, the BPT pruning is focussed on the hyperspectral data classification. Hence, we propose a pruning strategy populating the nodes with the density probability function of belonging to each class. Such a task can be achieved using a multi-class classifier output. Here, we use Support Vector Machine as a classifier which has demostrated its advantages in high dimensional data. We note that being supervised, SVM needs firstly to construct a model to be able to classify the data. Then, we start constructing the model by training the SVM classifier using some leaves nodes according to the available ground truth. After the model construction, modelling each R i by its mean spectrum, all nodes are populated by their class probability estimation Cp Ri and their predicted class Class Ri . Using Cp Ri values, we define an increasing iterative cost C along tree branches using a node impurity measure. The impurity of a node is interpreted by how mixed is the node, that is, the proportion of elements of different classes in the same region. To measure that, we propose a popular impurity function such as the entropy. Therefore, merging R i at level l, the cost associated to R i is computed using the following equation:

C(R i ) = C - Nc t=0 Cp Ri (t) log(Cp Ri (t)) (6)
where N c is the number of classes and C is the maximum cumulative cost until the l -1 branch level. It should be noticed that measuring the sum of all the impurities, a maximum threshold λ should be set to determine the last pure node. Thus, a node R i is removed if C(R i ) < λ and if all its ancestors also satisfy this condition. After tree pruning, we construct the classification map by selecting the lower nodes of the resulting pruned tree. Regions contained in these nodes are labelled by the Class Ri which has been assigned by the SVM classifier in the tree population.

EXPERIMENTAL RESULTS

Experiment with AVIRIS Indian Pines

In our first experiment, Indian Pines AVIRIS hyperspectral data containing 200 spectral bands having a spatial dimension of 145 X 145 pixels is used. The whole image is formed by 16 different classes having an available ground truth. Before constructing BPT as detailed in Section 2, some parameters such as the number of bins N bins used to represent P k R should be set. In our case, having different ranges of values in each chanel, we set N bins as the minimum range difference found in the image (N bins =46). Once the BPT has been created, we train the SVM classifier selecting randomly 30% of samples for each class from the reference data. After that, Cp R and Class R values are assigned to each node to perform the pruning task. In this pruning step, we should set λ in order to define the maximum impurity cost allowed along BPT branches. After some experimental tests, we set λ=20. Fig. 2 compares the obtained results using the BPT pruning against a classical SVM pixel classification. The same training samples are used for both classification methods. In this second experiment, data from the ROSIS-03 optical sensor over the University of Pavia is presented. The image is formed by 103 denoised channels possesing 610 X 340 pixels. In this work, due to space limitations, only the top-down corner of this image is considered.

For this example, we should increase N bins to 100 considering that this second data has a smaller spatial resolution (1.3 m per pixel). Although the merging criterion is not strongly dependent of the N bins , it is better to take it into account. It can be observed that, using the BPT, a better classification map is also obtained for this second data set . Despite of the improvement, some noise is still present in the results. This implies that our pruning criterion can be improved. Regarding the global accuracy, the simple SVM classifier reaches 90.68 % whereas our proposed BPT pruning achieves 95.19%. It should be observed that BPT pruning improves the classification accuracy preserving most of the edges and shapes.

CONCLUSIONS

In this work, Binary Partition Trees have been proposed as a new representation for hyperspectral images. Obtained through a recursive region merging algorithm, they can be interpreted as a new region-based and hierarchical representation of the hyperspectral data. The main advantatge of BPT is that it can be considered as a generic representation. Hence, it can be constructed once and used for many applications. Many tree processing techniques can be formulated as pruning strategies. Concerning the BPT construction, a solution for the problem of the spectra variability for clustering hyperspectral data has been proposed using statistical region models. BPT enables the extraction of a hierarchically structured set of regions representing a semantic content of the image. As a first example of BPT processing, we have proposed and illustrated a pruning strategy to classify the hyperspectral data. Experimental results have shown that the proposed method improves the classification accuracies of a classical SVM, providing classification maps with a reduced amount of noise. Future work will be conducted for improving the merging criterion given that information between bands is not introduced in our similarity measure. Regarding the pruning strategy, new techniques are currently being studied to improve the accuracy and the robustness of the segmentation results.

Fig. 1 .

 1 Fig. 1. Example of BPT construction

Fig. 2 .

 2 Fig. 2. Obtained classification map. Left: SVM result. Right: Pruning BPT result

  Fig. shows the results obtained after applying BPT pruning.

Fig. 3 .

 3 Fig. 3. Obtained classification map. Left: SVM result. Right: Pruning BPT result

Table 1 .

 1 Class Specifical Accuracy in percentage

	Class	Simple SVM Pruned BPT
	1	86.11	94.44
	2	88.39	93.41
	3	83.45	89.03
	4	77.56	80.77
	5	95.18	92.77
	6	97.39	98.39
	7	83.33	88.89
	8	97.85	99.08
	9	64.29	100
	10	84.98	88.70
	11	91.19	96.72
	12	92.93	93.66
	13	100	98.59
	14	96.99	99.42
	15	67.72	98.43
	16	95.30	100
	Overall	87.67	94.52


Silvia Valero

Philippe Salembier

Jocelyn Chanussot

COMPARISON OF MERGING ORDERS AND PRUNING STRATEGIES FOR BINARY PARTITION TREE IN HYPERSPECTRAL DATA

Keywords: Binary Partition Tree, Hyperspectral data Segmentation, Merging orders, Pruning strategies

Hyperspectral imaging segmentation has been an active research area over the past few years. Despite the growing interest, some factors such as high spectrum variability are still significant issues. In this work, we propose to deal with segmentation through the use of Binary Partition Trees (BPTs). BPTs are suggested as a new representation of hyperspectral data representation generated by a merging process. Different hyperspectral region models and similarity metrics defining the merging orders are presented and analyzed. The resulting merging sequence is stored in a BPT structure which enables image regions to be represented at different resolution levels. The segmentation is performed through an intelligent pruning of the BPT, that selects regions to form the final partition. Experimental results on two hyperspectral data sets have allowed us to compare different merging orders and pruning strategies demonstrating the encouraging performances of BPT-based representation.

INTRODUCTION

A hyperspectral image is set of hundred of images I λ (p) where λ ∈ {1, , N} indexes the spectral band wavelength and p indicates the spatial pixel position. This whole set of images can be seen as a three dimensional data cube where each pixel is represented by the spectrum related to the light absortion and/or scattering properties of the spatial region that it represents. During the last years, the segmentation of these images in meaningful regions has remained a challenging problem due to the huge amount of information contained in their high dimensionality. Thus, new segmentation techniques for hyperspectral data based on morphological profiles [START_REF] Plaza | Advanced Processing of Hyperspectral Images[END_REF], Bayesian segmentation [START_REF] Li | Semi-supervised hyperspectral image segmentation[END_REF] and hierarchical segmentation [START_REF] Gualtieri | Hierarchical Segmentation of Hyperspectral Data[END_REF] have been published in the recent years. These approaches compute a partition directly from a pixel-based representation of the image which is generally not robust for two following main reasons. First, the pixels may be corrupted by noise and second, the observation scale is too low to have a good estimation of local as well as global properties. Therefore, we propose to firstly develop a multiscale and region-based representation of the image and, in a second step, to derive the final partition from this representation. Note that this representation is based on regions which will allow a robust estimation of the parameters representing the properties of the data. Moreover, the representation is multiscale: this provides both a local and a global view on the data. For such a representation, we propose the Binary Partition Tree (BPT) [START_REF] Salembier | Binary partition tree as an efficient representation for image processing, segmentation, and information retrieval[END_REF], which stores hierarchically a region-based representation in a tree structure.

The BPT construction is often based on an iterative region merging algorithm. Therefore, a good similarity metric is needed to establish the merging order between regions. Working with hyperspectral data, the definition of a spectral similarity distance is not straighforward. Theoretically, the best classical distances between spectra are based on the overall shape of the reflectance curve. In order to compute a distance between regions, a model for each region must firstly be defined. The simplest solution is to use a first order model: the mean. Hence, classical spectral distances between the mean of each region can be used. Unfortunately, some limitations may come from the poor modeling based on the mean due to the high spectral variability of the pixels belonging to the same class. Therefore, this paper investigates alternative models. We propose to use the histogram as a non parametric model of each region. This requires the definition of a robust distance between histograms. Once the BPT is constructed, the final partition can be extracted by a pruning strategy which should select the most interesting regions in the tree branches according to a specific criterion. The proposed strategy significantly differs from the classical segmentation by region merging where it is assumed that the final partition can be simply obtained from the iterative merging of regions. The contributions of this work are as follows: 1) we present a comparison between different region models and similarity metrics to construct a robust hyperspectral BPT in such a way that the most interesting or useful regions are represented, 2) we introduce a new hyperspectral data segmentation approach using pruning strategies on the BPT. The advantages of this approach is demonstrated over the classical iterative merging approach where a simple stopping criterion is used to stop the merging and define the final partition. The paper is organized as follows. Section 2 reviews the BPT construction and introduces the different similarity measures which have been compared. Section 3 proposes an intelligent BPT pruning strategy in order to perform the segmentation of the hyperspectral data. Experimental results are presented in Section 4, and Section 5 concludes the paper.

BPT REGION MODELS AND MERGING ORDER CRITERIA

The BPT is a tree structure which represents an image containing n pixels by 2n-1 nodes. Leaves nodes represent the original pixels of the image. Furthermore, the remaining tree nodes represent the image regions formed by the merging of their two child nodes corresponding to two neighboring regions. The BPT is generally constructed by an iterative region merging algorithm. As a result, the BPT construction relies on two important choices: a region model MR and a merging order criterion O(Ri, Rj).

On the one hand, the merging criterion corresponds to the similarity 2565 978-1-4244-7994-8/10/$26.00 ©2010 IEEE ICIP 2010

between neighboring regions which determines the order in which regions are merged and create new nodes in the tree. On the other hand, the region model specifies how an hyperspectral region is represented and how to model the union of two regions.

In our case, two types of region models are studied. The first one consists in a first order statistical model, assuming that all pixels belonging to one region have approximatively a constant spectrum. For the second type, the proposed region model is based on higher order statistics represented by probability density functions (pdfs) [START_REF] Calderero | Region Merging Techniques Using Information Theory Statistical Measures[END_REF].

The definition of both models allows us to study two different effects in hyperspectral region merging criterion: first, the importance of the shape of reflectance curves, and, second, the influence of the large spectral variability of the pixels belonging to the same class.

Constant Region Model

The constant region model MR is defined as a vector with N components which corresponds to the average of the values of all pixels p ∈ R in each band λ k .

MR(λ k ) = 1 NR p∈R I λ k (p) k ∈ [1, ..., N ] (1)
with NR the number of pixels contained in region R.

Using this model, MR can be modeled as a random variable in the λ dimension by the vector

PR(λ) = (p λ 1 , p λ 2 , ..., p λ N )
where

p λ k = MR(λ k ) / N k=1 MR(λ k ) (2)
Note that the definition of PR(λ) allows us to propose for O(Ri, Rj) a spectral similarity measure taking into account the overall shape of the reflectance curves. For instance, we propose to use the Spectral Information Divergence [START_REF] Chang | Spectral information divergence for hyperspectral image analysis[END_REF].

Spectral Information Divergence

The Spectral Information Divergence computes the distance between two probability distributions PR i (λ) and PR j (λ). In our case, we use this measure to define the merging criterion by:

OSID(Ri, Rj) = argmin Ri,Rj { D(Ri, Rj) + D(Rj, Ri) } (3)
with D(Ri, Rj) the Kullback Leibler divergence between two probability distributions:

D(Ri, Rj) = N k=1 P R i (λ k ) log P R i (λ k ) P R j (λ k ) (4)

Statistical Region Model

The statistical region model does not assume the homogeneity of the spectral values in a region R. It is defined as a set of N histograms

MR = {H λ 1 R , H λ 2 R , ..., H λ N R } (5)
where each H

λ k
R is the empirical spatial distribution of the region R in the band λ k , formed by:

H λ k R = {H λ k R (a1)H λ k R (a2), ....H λ k R (a |χ| )} (6)
with ai the possible values of the pixels in each band λ k . We must remark that this region model can also be defined when tree leaves are single pixels by exploiting the image self-similarity. The probability density function for individual pixels can actually be estimated and the precise modeling of the pixel's pdf is important in order to get very precise region contours [START_REF] Dimiccoli | Hierarchical region-based representation for segmentation and filtering with depth in single images[END_REF]. Following the statistical analysis, two different similarity metrics between histograms are proposed as merging criterion. The first metric corresponds to the classical bin-to-bin Battacharya Coefficient metric [START_REF] Calderero | Region Merging Techniques Using Information Theory Statistical Measures[END_REF], which assumes that the histograms are already aligned. The second one corresponds to the cross-bin diffusion distance [START_REF] Ling | Diffusion distance for histogram comparison[END_REF] and is known to be less sensitive to quantization, noise effect and histogram misalignment.

Battacharya Coefficient

The Bhattacharyya coefficient between two adjacent regions Ri and Rj of a given band λ k is defined by

BC(H λ k R i , H λ k R j ) = -log( |χ| s=1 H λ k R i (as) 1 2 H λ k R j (as) 1 2 ) (7)
If the two pdfs overlap perfectly, the Bhattacharyya coefficient is 0. Consequently, a merging criterion of a pair of adjacent regions can be defined as the sum of the N dissimilarity measures obtained for the different bands:

OBC(Ri, Rj) = argmin Ri,Rj N k=1 BC(H λ k R i , H λ k R j ) (8)

Diffusion Distance

The diffusion distance [START_REF] Ling | Diffusion distance for histogram comparison[END_REF] is computed by constructing a Gaussian pyramid diffusion process. This process consists in convolving a Gaussian filter φ(x, σ) with the histogram difference d l (x), where x ∈ R m is a vector.

d0(x) = H λ k R i (x) -H λ k R j (x) (9)
d l (x) = [d l-1 (x) * φ(x, σ)] ↓2 l ∈ [1, ..., L] (10)
The notation ↓2 denotes downsampling by a factor of two. L is the number of pyramid layers and σ is the constant standard deviation for the Gaussian filter φ. From the Gaussian pyramid, a distance K between the histograms can be computed summing up the L1 norms of the various levels:

K(H λ k R i , H λ k R j ) = L l=0 |d l (x)| (11)
Consequently, the proposed merging criterion using the diffusion distance defined in previous equations is derived as:

ODD(Ri, Rj) = argmin Ri,Rj N k=1 K(H λ k R i , H λ k R j ) (12)
To conclude this section, we would like to remark that the area of the regions is not included in any proposed merging order. Thus, these approaches may suffer from small and meaningless regions into the generated partition. To overcome this limitation, we propose to give priority to the fusion between small regions.The approach consists in forcing the merging of regions that have an area smaller than a given percentage (typically 15%) of the average size of the regions created by the merging process [START_REF] Calderero | Region Merging Techniques Using Information Theory Statistical Measures[END_REF].

BPT PRUNING

In a BPT segmentation framework, a pruning strategy can be interpreted as an image filtering tool that aims to achieve an optimal segmentation inside a set of hierarchical partitions. This corresponds to a BPT simplification technique where the resultant tree contains fewer nodes than the original. The task consists in evaluating some regions (or nodes) cost by performing an analysis running from the leaves to the tree root. Moving along tree branches, the pruning analyzes the cumulative cost eC associated to each BPT node. Setting a threshold δT , the pruning then removes all nodes having a cost lower than δT . In the following, we compare two different pruning strategies in order to corroborate the efficiency of the BPT representation for the analysis of hyperspectral images.

Number of Regions as Pruning Criterion

A classical pruning criterion is the number of regions in the BPT following the merging sequence. In this case, the eC (N k ) associated to a node N k is the number of non merged nodes and δT corresponds to the desired final number of regions. This technique implies that a segmentation result of an arbitrary number of regions R can be found by undoing the last R -1 mergings over the initial partition. Note that using this pruning strategy, the partition result is always a partition that was obtained following the region merging sequence. Thus, this strategy follows the classical approach of iterative region merging segmentation that assumes that the best partition can be obtained by stopping the iterative merging at some point. In practice, this assumption is rarely true. Consequently, we propose a more intelligent pruning algorithm which is not relying so much on the merging order.

Region homogeneity as Pruning Criterion

The next pruning strategy is based on maximizing the homogeneity of the regions given a BPT branch. A classical criterion to quantify the homogeneity of a cluster is the intra and inter variance of the region. The proposed strategy consists in evaluating first the homogeneity of a node N k in relation with its sibling Ns:

Hom(N k ) = p∈N k N k (p) -N k + p∈N k N k (p) -Ns (13)
with Ns the sibling of N k , and N k , Ns the mean of all the pixels belonging to these regions. Using Hom(N k ), we define a cumulative error cost eC taking into account previous errors:

eC (N k ) = K i=1 Hom(Ni) ( 14
)
Given eC (N k ), the pruning strategy consists in detecting the rate of change at each node along the branch [START_REF] Lu | Image segmentation by binary partition tree[END_REF]. To obtain the rate of change, one of the most popular choices is to calculate the second derivatives. It is estimated by the following equation:

e C (N k ) = eC (N k -) + eC (N k + ) -2 * eC (N k ) (15)
where eC (N k -) is the previous cost along the branch and eC (N k + ) is the next one (corresponding to parent node cost). Hence, the pruning removes a node N k if e C (N k ) < δT and if all its ancestors also satisfy this condition. The segmentation is thus constructed by selecting the leaf nodes of the resulting pruned tree.

EXPERIMENTAL RESULTS

In this section we provide a complete evaluation of the merging order criteria of Section 2. First experiments have been performed using a hyperspectral image created manually. Using the partition shown in Fig. 1(b), we have filled each region with a set of spectra belonging the same class material. The used spectra correspond to the ground truth of Indian Pines AVIRIS hyperspectral data, containing 200 spectral bands. Fig. 1(a) illustrates one of these bands, reflecting the wide variability between spectra of the same class. Firstly, three BPT concerning Fig. 1 are constructed using the proposed merging criteria presented in Section 2. In statistical region models, the number of bins is set to 200. This value changes for image bands having a lower range difference. In this case, the minimum range difference corresponds to the N bins . On the other hand, the maximum number of bins is set to N bins = 200. Regarding the diffusion distance, we set the gaussian kernel deviation σ = 0.5 and use a window size 3. After the construction, the two pruning strategies of section 3 provide different segmentation results for each BPT. Hence, the final partitions obtained by BPT pruning are used to evaluate the performances of the merging orders and of the pruning strategies. To evaluate the resulting partitions, the symmetric distance dsym [START_REF] Cardoso | Toward a generic evaluation of image segmentation[END_REF] is proposed as a quality evaluation. Having a partition P and a ground truth GT , the dsym corresponds to the minimum number of pixels whose labels should be changed between regions in P to achieve a perfect matching with GT , normalized by the total number of pixels in the image. Fig. 2 shows the segmentation results obtained by the three merging criteria of Section 2 and the two pruning strategies described in Section 3. Comparing the results, we observe that the smallest dsym are obtained using the region homogeneity as pruning criterion. This can be corroborated looking at the blue round region located on the bottom, which is only detected in the second row. Note that this result also highlights the importance of using a pruning strategy on the BPT instead of simply stopping an iterative merging algorithm. Regarding merging orders, Fig. 2 shows that the statistical region models yield to better results than constant ones. This limitation is due to the importance of the spectrum variability, which makes this last model insufficient. Another important remark is that comparing both statistical region models, ODD is less sensitive to the chosen number of bins and is hence more robust. As a second experiment, the top-down corner of the ROSIS-03 optical sensor over the University of Pavia is proposed. This image is formed by 103 denoised channels, Fig. 3 illustrates a RGB combination of three of them. For this second image, we have repeated the same procedure obtaining the results of Fig. 4. Both pruning results suggest that our merging orders achieve satisfactory results. However, it can be observed that the region homogeneity pruning criterion provides more realistics results. For instance, the first row results do not obtain either the shape of the building located at the right-bottom corner or the metal objects on the roof of the central rounded-squared building.

CONCLUSIONS

In this paper, BPTs have been proposed as a new type of hierarchical representation for hyperspectral imagery. These BPTs represent a set of regions structured by inclusion in a tree, which can be pruned for efficient hyperspectral image segmentation. BPT construction for hyperspectral data has been introduced comparing different merging orders. Being the hyperspectral data clustering straightforward, the use of statistical region models has demonstrated a high degree of reliability. Regarding pruning strategies, results have shown that the optimal segmentation can be rarely found simply following the merging sequence. For this reason, the region homogeneity pruning criterion clearly outperforms the straightforward pruning criterion based on the number of regions. Hence, BPT shows that the tree structure allows a robust, generic and also reliable segmentation.The performances of the proposed method were assessed using a quantitative evaluation based on a synthetic image using real spectra measured by the AVIRIS sensor, and a qualitative evaluation based on a real hyperspectral image acquired by the sensor ROSIS.

Fig. 1 :

 1 Fig. 1: Manually created test image, with real sets of spectra

  (a) O DD , dsym=0.11 (b) O BC , dsym=0.13 (c) O SID , dsym=0.29 (d) O DD , dsym=0.02 (e) O BC , dsym=0.03 (f) O SID , dsym=0.13

Fig. 2 :

 2 Fig. 2: First row shows the results obtained for the number of regions pruning criterion ( δT = 6 regions) when different models are used for the construction. Second row shows the results for the region homogeneity pruning criterion, with δT =6.106

Fig. 3 :

 3 Fig. 3: RGB combination of Pavia Rosis data set

Fig. 4 :

 4 Fig. 4: First row shows the results obtained for the number of regions pruning criterion ( δT = 85 regions) when different models are used for the construction. Second row shows the results for the region homogeneity pruning criterion

Proceedings of 2010 IEEE 17th International Conference on Image ProcessingSeptember 26-29, 2010, Hong Kong