Adrià Gascón{1}

Guillem Godoy{1}

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

Closure of Tree Automata Languages under Innermost Rewriting

Keywords: Term Rewriting, Tree Automata, Rewrite Strategies

Preservation of regularity by a term rewriting system (TRS) states that the set of reachable terms from a tree automata (TA) language (aka regular term set) is also a TA language. It is an important and useful property, and there have been many works on identifying classes of TRS ensuring it; unfortunately, regularity is not preserved for restricted classes of TRS like shallow TRS. Nevertheless, this property has not been studied for important strategies of rewriting like the innermost strategy -which corresponds to the call by value computation of programming languages. We prove that the set of innermost-reachable terms from a TA language by a shallow TRS is not necessarily regular, but it can be recognized by a TA with equality and disequality constraints between brothers. As a consequence we conclude decidability of regularity of the reachable set of terms from a TA language by innermost rewriting and shallow TRS. This result is in contrast with plain (not necessarily innermost) rewriting for which we prove undecidability. We also show that, like for plain rewriting, innermost rewriting with linear and right-shallow TRS preserves regularity.

Introduction

Finite representations of infinite sets of terms are useful in many areas of computer science. The choice of a formalism for this purpose depends on its expressiveness, but also on its computational properties. Finite-state Tree Automata (TA) [START_REF] Comon | Tree automata techniques and applications[END_REF] are a well studied formalism for representing term languages, due to their good computational and expressiveness properties. They are used in many fields of computer science, from a theoretical and a practical point of view. For instance, for the analysis of systems or programs, when configurations can be represented by trees (e.g. concurrent processes with parallel and sequential composition operators) TAs provide a finite representation of possibly infinite sets of configurations.

Term rewriting is a general formalism for the symbolic evaluation of terms by replacement of some patterns by others, following oriented equations, or rewrite rules, given in a finite set (a term rewriting system, or TRS). Plain rewriting is sometimes too general, and in many contexts rewriting is applied with specific strategies giving a finer representation of the system behaviour. This is the case of the innermost strategy, which corresponds to the call by value computation of programming languages, where arguments are fully evaluated before the application of the function.

In the above application to system verification, transitions in infinite state systems can usually be represented by rewrite rules. There have been many studies of the connections between TA and rewriting, and a central property in this domain is the preservation of regularity. It states that for any given regular language L (which means that L is accepted by a TA), the set of reachable terms from L by a TRS R, denoted R * (L) is also regular. Preservation of regularity has been widely studied. The first result of this kind was that preservation of regularity holds for every ground TRS, as shown in [START_REF] Brainerd | Tree generating regular systems[END_REF]. In [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF] this property was established for linear (variables occur at most once in every left-hand and right-hand side of a rule) and right-flat (the right-hand sides of the rules have height 0 or 1) TRS. There have been several extensions of this result, e.g. [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] Durand | Bottom-up rewriting is inverse recognizability preserving[END_REF], and [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF] represents a breakthrough since the left-linearity condition (linearity of left-hand sides of rules of the TRS) was dropped. However, in all the above cases, the condition of right-linearity remains necessary and in fact, a rewrite rule like g(x) → f (x, x) does not preserve regularity. Moreover, only plain rewriting is considered in these works, except in [START_REF] Durand | Bottom-up rewriting is inverse recognizability preserving[END_REF] where the bottom-up strategy is considered; there have been (up to our knowledge) no studies of regularity preservation under the innermost strategy.

The aim of this work is to study the preservation of regularity for innermost rewriting, and to identify a class of TRS for which better results can be found under the innermost strategy than under plain rewriting. We consider the class of shallow (all variables occur at depth 0 or 1 in the terms of the rules) TRS. Although the shallow case seems restrictive, for plain rewriting, shallow TRS do not preserve regularity. Moreover, several interesting properties of TRS, like reachability, joinability, confluence [START_REF] Mitsuhashi | The confluence problem for flat TRSs[END_REF] and termination [START_REF] Godoy | Termination of rewriting with right-flat rules[END_REF], are undecidable for shallow TRS, while adding certain linearity restrictions allows the decidability of all these problems [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] Godoy | Confluence of shallow right-linear rewrite systems[END_REF][START_REF] Godoy | Termination of rewriting with right-flat rules[END_REF]. Hence, from a theoretical point of view, the shallow case draws a frontier for decidability when one considers classes of TRS defined by syntactic restrictions.

Our main result (Theorem 4.9, Section 4.2) is that, given a regular language L and a shallow TRS R, the set R (L) of terms reachable from L using R with the innermost strategy is recognized by tree automata extended with equality and disequality constraints between brothers in their state transitions. This kind of automata, which we call BTTA, was introduced in [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF] as an extension of TA, and it has also good closure and decidability properties, but with worst complexity than standard TA. This is in contrast with the situation with plain rewriting: R * (L) (the set of terms reachable from L using R with plain rewriting) is in general neither a TA nor a BTTA language under the same hypotheses (Proposition 3.2, Section 3).

One of the classical techniques for proving results of preservation of regularity consists of adding transitions to the automaton recognizing the starting language L, in order to simulate rule applications of R and recognize also all the terms reachable from L. Apparently, this completion technique which works well for standard TAs (in all the regularity preservation results cited so far) does not work for general shallow TRS. Innermost rewriting cannot be simulated by TA transitions, despite it does operate almost in a bottom-up fashion for shallow TRS [START_REF] Durand | Bottom-up rewriting is inverse recognizability preserving[END_REF]. The reason follows from two other results of the paper:

• First, we show that innermost rewriting with flat TRS (TRS whose all left-handside and right-hand-sides of rules have depth at most one) does not preserve regularity (Proposition 4.2, Section 4). As a consequence, we need to consider BTTAs instead of standard TAs.

• Second, flat and linear TRS do neither preserve BTTA-recognizably (Proposition 4.3, Section 4.1). Consequently, TA completion cannot work in this case.

The main result is obtained in two steps. First, we reduce the problem of representing the reachable terms from a regular set to the reachable terms from a constant. Next, we give a direct construction of a BTTA recognizing the reachable terms from a constant. It is based on a representation of the set of reachable terms introduced in [8] using constrained terms. As an immediate consequence of the main result, we obtain from [START_REF] Bogaert | The recognizability problem for tree automata with comparisons between brothers[END_REF] that given a regular language L and a shallow TRS R, it is decidable whether R (L) is regular in the case of innermost rewriting. In contraposition, we prove undecidability of regularity of R * (L) when plain rewriting is considered.

Another positive result (Theorem 5.2, Section 5.1) is that, like for plain rewriting, innermost rewriting with linear and right-shallow TRS preserves regular languages. This result has been independently obtained in [START_REF] Kojima | Innermost reachability and context sensitive reachability properties are decidable for linear right-shallow term rewriting systems[END_REF]. In our case it is proved with a non trivial adaptation of the TA completion technique of e.g. [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF][START_REF] Jacquemard | Decidable approximations of term rewriting systems[END_REF]. The cases of plain and innermost rewriting are different in essence to treat, and some subtle differences need to be introduced. We show in particular that even though TA completion permits to establish that right-linear and right-flat TRS (i.e. when left-hand sides of rules might be not linear) preserve regular languages under plain rewriting, we show that this property is no longer true for under innermost rewriting (Proposition 5.4, Section 5.2).

Preliminaries

We use standard notation from the term rewriting literature [START_REF] Dershowitz | Rewrite systems[END_REF]. A signature Σ is a finite set of function symbols with arity. We write Σ m for the subset of function symbols of Σ of arity m. Given an infinite set V of variables, the set of terms built over Σ and V is denoted T (Σ, V), and the subset of ground terms is denoted T (Σ). The set of variables occurring in a term t ∈ T (Σ, V) is denoted vars(t). A substitution σ is a mapping from V to T (Σ, V). The application of a substitution σ to a term t is written σ(t), and is the homomorphic extension of σ to T (Σ, V).

A term t is identified as usual to a function from its set of positions (strings of positive integers) Pos(t) to symbols of F and V. We note Λ the empty string (root position). The length of a position p is denoted |p| and also called depth. The height of a term t, denoted h(t), is the maximum of {|p| p ∈ Pos(t)}. A subterm of t at position p is written t| p , and the replacement in t of the subterm at position p by u denoted t[u] p . A term rewriting system (TRS) over a signature Σ is a finite set of rewrite rules ℓ → r, where ℓ ∈ T (Σ, V) \ V (it is called left-hand side of the rule) and r ∈ T (Σ, vars(ℓ)) (it is called right-hand side). A term s ∈ T (Σ, V) rewrites to t by a TRS R at a position p of s with a substitution σ, denoted s ----→ R,p,σ t (p and σ may be omitted in this notation) if there is a rewrite rule ℓ → r ∈ R such that s| p = σ(ℓ) and t = s[σ(r)] p . In this case, s is said to be reducible. The set of irreducible terms, also called R-normal-forms, is denoted by NF R . The transitive and reflexive closure of

--→ R is denoted --→ * R . Given L ⊆ T (Σ), we note R * (L) = {t | ∃s ∈ L, s --→ * R t}.
The above rewrite step is called innermost if all proper subterms of s| p are R-normal forms. In this case, we write s --→ ı R t, and --→ R for the the transitive and reflexive closure of this relation, and R (L) for {t | ∃s ∈ L, s --→ R t}. We shall also use the notations NF * R (s) and NF R (s) (with s ∈ T (F, V)) for resp. R * ({s}) ∩ NF R and R ({s}) ∩ NF R .

A TRS is called linear (resp. right-linear, left-linear ) if every variable occurs at most once in each term (resp. right-hand side, left-hand side) of the rules. It is called shallow (resp. right-shallow, left-shallow ) if variables occur at depth 0 or 1 in the terms (resp. in the right-hand sides, in the left-hand sides) of the rules and flat (resp. right-flat, left-flat) if the terms (resp. the right-hand sides, the left-hand sides) in the rules have height at most 1. A rule ℓ → r is called collapsing if r is a variable.

Tree automata with constraints between brothers

A tree automaton (TA) A on 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).

A Bogaert-Tison tree automaton (BTTA, or tree automaton with constraints between brothers) is defined like a TA except that its states are unary and its transitions are constrained rewrite rules of the form f q 1 (x 1 ), . . . , q m (x m ) → q f (x 1 , . . . , x m ) c , or ε-transitions q 1 (x 1 ) -→ q(x 1 ), where x 1 , . . . , x m are distinct variables and the constraint c is a Boolean combination of equalities x i = x j . Equivalently, the constraint c can be defined as a partition P of {1, . . . , m} with the same meaning as a conjunction of equalities x i = x j for the indexes i, j such that i ≡ P j, and disequalities x i = x j for the indexes i, j such that i ≡ P j. Following the notations of [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF], the above transitions are written f (q 1 , . . . , q m ) -→ c q (or f (q 1 , . . . , q m ) → q when c is true) and q 1 → q, and every equality x i = x j (resp. disequality x i = x j ) in the constraint c is written i = j (resp. i = j). Note that every TA is the special case of BTTA whose constraints are all equal to true.

The language L(A, q) of a BTTA A in state q is the set of ground terms accepted in state q by A, i.e. the terms t such that t --→ * ∆ q(t). The language L(A) of A is q∈Q f L(A, q) and a set of ground terms is called regular (resp. BT-regular ) if it is the language of a TA (resp. BTTA).

Example 2.1

The following BTTA recognizes the set of Bin of complete binary trees over Σ = {a : 0, f : 2}, whose internal nodes are labeled by f and whose leaves are labeled by a: {q}, {q}, {a → q, f (q, q) ---→ 1=2 q . It is well known that Bin is not regular. 3

A BTTA A is called deterministic (resp. complete) if for every term t ∈ T (Σ), there is at most (resp. at least) one state q such that t ∈ L(A, q). If A is deterministic and complete, this unique state is denoted A(t). A BTTA A is normalized if it does not contain ǫ-transitions, constraints in transitions are defined using partitions, and for every function symbol f with arity m, states q 1 , . . . , q m and partition P of {1, . . . , m}, A contains exactly one rule of the form f (q 1 , . . . , q m ) -→ P q. A normalized BTTA A is deterministic and complete, and any BTTA can be transformed into a normalized one recognizing the same language. If A is normalized, we write A(t, P ), for a flat term t ∈ T (Σ ∪ Q), to denote the unique state q such that t -→ P q is a transition of A. BTTA are useful for representing the set of normal forms of certain classes of TRSs, like flat TRSs, see e.g. [START_REF] Comon | Tree automata techniques and applications[END_REF].

Lemma 2.2 [3] Let R be a flat TRS over Σ. There exists a normalized BTTA B = (Q B , Q f B , ∆ B ) on Σ which recognizes the set of ground R-normal forms. Moreover |Q B \ Q f B | = 1. Proof. The construction of B = (Q B , Q B \{q reject }, ∆ B ) on Σ is as follows. Its set of states Q B is {q c | c ∈ Σ 0 } ∪ {q, q reject }
where all of them except q reject are accepting states. Its set of rules ∆ B contains:

• the rules c → q c for every constant c that is a R-normal form.

• the rules c → q reject for every constant c that is not a R-normal form.

• the rules f (q 1 , . . . q m ) -→ c q reject such that either some q i is q reject and c is true, or every q i is different from q reject and c is f (ℓ 1 ,...,ℓm)→r∈R,∀1≤i≤m ℓ i ∈Σ 0 ⇒q i =q ℓ i 1≤i<j≤m ℓ i =ℓ j ∈V i = j.

• the rules f (q 1 . . . q m ) -→ c q such that every q i is different from q reject and c is

f (ℓ 1 ,...,ℓm)→r∈R,∀1≤i≤m ℓ i ∈Σ 0 ⇒q i =q ℓ i 1≤i<j≤m ℓ i =ℓ j ∈V i = j. 2
Example 2.3 Let Σ be the signature {a : 0, g : 1, f : 2} and R be the flat TRS

{g(x) → f (x, x)}. The BTTA B recognizing the ground R-normal forms is B = {q a , q, q reject }, {q a , q}, ∆ with ∆ = {a → q a } ∪ {g(q * ) → q reject , f (q * , q reject ) → q reject , f (q reject , q * ) → q reject | q * = q a , q, q reject } ∪ {f (q ′ , q ′ ) → q | q ′ = q a , q}. 3
3 Closure under plain rewriting with shallow TRS

Right-(shallow and linear) TRSs preserve regularity [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF]. It is well known that right-linearity cannot be omitted, as the following example shows. The set R * (L) is not regular because its intersection with the regular set T ({a, f }) is the non-regular set Bin of complete binary trees over Σ = {a : 0, f : 2}, and the class of regular tree languages is closed under intersection. 3

We show below that considering BTTA does not help in this case.

Proposition 3.2 In general, R * (L) is not BT-regular when L is a regular tree language and R a flat TRS.

Proof. Let us consider R, L and Bin as in Example 3.1. The set R * (L) is not BTregular. Indeed, the intersection of R * (L) with the regular (hence BT-regular) set

L 2 := {f (s, t) | s ∈ T ({g, a}), t ∈ T ({f, a})} is the subset L ′ of terms f (s, t) ∈ L 2 with t ∈ Bin and h(s) = h(t)
. This latter set is not BT-regular, as shown below. It follows that R * (L) is not BT-regular because the class of BT-regular tree languages is closed under intersection [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF].

Let us now show that L ′ is not BT-regular. Assume that it is recognized by a BTTA A = (Q, Q f , ∆) on Σ with n states, and for all i ≥ 1 let f (s i , t i ) be the term of L ′ with h(s) = h(t) = i. For each i, there exists a reduction sequence f (s i , t i ) --→ * ∆ q(f (s i , t i )) with q ∈ Q f , and we consider the last rule ρ i of ∆ applied in this reduction sequence. There exist two distinct indexes

i 1 , i 2 ≥ 1 such that ρ i 1 = ρ i 2 . Let f (q 1 (x 1 ), q 2 (x 2 )) -→ c q(f (x 1 , x 2
)) be this unique rule of ∆. Note that the constraint c does not contain the equality x 1 = x 2 , actually c may be

x 1 = x 2 or true. In both cases, it follows that f (s i 1 , t i 2 ) --→ * ∆ f (q 1 (s i 1 ), q 2 (t i 2 )) --→ ρ i 1 q(f (s i 1 , t i 2 )). This is contradiction with the fact that f (s i 1 , t i 2 ) / ∈ L ′ because h(s i 1 ) = h(t i 2 ). 2
4 Closure under innermost rewriting with shallow TRS

The essential problem in Proposition 3.2 relies on the fact that after an application of the rule g(x) → f (x, x) on a term g(t), producing f (t, t), the following application of rewrite rules can change the two occurrences of t in different ways, producing terms f (t 1 , t 2 ) with t 1 = t 2 . The equality constraints of BTTA have not the expressive power to capture the relation relating t 1 and t 2 (i.e. that both are reachable from a common term). The situation is getting better when the innermost strategy is applied.

Example 4.1 In Example 3.1, when we apply the rule g(x) → f (x, x) to terms of L = {g n (a) | n ≥ 0} with the innermost strategy, the subterm where it is applied must be g(t) for a R-normal form t. Hence, in the term f (t, t) obtained, t cannot be modified by rewriting. Hence R (L) = {g n (t) | t ∈ Bin, n ≥ 0}. This set is BT-regular; it is indeed recognized by the following BTTA:

{q, q g }, {q, q g }, {a → q, f (q, q) ---→ 1=2 q, g(q) → q g , g(q g ) → q g .

3

Note however that R (L) is not regular in the above example.

Proposition 4.2 In general, R (L) is not regular when L is a regular tree language L and R a flat TRS.

Closure of BTTA languages with flat TRS

Linear and flat TRSs preserve regularity [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF]. This result cannot be extended to BT-regularity, neither for plain nor innermost rewriting.

Proposition 4.3 In general, R * (L) and R (L) are not BT-regular when L is BTregular and R is a flat and linear TRS.

Proof. The tree language L = {h(f n (0), f n (0)) | n ≥ 0} is recognized by the following BTTA, with one equality constraint tested at the root position: {q, q f }, {q f }, {0 → q, f (q) → q, h(q, q) ---→ 1=2 q f } . Note that L is not regular.

Let us consider the flat and linear TRS R = {f (x) → g(x)} and the regular tree language

L ′ = {h(f n (0), g m (0)) | n ≥ 0}. The closure R * (L) ∩ L ′ = {h(f n (0), g n (0))} is not BT-recognizable, hence R * (L) is neither BT-recognizable.
This is also true if we consider innermost rewriting. 2

Closure of TA languages with shallow TRS

The classical approach for proving preservation of regularity [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] consists in completing a TA recognizing the original language L with new rules inferred using R. This method cannot be generalized to BT-regular languages, according to Proposition 4.3. Therefore, we follow a different approach. We prove first that given a regular tree language L and a flat TRS R on a signature Σ , we can generate a new TRS R c over an extended signature including a new constant c such that R c ({c}) coincides with R (L) on the given signature Σ. This simple and enabling result permits to represent the set of terms innermostreachable from a regular term set as the set of terms innermost-reachable from a constant.

Later, we show how to compute a BTTA recognizing the terms innermostreachable from a constant. To this end we make use of some results in [START_REF] Godoy | Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems[END_REF] on innermost rewriting with shallow TRSs.

Simplifying assumptions on the signature and the TRS.

All the results of this section are concerned with shallow TRS over an arbitrary signature. In order to simplify the proof, we shall assume fixed from now on in this section a TRS R over a signature Σ who following these two non restrictive assumptions:

• Σ contains several constant function symbols and only one non-constant symbol f of arity m,

• the TRS R is flat.

Such assumptions, already used e.g. in [START_REF] Godoy | Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems[END_REF], can be made without loss of generality for the problem considered here, as shown in Appendix.

Reduction to terms innermost-reachable from constants.

Our goal is to reduce the effort of characterizing the set of terms innermost-reachable with R from a regular language L to characterizing the set of terms innermostreachable from a single constant. The idea is to add to the rewrite system R the inverse of the transition rules of a TA A recognizing L. We show then that the generation of the terms of L starting from the final states of A and using the transitions of A backward can be performed following the innermost strategy.

Lemma 4.4 For every flat TRS R and regular language L, over a signature Σ, there exists an extension

Σ ′ ⊃ Σ, a constant c ∈ Σ ′ \ Σ and a flat TRS R c over Σ ′ such that R c ({c}) ∩ T (Σ) = R (L).
Proof. Let A = (Q, Q f , ∆) be a TA on Σ recognizing L. Without loss of generality, we assume that every state

q ∈ Q is the target of a rule of ∆. Let Σ ′ be Σ ∪ Q ∪ {c}, where c is a new constant not in Σ ∪ Q and let R c be R ∪ ∆ -1 ∪ {c → q | q ∈ Q f }. We prove that R c ({c}) ∩ T (Σ) = R (L). Direction ⊇. Let t ∈ R (L) and let s ∈ L such that s --→ R t. We have s --→ ∆ q ∈ Q f . Therefore c ---→ ı c→q q ---→ ∆ -1 s --→ R t and hence c --→ Rc t.
Direction ⊆. Let t ∈ T (Σ) be such that c --→ Rc t. Since c ∈ Σ, there is necessarily in this derivation at least one rewrite step of the form c --→ ı Rc q for q ∈ Q f . The subderivation q --→ Rc t can contain alternate rewrite steps using rules of ∆ -1 or of R. We want to show that these rewrite steps can be commuted such that a (∆ -1 ∪ R)innermost derivation of the form q ---→ *

∆ -1 s --→ * R t is possible. To this end it is sufficient to see that any (∆ -1 ∪ R)-innermost subderivation u ---→ R,p 1 v -----→ ∆ -1 ,p 2 w can be commuted to a (∆ -1 ∪ R)-innermost subderivation u -----→ ∆ -1 ,p 2 v ′ ---→ R,p 1
w, which will be straightforward if we prove that the positions p 1 and p 2 are disjoint. Note that the term u| p 1 does not contain any symbol q ∈ Q: otherwise the rewrite step u ---→ R,p 1 v would not be (∆ -1 ∪ R)-innermost since there exists a rule of the form q → r in ∆ -1 according to our assumptions. Hence, v| p 1 does not contain any symbol q ∈ Q neither. Therefore, the rewrite step v -----→ ∆ -1 ,p 2 w is produced at a position p 2 disjoint with p 1 , and we are done. Hence, there exists a (∆ -1 ∪ R)innermost derivation q ---→ * ∆ -1 s --→ * R t. In order to prove that t ∈ R (L) it suffices to see that s ∈ L. Since s --→ ∆ q ∈ Q f , it is enough to prove that s ∈ T (Σ), i.e. that s does not contain any symbol q ∈ Q. Suppose that s| p is a certain q ∈ Q. Similarly as before, no rule in R can be applied at a position p ′ < p. Otherwise this rewrite step would not be innermost. Hence, repeated applications of rules of R under innermost rewriting do not remove q. Therefore, q is a symbol occurring in t, a contradiction. 2

Note that this reduction works only when the innermost strategy is used. However, it is valid for any class of TRS closed under the addition of ground rules. The following BTTA B is built following the construction in the proof of Lemma 4.4 for the recognition of the ground normal forms for this extended TRS. It extends the BTTA of Example 2.3. B = {q a , q c , q, q reject }, {q a , q c , q}, ∆ with ∆ = {a → q a , c → q reject } ∪ {g(q * ) → q reject , f (q * , q reject ) → q reject , f (q reject , q * ) → q reject | q * = q a , q c , q, q reject } ∪ {f (q ′ , q ′ ) → q | q ′ = q a , q c , q}. Note that B can be cleaned: all the transition rules with q c in left hand side can be removed since no term is recognized in this state. 3

Weak normal forms and constrained terms.

From [START_REF] Godoy | Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems[END_REF], we have the following definitions and results. A term t is a weak normal form if it is either a constant or a term of the form t = f (t 1 , . . . , t m ) such that every t i is either a constant or a normal form. Let P(Σ 0 ) denotes the powerset of Σ 0 minus the empty set. A constraint C is a partial function C : V → P(Σ 0 ) i.e. an assignment from variables to non-empty sets of constants. We say that a substitution σ is a solution of a constraint C (with respect to a TRS R) if for all x in dom(C), σ(x) ∈ NF R (C(x)) \ Σ 0 . A constrained term is a pair denoted t|C, where t is a flat term and C is a constraint, with dom(C) = vars(t). A term σ(t) is called an instance of t|C if σ is a solution of C. Note that every instance of a constrained term is a weak normal form.

In [START_REF] Godoy | Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems[END_REF] it is shown how to compute for every flat TRS R and for every constant c ∈ Σ 0 two finite sets r c and r c of flat constrained terms whose set of instances (resp. normal form of instances) contain exactly the weak normal forms (resp. non-constant normal forms) innermost-reachable from c. More precisely, r c and r c satisfy the following properties.

(a) for every t|C ∈ r c , there exists at least one solution of C, and all instances of t|C are innermost-reachable from c.

(b) for every t|C ∈ r c , all non-constant normal form instances of t|C are innermostreachable from c.

(c) for every weak normal form s innermost-reachable from c, there exists some constrained term t|C ∈ r c such that s is an instance of t|C.

(d) for every non-constant normal form s innermost-reachable from c, there exists some constrained term f (t 1 , . . . , t m )|C ∈ r c such that s is an instance of f (t 1 , . . . , t m )|C. The set of weak normal forms innermost-reachable from c is {c, a, g(c), g(a), f (c, c)} ∪ {g(t), f (t, t) | t ∈ Bin}, and its subset of normal forms innermost-reachable from c is is {a} ∪ {f (t, t) ∈ Bin}. The following sets satisfy the above properties:

r c = c|∅, a|∅, g(c)|∅, g(a)|∅, f (c, c)|∅, f (a, a)|∅, g(x)|{x → {c}}, f (x, x)|{x → {c}} , r c = f (a, a)|∅, f (x, x)|{x → {c}} , r a = a|∅ , r a = ∅ 3
4.2.4 Recognizing terms innermost-reachable from constants.

We assume some sets r c and r c as above and we construct a normalized BTTA A R which recognizes the terms innermost-reachable from constants in Σ 0 using R with the innermost strategy. For this purpose, we shall use the BTTA B of Lemma 2.2 recognizing the ground normal forms of R.

Let Q 0 = {q ∈ Q B | ∃d ∈ Σ 0 , B(d) = q}, and
Q 1 = Q f B \Q 0 .
Without loss of generality we assume that only constants lead to states in Q 0 . Thus, the states of Q 1 characterize the set of non-constant R-normalform. The states of A R are pairs S, q , where S ⊆ Σ 0 and q ∈ Q B . The intuitive idea is that a term t will lead to S, q with A R if it leads to q with B and S is the set of all constants that innermost-reach t with R. To this end, the set of transition rules contains:

• b → {d | b|∅ ∈ r d }, B(b)
, for every constant b.

• f S 1 , q 1 , . . . , S m , q m -→ P S, B f (q 1 , . . . , q m ), P , for every S 1 , . . . , S m ⊆ Σ 0 , q 1 , . . . , q m ∈ Q B , and partition P of {1, . . . , m}, and where S is the set of constants c ∈ Σ 0 such that there exists f (α 1 , . . . , α m )|C ∈ (r c ∪ r c ) with:

i. ∀1 ≤ i ≤ m, if α i ∈ Σ 0 then α i ∈ S i and if α i ∈ V then C(α i ) ⊆ S i and q i ∈ Q 1 , ii. ∀1 ≤ i < j ≤ m, if α i = α j ∈ V then i ≡ P j and if f (α 1 , . . . , α m )|C ∈ r c \ r c then B f (q 1 . . . q m ), P ∈ Q 1 and every α i ∈ Σ 0 (1 ≤ i ≤ m) is in NF R .
By construction, the automaton A R is normalized.

Example 4.7 Let us come back to Examples 4.5 and 4.6. The BTTA constructed as above in this case has the following transitions rules (we forget several useless rules for the sake of clarity):

a → {a, c}, q a , c → {c}, q reject , f {a, c}, q ′ , {a, c}, q ′ ---→ 1=2 {c}, q (q ′ = q a , q), f {c}, q ′ , {c}, q ′ ---→ 1=2 {c}, q , g( {a, c}, q * ) → {c}, q reject , g( {c}, q * ) → {c}, q reject (q * = q a , q, q reject ). 3

The following lemma states the correctness of the construction of the BTTA A R .

Lemma 4.8 For all t ∈ T (Σ) A R (t) = {d ∈ Σ 0 | d --→ R t}, B(t) .
Proof. Let A R (t) = S, q . It is straightforward by construction that B(t) = q. We prove S = {d ∈ Σ 0 | d --→ R t} by induction on the size of t. We first consider the case where t is a constant. By definition of A R , S = {d ∈ Σ 0 | (t|∅) ∈ r d }. It suffices to see that the conditions d --→ R t and (t|∅) ∈ r d are equivalent when t is a constant. This is a consequence of conditions (a) and (c) above. Now, assume that t is of the form f (t 1 , . . . , t m ). Let S 1 , q 1 = A R (t 1 ), . . . , S m , q m = A R (t m ). By induction hypothesis, B(t i ) = q i and S i = {d ∈ Σ 0 | d --→ R t i }, for every i ∈ {1, . . . , m}. Let f S 1 , q 1 , . . . , S m , q m -→ P S, q be the rule fired in the last applied transition of A R (t). Then, it holds that i ≡ P j iff t i = t j . We prove the two inclusions of S = {d ∈ Σ 0 | d --→ R t} separately. Direction ⊆. Let c ∈ S. By construction of A R there exists a constrained term f (α 1 , . . . , α m )|C ∈ (r c ∪ r c ) for which the above conditions i and ii hold.

Let σ be a substitution of domain vars(f (α 1 , . . . , α m )) with σ(α i ) := t i . The substitution σ is well defined: if for different i and j we have α i = α j ∈ V, by condition ii, it implies that i ≡ P j and then t i = t j . It holds that every such σ(α i ) is a non-constant normal form, because α i ∈ V implies that

q i = B(t i ) ∈ Q 1 due to condition i. Moreover, σ(α i ) is reachable from C(α i ) because α i ∈ V implies C(α i ) ⊆ S i from condition i and S i = {d ∈ Σ 0 | d --→
R t i } by induction hypothesis. Altogether, it follows that σ(f (α 1 , . . . , α m )) is an instance of f (α 1 , . . . , α m )|C ∈ (r c ∪r c ). We know that either f (α 1 , . . . , α m )|C ∈ r c or f (α 1 , . . . , α m )|C ∈ r c \r c . On the one hand, if f (α 1 , . . . , α m )|C ∈ r c then, by condition a, c --→ R σ(f (α 1 , . . . , α m )). On the other hand, if f (α 1 , . . . , α m )|C ∈ r c \ r c then condition ii implies that B(f (q 1 , . . . , q m ), P ) ∈ Q 1 , and hence q ∈ Q 1 and t is a non-constant normal form. Moreover, the α i 's that are constants are also normal forms. For every one of these constants α i we know that α i ∈ S i , and hence we also have α i --→ R t i . But since this α i is a normal form it follows that α i = t i . This implies that σ(f (α 1 , . . . , α m )) = t, and hence, that t is a non-constant normal form that is an instance of f (α 1 , . . . , α m )|C ∈ r c , and by condition b, c --→ R σ(f (α 1 , . . . , α m )). Hence it suffices to show that σ(f (α 1 , . . . , α m )) --→ R t in order to conclude. By definition of σ, terms σ(f (α 1 , . . . , α m )) and t can only differ in the positions i such that α i is a constant. But in such cases we know that α i ∈ S i , and using

S i = {d ∈ Σ 0 | d --→ R t i } we obtain α i --→ R t i . Hence, σ(f (α 1 , . . . , α m )) --→ R t follows.
Direction ⊇. Let c be such that c --→ R t. Since t is not a constant, the previous derivation can be written by making explicit the last rewrite step at position Λ as (>Λ represents any position other than Λ):

c --→ R ---→ R,Λ f (s 1 , . . . , s m ) ----→ R,>Λ t = f (t 1 , . . . , t m )
Hence, there exist (sub-)derivations s i --→ R t i . The term s = f (s 1 , . . . , s m ) is a weak normal form, and hence, by condition c, there exists a constrained term u|C ∈ r c such that s is an instance of u|C. At this point, either there exists such a u of the form f (α 1 , . . . , α m ), or every u satisfying this condition is a variable. In the second case, s is necessarily a normal form, and hence, by condition d, there exists a constrained term f (α 1 , . . . , α m )|C in r c such that s is an instance of f (α 1 , . . . , α m )|C. For proving that c ∈ S, it suffices to show that the conditions i and ii hold.

If a certain α i is a constant, then it coincides with s i , which R-reaches t i . Since

S i = {d ∈ Σ 0 | d --→ R t i }, it necessarily contains α i .
If a certain α i is a variable, then s i coincides with t i and is a non-constant normal form reachable from C(α i ). Hence, q i = B(t i ) is in Q 1 , and again since

S i = {d ∈ Σ 0 | d --→ R t i }, it necessarily includes C(α i ). If α i = α j ∈ V then s i = s j
and since both are normal forms we also have t i = t j , from which i ≡ P j follows.

In the case where f (α 1 , . . . , α m )|C belongs to r c \ r c , f (s 1 , . . . , s m ) is a nonconstant normal form. Therefore, q = B(f (q 1 , . . . , q m ), P ) ∈ Q 1 and all the constants α i are also normal forms.

2

Given a flat TRS R and a regular set L, the BTTA A Rc (corresponding to the R c associated to R as in Lemma 4.4), restricted to the signature Σ of R, recognizes R (L) by marking as accepting states the pairs S, q such that c ∈ S, according to Lemmas 4.4 and 4.8. Together with the simplifying assumptions on the TRS, this permits to conclude the proof of Theorem 4.9.

Theorem 4.9 R (L) is BT-regular when L is regular and R is shallow.

Ground reachability (is a given ground term t reachable from another given ground term s?) and joinability (does there exists a term u reachable from two given ground terms s and t?) are undecidable for flat TRSs [START_REF] Mitsuhashi | The confluence problem for flat TRSs[END_REF]. They become decidable when the innermost strategy is applied [START_REF] Godoy | Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems[END_REF]. We can express this property here as a corollary of Theorem 4.9.

Corollary 4.10 Ground reachability and joinability are decidable for innermost rewriting with shallow TRS.

Proof. When restricting to innermost rewriting, t is reachable from s iff t ∈ R ({s}). Since {s} is a regular language when s is ground, R ({s}) is BT-regular by Theorem 4.9. Therefore ground reachability reduces to the membership problem for BTTA, which is decidable.

Similarly, s and t are joinable iff R ({s}) ∩ R ({t}) = ∅. By Theorem 4.9 and closure of BT-languages under Boolean operations [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF], we obtain a reduction of ground joinability to the emptiness problem for BTTA, which is also decidable. 2

In [START_REF] Bogaert | The recognizability problem for tree automata with comparisons between brothers[END_REF] the decidability of the regularity of a BTTA was shown. Combining this result with Theorem 4.9 we obtain the following corollary.

Corollary 4.11 Given a regular language L and a shallow TRS R, it is decidable whether R (L) is regular. This result does not hold when we deal with plain rewriting. In [START_REF] Mitsuhashi | The confluence problem for flat TRSs[END_REF] it has been proved that reachability is undecidable for flat TRSs by reduction of the Post correspondence problem into 0 --→ * R 1. We show below how to extend R into R 0 such that R * 0 (0) is regular iff 0 --→ * R 1. Theorem 4.12 Given a regular language L and a flat TRS R, it is undecidable whether R * (L) is regular.

Proof. In [START_REF] Mitsuhashi | The confluence problem for flat TRSs[END_REF] it is proved that reachability is undecidable for flat TRSs by reduction of a PCP instance P into a TRS R over a signature including {0, 1} such that P has a solution iff 0 --→ * R 1. The reduction in [START_REF] Mitsuhashi | The confluence problem for flat TRSs[END_REF] also satisfies that if P has no solution, the 0 does not reach any term containing 1 nor any term containing 0 properly.

This reduction can be modified by adding new symbols {f, h, g, a, b, c} to the current signature Σ, and adding two new sets of rules to R:

R 1 = {0 → f (a, b), a → g(a), b → g(b), a → c, b → c, f (x, x) → h(x,
x)} and R 2 containing all the necessary rules for making R * 2 (1) to be T (Σ ∪ {f, h, a, b, c}). The rules of R ensure (R ∪ R 1 ∪ R 2 ) * (0) to be a non-regular language, unless 0 --→ * R 1. Note that if P has solution, then 0 --→ * R 1, and hence (R ∪ R 1 ∪ R 2 ) * (0) is T (Σ ∪ {f, h, a, b, c}), which is regular. Otherwise, if P has no solution, then 0 does not reach any term containing 1, nor containing 0 properly, and hence

(R ∪ R 1 ∪ R 2 ) * (0) ∩ T ({h, c}) is the set {h(g n (c), g n (c)) | n > 0}, which is not regular. 2
5 Innermost rewriting and right-shallow TRS

In this section, we study the closure of regular languages under innermost rewriting with TRS whose right-hand sides of rules are shallow. We show that regularity is preserved by innermost rewriting with linear right-shallow TRSs (Subsection 5.1), but not by innermost rewriting with right-(linear and flat) (non left-linear) TRSs (Subsection 5.2). The first result was also proved independently in [START_REF] Kojima | Innermost reachability and context sensitive reachability properties are decidable for linear right-shallow term rewriting systems[END_REF].

5.1 TA languages and linear and right-shallow TRS First, we observe that every right-shallow TRS R can be transformed into a rightflat TRS R ′ (on an extended signature) such that for all s, t ∈ T

(Σ), s --→ R t iff s --→ R ′ t.
The idea is to add a new constant c r and a rule c r → r for every ground proper subterm r of a right-hand side of a rule of R, and to replace r by c r in all the right-hand sides of R. This transformation preserves linearity and reachability between terms of the original signature.

Let A = (Q, Q f , ∆) be a deterministic and complete TA on Σ recognizing a tree language L, and let R be a linear and right-flat TRS. For all c ∈ Σ 0 we denote as q c the unique state of Q such that c → q c ∈ ∆. We assume moreover wlog that L(A, q c ) = {c}.

We construct a finite sequence of TA A 0 , A 1 , . . . whose last element recognizes R (L). The construction of the sequence is incremental. Every A k+1 is obtained from A k by the addition of some new transitions, such that if some term s is recognized by A k and s rewrites (in one step of innermost rewriting) to t, then t is recognized by A k+1 .

In order to restrict to innermost rewriting, we shall use a complete and deterministic TA B = (Q B , Q f B , ∆ B ) (without ε-transitions) recognizing the ground R-normal forms (see e.g. [START_REF] Comon | Tree automata techniques and applications[END_REF] for its construction). As in Lemma 2.2, we can assume that B has only one non-accepting state q reject . Let A 0 be a TA recognizing L(A):

A 0 := Q × Q B , Q f × Q B , ∆ 0
where ∆ 0 is the set of transitions f q 1 , q ′ 1 , . . . , q m , q ′ m → q, q ′ such that f (q 1 , . . . , q m ) → q ∈ ∆ and f (q ′ 1 , . . . , q ′ m ) → q ′ ∈ ∆ B . The addition of transition rules to A k , giving A k+1 , is defined by the superposition of rules of R into a sequence of transitions of ∆ k . More precisely, A k+1 \A k contains all the transitions which can be constructed from a rewrite rule ℓ → r of R (we let ℓ = f (ℓ 1 , . . . , ℓ m )) and a substitution θ of the variables of ℓ into states of Q × Q f B whose accepted language wrt A k is not empty, such that: θ(ℓ) --→ * ∆ k q 0 , q reject , and the last step of the above reduction is f q 1 , q ′ 1 , . . . , q m , q ′ m --→ ∆ k q 0 , q reject and for all i ≤ m, q ′ i = q reject . There are two cases for the transitions of A k+1 \ A k : • case 1: r is a variable. In this case, r ∈ vars(ℓ). Let q, q ′ = θ(r), we add the ε-transition q, q ′ -→ q 0 , q ′ .

• case 2: r = g(r 1 , . . . , r m ). We add all the transitions g q 1 , q ′ 1 , . . . , q m , q ′ m → q 0 , q ′ such that g(q ′ 1 , . . . , q ′ m ) → q ′ ∈ ∆ B and for each i ≤ m, if r i is a variable then q i , q ′ i := θ(r i ), otherwise, if r i is a constant then q i is q r i and there is no restriction for q ′ i .

All the TAs have the same state set, hence the construction terminates with a fixpoint denoted A * . The number |A * | of states of A * is at most |A| × |B|, and the number of rules of A * is polynomial in the same measure3 , if we assume as usual that the maximum arity m of a function symbol is fixed for the problem.

We show that L(A * ) = R (L(A)), more precisely, that for all t ∈ T (Σ), t ∈ L A * , q, q ′ iff t ∈ L(B, q ′ ) and there exists s ∈ L(A, q) such that s --→ R t. To this end we follow the principle of the proofs given e.g. in [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting 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], but some technical difficulties appear when we try to replace a subterm by another subterm while preserving an execution with ∆ * . They are solved thanks to the following technical Lemma 5.1.

Lemma 5.1 For all t ∈ T (Σ ∪ Q A * ), if t q 0 , q reject p --→ * ∆ * q, q reject then, for all q ′ ∈ Q B , there exists q ′′ ∈ Q B such that t[ q 0 , q ′ ] p --→ * ∆ * q, q ′′ .
Proof. First of all, we note that no ε-transition is applied in t --→ * ∆ * q, q reject at position p ′ ≤ p wrt the prefix ordering. This is due to the fact that the ε-transitions are always of the form , q nr → , q nr ∈ Q B for some q nr different from q reject , since this kind of transitions are derived in case 1 using rules where the right-hand side is a variable, and hence, it is necessarily instantiated by a normal form.

Hence, it suffices to prove the statement of the lemma for the case where t is of the form f ( q 1 , q ′ 1 , . . . , q m , q ′ m ), p is a certain position i, and there is just one rewrite step derivation with a rule of the form f ( q 1 , q ′ 1 , . . . , q i , q ′ i , . . . , q m , q ′ m ) → q, q reject . The global statement is then obtained inductively. In this case, q i is q 0 , and q ′ i is q reject . If the rule f ( q 1 , q ′ 1 , . . . , q i , q ′ i , . . . , q m , q ′ m ) → q, q reject is in ∆ 0 , by the definition of ∆ 0 we have that for any q ′ ∈ Q B there exists also an alternative rule of the form f ( q 1 , q ′ 1 , . . . , q i , q ′ , . . . , q m , q ′ m ) → q, q ′′ , for some q ′′ , and we are done. Otherwise, assume that this rule f ( q 1 , q ′ 1 , . . . , q i , q ′ i , . . . , q m , q ′ m ) → q, q reject is not in ∆ 0 . Then it has been derived by case 2 using a rule ℓ → f (r 1 , . . . , r m ) ∈ R. Moreover, by the conditions of case 2 and the fact that q ′ i is q reject we know that r i is not a variable, and hence, it is a constant. Again by the conditions of case 2, for any q ′ ∈ Q B there exists also an alternative rule of the form f ( q 1 , q ′ 1 , . . . , q i , q ′ , . . . , q m , q ′ m ) → q, q ′′ , for some q ′′ , and we are done. 2

Theorem 5.2 R (L) is regular when L is regular and R is linear and right-shallow.

The proof of the correctness of the construction of A * is a direct consequence of the following Lemma 5.3. Lemma 5.3 For all t ∈ T (Σ), t ∈ L A * , q, q ′ iff t -→ * B q ′ and there exists s ∈ L(A, q) such that s --→ R t.

Proof. Direction ⇐. We prove it by induction on the number of rewrite steps of s --→ R t. For 0 rewrite steps we have s = t, and hence, t --→ * ∆ q. From the construction of ∆ 0 , t --→ * ∆ 0 q, q ′ follows, and since ∆ 0 ⊆ ∆ * we also have t --→ * ∆ * q, q ′ , and we are done. Hence, assume that there is at least one rewrite step in s --→ R t. We can write this derivation by making explicit the last rewrite step as s --→ R t[σ(l)] p -----→ ı ℓ→r,p,σ t[σ(r)] p = t. By induction hypothesis, t[σ(ℓ)] p --→ * ∆ * q, q reject (the q reject is due to the fact that t[σ(ℓ)] p is not a normal form). By re-ordering the rule applications of ∆ * , we can assume that this derivation is of the form

t[σ(ℓ)] p --→ * ∆ * t[θ(ℓ)] p --→ * ∆ * t[ q 0 , q reject ] p --→ * ∆ * q, q reject
where θ is a mapping from variables to states of ∆ * . By the conditions for adding new rules into the ∆ j 's, we also have θ(r) --→ * ∆ * q 0 , q ′ 0 for some q ′ 0 ∈ Q B , and since the variables of r occur also in ℓ, there exists a derivation σ(r) --→ * ∆ * θ(r) --→ * ∆ * q 0 , q ′ 0 , and hence, by Lemma 5.1,

t[σ(r)] p --→ * ∆ * t[θ(r)] p --→ * ∆ * t[ q 0 , q ′ 0 ] p --→ * ∆ * q, q ′′
for some q ′′ . But this q ′′ is necessarily q ′ since ∆ * simulates B on the second component of the pairs, and we are done. Direction ⇒. The fact that t -→ * B q ′ follows directly from the construction of B: note that all the ∆ i 's always simulate the execution of B for the second component of the pair of states. For proving that ∃s : (s --→ * ∆ q ∧ s --→ R t), we do an induction on the measure defined as follows. For a concrete derivation t --→ * ∆ * q, q ′ , we call Rules(t --→ * ∆ * q, q ′ ) the multiset of all rules used in it, and define Ind(t --→ * ∆ * q, q ′ ) as the multiset obtained by replacing every occurrence of a rule ℓ → r in Rules(t --→ * ∆ * q, q ′ ) by the least index i such that ℓ → r ∈ ∆ i . We compare indexes of derivations by the multiset extension of the usual ordering on natural numbers, and prove the statement of the lemma by induction on this ordering. Now, we distinguish cases depending on whether the last rewrite step of t --→ * ∆ * q, q ′ is an ε-transition or not. Assume first that it is an ε-transition. Then, this derivation can be written of the form t --→ * ∆ * q 0 , q ′ --→ ∆ * q, q ′ for a certain state q 0 , q ′ of Q ∆ * . The rule q 0 , q ′ → q, q ′ is not in ∆ 0 , and has been necessarily added into some ∆ i with i > 0 by case 1, using a collapsing rule ℓ → x ∈ R and a substitution θ such that θ(x) = q 0 , q ′ and θ(ℓ) ----→ * ∆ i-1

q, q reject . Moreover, for the rest of variables y of ℓ different from x, there exist terms t y ∈ T (Σ) such that t y ----→ * ∆ i-1 θ(y). We define a substitution σ such that σ(y) = t y for every of such y, and σ(x) = t. The substitution σ is well defined because R is right-linear.

Hence, we have a one rewrite step derivation σ(ℓ) ----→ ı ℓ→x,σ t, which is innermost due to the conditions for the addition of the rule to ∆ i (condition q ′ i = q reject there). Now, note that the multiset Ind(t --→ * ∆ * q 0 , q ′ ) has just one less i than Ind(t --→ * ∆ * q, q ′ ), and that the multiset Ind(θ(ℓ) ----→ * ∆ i-1

q, q reject ) and the respective multisets Ind(t y ----→ * ∆ i-1 θ(y)) contain numbers smaller than i. Therefore, composing the previous derivations we can construct a derivation σ(ℓ) --→ * ∆ * q, q reject smaller than t --→ * ∆ * q, q ′ . Hence, by induction hypothesis, there exists a term s such that s --→ R σ(ℓ) and s --→ * ∆ q, and, since t is R-reachable from s, we are done. Now, assume that the last rewrite step of t --→ * ∆ * q, q ′ is not an ε-transition. Hence, this derivation can be written by making explicit the last step as t --→ * ∆ * f ( q 1 , q ′ 1 , . . . , q m , q ′ m ) --→ ∆ * q, q ′ . Thus, if we write t of the form f (t 1 , . . . , t m ), we can take (sub-)derivations t

1 --→ * ∆ * q 1 , q ′ 1 , . . . ,t m --→ * ∆ * q m , q ′ m . Every Ind(t i --→ * ∆ * q i , q ′ i ) is smaller than Ind(t --→ * ∆ *
q, q ′ ), and thus, by induction hypothesis there exist terms s 1 , . . . s m and derivations s i --→ * ∆ q i and s i --→ R t i . At this point we distinguish cases depending on whether the rule f ( q 1 , q ′ 1 , . . . , q m , q ′ m ) → q, q ′ belongs to ∆ 0 or not. Assume first that it belongs to ∆ 0 . Then, by the definition of ∆ 0 , there exists also a rule f (q 1 , . . . , q m ) → q in ∆. Therefore, by composing this and the previous derivations, we have f (s 1 , . . . , s m ) --→ * ∆ q, but also f (s 1 , . . . , s m ) --→ R f (t 1 , . . . , t m ) = t, and we are done. Now, assume that f ( q 1 , q ′ 1 , . . . , q m , q ′ m ) → q, q ′ has been added by case 2 into some ∆ i with i > 0 using a rule of the form ℓ → f (r 1 , . . . , r m ) and a substitution θ satisfying the following properties. On the one side, θ(ℓ) ----→ * ∆ i-1

q, q reject . On the other side, for every r i , if r i is a variable then q i , q ′ i is θ(r i ) and q ′ i = q reject , and otherwise, if r i is a constant then q i is q r i and there is no restriction on q ′ i . Moreover, for the variables y occurring in ℓ and not in f (r 1 , . . . , r m ) there exist terms t y ∈ T (Σ) such that t y ----→ * ∆ i-1 θ(y). We define a substitution σ such that σ(y) = t y for every of such y, and σ(r i ) = t i for the r i that are variables. As above, σ is well defined because R is right-linear. Hence, we have a one rewrite step derivation σ(ℓ) - ----------→ ℓ→f (r 1 ,...,rm),σ σ(f (r 1 , . . . , r m )), which is innermost due to the conditions for the addition of the rule to ∆ i , again. The terms σ(f (r 1 , . . . , r m )) and t = f (t 1 , . . . , t m ) can differ only in the positions i such that r i is a constant. For an i of this kind, q i is q r i , and the only term of T (Σ) that can be derived into q r i with ∆ is r i . Therefore, s i is r i , and hence, there exists a derivation r i --→ R t i . This implies that σ(f (r 1 , . . . , r m )) --→ R t. To conclude, it suffices to see that there exists a term s such that s --→ R σ(ℓ) and s --→ * ∆ q. To this end, we will prove that there exists a derivation σ(ℓ) --→ * ∆ * q, q reject smaller than t --→ * ∆ * q, q ′ , and the statement will follow by induction hypothesis. But this is identical to what we have done in a previous case. Note that the multiset Ind(θ(ℓ) ----→ * ∆ i-1

q, q reject ) and the respective multisets Ind(t y ----→ * ∆ i-1 θ(y)) contain numbers smaller than i. Moreover, for the variables x that occur in f (r 1 , . . . , r m ), left-linearity ensures that the indexes are preserved in these cases. Therefore, composing the previous derivations we can construct a derivation σ(ℓ) --→ * ∆ * q, q reject smaller than t --→ * ∆ * q, q ′ , and we are done.

Conclusion and further work

We have covered much of the cases of closure of TA and BTTA languages by innermost rewriting, providing results for each case. The positive results are that the set of terms innermost-reachable from a regular language with a shallow TRS is BT-regular, and it is regular when the TRS is linear and right-shallow. Moreover, given a shallow TRS, regularity of the innermost-reachable terms from a regular language is decidable. Other consequences are the decidability of the problems of ground reachability, ground joinability and regular tree model checking (given two regular languages L init and L bad and the TRS R, do we have R L init ∩ L bad = ∅?) for innermost rewriting with TRS in the above classes.

As future work, it could be interesting to consider other variants of TA with more general or different constraints, and to consider other strategies of rewriting different from innermost. the form f (q 1 , . . . , q n , q ′ g , . . . , q ′ g ) -----------→ P ∪{{n+1,...,m}} q by converting these rules into g(q 1 , . . . , q n ) -→ P q.

Second assumption: flat TRS.

Finally we do a last transformation that allows us to assume that all rules in R are flat. If this was not the case, we can modify R as follows. First remove all rules l → r such that l has a proper subterm that is not a normal form: note that in such a case this rule is useless for innermost rewriting. Second, we proceed by applying several times the following transformation step a), until the obtained TRS is left-flat.

Step a. If there is a non-constant term t that is a proper subterm of a left-hand side of a rule4 in R, then create a new constant c, replace all occurrences of t in the left-hand sides of the rules of R by c, and add the rule t → c to R.

In the following two lemmas and proofs we assume that R ′ is obtained from R by the previous transformation with t and c, Σ is the original signature, and Σ ′ is Σ ∪ {c}.

Lemma A.2 Let s 1 , s 2 be terms in T (Σ, V). Then,

s 1 --→ R s 2 iff s 1 --→ R ′ NF {t→c} (s 2 ).
Proof. Direction ⇒. We first show that if s 1 --→ 2

The new R ′ does not necessarily preserve the language of reachable terms from a given regular set. Since our global goal is to justify that this reachable set is BT-regular, we will need to retrieve it by, essentially, inverting the transformation. This can be done using Lemma A.3 below.

At this point we assume that L is a regular language and A ′ is a BTTA recognizing R ′ (L). Without loss of generality, we assume that A ′ has two states q c and q t such that c and t are the only terms that run to q c and q t , respectively, by A ′ . Moreover, for the case of c we assume the existence of a rule c → q c . We construct a BTTA A for R (L) by removing c → q c from A ′ and adding q t → q c . Lemma A.3 L(A) = R (L).

Example 3 . 1

 31 Let Σ = {a : 0, g : 1, f : 2} and R := {g(x) → f (x, x)} as in Example 2.3 and let L be the regular language {g n (a) | n ≥ 0} = {a, g(a), g(g(a)), . . .}.

Example 4 . 5

 45 Let Σ = {a : 0, g : 1, f : 2}, R := {g(x) → f (x, x)} and L = {g n (a) | n ≥ 0} as in Example 3.1. In order to fulfil the conditions of Lemma 4.4, we let Σ ′ = Σ ⊎ {c}, and R c = R ∪ {c → g(c), c → a}.

Example 4 . 6

 46 Let us consider the TRS R c = {g(x) → f (x, x), c → g(c), c → a} of Example 4.5. We have NF R (c) = Bin, the set of complete binary trees of T {a, f } .

2 5. 2 Proposition 5 . 4

 2254 Closure of TA languages with right-(linear and flat) TRSWhen we drop the restriction that R is left-linear in Theorem 5.2, we lose regularity preservation with innermost rewriting. This is in contrast with plain rewriting, since regularity is preserved for right-linear and right-shallow TRSs[START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF]. In general, R (L) is not BT-regular when L is regular and R is right-linear and right-flat.Proof. Let L = {f (f (a, a), c)}, and R = {f (x, c) → x, f (g(x), x) → h(x), h(x) → h(x), a → g(a), a → b}. The intersection of R (L) with the language of all terms containing only the symbols f , g, b is the set {f (g n (b), g m (b)) | n = m + 1}, which is not BT-regular.2

ı R s 2

 2 , then NF {t→c} (s 1 ) --→ R NF {t→c} (s 2 ). This is because if l → r ∈ R is the used rule in s 1 --→ ı R s 2 ,then, using the corresponding l[c] . . . [c] → r obtained by the transformation from R into R ′ we have NF {t→c} (s 1 ) -------→ ı l[c]...[c]→r ---→ t→c NF {t→c} (s 2 ). Now, from any derivation s 1 --→ R s 2 can be obtained a derivation s 1 ---→ t→c NF {t→c} (s 1 ) --→ R ′ NF {t→c} (s 2 ) by applying several times the previous observation. Direction ⇐. On the other side, consider any rewrite step u --→ ı R ′ v. It holds that NF {c→t} (u) --→ R 0,1 NF {c→t} (v). Therefore, since s 1 and s 2 are terms without the constant c, s 1 --→ R ′ NF {t→c} (s 2 ) implies s 1 = NF {c→t} (s 1 ) --→ R NF {c→t} (NF {t→c} (s 2 )) = s 2 .

Note however that |B| can be exponential in the size of R in the worst case.

Note that the subterm t is a normal form.

 [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF]The first two authors were supported by Spanish Min. of Educ. and Science by the FORMALISM project (TIN2007-66523) and by the LOGICTOOLS-2 project (TIN2007-68093-C02-01)

Appendix

A Simplifying assumptions

We show that the assumptions of Section 4.2 can be made without loss of generality. Such assumptions have appeared in some previous works, in particular [START_REF] Godoy | Innermost-reachability and innermost-joinability are decidable for shallow term rewrite systems[END_REF].

First assumption: signature.

We assume that all terms are constructed over a given fixed signature Σ that contains several constants and only one non-constant function symbol f . If this was not the case, we can define a transformation T from terms over Σ into terms over a new signature Σ ′ as follows. Let m be the maximum arity of a symbol in Σ plus 1. We chose a new function symbol f with arity m and define the new signature

Note that all symbols of Σ appear also in Σ ′ but with arity 0. Now, we recursively define T : T (Σ, V) → T (Σ ′ , V) as T (c) = c and T (x) = x for constants c ∈ Σ 0 and variables x ∈ V, and T (g(t 1 . . . t k )) = f (T (t 1 ), . . . , T (t k ), g, . . . , g) for terms headed with g ∈ Σ \ Σ 0 . We denote {T (l) → T (r) | l → r ∈ R} by T (R) for a given TRS R. Note that the size of T (R) is at most m times the size of R, and hence, this transformation can be easily obtained in polynomial time. Note also that T preserves linearity, flatness and shallowness.

Lemma A.1 Let s, t be terms in T (Σ, V) and R a TRS with all its terms in

Proof. By the recursive definition of T it is easy to see that T (u[v] p ) = T (u)[T (v)] p for all terms u, v ∈ T (Σ, V). Moreover, for any substitution σ : V → T (Σ, V), T (uσ) = T (u)T (σ), where we understand T (σ) as the substitution {x → T (xσ) | x ∈ dom(σ)}, i.e. the substitution holding xT (σ) = T (xσ). Hence, for every rule

Moreover, all rule applications with T (R) on terms of the form T (u) are always of the form T (u) --------→ ı T (l)→T (r),p T (v). The lemma follows from these considerations.

2

Recall that our goal is to compute a BTTA for R (L) for a given regular language L and TRS R. After the previous change the TRS R ′ works on a different signature. Thus we need to adapt the TA A for L. This can be done easily with the transformation T (g(q 1 , . . . , q n ) → q) → (f (q 1 , . . . , q n , q g , . . . , q g ) → q) for every rule g(q 1 , . . . , q n ) → q, and adding a rule g → q g for every new constant g. If L ′ is the language recognized by A ′ , after computing a BTTA A ′ 2 for R ′ (L ′ ) we can retrieve an automaton for R (L) as follows. Without loss of generality we can assume that for every new constant g, there is a state in A ′ 2 , which we call q ′ g , such that g is the only term that reaches q ′ g with R ′ . Note also that, by previous lemma, the reachable terms from L ′ are images of terms of the original signature by T . Hence, we can just invert the transformation for the rules of Proof. Direction ⊇. Let s 2 ∈ R (L). Then, there exists a term

, and by the construction of A, s 2 ∈ L(A).

Direction ⊆. Let s 2 ∈ L(A). Then, there exists a derivation from s 2 into an accepting state of A using the rules of A. Let s ′′ 2 be obtained from s 2 by replacing the subterms t that are rewritten to q c in the previous derivation by c. Then, s ′′ 2 ∈ L(A ′ ), and hence, there exists

Let s ′ 2 be obtained from s ′′ 2 (or from s 2 , it does not matter) by replacing all the occurrences of t by c. Since the rule t → c is in R ′ , we also have s 1 --→ R ′ s ′ 2 , and since s ′ 2 = NF t→c (s 2 ), by Lemma A.2, s 1 --→ R s 2 and hence s 2 ∈ R (L). 2

Finally, we apply several times the following transformation step until the TRS is right-flat.

Step b.

If there is a non-constant term t that is a proper subterm of a right-hand side of a rule in R, then create a new constant c, replace all occurrences of t in the right-hand sides of the rules of R by c, and add the rule c → t to R.

Lemma A.4 Let s 1 , s 2 be terms in T (Σ, V) and let R ′ be obtained from R by the previous transformation step b). Then,

Since in step b) the reachable terms over the original signature are preserved, a simple intersection allows to retrieve the desired BTTA.

Every step (a or b) decreases the total sum of the number of positions at depth more than one in all the left-hand and right-hand sides of R. Moreover, also at every step, the total size of the TRS increases by the size occupied by a constant. Hence, this process terminates in polynomial time.