Florent Jacquemard
email: florent.jacquemard@lsv.ens-cachan.fr

Michael Rusinowitch

Closure of Hedge-Automata Languages by Hedge Rewriting

We consider rewriting systems for unranked ordered terms, i.e. trees where the number of successors of a node is not determined by its label, and is not a priori bounded. The rewriting systems are defined such that variables in the rewrite rules can be substituted by hedges (sequences of terms) instead of just terms. Consequently, this notion of rewriting subsumes both standard term rewriting and word rewriting. We investigate some preservation properties for two classes of languages of unranked ordered terms under this generalization of term rewriting. The considered classes include languages of hedge automata (HA) and some extension (called CF-HA) with context-free languages in transitions, instead of regular languages. In particular, we show that the set of unranked terms reachable from a given HA language, using a so called inverse context-free rewrite system, is a HA language. The proof, based on a HA completion procedure, reuses and combines known techniques with non-trivial adaptations. Moreover, we prove, with different techniques, that the closure of CF-HA languages with respect to restricted context-free rewrite systems, the symmetric case of the above rewrite systems, is a CF-HA language. As a consequence, the problems of ground reachability and regular hedge model checking are decidable in both cases. We give several counter examples showing that we cannot relax the restrictions.

Introduction

In many applications the system states can be modeled by words or trees, sets of configurations by word or tree languages and the transitions of the system can be represented by rewrite rules. In this setting verifying whether a system can enter a set of unsafe states can be expressed as a reachability problem. This approach to the analysis of infinite-state systems requires the computation of the closure of languages under rewrite rules or at least an over-approximation of this closure. Since the usually considered languages are regular the approach is called regular model checking [START_REF] Bouajjani | Regular model checking[END_REF][START_REF] Abdulla | A survey of regular model checking[END_REF]. Regular model checking has been quite successful in protocol and hardware verification. For increasing the scope of regular model checking it is therefore important to be able to derive new classes of languages and rewrite systems such that the rewrite closure is computable.

Unranked trees as well as ordered sequences of unranked trees called hedges [START_REF] Murata | Hedge Automata: a Formal Model for XML Schemata[END_REF][START_REF] Murata | Taxonomy of xml schema languages using formal language theory[END_REF][START_REF] Dal-Zilio | XML schema, tree logic and sheaves automata[END_REF] are flexible structures that are quite appealing to represent XML documents where the number of nodes can be modified, for instance when these nodes correspond to database records. Unranked trees have also been employed to model multithreaded recursive program configurations where the number of parallel processes is unbounded [START_REF] Bouajjani | On computing reachability sets of process rewrite systems[END_REF][START_REF] Orso | Regular Hedge Model Checking[END_REF]. Hedge-automata (HA) are considered now as the natural model of automata for unranked trees. A hedge automaton is a variation of tree automata for hedges. Given a hedge, a hedge automaton assigns some state to a node whenever the sequence of states of the siblings belong to some specified word language (sometimes called horizontal language).

Although regular model checking with languages for words and ranked trees (where function symbols have fixed arity) has been widely investigated, very few results are available for unranked trees and almost none exists on the computation of exact reachability sets for HA languages.

In this paper we tackle the problem above by proving (Theorem 1) that we can compute a HA for recognizing the rewrite closure of a language defined by a given HA, for the class of rewrite systems with inverse context-free rules, which are rules whose right-hand side is of type f (x) where x is a variable. Hence in that case we can compute the exact reachability set from the initial one. The rewriting notion that we consider here for unranked terms generalizes ranked term rewriting and is close to the one that has been introduced by [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF]. The idea is that the variables in the rewrite rules can be substituted by hedges (sequences of terms) instead of just terms. Moreover our results cannot be derived from related ones on ranked terms (e.g. [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF]) using encodings of unranked terms into ranked ones (such as the First-Child-Next-Sibling encoding or the encoding used in stepwise automata [START_REF] Comon | Tree automata techniques and applications[END_REF]). Relaxing the condition in the definition in the above class of rewrite systems leads to counterexamples (Propositions 3-6).

We have also considered a more general class of automata for unranked ordered trees, called CF-HA, where word context-free languages are used instead of regular ones at the horizontal level. We show (Theorem 2) that CF-HA are preserved by rewrite closure using context-free rewrite rules. Context-free rewrite rules are the symmetric case of inverse context-free rules, i.e. rules with left-handside of the form f (x). Some additional restrictions are assumed for this result, they cannot be relaxed as shown by the counter examples in Proposition 7-10.

Related works.

Whether the rewrite closure of regular ranked trees languages is regular too is a problem that has been addressed in [START_REF] Salomaa | Deterministic Tree Pushdown Automata and Monadic Tree Rewriting Systems[END_REF][START_REF] Gilleron | Regular tree languages and rewrite systems[END_REF][START_REF] Jacquemard | Decidable approximations of term rewriting systems[END_REF][START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF][START_REF] Takai | Right-linear finite path overlapping term rewriting systems effectively preserve recognizability[END_REF][START_REF] Seki | Layered Transducing Term Rewriting System and Its Recognizability Preserving Property[END_REF][START_REF] Durand | Bottom-up rewriting is inverse recognizability preserving[END_REF]]. An important breakthrough of the proof in [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] (against former results) is that it works for TRS which are not left-linear. H. Ohsaki introduces equational tree automata for associative and commutative theories in [START_REF] Ohsaki | Beyond the regularity: Equational tree automata for associative and commutative theories[END_REF] and study their closure properties for Boolean operations. T. Touili has studied the regular model checking problem for HA [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF]. She shows how to compute the image of a HA language in one step of rewriting by a right-linear rewrite system. She also gives a procedure to compute an over-approximation of the rewrite closure of a HA. We rather compute exactly this closure for a class of non-linear rewrite systems.

Our first main result (Theorem 1) can be viewed as a non trivial generalization of both [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] and [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF], with proof techniques extending both former constructions.

C. Löding and A. Spelten [START_REF] Löding | Transition graphs of rewriting systems over unranked trees[END_REF] compute exact rewrite closure of HA for extensions of ground term rewriting and prefix word rewriting. These results cannot be compared to ours since in our case variables (that can be substituted by arbitrarily large hedges) allow non local hedge transformations.

There exists other rewriting notions like the top-down XML transformations [START_REF] Martens | On the complexity of typechecking top-down XML transformations[END_REF] or the relabeling transducers of [START_REF] Orso | Regular Hedge Model Checking[END_REF] but they do not cover our notion since either they use specific hedge traversal strategies or they are structurepreserving.

Layout of the paper. In Section 2 we introduce terms, hedges and the related rewriting concepts. In particular we define hedge rewriting systems (HRS) and context-free rewrite rules. In Section 3 we recall the hedge-automata classes HA and CF-HA that we shall investigate. In Section 4 we show that the class of HA languages, (i.e. recognized by HA) is preserved by rewrite closure for rewriting systems containing rules that are inverse context-free. In Section 5 we show that a class of context-free hedge rewrite systems preserves CF-HA languages. In both Sections 4 and 5, we also exhibit some counter-examples obtained when trying to relax the conditions on rules.

Hedge Rewriting

We consider a finite alphabet Σ and an infinite set of variables X . The set of terms over Σ and X is T (Σ, X ) := X ∪ f (h) f ∈ Σ, h ∈ H(Σ, X ) and the set H(Σ, X ) of hedges over Σ and X is the set of finite (possibly empty) sequences of terms of T (Σ, X ). When h is empty, f () will be simply written f . We will sometimes consider a term as a hedge of length one, i.e. consider that T (Σ, X ) ⊂ H(Σ, X ). The sets of ground terms (terms without variables) and ground hedges are respectively denoted T (Σ) and H(Σ). A hedge h ∈ H(Σ, X ) is called linear if every variable of X occurs at most once in h.

The set of variables occurring in a term t ∈ T (Σ, X ) is denoted var (t). A substitution σ is a mapping from X to H(Σ, X ) of finite domain. The application of a substitution σ to a hedge h ∈ H(Σ, X ), denoted hσ, is the homomorphic extension of σ to H(Σ, X ), defined, for t 1 , . . . , t n ∈ T (Σ, X ), with n ≥ 0, by

(t 1 . . . t n )σ := t 1 σ . . . t n σ and f (h)σ := f (hσ).
The set of positions Pos(t) of a term t ∈ T (Σ, X ) is a set of sequences of positive integers. The empty sequence, denoted ε, is the root position of a term. The subterm of t at position p, denoted t| p , is defined by

f (t 1 . . . t n )| ip := t i | p if i ≤ n and, f (h)| ε := f (h). The replacement in t ∈ T (Σ, X ) of the subterm at position p by t ′ ∈ T (Σ, X ) is denoted t[t ′ ] p .
The depth of a term is the maximal length of one of its positions.

A context is a linear hedge of

H Σ, {x} , denoted C[x]. The application of a context C[x] to a hedge h is defined by C[h] := C{x → h}.
A hedge rewriting system (HRS) is a set of rewrite rules of the form ℓ → r where ℓ ∈ T (Σ, X ) \ X and r ∈ T (Σ, X ) (ℓ and r are respectively called lhs and rhs of the rule). The rewrite relation --→ R of an HRS R is the binary relation on H(Σ, X ) defined by h --→ R h ′ iff h = (t 1 . . . t n ), there exists i ≤ n, a position p ∈ Pos(t i ), a rule ℓ → r ∈ R and a substitution σ such that t i | p = ℓσ and

h ′ = t 1 . . . t i-1 t i [rσ]t i+1 . . . t n . The reflexive and transitive closure of --→ R is denoted --→ * R . Example 1. With R = {g(x) → x}, --→
R associates to a term g(h) the hedge h of its arguments. With R = {g(x) → g(axb)}, g(c) --→ * R g(a n cb n ) for every n ≥ 0. Given a set of terms L ⊆ T (Σ) and an HRS R, we note R * (L) the set {t ∈ T (Σ) | ∃s ∈ L, s --→ * R t}. We restrict to terms (instead of hedges) because we are mainly interested in term languages below.

A rewrite rule ℓ → r is called left-linear (resp. right-linear, linear

) if ℓ (resp. r, both) is linear, left-ground (resp. right-ground ) if ℓ ∈ T (Σ) (resp. r ∈ T (Σ)), collapsing if r ∈ var (ℓ), it is called context-free if ℓ = f (x) with x ∈ X (it is not required that x ∈ var (r) however) and inverse context-free if r → ℓ is context-free, prefix (resp. postfix ) if r = g(t 0 . . . t n x) (resp. r = g(x t 0 . . . t n ))
with x ∈ var (ℓ) and no variable of ℓ occurs in the terms t 0 , . . . , t n . A rewrite system is said to have one of the above properties if all its rules have this property.

Example 2. We give a few applications of our rewrite rules in the vein of [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF]. A context-free rule doc(x) → doc(axā) can be employed to introduce tags in an XML document. An inverse context-free rule can be used to eliminate comments doc(x comment y comment) → doc(x). Non left-linear inverse context-free rules are quite useful for processing list of items as in: doc(todo x todo y done x done) → doc(y).

Note that hedge rewriting cannot be reduced to term rewriting through encoding of unranked trees into ranked trees like the First-Child/Next-Sibling encoding, or the encoding used in stepwise automata (see details in the companion report [START_REF] Jacquemard | Rewrite closure of hedge-automata languages[END_REF]).

Hedge-Automata, Context-Free Hedge-Automata

We recall now the definition of hedge-automata [START_REF] Murata | Hedge Automata: a Formal Model for XML Schemata[END_REF] (denoted HA) and the less known class of context-free hedge automata (denoted CF-HA) introduced in [START_REF] Ohsaki | Recognizing boolean closed A-tree languages with membership conditional rewriting mechanism[END_REF] and where they are shown to recognize the closure of regular (ranked) tree languages modulo associativity.

A hedge automaton (resp. context-free hedge automaton) is a tuple

A = (Q, Σ, Q f , ∆) where Q is a finite set of states, Σ is an unranked alphabet, Q f ⊆ Q is a set of final
states, and ∆ is a set of transitions of the form f (L) → q where f ∈ Σ, q ∈ Q and L ⊆ Q * is a regular word language (resp. a context-free word language). When Σ is clear from the context it is omitted in the tuple specifying A.

We define the move relation between ground hedges in T (Σ ∪ Q) as follows: for every terms t, t ′ we have t

--→ A t ′ if there exists a context C[x] and a transition f (L) → q in ∆ such that t = C[f (q 1 . . . q n )], q 1 . . . q n ∈ L and t ′ = C[q]. The 4 relation --→ * A is the transitive closure of --→ A . Following [23], we extend --→ A to terms of T (Σ ∪ 2 Q * ) as follows: C f (L 1 . . . L n ) --→ A C[q] if there exists a rule f (L) → q in A such that L 1 . . . L n ⊆ L (in
this definition, a lone state q is considered as a singleton set {q}).

The language denoted by L(A, q) is the set of ground terms t ∈ T (Σ) such that t --→ * A q. A term is accepted by A if there is q ∈ Q f such that t ∈ L(A, q). The language denoted by L(A) is the set of terms accepted by A.

It is know that for both classes of automata [START_REF] Murata | Hedge Automata: a Formal Model for XML Schemata[END_REF][START_REF] Ohsaki | Recognizing boolean closed A-tree languages with membership conditional rewriting mechanism[END_REF] membership and emptiness problems are decidable. Moreover HA are closed under Boolean operations.

We call a HA or CF-HA A = (Q, Q f , ∆) normalized if for every f ∈ Σ and every q ∈ Q, there is at most one transition rule f (L f,q ) → q in ∆. Every HA (resp. CF-HA) can be transformed into a normalized HA (resp. CF-HA) in polynomial time by replacing every two rules f (L 1 ) → q and f (L

2 ) → q by f (L 1 ∪ L 2 ) → q. A HA A = (Q, Q f , ∆) is called deterministic iff for all two transitions rules f (L 1 ) → q 1 and f (L 2 ) → q 2 in ∆, either L 1 ∩ L 2 = ∅ or q 1 = q 2 .
It is called complete if for all f ∈ Σ and and w ∈ Q * , there exists at least one rule f (L) → q ∈ ∆ such that w ∈ L. When A is deterministic (resp. complete), for all t ∈ T (Σ), there exists at most (resp. at least) one state q ∈ Q such that t ∈ L(A, q).

Every HA can be completed by adding a sink state (and using the closure properties of regular languages). A determinization procedure (with a subset construction) which preserves completeness is described in Section 4.1 (see also [START_REF] Comon | Tree automata techniques and applications[END_REF]).

Epsilon-and Collapsing Transitions

We can extend HA and CF-HA with ε-transitions of the form q → q ′ , where q and q ′ are states, without augmenting the respective expressiveness of these classes. We also consider the extensions of HA (resp. CF-HA), with collapsing transitions of the form L → q where L is a regular (resp. CF) language and q is a state. The move relation for the extended set of transitions is defined as for HA and CF-HA for standard transition and by C[q 1 . . . q k ] --→

A C[q] if L → q is a collapsing transition of A and q 1 . . . q k ∈ L. Note that the collapsing transition L → q is never applied at the root position (i.e. the above context C cannot be a variable) because HA and CF-HA are limited to the recognition of terms only (and not hedges).

Unlike ε-transitions, collapsing transitions strictly extend HA in expressiveness. However, we show that they can be eliminated for CF-HA. Proposition 1. For every extended HA or CF-HA with collapsing transitions A, there exists a CF-HA A ′ (without collapsing transitions) such that L(A ′ ) = L(A).

Proof. Assume that L → q is a collapsing transition of A. Then we get a CF-HA A ′ such that L(A ′ ) = L(A) by replacing every transition f (L 1 ) → q 1 by the transition f (L 2 ) → q 1 where L 2 is the context-free word language generated by the grammar G 2 as follows. We consider a context-free grammar G for L (resp.

G 1 for L 1 ) with axiom X (resp. X 1 ). The axiom of G 2 is X 1 and the set of productions in G 2 contains i) G[q ← -X q ] ∪ G 1 [q ← -X q ] i.e. the terminal q is replaced by a non terminal X q and ii) we add to these rules the production: X q := q | X. We can iterate this construction to eliminate all collapsing transitions. ⊓ ⊔ Proposition 2. There exists an extended HA with collapsing transitions whose language is not a HA language.

Proof. Consider the extended HA A = ({q, q a , q b , q f }, {g, a, b, c}, {q f }, ∆) where

∆ = {c -→ q, a -→ q a , b -→ q b , g(q) -→ q f , q a qq b -→ q}
Its recognized language is {g(a n cb n ) | n ≥ 0} and this is not a HA language. ⊓ ⊔

Decision Problems

The problem of ground reachability and ground joinability are to decide that, given two ground terms s, t ∈ T (Σ) and a HRS R, whether, s

--→ * R t, respectively, s --→ * R • ← -- * R t.
Regular hedge model checking is the problem to decide, given two HA languages L init and L err and a HRS R whether R * (L init ) contains a term of L err . Ground reachability is reducible to regular hedge model-checking. Indeed, given s, t and R, s --→ * R t iff R * {s} ∩ {t} = ∅. Note also that if ground-reachability (hence regular hedge model-checking) is undecidable for a class of HRS, then R * (L) is not recursive in general when R is in this class and L is a HA or CF-HA. Indeed, by definition s --→ * R t iff t ∈ R * {s} .

Closure of Regular Hedge Automata Languages

In this section, we prove one result of preservation of HA language for a class of HRS, and give several counter example showing that the restrictions defining this class of HRS are necessary.

Inverse Context-Free Rewrite Rules

Theorem 1. The closure R * (L) of a HA language L ⊆ T (Σ) under rewriting by an inverse context-free HRS R is a HA language.

Proof. Let A = (Q, Q f , ∆) be a complete and normalized HA recognizing L. We shall construct below a finite sequence of HA A i i≥0 whose last element recognizes R * (L). Our construction uses elements of [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] and [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF], but it is not a simple combination of both. Indeed, on one side we generalize [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF] to an unbounded number of rewriting steps, and on the other side we generalize [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] to unranked tree languages. Both generalizations are non-trivial and require new constructions and new conditions.

For each f ∈ Σ, q ∈ Q, we note L f,q the language in the transition (assumed unique) f (L f,q ) → q ∈ ∆. We construct first from A a deterministic HA

A d = (Q d , Q f d , ∆ d ) recognizing L.
The HA A d is obtained by a subset construction, see e.g. [START_REF] Comon | Tree automata techniques and applications[END_REF], with

Q d := 2 Q , Q f d := {s ∈ Q d | s ∩ Q f = ∅} and ∆ d := f (L f,s ) → s f ∈ Σ, s ⊆ Q where L f,s := q∈s S f,q \ q /
∈s S f,q and S f,q = s 1 . . . s n ∈ Q * d ∃q 1 ∈ s 1 , . . . , q n ∈ s n , q 1 . . . q n ∈ L f,q1 . Next, following the approach of [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF], we define first the set of languages of Q * d that will be used in the transitions of the A i 's constructed below. However, we must consider here a bigger set than [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF] in order to deal with non linear variables in lhs of rules. Let L be the smallest set of subsets of

Q * d such that i. all L f,s (for f ∈ Σ and s ∈ Q d ) and Q * d are in L, ii. if L ∈ L and u, v ∈ Q * d , then u -1 L v -1 ∈ L, where u -1 L v -1 := {w ∈ Q * d | uwv ∈ L}, iii. if L 1 , L 2 ∈ L then L 1 ∩ L 2 ∈ L, iv. if L 1 , L 2 ∈ L then L 1 \ L 2 ∈ L.
Note that the condition Q * d ∈ L in i together with iii and iv imply that L is also closed under union (if

L 1 , L 2 ∈ L then L 1 ∪ L 2 ∈ L), by De Morgan's Law.
Let us show that L is finite and that all its members are regular languages. First, let us note that L 1 , the smallest set satisfying i and ii above, is a finite set of regular languages of Q * d , since every L f,q is regular by hypothesis. The closure L 2 of L 1 under iii and then iv is also a finite set of regular languages. The following lemma shows that L 2 fulfills ii, i.e. that L 2 = L.

Lemma 1. For all L 1 , L 2 ⊆ Q * d , u 1 , u 2 , v 1 , v 2 , u, v ∈ Q * , we have u -1 u -1 1 L 1 v -1 1 ∩ u -1 2 L 2 v -1 2 v -1 = (u 1 u) -1 L 1 (vv 1 ) -1 ∩ (u 2 u) -1 L 2 (vv 2 ) -1 , u -1 u -1 1 L 1 v -1 1 \ u -1 2 L 2 v -1 2 v -1 = (u 1 u) -1 L 1 (vv 1 ) -1 \ (u 2 u) -1 L 2 (vv 2 ) -1 .
Proof. The set in the left-hand-side of the first identity in Lemma 1 is

A = ℓ | uℓv ∈ {ℓ ′ | u 1 ℓ ′ v 1 ∈ L 1 and u 2 ℓ ′ v 2 ∈ L 2 }
, and the set in its right hand side is

B = ℓ | u 1 uℓvv 1 ∈ L 1 and u 2 uℓvv 2 ∈ L 2 . If ℓ ∈ A, then u 1 uℓvv 1 ∈ L 1 and u 2 uℓvv 2 ∈ L 2 , hence ℓ ∈ B. Conversely, if ℓ ∈ B, then uℓv ∈ u -1 1 L 1 v -1 1 ∩ u -1 2 L 2 v -1 2 , hence ℓ ∈ A.
The proof is very similar for the identity with the complementation.

⊓ ⊔

Let us now construct the HA A 0 , A 1 , ... as announced. The set of states and final states of each of these HA are respectively Q d and Q f d . We give below an iterative construction of the respective transition sets ∆ i , i ≥ 0. Let ∆ 0 = ∆ d . Assume that ∆ i has been constructed and contains one transition f (L i f,s ) → s for every f ∈ Σ and s ∈ Q d ; ∆ i+1 is obtained from ∆ i as follows: choose (non deterministically) an inverse context-free rewrite rule ℓ → g(x) ∈ R, and a substitution τ :

var (ℓ)∪{x} → {L ′ ∈ L|∀s 1 . . . s k ∈ L ′ , ∀j ≤ k, L(A i , s j ) = ∅}, such that ℓτ --→ * Ai s ′ ∈ Q d .
Let L ′ = xτ (note that if the variable x does not occur in ℓ, then L ′ is an arbitrary language of L of sequences of states reachable by A i ); ∆ i+1 is obtained as follows: for each s ∈ Q d , 1. replace the rule g L i g,s → s by g L i g,s ∩ L ′ → s ∪ s ′ and g L i g,s \ L ′ → s 2. after this operation, normalize the set of transition rules with the operation described in Section 3 (page 5). (Note that if s ′ ⊆ s then the normalization merges the 2 rules and regenerate g L i g,s → s.)

The idea behind this construction is that if s ′ is reachable from a lhs ℓτ of rewrite rule, then the states in s ′ must also be reachable from the corresponding rhs g(xτ ). Note that for all transitions g L) → s produced by the algorithm, we have L ∈ L (even after normalization), according to the closure properties of this set. Since L and the set of states s is finite (no new state is added) this shows that the construction terminates say with a HA A j that will be denoted A * .

We can also show the following invariant: every A i constructed in the algorithm is deterministic, complete and normalized. Indeed, assume that A i has these properties. If s ′ ⊆ s no transition is added and the invariant is trivially preserved; hence we can assume now s ′ ⊆ s. If another rule g L i g,s∪s

′ → s ∪ s ′ was in ∆ i it is merged with g L i g,s ∩ L ′ → s ∪ s ′ by normalization produc- ing the rule g (L i g,s ∩ L ′ ) ∪ L i g,s∪s ′ → s ∪ ′ . Hence there is at most one L i+1 g,s∪s ′ = (L i g,s ∩ L ′ ) ∪ L i g,s∪s ′ such that g L i+1 g,s∪s ′ ) → s ∪ s ′ ∈ ∆ i+1 . Note also that there is at most one L i+1 g,s = L i g,s \ L ′ such that g L i+1 g,s ) → s ∈ ∆ i+1 .
It is easy to see (from the fact that A i is deterministic and normalized) that L i+1 g,s∪s ′ , L i+1 g,s , and L i+1 g,s ′′ , for all s ′′ ∈ {s, s ′ }, are pairwise disjoint, hence A i+1 is deterministic. From the facts that A i is complete and that L i g,s ∩ L ′ and L i g,s \ L ′ form a partition of L i g,s , we deduce that A i+1 is also complete. We show in [START_REF] Jacquemard | Rewrite closure of hedge-automata languages[END_REF] that L(A * ) = R * (L). Let us simply sketch the proof here for space reasons. The proof of the direction L(A * ) ⊆ R * (L) relies on the following lifting lemma. Lemma 2. For all i ≥ 0, t ∈ T (Σ, X ), σ : var (t) → H(Σ) and θ : var (t) → Q * d such that for all x ∈ var (t), xσ and xθ have the same length, if tθ --→ * Ai s 0 ∈ Q d , and for all x ∈ var (t), all components (xθ)| j of xθ (state of Q d ) and q ∈ (xθ)| j , there exists u ∈ L(A i , q) such that u --→ * R (xσ)| j , then for all q ′ ∈ s 0 , there exists v ∈ L(A i , q ′ ) s. t. v --→ * R tσ. Lemma 2 is proved (see [START_REF] Jacquemard | Rewrite closure of hedge-automata languages[END_REF]) by induction on i, and, for the induction step, by a second induction on the number of applications of a rule of ∆ i+1 \ ∆ i in the reduction tθ ----→ * Ai+1 s 0 . Intuitively, every such application corresponds to a rewrite step in v --→ * R tσ. Now, for the particular case of Lemma 2 where t ∈ T (Σ), we have that if t --→ * Ai s 0 , for some i and s 0 ∈ Q f d , for all q f ∈ s 0 , where q f is a final state of A, there exists u ∈ L(A, q f ) ⊆ L(A) such that u --→ * R t. This terminates the proof of the direction L(A * ) ⊆ R * (L).

For the direction L(A * ) ⊇ R * (L), assume that t ∈ L(A) and that t --→ * R t ′ . We show in [START_REF] Jacquemard | Rewrite closure of hedge-automata languages[END_REF] that t ′ ∈ L(A i ) for some i by induction on the length of the rewrite sequence.

⊓ ⊔ Corollary 1. Ground reachability, ground joinability and regular hedge modelchecking are decidable for inverse context-free HRS.

We present in the next subsections (4.2-4.4) some counter examples showing that relaxing the assumption on R in Theorem 1 invalidate the result.

Collapsing Rewrite Rules

Collapsing rules preserve regularity of term languages [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] when the function symbols are ranked. Indeed, in this case, if R is left-linear and collapsing, a tree automaton (TA) recognizing L can be completed into a TA recognizing R * (L) just by the iterated addition of ε-transitions of the form xτ → q when there is ℓ → x ∈ R and a substitution τ : var (ℓ) → Q such that ℓτ --→ * A q. When R is just collapsing (not left-linear), the construction requires determinism and hence is more complicated but the idea is the same [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF].

In the case of unranked terms and HA, if we want to follow the principles of the construction of Section 4.1, we need to add collapsing transitions and not just ε-transitions. But the addition of collapsing transitions does not preserve HA languages (Proposition 1). The following proposition shows that the above construction is actually not possible for collapsing rewrite rules. Proposition 3. R * (L) is not a HA language in general when L is a HA language and R is a linear collapsing HRS.

Proof. use the principle of the construction in the proof of Proposition 1. Let Σ = {f, g, a, b, c}, let L be the language of the HA A = {q, q a , q b , q f }, {q f }, {c → q, a → q a , b → q b , g(q a qq b ) → q, f (q) → q f } and let R = {g(x) → x}. Assume that R * (L) is a HA language. Its intersection with the HA language {f (a * cb * )} is {f (a n cb n ) | n ≥ 0}. It is not a HA language. This contradicts the fact that HA languages are closed under intersection.

⊓ ⊔

Note that the completion of the above A, following the procedure in the proof of Theorem 1, would add the collapsing transition q a qq b → q.

Flat Linear Rewrite Rules

In the case of ranked terms, it is known [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] that regularity of tree languages is preserved under rewriting with systems with right-linear rules of the form ℓ → f (u 1 , . . . , u n ) where f has arity n and each u i (i ≤ n) is either a ground term or a variable of var (ℓ). We call such a rule flat if its lhs and rhs both have depth one. Note that this class of TRS is not captured by the HRS of Theorem 1 (when restricted to ranked terms). The above regularity preservation result is no longer true for unranked terms.

Proposition 4. R * (L) is not a HA language in general when L is a a HA language and R is a context-free, linear and flat HRS. Moreover, it can be assumed that all the rules of R are prefix or postfix.

Proof. Let us consider the context-free HRS R = {g(x) → g(axb)} of Example 1, and the HA language L = {g(c)}. The language R * (L) = {g(a n cb n ) | n ≥ 0} is not HA. We can transform the above R into R ′ = {g(x) → g ′ (ax), g ′ (y) → g(yb)} whose rules are prefix or postfix (and linear) and which is such that

R ′ * (L) ∩ T ({g, a, b}) = R * (L). ⊓ ⊔
Note that the language in the above proof is recognized by a CF-HA. We shall show below (Theorem 2 in Section 5) that context-free HRS like the R above preserve CF-HA languages.

We show now the stronger result that the closure of a HA language under rewriting with a flat HRS, even linear, is neither HA, nor CF-HA and actually not even recursive. Proposition 5. R * (L) is not recursive in general when L is a HA language and R is a linear and flat HRS whose rules contain at most two variables.

Proof. We reduce the blank accepting problem for TM to ground reachability for an HRS. Let M be a TM with a tape alphabet Γ and a state set S and let Σ = Γ ∪ S ∪ {g}. A configuration of M is represented by a term g(w) where w is a word of Γ * SΓ * (the position of the state symbol indicates the position of the head of M and the rest represents the contents of the tape). We assume, wlog unique blank initial and final configurations, respectively c i and c f . We consider a HRS R containing one rule for each transition of M. For instance, R contains a rule f (xasy) → f (xs ′ a ′ y) corresponding to a transition s, a → L, s ′ , a ′ (with s, s ′ ∈ S and a, a ′ ∈ Γ ) and f (xasby) → f (xa ′ bs ′ y) to the transition s, a → R, s ′ . The blank tape is accepted by

M iff c i --→ * R c f . ⊓ ⊔
As a consequence, regular hedge model checking is undecidable for the HRS of Proposition 5, according to the remarks in Section 3.2.

Rewrite Rules with Flat and One-Variable or Ground Right-Hand-Sides

If we relax the inverse context-free condition, with only one variable allowed in the rhs of rules, but possibly with two occurrences, both at depth 1, then the result of Theorem 1, again, is not valid anymore.

Proposition 6. R * (L) is not recursive in general when L is a HA language and R is a HRS whose rhs of rules are ground or of the form d(xx).

We reduce in [START_REF] Jacquemard | Rewrite closure of hedge-automata languages[END_REF], the blank accepting problem for a TM to ground reachability for a HRS with right-ground (but not left-linear) rules and a rule d(xx) → d ′ (xx).

Closure of Context-Free Hedge Automata Languages

It has been observed [START_REF] Hofbauer | Deleting string rewriting systems preserve regularity[END_REF] that in several cases, one class of word rewrite system preserves regularity and its symmetric class preserves context-free languages. In this section, we prove a similar result by showing that a restricted case of contextfree HRS, i.e. of the symmetric version of the systems considered in Section 4, preserve CF-HA languages. We give next some counterexamples showing that the restrictions are necessary for this result.

Linear Restricted Context-Free Rewrite Rules

We call a HRS R restricted context-free if it is context-free, and moreover, for all rule f (x) → r ∈ R, x can occurs in r only at depth at most 1. Note that this definition includes the case of collapsing rules f (x) → x.

Theorem 2. The closure R * (L) of a CF-HA language L under rewriting by a linear restricted context-free HRS R is a CF-HA language.

Proof.

Let A L = (Q L , Q f L , ∆ L
) be a normalized CF-HA recognizing L. We shall construct an extended CF-HA A ′ with collapsing transitions (see Section 3.1 for the definition) recognizing R * (L). The result follows then from Proposition 1.

First, let us construct for each rule f (x) → g(r 1 . . . r n ) ∈ R and every subterm r = x amongst r 1 , . . . , r n (let us denote rhs(R) the set of such subterms) a CF-HA (with collapsing transitions) A r = (Q r , ∅, ∆ r ) characterizing the set of ground instances of r. We have in A r one state q u ∈ Q r for each non-variable subterm u of r, and a universal state q ∀ ∈ Q r . Below, for every subterm u of r, we shall write q u to denote either the state q u if u is not a variable or q ∀ otherwise. The set of final states of A r is left unspecified. It is indeed not relevant to our purpose since A r is only used as a part of the CF-HA A ′ constructed below. The transition set ∆ r contains one rule f (q u1 . . . q un ) → q f (u1...un) for each subterm f (u 1 . . . u n ) of r (as specified above, q i is q ∀ if u i is a variable and q i is a state q ui otherwise). It contains moreover one collapsing transition q * ∀ → q ∀ and one transition rule f (q * ∀ ) → q ∀ for each f ∈ Σ. The states sets Q r and Q L are assumed pairwise disjoint. Let A :

= (Q, Q f L , ∆) with Q := Q L ⊎ r∈rhs(R) Q r and ∆ := ∆ L ⊎ r∈rhs(R) ∆ r .
For each f ∈ Σ, q ∈ Q, let L f,q be the context-free language in the transition (assumed unique) f (L f,q ) → q ∈ ∆, and let G f,q = (Q, N f,q , I f,q , P f,q ) be a CF grammar generating L f,q , with alphabet (set of terminal symbols) Q, set of non terminal symbols N f,q , axiom I f,q ∈ N f,q , and set of production rules P f,q . The sets of non-terminals N f,q are assumed pairwise disjoint.

We complete the grammars G f,q with new non-terminals I ′ f,q and some sets P ′ f,q of new production rules containing: i. I ′ f,q := I f,q for all f ∈ Σ, q ∈ Q, ii. I ′ g,q := q r1 . . . q rn I ′ f,q q s1 . . . q sm for each rule f (x) → g(r 1 . . . r n xs 1 . . . s m ) ∈ R, with n, m ≥ 0, and x / ∈ var (r 1 , . . . , r n , s 1 , . . . , s m ), and iii. I ′ g,q := q r1 . . . q rn (with n > 0), or I ′ g,q := ε (with n = 0), for each rule f

(x) → g(r 1 . . . r n ) ∈ R with x / ∈ var (r 1 , . . . , r n ), if L(A, q) ∩ f H(Σ) = ∅.
Note that in the cases ii and iii cover all the cases of linear restricted context-free rewrite rules, except the collapsing rules.

Let N = f ∈Σ,q∈Q N f,q ∪ {I ′ f,q } and P = f ∈Σ,q∈Q

(P f,q ∪ P ′ f,q ).
Let us clean up these sets: if the language generated by a CF grammar Q, N, I ′ f,q , P is empty then we remove I ′ f,q from N and all the productions of P which contain I ′ f,q . We iterate this operation, until there is no remaining non-terminals generating an empty language in N (note that the construction stops since we only remove non-terminals and productions). Let us note N ′ and P ′ the sets of non-terminals and productions obtained. For each f ∈ Σ, q ∈ Q, let G ′ f,q = Q, N ′ , I ′ f,q , P ′ , and let L ′ f,q be its language. Finally,

A ′ = (Q, Q f L , ∆ ′
) is obtained by the addition of collapsing transitions corresponding to the collapsing rewrite rules in R

∆ ′ = f (L ′ f,q ) → q f ∈ Σ, q ∈ Q, L ′ f,q = ∅ ∪ {L ′ f,q → q | f (x) → x ∈ R} We show in [11] that L(A ′ ) = R * L(A) .
The proof of the direction ⊆ is by induction on the number of application of collapsing transitions other than q * ∀ → q ∀ in a reduction by A ′ . For the base case, we need to consider the occurrences of non-terminals I ′ g,q in the derivations with the grammars G ′ f,q . Intuitively every occurrence of such I ′ g,q corresponds to a rewrite step with a context-free rule of R.

The proof of the direction ⊇ is by induction on the length of a rewrite sequence u --→ * R t for u ∈ L(A).

⊓ ⊔ Corollary 2. Reachability and regular hedge model-checking are decidable for linear restricted context-free HRS.

Proof. The intersection of an CF-HA language and a HA languages is a CF-HA language, and emptiness of CF-HA is decidable.

⊓ ⊔

It is shown in [START_REF] Ohsaki | Recognizing boolean closed A-tree languages with membership conditional rewriting mechanism[END_REF] that the languages of CF-HA are closures of regular tree languages modulo associativity of one or several binary function symbols. Therefore, the above results are also valid for these languages.

Linear Context-Free Rewrite Rules

Context-free HRS are named after context-free tree grammars, whose production rules have the form N (x 1 , . . . , x n ) → r where N is a non-terminal of arity n (from a finite set N ), x 1 , . . . , x n ∈ X and r ∈ T Σ ∪ N , {x 1 , . . . , x n } . Note that our definition of context-free HRS is restricted to unary non-terminals. However, even for this case of unary non-terminals and right-linear rewrite rules, the result of Theorem 2 cannot be generalized to context-free HRS. Proposition 7. R * (L) is not a CF-HA language in general when L is a CF-HA language and R is a linear context-free HRS.

Proposition 10. R * (L) is not recursive in general when L is a CF-HA language and R is an inverse context-free HRS.

Proof. Let R 1 be the subset of the context-free rewrite rules of the HRS of the above proof of Proposition 9, and R 2 be the subset of the other rules. Note that R 2 is an inverse context-free HRS.

By Theorem 2, L = R * 1 {f 0 (c)} is a CF-HA language. Like in the proof of Proposition 9, we have that f 1 (c) ∈ R * 2 (L) iff the PCP has a solution. Hence, because of the decidability of the membership problem for CF-HA, R * 2 (L) cannot be a CF-HA language.

⊓ ⊔

Conclusion

We have shown that HA and CF-HA languages are preserved by rewrite closure for interesting classes of non ground hedge rewriting rules. These rules allow us for instance to modify the structure of XML documents when processing them. We plan to extend our results to non ordered unranked trees by considering sheaves automata as in [START_REF] Dal-Zilio | XML schema, tree logic and sheaves automata[END_REF] or commutative hedge automata (see [START_REF] Bouajjani | On computing reachability sets of process rewrite systems[END_REF] for application to process rewrite systems). Regularity preservation has been studied in the case of ranked terms for transducing term rewriting system, i.e. rewrite rules corresponding to transducers rules [START_REF] Seki | Layered Transducing Term Rewriting System and Its Recognizability Preserving Property[END_REF]. A generalization of such classes of TRS to hedge rewriting seems conceptually close to XML transformations [START_REF] Martens | On the complexity of typechecking top-down XML transformations[END_REF] and we plan to study the preservation of HA or CF-HA languages w.r.t. to such HRS.

Note that S f,q and L f,s are indeed regular languages, see[START_REF] Comon | Tree automata techniques and applications[END_REF].

Proof. Let us consider the context-free HRS: R = {f (x) → g(f (ax))} and let L = {f (c)}. The set R * (L) is g(g(. . . g( n f (a n c)))) n ∈ N .

Using a pumping argument, we can show that it is not a CF-HA language. ⊓ ⊔ The above counter-example shows the importance for Theorem 2 of the condition, in the definition of restricted context-free HRS, that the variable x in a lhs of rule occurs at a shallow position in the corresponding rhs.

Restricted Context-Free Rewrite Rules

If we keep the restricted context-free condition (the variable x in the lhs of a rule occurs at a shallow position in the corresponding rhs) but we drop the linearity condition, we also lose the CF-HA preservation result of Theorem 2.

Proposition 8. R * (L) is not a CF-HA language in general when L is a CF-HA language and R is a restricted context-free HRS.

which is not a CF-HA language. Assume indeed that this language is recognized by a CF-HA (Q, Q f , ∆). It means that ∆ contains a transition f (L) → q where L is a context-free language of words of Q * of length 2 k , k ≥ 0. The image of L under the strictly alphabetic homomorphism which translates every state q ∈ Q into a is context-free. As it is a one letter language, it is also regular. But it is well known that this language {a n | n = 2 k , k ≥ 0} is actually not regular. ⊓ ⊔

Mixing Inverse CF and Restricted CF Rewrite Rules

We show now that the results of Theorems 1 and 2 cannot be combined. In other terms, for some HRS containing both linear inverse context-free and restricted context-free rules, the set of descendants of a HA language is not a HA language, neither a CF-HA language and even not recursive.

Proposition 9. R * (L) is not recursive in general when L is a HA language and R is a HRS whose rules are either inverse context-free or restricted context-free and contain only one variable.

Proof. We reduce the Post Correspondence Problem (PCP). Let us consider an instance

Let R be an HRS containing a rule f 0 (x) → f 0 ( u i xv i ) for each pair u i , v i ∈ P ( u i is the mirror image of u i ), and two rules f 0 (axa) → f 1 (x) and f 1 (axa) → f 1 (x) for each a ∈ Γ . We assume that f 0 , f 1 , and c are symbols not in Γ . We have that f 0 (c) --→ * R f 1 (c) iff P has a solution.

⊓ ⊔

Moreover, as we have shown that context-free HRS do not preserve HA languages (Proposition 4), the symmetric also holds for inverse-context-free HRS and CF-HA languages.