Sébastien Limet
email: flimet@lifo.univ-orleans.fr

Pierre Réty

E-unification by means of tree tuple synchronized grammars

Keywords: E-unification, narrowing, tree languages, decidability 1, 1), (R 1 2, 1))

E-unification by means of tree tuple synchronized grammars

Introduction

First order E-unification [START_REF] Plotkin | Building-in equational theories[END_REF] is a tool that plays an important role in automated deduction, in particular in functional logic programming and for solving symbolic constraints (see Baader and Siekmann [START_REF] Baader | Unification theory[END_REF] for an extensive survey of the area). It consists of finding instances to variables that make two terms equal modulo to an equational theory given by a set of equalities, i.e. it amounts to solving an equation (called a 'goal'). General E-unification is undecidable and may have infinitely many solutions. This is why E-unification procedures, like narrowing, often loop, enumerating an infinite set of unifiers or computing unproductive branches [START_REF] Hullot | Canonical forms and unification[END_REF][START_REF] Nutt | Basic narrowing revisited[END_REF][START_REF] You | Enumerating outer narrowing derivations for constructor-based term rewriting systems[END_REF][START_REF] Chabin | Narrowing directed by a graph of terms[END_REF][START_REF] Moreno-Navarro | Logic programming with functions and predicates: The language BABEL[END_REF][START_REF] Bockmayr | Narrowing strategies for arbitrary canonical systems[END_REF][START_REF] Antoy | A needed narrowing strategy[END_REF][START_REF] Burghardt | Regular substitution sets: a means of controlling E-unification[END_REF]. From the programming point of view, it is very important to avoid infinite loops when possible.

When solving equations in a computation (of a functional logic program, for instance), most of the time it is not interesting to enumerate the solutions. It is more important to test whether the equation has at least one solution (unifiability test), and to have a finite representation of the solutions. The first point allows us to cut off unproductive branches, and the second avoids the generation of an infinite sets of solutions.

We have several aims in this paper. First, we want to define restrictions on the unification problem that ensure the decidability of unifiability. In addition to the confluence and constructor-based property of the rewrite system that represents the equational theory, there are four other restrictions shown to be necessary in deciding unifiability (i.e. if any of them are not satisfied, unifiability is undecidable). Thus, these restrictions define a limit between decidability and undecidability of unifiability. Our second goal is to give an E-unification procedure that never loops when our restrictions are verified, and that decides upon unifiability. The problem is that theories defined in this framework may be infinitary, i.e. for some 1365-8050 c 1997 Chapman & Hall goals the set of solutions cannot be described by a finite complete set of unifiers. So we need a way in which to represent infinite sets of substitutions.

A solution being defined by the instances of the variables of the goal, i.e. by a tuple of terms, and terms being trees, the set of solutions can be viewed as a tree tuple language. To describe this language, we introduce an ad hoc kind of grammar, the Tree Tuple Synchronized Grammars (TTSG). Their particularity is the notion of synchronization, i.e. the fact that some productions must be applied at the same time. For this reason TTSGs can define languages like fd(a i (0);b i (0);c i (0))g. The class of languages defined by TTSGs is larger than we need, and does not have nice properties. Fortunately, we do not build many TTSGs from a unification problem, and the recognized languages have particular properties: their intersection is a language recognized by a TTSG, and emptiness is decidable.

As Example 8.8 shows, symmetric binary trees appear to be the solution to some unification problem that satisfy our restrictions. Therefore, introducing a new kind of grammar was necessary because, as far as we know, there is no standard grammar or tree automaton technique that can express the symmetric binary trees, and whose emptiness is decidable.

Some authors have already used tree languages to represent infinite sets of solutions. For example inGilleron et al. [START_REF] Gilleron | Some new decidability results on positive and negative set constraints[END_REF], they are used to solve set constraints, but without synchronization. The notion of synchronization has already appeared in string grammars, for example, as in parallel communicating grammar systems [START_REF] Dumitrescu | Pattern Languages versus Parallel Communicating Grammar Systems[END_REF] and in tree grammars [START_REF] Guan | Tree Grammars with Multilinear Interpretation[END_REF]. However the TTSGs are not identical to the coupled context-free grammars of Guan et al. [START_REF] Guan | Tree Grammars with Multilinear Interpretation[END_REF] because we need a finer control of synchronizations which is achieved thanks to a tuple of integers. The following example explains the principle of our procedure. Step 1. The goal f (g(x)) ? =0is decomposed into three parts, g(x) ? = y 1 , f (y 2 ) ? = y 3 and 0 ? = y 4 , where y 1 ;y 2 ;y 3 ;y 4 are new variables. The set of ground data-solutions of g(x) ? = y 1 can be considered as an infinite set of pairs of terms defined by f(t 1 ;t 2 )jg(t 2 ) ! t 1 g. This set is considered as a language (say L 1 ) of pairs of trees where the two components are not independent. In the same way, the set of ground data-solutions of f (y 2 ) ? = y 3 can be viewed as the language (say L 2 ) of pairs of trees that describes the set f(t 1 ;t 2 )jf(t 2 ) ! t 1 gand 0 can be viewed as the language (say L 3 ) of 1-tuple reduced to f(0)g. These languages can be described by TTSGs. The grammars are computed from the rewrite system and the goal.

Step 2. Once these three TTSGs are constructed, the initial goal is re-composed by two steps. First, the languages L 1 and L 2 are combined to get the language L 4 of the ground data-solutions of f (g(x)) ? = y 3 . This is done by computing a special kind of intersection between two TTSGs that corresponds to the join operation in relational databases. The result is a TTSG that describes the language of triples of trees defined by f(t 1 ;t 2 ;t 3 )j(t 2 ;t 3 ) 2L 1 and (t 1 ;t 2 ) 2L 2 g .I no t h e rw o r d s ,t 2 is the result of g(x) when instantiating x by t 3 ; moreover, t 2 belong to the definition domain of the function f , and t 1 is the result of f (t 2 ),i.e.off(g(t 3 )). Secondly, the TTSG of L 4 is combined with the TTSG of L 3 in the same way. We get a TTSG that describes the language of triples of trees L 5 defined by f(t 1 ;t 2 ;t 3 )jt 1 =0and (t 1 ;t 2 ;t 3 ) 2L 4 g .A s t 3 is an instance of x, t 1 is the result of f (g(t 3 )) and t 1 =0 , and we get a finite description of the ground data-substitutions such that f(g(x)) ! 0. Moreover, it is decidable whether the language L 5 is empty or not. Therefore, we can decide upon the unifiability of f (g(x)) ? =0 .

Soundness and completeness of the method come from the correspondence between narrowing and the derivations of TTSGs built by Step 1 (Theorem 6.5), as well as soundness and completeness of narrowing of the confluent constructor-based rewrite systems (Theorem 2.1), and soundness and completeness of the intersection algorithm (Theorem 7.9).

Decidability of the emptiness of languages recognized by TTSGs built from unification problems (Theorem 8.6), comes from the following facts. The number of leaves of the computations (the tree tuples derived from the axiom) is of course not bounded. However, when considering a TTSG that comes from a unification problem, and thanks to the control, the leaves of any computation can be divided into subsets, called transclasses (Definition 7.3), whose size is bounded. Then by pumping techniques, emptiness can be tested.

This paper is organized as follows. Sect. 2 recalls some basic notions of rewriting techniques. Sect. 3 describes related work on the decidability of unifiability. Our restrictions are given in Sect. 4, where some undecidability results are also given. The TTSG is defined in Sect. 5, and the two steps of our algorithm are respectively given in Sects. 6 and 7. Then Sect. 8 sets our decidability result. Sect. 9 concludes the paper, and discusses future extensions to this work.

Preliminaries

We recall some basic notions that concern rewriting techniques. For more details see Dershowitz and Jouannaud [START_REF] Dershowitz | Rewrite systems[END_REF].

Let be a finite set of symbols and V be an infinite set of variables, T [V is the first-order term algebra over and V . is partitioned in two parts: the set F of function symbols,andthesetC of constructors.

The terms of

[V to T [V .
Adata substitution is a substitution such that, for each variable x, x is a data term. The operator : denotes the composition of substitutions. j Va r t is the restriction of to the set of variables of t.

In the following x; y; z denote variables, s; t; l; r denote terms, f; g; h function symbols, c is a constructor symbol, u; v; w are occurrences, and ; are substitutions.

We generalize the occurrences (as well as the above notation) to tuples in the following way: let p = (p 1 ;:::;p n ) a tuple, 8i 2 [1;n] pj i = p i ,a n dw h e nt h ep i 's are terms, pj i:u = p i j u . Moreover, we define the concatenation of two tuples by (t 1 ;:::;t n ) (t 0 1 ;:::;t 0 n 0)=( t 1 ;:::;t n ;t 0 1 ;:::;t 0 n 0) and the component elimination by (t 1 ;:::;t i ;:::;t n )n i =( t 1 ;:::;t i 1 ;t i+1 ;:::;t n ) A Term Rewrite System (TRS) is a finite set of oriented equations called rewrite rules or rules; lhs means left-hand side and rhs means right-hand side. For a TRS R,therewrite relation is denoted by R and is defined by t ! R s if there exists a rule l ! r in R, a non-variable occurrence u in t,anda substitution , such that tj u = l and s = t[u r]. The reflexive-transitive closure of ! R is denoted by R , and the symmetric closure of ! R is denoted by = R .

A TRS is said to be confluent if t ! R t 1 and t ! R t 2 implies t 1 ! R t 3 and t 2 ! R t 3 for some t 3 .

If the lhs (resp. rhs) of every rule is linear, the TRS is said to be left-(resp. right-)linear. If it is both left and right-linear the TRS is said to be linear.AT R Si sconstructor based if every rule is of the form f(t 1 ;:::;t n ) !r,wherethet i 's are data terms.

The (data)-substitution is a (data)-R-unifier of t and t 0 if t = R t 0 .T h es e tS of substitutions is a complete set of (data)-R-unifiers of t and t 0 if it contains only (data)-R-unifiers of t and t 0 , and for each (data)-R-unifier of t and t 0 there exist 2 S and a substitution such that = R :. The theory defined by the TRS R is finitary if every pair of terms has at least a finite complete set of R-unifiers. When R = ;

the most general unifier is denoted mgu. = t 0 n such that t n and t 0 n are unifiable by the mgu , and = : n ::: 1 j Va r (t0)[Va r (t 0 0 ) is a complete set of data-R-unifiers of t 0 and t 0 0 . This is a consequence of the lifting lemma [START_REF] Hullot | Canonical forms and unification[END_REF]. Note that the termination of R is not required here because we look only for data solutions, which are in normal form. So we do not need to normalize them before applying the lifting lemma.

Related Decidability Results

In term rewriting, some authors have already established decidability results for unifiability, assuming some restrictions on the TRS. The first result assumed the rewrite system to be ground [START_REF] Kozen | Positive first order logic is np-complete[END_REF]. Hullot [START_REF] Hullot | Canonical forms and unification[END_REF] extended it to rewrite systems whose rhs's are either variables or ground terms (Mitra [16] allows rhs's to be data terms). Actually, these results are very restrictive because they forbid recursivity.

Christian [START_REF] Christian | Some termination criteria for narrowing and E-unification[END_REF] defines a new criterion: every rewrite rule's lhs is flat (f(s 1 ;::

:;s n )is flat if 8i 2 [1;n],
s i is either a variable or a ground data term), and the rewrite rules are oriented by a well founded ordering.

Comon et al. [START_REF] Comon | Syntacticness, cycle-syntacticness and shallow theories[END_REF] show that decidability also holds for shallow rewrite systems (the sides of rewrite rules have variables occurring at a depth of at most one). Nieuwenhuis [START_REF] Nieuwenhuis | Basic paramodulation and decidable theories[END_REF] extends the shallow theories to standard theories that allow non-shallow variables.

The restriction of Kapur and Narendran [START_REF] Kapur | Matching, unification and complexity[END_REF], extended by Mitra [START_REF] Mitra | Semantic Unification for Convergent Rewrite Systems[END_REF] imposes that for every rule, every subterm of the rhs having a function symbol on top is a strict subterm of the lhs. For all these restrictions the theory is finitary, i.e. there always exists a finite complete set of unifiers. Most decidability proofs are thus based on the fact that there exists a complete narrowing strategy whose search space is always finite.

As regards non-finitary theories, a decidability result is established by Mitra [START_REF] Mitra | Semantic Unification for Convergent Rewrite Systems[END_REF][START_REF] Mitra | Semantic Unification for Convergent System[END_REF] for constructorbased rewrite systems, assuming that, for every function symbol f, there is at most one rewrite rule among the rules defining f that does not have a data term as the rhs. Moreover, this rhs must contain only one function symbol, and the subterm rooted by this function is flat in the sense of Christian [START_REF] Christian | Some termination criteria for narrowing and E-unification[END_REF]. Thanks to the notion of iterated substitution, Mitra is able to represent finitely the infinite set of unifiers and decide upon unifiability. Kaji et al. [START_REF] Kaji | Solving a unification problem under constrained substitutions using tree automata[END_REF] give a procedure that, when it terminates, decides upon unifiability by means of tree automata. They assume linearity for the goal, right linearity and (nearly) left linearity for the TRS. Unfortunately, their procedure does not represent the set of solutions, and does not terminate for an example like fs(x)+ys(x+y); 0+x xgbecause of the superposition of s(x) with s(x+y). Note that our algorithm works (and terminates) for this example when solving linear equations, since our restrictions are satisfied (see Sect. 4).

Faßbender and Maneth [START_REF] Faßbender | A strict border for the decidability of E-unification for recursive functions[END_REF] give a decision procedure for unifiability without representing the set of solutions. However, they need very strong restrictions. Only one function can be defined, and every constructor and every function is monadic (i.e. admits at most one argument).

Additional Restrictions and their Need

The four additional restrictions are:

1. Linearity of rewrite rules: every rewrite rule side is linear.

2.

No in : if a subterm r of some rhs unifies with some lhs l (after variable renaming to avoid conflicts), then the mgu is actually a match from r into l.

3.

No nested functions in rhs's: in a right-hand side, a function symbol does not appear below a function symbol. For example, f and g are nested in f(g(x)) but not in c(f(x);g(y)).

4. Linearity of the goal: the goal does not contain several occurrences of the same variable.

These restrictions together define a class of rewrite systems incomparable with those of related work, and they allow non-finitary theories. For example, the rewrite system ff(s(x)) f(x);f(0) 0g.T he (even minimal) complete set of solutions, and also the narrowing search space, may be infinite.

To show that the above restrictions are necessary all together to get the decidability of unifiability, we prove that if one of them is removed, then there exists a rewrite system satisfying the other three, and that encodes a well-known undecidable problem, the Post correspondence problem.

Definition 4.1 Post Correspondence Problem (Post 1946)

Let A and C be finite disjoint alphabets and and 0 be two morphisms from A to C .T h e P o s t correspondence problem for and 0 consists of finding a non-empty sequence 2 A + such that ()= 0 ( ). We use the following code: given A = fa 1 ;:::;a n gand C = fc 1 ;:::;c m g, to each a i 2 A (resp. c i 2 C) we associate the unary symbol a i (resp. c i ). The constant ? represents the end of words. Thus, the word abc is represented by the term a(b(c(?))).I f! denotes the word abc, !(?) denotes the term a(b(c(?))). In the proofs ? will sometimes be omitted to simplify the expressions. We need to represent prefixes, i.e. beginning of words whose end is unknown. To do this we use non-ground terms, for example, the term a(b(c(x))) denotes the prefix abc.

Proof. Let R 1 = f f(a i (x)) ! ! i (f (x)) f 0 (a i (x)) ! ! 0 i (f (x)) ji =1 ;:::;n f(?) ! ? f 0 (?) ! ? h(x) ! c(x; f(x)) h 0 (x) ! c(x; f 0 (x)) g
where ! i and ! 0 i respectively denote (a i ) and 0 (a i ). R 1 respects all the restrictions but linearity. Obviously, f encodes and f 0 encodes 0 . Then for any words ; 2 A ,t h ev a l u eo fh() (resp. h 0 ())i sc(; ()) (resp. c(; 0 ())). Therefore, h()= h 0 ( )implies c(; ()) = c(; 0 ()),a n ds o = and ()= 0 ( )because c is a constructor. Thus, looking for and different from ? such that h()= R 1 h 0 ( )amounts to solving the Post correspondence problem.

If we can decide unifiability under restrictions 2-4, we can do it for any linear goal, then for all the goals c i = h(a i (x)) ? = h 0 (a i (y)) (i =1 ;:::;n). This amounts to deciding the unifiability of h() ? = h 0 () forbidding = ? and = ?. This is therefore impossible.

2

Lemma 4.4 Forbidding in is necessary to decide unifiability. Proof. The following rewrite system comes from Domenjoud [START_REF] Domenjoud | Combination techniques for non-disjoint equational theories[END_REF]. Let R 2 = f f(a i (x);y) ! ! i (f(x; a i (y))) ji =1 ;:::;n f 0 (a i (x);y) ! ! 0 i (f 0 (x; a i (y))) ji =1 ;:::;n f(?;y) ! h(y) f 0 (?;y) !h(y) g

where ! i and ! 0 i respectively denote (a i ) and 0 (a i ). The function f encodes , and the second argument save the reverse of the word for which is computed, i.e. for any word 2 A , f(; ?) ! ()(f(?; )) ! ()(h()),where is the reverse of . For example, f(a 1 (a 2 (?)); ?) ! ! 1 (f (a 2 (?);a 1 (?)))

! ! 1 (! 2 (f (?;a 2 (a 1 (?))))) ! ! 1 (! 2 (h(a 2 (a 1 (?))))) For the same reasons, f 0 (; ?) ! 0 ()(h( )).

Therefore, f(; ?)=f 0 ( ;?) implies ()(h()) = 0 ()(h( )),a n dt h e n()= 0 ( )and = . Thus, ()= 0 ( ), i.e. solving f(; ?) ? = f 0 (; ?)amounts to solve the Post correspondence problem, if = ? and = ? are forbidden.

We conclude this proof in a similar way as the previous one, by considering the linear goals c i = f(a i (x); ?) ? = f 0 (a i (y); ?);i=1;:::;n 2 Lemma 4.5 Forbidding nested functions is necessary to decide unifiability.

Proof. Let R 3 = f f(a i (x);h(y)) ! ! i (f (x; g i (y))) j i =1 ;:::;n f 0 (a i (x);h(y)) ! ! 0 i (f 0 (x; g i (y))) j i =1 ;:::;n f(?;h(y)) ! h(y) f 0 (?;h(y)) ! h(y) g i (y) ! h(a i (y)) j i =1 ;:::;n g where ! i and ! 0 i denote respectively (a i ) and 0 (a i ).

This rewrite system looks like the previous one, except that the second argument appearing under the constructor h, which avoids in 's but introduces nested functions. Since the nested function g i (y) rewrites into h(a i (y)), we get the same situation as in the previous proof if we consider the goals c i = f(a i (x);h(?)) ? = f 0 (a i (y);h(?));i=1 ;:::;n 2 Lemma 4.6 Linearity of the goal is necessary to decide unifiability.

Proof. Let R 4 = f f(a i (x)) ! ! i (f (x)) f 0 (a i (x)) ! ! 0 i (f 0 (x)) j i =1 ;:::;n f(?) ! ? f 0 (?) ! ?) g
where ! i and ! 0 i respectively denote (a i ) and 0 (a i ). We consider the non-linear goals c i = f(a i (x)) ? = f 0 (a i (x)) for i =1 ;:::;n. NT is a finite set of non-terminals and the terminals are the constructors of the signature. Upper case letters denote elements of NT. Definition 5.1 A production is a rule of the form X =>t ,w h e r eX 2 NT and t 2 T C[NT .Apack of productions is a set of productions coupled with a non-negative integer (called level) and denoted fX 1 =>t 1 ;:::;X n =>t n g k .

When k =0the pack is a singleton of the form fX 1 =>c ( Y 1 ;:::;Y n )g 0 ,wherec is a constructor and Y 1 ;:::;Y n non-terminals. The production is said free, and is written more simply as X 1 => c(Y 1 ;:::;Y n ).

When k>0the pack is of the form fX 1 =>Y 1 ;:::;X n =>Y n g k ,w he reY 1 ;:::;Y n are non- terminals. The productions of the pack are said to be synchronized. Sz is a positive integer that defines the size of tuples of control, Cis the set of constructors (terminals in the terminology of grammars), NT is the finite set of non-terminals, PP is a finite set of packs of productions of a level less than or equal to Sz, TIis the axiom of the TTSG. It is a tuple ((I 1 ;ct 1 );:::;(I n ;ct n )),w hereeveryI i is a non-terminal and every ct i is a Sz-tuple of control that may contain 0's and ?'s. ? means that this component of the control is not used. In fact, Sz is the number of intersections +1 used to build the grammar. This is why in Sect. 6, no intersections between TTSGs having yet been computed, the tuples of control are 1-tuples, i.e. non-negative integers.

A computation of the grammar is a tuple of trees derived from the axiom by applying productions. In a computation, a tuple of control is associated with each non-terminal occurrence. The control is for simulating variable renaming within narrowing. At this moment, single integers may suffice, but we need tuples of integers in order to get stability of TTSGs by intersection.

Intuitively, a free production X =>c ( Y 1 ;:::;Y n ) can be applied as soon as X appears in a computation of the grammar, and then Y 1 ;:::;Y n preserves the same control as X. On the other hand, a pack of productions fX 1 =>Y 1 ;:::;X n =>Y n g k can be applied iff X 1 ;:::X n occur in the same computation and the kth components of their controls are identical (and are not ?). The X i 's are then replaced by the Y i 's, and the kth component of control is set to a new fresh value.

Definition 5.4

The set of computations of a TTSG Gr =( Sz;C;NT;PP;TI), denoted CompGr, is the smallest set defined by: TI is in Comp(Gr), if tp is in Comp(Gr) and tpj u =( X; ct), and the free production X =>c ( Y 1 ;:: Comp(Gr) and there exist n pairwise different occurrences u 1 ;:::;u n of tp, such that 8i 2 [1;n] tpj ui =( X i ;ct i ) and ct i j k = a (a 2 IN), and the pack of productions fX 1 => Y 1 ;:::

:;Y n ) is in PP, then tp[u c((Y 1 ;ct);:::;(Y n ;ct))] is in Comp(Gr), if tp is in
;X n =>Y n g k 2PP,thentp[u 1 (Y 1 ;ct 1 [k b])] :::[u n (Y n ;ct n [k b])] (where b is a new integer) is in Comp(Gr).
The symbol => also denotes the above two deduction steps; a derivation of Gr is a sequence of computations TI =>t p 1 = > ::: =>t p n .

The ith component of a TTSG denotes any tree appearing as the ith component of a computation. Definition 5. [START_REF] You | Enumerating outer narrowing derivations for constructor-based term rewriting systems[END_REF] The language recognized by a TTSG Gr, denoted RecGr, is the set of tuples of ground data terms Comp(Gr) \ T n C .

Step 1: Transformation of a TRS into TTSGs

This is the first step of our method. In the rest of the paper, the TRS is assumed to be confluent and constructor-based, and satisfies restrictions (1)-( 4). The aim is to convert the TRS and the goal into several TTSGs that simulate narrowing.

TTSGs contain only regular productions (free productions) and synchronization constraints (synchronized productions). This is because, thanks to the restrictions, we have to simulate only particular narrowing steps:

We start from a linear term, since the goal is linear. Consider the narrowing step t ; [u;lr;] t 0 =( t)[u r],w h e r et is linear. Now t 0 = t[u r] because there is no in ,a n dt h e n t 0 = t[u r] because t is linear. Thus, the resulting term t 0 is simple ( does not apply), and can be easily expressed by a grammar. This property is still preserved when applying a narrowing step on t 0 ,sincet 0 is linear thanks to the linearity of r.

Nested functions on rhs's may create in , as shown in the proof of Lemma 4.5.

Consider now the narrowing derivation t 0 ; [START_REF] Plotkin | Building-in equational theories[END_REF]

:; [n] t n
The narrowing substitutions are composed of subterms of lhs's. If lhs's are not linear, then it may be that the term n ::: 1 x contains 2 n times the same variable y. In other words, the number of variables that must be replaced next by the same term is not bounded. This cannot be easily expressed by a grammar.

Without the restrictions, we would get context-sensitive productions whose emptiness would be undecidable.

Consider again Example 1.1. For this example, three TTSGs will be constructed: one for g(x), one for f (y 2 ) and one for 0. Intuitively, the TRS and the goal are considered as a kind of tree automaton (in fact several automata), where states are the occurrences of the terms and transitions are subterm relationships and unification relationships. The idea is to extract tree grammars from the automata. Recall that the terminals of the grammars are the constructors.

Non-Terminals

To each occurrence of each term of the TRS and the goal we associate a non-terminal. Next the productions will be deduced from subterm relations and syntactic unifications. For each rewrite rule i (see Figure 1): to each non-variable occurrence u of the lhs (resp. rhs) is associated the non-terminal L i u (resp. R i u ), except when u = , where we even associate R i u to the lhs, to the occurrences of variables x;y;::: are associated the non-terminals X i ;Y i ;:::.T h e r ei sa n exception when x is on a rhs and is the leaf of a branch that contains only constructors. In this case, we associate X 0i . This avoids confusion between the occurrences of x in the lhs and rhs.

In the same way, for the goal:

the non-terminal G l u (resp G r u ) is associated with each non-variable occurrence u of the lhs (resp. rhs) of the goal, the non-terminals X l ;Y l ;:::(resp X r ;Y r ;:::) are associated with the occurrences of the variables x;y;:::of the goal.

NTt; u denotes the non-terminal associated with the occurrence u of t.

An additional non-terminal A l u (resp. A r u ) is associated with the non-variable arguments of the function of the goal (here, occurrence 1 of fgx to encode the variable y 2 ). t being a side of the goal, ANTt; u denotes the additional non-terminal associated with the occurrence u of t.

f G l g G l 1 A l 1 x X l 0 G r =? R 1 R 1 L 1 1 L 1 1:1 X 1 R 2 L 2 1 X 1 X 2 R 2 X 2 R 3 L 3 1 R 3 R 4 L 4 1 X 4 R 4 R 4 1 X 4 R 5 L 5 1 R 5

Productions

Two kinds of production are deduced from the TRS. Free productions are similar to the productions of regular tree grammars. These productions generate constructor symbols and are deduced from subterm relations. The second kind of productions are synchronized productions, and they come from syntactically unifiable terms. These productions are empty (they do not produce any constructors).

Explanations

The way in which the productions are deduced is motivated by narrowing techniques. From the correspondence between rewriting and narrowing (lifting lemma [START_REF] Hullot | Canonical forms and unification[END_REF]), the languages L 1 ; L 2 of Example 1.1 are the ground instances of the data solutions computed by narrowing. This is why we look for narrowing possibilities. For instance, the subterm gx of the rhs of Rule (4) in Example 1.1 unifies with the lhs of the same rule. Therefore, the narrowing step gx ; [;r4;x7 s(x 0 )] sgx 0 is possible. This step achieves two operations: it maps the variable x to sx 0 ; and it sets the result of the narrowing step to sgx 0 .

From the TTSG's point of view, this narrowing step is simulated as follows. The subterm gx is represented by the non-terminal R 4 1 (see Figure 1) and the variable x by X 4 . Therefore, the pair R 4 1 ;X 4

encodes gx;x. The fact that gx unifies with gsx 0 (the renamed version of the lhs of Rule 4) is encoded by the empty production R 4 1 R 4 . The fact that the previous unification instantiates x is encoded by the empty production X 4 L 4 1 . To force these two operations to be achieved at the same time, the two productions are synchronized in the pack of productions fR 4 1 R 4 ;X 4 L 4 1 g. Thus,

when it is applied on R 4
This is the aim of the free productions deduced from subterm relationships. In our example, we have just narrowed g(x) on top with Rule (4), and we get s(g(x 0 )). So the narrowing step generates a term with the constructor s on top whose argument is the function call g(x 0 ). This is encoded by the free production R 4

s(R 4 1 ).I n t h e s a m e w a y ,x is instantiated by s(x 0 ) which is encoded by the free production L 4 1 s(X 4 ). The narrowing step is achieved entirely by the derivation (R 4

;L 4 1 ) (s(R 4 1 );L 4 1 ) (s(R 4 1 );s(X 4 ))

One can easily see that a second application of Rule (4) on s(g(x 0 )) can be simulated by again applying the pack of productions and then the two free productions.

Making Productions

Free productions. For any term t in the TRS or in the goal and any constructor position u in t (i.e. t(u) is a constructor), we create the free production NT(t; u) t(u)(NT(t; u:1);:::;NT(t; u:n)) where n is the arity of t(u). In our example, we get:

L 1 1 s(L 1 1:1 );L 1 1 : 1 s(X 1 ) ;L 2 1 p(X 2 ) ;L 3 1 0;R 3 0; L 4 1 s(X 4 ) ;R 4
s(R 4 1 ) ;L 5 1 0;R 5 0;G r 0 Synchronized productions. For all r i j u and l j syntactically unifiable, we create the pack of productions (i.e. the set of synchronized productions) fNT(r i ;u)NT(l j ;); NT(r i ; u:v 1 ) NT(l j ;v 1 );:::; NT(r i ; u:v n ) NT(l j ;v n )g where v 1 ;:::v n are the variable occurrences of r i j u . Note that if = mgu(r i j u ;l j ), from the in restriction we know that r i j u = l j , therefore v 1 ;:::;v n are also occurrences of l j .

For our example, r 1 unifies with l 1 ;l 2 and l 3 , which gives the synchronized productions

fR 1 R 1 ;X 1 L 1 1 g; fR 1 R 2 ;X 1 L 2 1 g; fR 1 R 3 ;X 1 L 3 1 g
r 2 also unifies with l 1 ;l 2 and l 3 ,soweget

fR 2 R 1 ;X 2 L 1 1 g; fR 2 R 2 ;X 2 L 2 1 g; fR 2 R 3
;X 2 L 3 1 g Finally, r 4 j 1 unifies with l 4 and l 5 ,soweget fR 4 1 R 4 ;X 4 L 4 1 g; fR 4 1 R 5 ;X 4 L 5 1 g

To generate the synchronized productions coming from the goal, remember that we consider f(y 2 ), g(x) and 0. For each function occurrence u of the goal t such that t(u)=l j ( )(i.e. t(u)(x 1 ;:::;x n ) unifies with l j ), we create the synchronized productions: fNT(t;u) NT(l j ;); ANT (t; u:1) NT(l j ;1);:::; ANT(t; u:n) NT(l j ;n)g

The language derived from NT(t; u) expresses the terms issued by narrowing from t(u)(x 1 ;:::;x n ), while the languages derived from ANT (t; u:i) express the instances of the fictitious variables x i .I n Example 1.1, f(y 2 ) unifies with l 1 ;l 2 and l 3 ; this gives the synchronized productions

fG l R 1 ;A l 1 L 1 1 g; fG l R 2 ;A l 1 L 2 1 g; fG l R 3 ;A l 1 L 3 1 g g(x)
unifies with l 4 and l 5 ,soweget fG l 1 R 4 ;X l L 4 1 g; fG l 1 R 5 ;X l L 5 1 g

Note that, within the goal, the argument of the function symbol g is a variable, therefore we do not need an additional non-terminal A l

1:1 for it.

Productions to Express Ground Instances

The languages we want to express are the ground data instances of the solutions provided by narrowing. The productions described so far express the solutions provided by narrowing. Let us see on an example of the problem. We consider the rewrite rule

fx 1 ! 0
and the term fy. The productions associated with this problem are R 1

) 0; fG l ) R 1 ;Y )X 1 g
From the pair G l

;Ywhich represents f y;y, we get the derivation:

G l ;Y)R 1 ;X 1 )0;X 1
No more production is applicable, therefore from a grammar point of view, this language is empty because of the non-terminal X 1 . The meaning of this derivation is that fy narrows to 0 for any value of y.Since we are only interested in ground data solutions, the non-terminal X 1 has to be derived into any ground data term. For this, the grammar that generates any term of T C is constructed.

A new non-terminal ANY is introduced, and for all constructors c 2C, the free production ANY ) cANY;:::;ANYis created. The variables concerned with the problem are any variables x j appearing on the lhs of the rewrite rule but not on the rhs, or variables appearing in the goal in a branch that contains only constructors. For all these variables the production X j ) ANY is created. For technical reasons, this production is considered as synchronized, because it does not generate any constructors.

In the previous example, the only production created for ANY is ANY ) 0, because 0 is the only one. X 1 ) ANY is created for X 1 . Thus, the derivation terminates as follows: 0;X 1 )0;ANY)0; 0 In fact, the problem we just solved may be more complicated if a rewrite rule has the form fx 2 ! sx because in this case, we have to simulate that the x occurring on the lhs and the x occurring on the rhs must be instantiated by the same ground data term.

This can easily be simulated thanks to some synchronized productions, as follows (introduction of the control is necessary to understand why these productions work well):

c2Cthe free productions ANY c

Res ) cANY ;Y), which represents (f (y);y), a possible derivation is:

(G l ;Y))(R 2 ;X 2 ) )(s(X 02 );X 2 ) )(s(AN Y s Res );ANY s Var )
) (s(s(AN Y 1 Res ));s(AN Y 1 Var )) ) (s(s(AN Y 0 Res ));s(AN Y 0 Var )) ) (s(s(0));s(0))

Grammars

Many productions have been deduced from the TRS and the goal. Let us now define the grammars that are constructed with them. All the grammars considered have the same terminals (the constructors), the same non-terminals, and the same productions, as defined before. Just the axioms (tuples of non-terminals) are different. Note that the grammars could be optimized by removing non-reachable non-terminals and non-usable productions. For Example 1.1 we get the grammars:

Gr l defined by the axiom (G l ;A l 1 ), which generates the language L 2 , Gr l 1 defined by the axiom (G l 1 ;X l ), which generates the language L 1 , Gr r defined by the axiom (G r

), which generates the language L 3 .

Here is an example of derivation for Gr l :

(G l ;A l 1 ))( R 1 ;L 1 1 ) )(R 1 ;s(L 1 1:1 )) ) (R 1 ;s(s(X 1 ))) ) (R 2 ;s(s(L 2 1 ))) ) (R 2 ;s(s(p(X 2 )))) ) (R 3 ;s(s(p(L 3 1 ))))
) (0;s(s(p(L 3 1 ))))

) (0;s(s(p(0))))

This encodes the narrowing derivation f(y 2 ) ; [;1;y27 s(s(x1))] f(x 1 ) ; [;2;x17 p(x2)] f(x 2 ) ; [;3;x27 0] 0 where the resulting term is 0,a ndy 2 is instantiated by s(s(p(0))).

In the general case, the definition of the grammars (i.e. of theirs axioms) is a little technical because of the constructors that may appear in the goal. Below, [u; v i [ denotes the set of occurrences appearing along the branch going from u to v i (v i is not included). For each non-variable occurrence u of the lhs l (resp. rhs r) of the goal such that u = or u is just under a function, let fv 1 ;:::;v n g (exhaustive list) be the occurrences appearing under u, such that for each i the branch [u; v i [ contains only one function f and v i is just under f, or v i is a variable occurrence and the branch [u; v i [ contains only constructors. We create the grammar Gr l u defined by the axiom (NT(l; u);ANT(l; v 1 ); :::;ANT(l; v n ))) (resp. G r u defined by the axiom NTr;u ;ANTr;v1;:::;ANTr;vn). Proof. 1. First sense. 1.1. For a computation different from the axiom. Since (c; c 1 ;:::;c n ) [P=fR j u R i ;X j L i v ; :::g] ::: the pack P is in the grammar. Then r j j u and l i are unifiable. Thus, if w:u is the occurrence of R j u in c, sj w:u = terms(cj w:u )=terms((R j u ;ct)) = Id ct (r j j u ) which is unifiable with l i .T h e ns ; [w:u;l i r i ;] t = s[w:u Id ct 0 (r i )]. On the other hand, from the grammar building, for each variable x j k in Id ct (r j j u ) at occurrence v we have x j k = ct 0 (l i j v )=terms((L i v ;ct 0 )).A s 8b;

d b = c b [(X j ;ct) (L i v ;ct 0 )] we get terms(d b )= terms(c b )[p terms((L i v ;ct 0 )) = terms(c b )[x j k (x j k )] = (terms(c b )) = s b .O n t h e other hand, d = c[w:u (R i ;ct 0 )].
T h e n terms(d)=terms(c)[w:u terms((R i ;ct 0 ))] = s[w:u Id ct 0 (r i )] = t.

For the axiom (in simplified form).

The reasoning is made on the lhs of the goal, but it is exactly the same for the rhs. Since (c; c 1 ;:::;c n ) [P=fG l u R i ;Au:kL i k ; :::g] :::the pack P is in the grammar, and so g(u)=l i ( ).Then sj u = g(u)(A l 1 ;:::;A l n ) ; [;l i ri;] tj u = Id ct 0 (r i ) with 8j; (A l j )=Id ct 0 (l i j j ).A s8j; d j = L i j , terms(d j )=Id ct 0 (l i j j )= ( a j )= ( terms(c j )).O n the other hand, terms(dj u )=terms((R i ;ct 0 ))=Id ct 0 (r i )=t j u .

Conversely. 2.1. For a computation different from the axiom.

Assume s ; [w:u;l i r i ;] t. Thus, sj w:u and l i are unifiable, so s(w:u) is a function. As s = terms(c),the function occurrences of s are non-terminal occurrences of c, of the form R j u . Thus, sj w:u = terms(cj w:u ) = terms((R j u ;ct)) = Id ct (r j j u ). Therefore, r j j u and l i are unifiable, then the pack P = fR j u R i ;X j L i v ; :::g is in the grammar. From the previous technical lemma, every X j appears in (c 1 ;:::;c n ) with ct as control number. Then (c; c 1 ;:::;c n ) [P] :

[free prods:] (d; d 1 ;:::;d n ) and (d; d 1 ;:::;d n ) is simplified form. We show as in (1.1) that (t; s 1 ;:::;s n )=terms(d; d 1 ;:::;d n ).

For the axiom (in simplified form).

sj u = g(u)(A l 1 ;:::;A l n ) ; [;l i r i ;] tj u = Id ct 0 (r i ),s og(u)=l i

, then the grammar contains the pack P = fG l u R i ;A u:k L i k ; :::g.Soas(cj u ;c 1 ;:::;c n )=( G l u ;A u:1 ;:::;A u:k ),w ehave (c; c 1 ;:::;c n ) [P] :

[free prods:] Proof. From the correspondence in one step and by induction over the length of derivations.

2 Theorem 6. [START_REF] You | Enumerating outer narrowing derivations for constructor-based term rewriting systems[END_REF] The tree tuple language recognized by the grammar gives exactly the ground data instances of the data terms computed by narrowing, thanks to the first component of tuples, as well as the corresponding instances of variables thanks to other components. Formally, let TI be the simplified form of the axiom, and let (s; a 1 ;:::;a n )be its associated tuple of terms ( From the grammar building, if j appears as the lhs of some production that does not contain ANY ,then x j appears in r j under a function. Therefore, the set of X j 's as the lhs of productions that do not contain ANY and the set of X j 's as the lhs of productions that contain ANY are disjoint. Moreover, if X j is derived into ANY , it can only be derived into trees that contain non-terminals like ANY . Therefore, if the given derivation contains the step X j ANY , the steps issued from X j can be done independently to the others: the order of steps in the derivation can be changed so that the productions dealing with ANY are done last.

TI

[prods without ANY ] (e; e 1 ;:::;e n )

[prods with ANY ] (d; d 1 ;:::;d n ) where (e; e 1 ; ::: ;e n ) is in simplified form. From the correspondence in several steps s ;

[] t and (t; a 1 ;:::;a n )=terms(e; e 1 ;:::;e n ). Applying productions containing ANY until having a tuple without non-terminals amounts to replacing all X j by ground data terms. Within (t; a 1 ;:::;a n ),t his amounts to instantiating each variable x j by a ground data term: let be this substitution. So we get = d; a 1 = d 1 ;:::;a n = d n .

Conversely.

From the correspondence in several steps TI [prods without ANY ] (e; e 1 ;:::;e n ) ,w h e r e(e; e 1 ;:::;e n ) is in simplified form and t; a 1 ;:::;a n )=terms(e; e 1 ;:::;e n ). For each variable x j of (t; a 1 ;:::;a n ), some productions containing ANY can be applied to derive X j into x j . Thus (e; e 1 ;:::;e n ) (d;d 1 ;:::;d n ).S i n c et isadataterm,(e; e 1 ;:::;e n ) contains only nonterminals like X j ,then(d; d 1 ;:::;d n ) contains only constructors, i.e. is a recognized tuple, and we have d = t; d 1 = a 1 ;:::

;d n = a n . 2 7
Step 2: Intersection of TTSGs over One Component

This section describes the second step of our method. Let us consider again Example 1.1. Recall that we have decomposed the problem into three parts g(x) ? = y 1 , f(y 2 ) ? = y 3 and 0 ? = y 4 . In Sect. 6.4, three TTSGs have been deduced from the problem to solve each of the three parts. The point now is to reconstruct the initial problem thanks to the one-component-intersection of sets of tuples. This operation corresponds to the join operation in relational algebra (relational databases).

Definition 7.1 Let E 1 be a set of n 1 -tuples and E 2 be a set of n 2 -tuples. The one component k 1 ;k 2 intersection of E 1 and E 2 is the set of n 1 + n 2 1-tuples defined by ftp 1 (tp 2 n k2 ) j tp 1 2 E 1 and tp 2 2 E 2 and tp 1 j k1 = tp 2 j k2 g.

For example, the one component 2, 1 intersection of the sets of pairs E 1 = f(0;s(0)); (s(0); 0)g and E 2 = f(s(0);s(s(0)); (s(s(0)); 0)g the set of triples E 3 = f(0;s(0);s(s(0)))g.

To get the solutions of the initial goal, we have to compute incrementally the one component k 1 ;k 2 intersection for each pair of grammars Gr 1 , Gr 2 such that the k 1 th component of the axiom of G 1 is G l u and the k 2 th component of the axiom of G 2 is A l u with the same u (resp. G r u and A r u ). For our example, this means that the possible instantiations of y 2 are restricted to the possible results for g(x). At the end, we also have to compute the intersection for components G l and G r . When considering any TTSGs, we have the following result:

Lemma 7.2 Emptiness of intersection over one component of languages recognized by TTSGs is undecidable.

Proof. The post correspondence problem can be encoded by the intersection over one component of two languages recognized by TTSGs. Let b be a binary constructor and consider the 1-tuple tree languages L = fb(; ())j 2 A + g and L 0 = fb(; 0 ())j 2 A + g. Let us write (a i )=c i;1 :::c i;pi for each a i 2 A.T h e nL is recognized by the TTSG Gr defined by the productions I ) b(X;Y ) and for each a i 2 A : fX ) X i ;Y ) Y i g, X i ) a i Z, Y i ) c i;1 Y i;2 ;Y i;2 ) c i;2 Y i;3 ;:::;Y i;pi ) c i;pi T, fZ ) X;T ) Y g, fZ )?;T )?g, and the axiom I. The TTSG Gr 0 that recognized L 0 is defined in the same way. Now checking emptiness of L \ L 0 amounts to checking the existence of 2 A + such that ()= 0 ( ), i.e. solving the post correspondence problem.

2

Moreover, the intersection of languages recognized by TTSGs is not always a language recognized by a TTSG. Fortunately, we do not consider any TTSGs, only TTSGs that come from a unification problem, and in this case the problem is decidable thanks to some particular properties. Sect. 7.1 gives preliminaries that define these properties, while Sect. 7.2 presents the intuitive idea and the detail of the intersection algorithm.

Preliminaries

Emptiness of intersection becomes decidable if the component k 1 (or k 2 ) has the property of external synchronization, which is the case for TTSGs coming from a unification problem. Roughly speaking, this means that at most one production can be applied on this component when using a pack of synchronized productions. So, an externally synchronized component of a TTSG behaves as a regular tree language in the sense that any branch of this component can be generated independently from the others.

Recall that now the control is not one integer, but a tuple of integers.

Algorithm

Before showing how the intersection is computed, let us explain how it works and why tuples of control are needed, instead of single integers.

Example 7.7 This example does not come from a unification problem, but it is easier to understand, and every component is nevertheless externally synchronized. Let

G 1 = (1; fs;0g; fX;X 0 ;Y;Y 0 ;Y 00 g; fX 0 0;Y 0 0;X 0 s(X);Y 0 s(Y 00 );Y 00 s(Y ); fX X 0 ;Y Y 0 g 1 g;

((X; 0); (Y; 0)))

and G 2 = ((1; fs;0g; fZ;Z 0 ;T;T 0 ;T 00 g; fZ 0 0;T 0 0;Z 0 = s(Z);T 0 s(T 00 );T 00 s(T ); fZ Z 0 ;T T 0 g 1 g;

((Z; 0); (T; 0)))

G 1 and G 2 generate the same language i.e. the pairs (s n (0);s 2n (0)). The 2,1 intersection of G 1 and G 2 is then the language of triples L 3 = f(s n (0);s 2n (0);s 4n (0))g The question is how to build from G 1 and G 2 a new TTSG G 3 that generates L 3 ? The idea is that the first component of L 3 will be generated by the productions of G 1 , the last component of L 3 will be generated by the productions of G 2 , therefore G 3 contains the non-terminals and the productions of both G 1 and G 2 .

The second component of L 3 is the intersection of the second component of G 1 with the first component of G 2 . The productions that generate it are built using the same idea as for the intersection of regular languages, i.e. by computing the Cartesian product of the grammars.

More precisely, let us note first that only the non-terminals Y; Y 0 ;Y 00 (resp. Z; Z 0 ) may appear in the second (resp. the first) component of G 1 (resp. G 2 ). Thus, for the intersection, the set of nonterminals is the Cartesian product fYZ;Y 0 Z; Y 00 Z; Y Z 0 ;Y 0 Z 0 ;Y 00 Z 0 g, and the free productions are fY 0 Z 0 s(Y 00 Z );Y 0 Z 0 0;Y 00 Z 0 s(YZ) g. The packs of productions are constructed such that if a synchronization was possible in the initial grammars, it is still possible in the intersection: for each pack of productions of G 1 (resp G 2 ) that deals with Y or Y 0 or Y 00 (resp. Z or Z 0 ), we create a new pack in G 3 .W eg e tffX X 0 ;YZ Y 0 Zg 1 ;fX X 0 ;YZ 0 Y 0 Z 0 g 1 gfrom the packs of G 1 and ffYZ YZ 0 ;T T 0 g 1 ;fY 0 Z Y 0 Z 0 ;T T 0 g 1 ;fY 00 Z Y 00 Z 0 ;T T 0 g 1 gfrom the packs of G 2 . The axiom of G 3 is ((X; 0); (YZ;0); (T; 0)).

Unfortunately, G 3 is not the desired grammar. Indeed, using the pack fX X 0 ;YZ Y 0 Zg 1 ,the axiom is derived into ((X 0 ; 1); (Y 0 Z; 1); (T; 0)). Now the pack fY 0 Z Y 0 Z 0 ;T T 0 g 1 cannot be applied because the control numbers of Y 0 Z and T are not equal, and no other production can derive Y 0 Z . The axiom can also be derived using the pack fYZ YZ 0 ;T T 0 g 1 ) ,b u tw eg e tt h es a m e conclusion. Thus the language recognized by G 3 is empty. This problem is solved by considering pairs of integers as control in G 3 , the first (resp. second) level being incremented when applying a pack that comes from G 1 (resp. G 2 ). So the packs of productions coming from G 2 must have 2 as rank, and are then ffYZYZ 0 ;T T 0 g 2 ;fY 0 Z Y 0 Z 0 ;T T 0 g 2 ;fY 00 Z Y 00 Z 0 ;T T 0 g 2 g -Sync2 = ffX1;1X2;1 X1;1 X 0 2;1 ;:::;X1;n X2;n X1;n X 0 2;n ;X 2;n+1 X 0 2;n+1 ;:::; X2;m X 0 2;m gSz 1 +k such that fX1;1;:::;X1;ng is a multiset whose elements are in Reach(Ii 1 ;PP1) and fX2;1;:::;X2;ngReach(Ii 2 ) and fX2;1 X 0 2;1 ;:::;X2;m X 0 2;m gk 2 PP2 TI 3 =( TI 0 1 [i 1

(I i1 I i2 ;ct i1 ct i2 )]) (TI 0 2 n i2 ) where TI 0 1 (resp. TI 0 2 ) comes from TI 1 (resp. TI 2 ) by replacing each control tuple ct j by ct j (? 1 ;:::;? Sz2 ) (resp. (? 1 ;:::;? Sz1 ct j )).

The definition of Sync 2 is more complicated than that of Sync 1 because the i 2 th component of G 2

is not assumed to be externally synchronized. So several productions (in fact n) of the pack fX 2;1 ) X 0 2;1 ;:::;X 2;m ) X 0 2;m g k of PP 2 may be applied together on the i 2 th component of G 2 .

following definition is needed in the proof of Theorem 7.9.

Definition 7.10 Let tp and tp 0 be two computations of (eventually different) TTSGs. Let t = tpj i and t 0 = tp 0 j i 0 . We write t l t 0 (resp. t r t 0 )if 8 u2O ( t ) , t ( u ) is a constructor symbol, which implies t(u)=t 0 ( u), and 8u 2 O(t), t(u)=(X; ct) implies t 0 (u)=( X 0 ;ct 0 ) and ct 0 = ct (?;:::;?) (resp. ct 0 = (?;:::;?)ct).

Proof. 1. First let us prove that for tp 1 2 Comp(G 1 ) and tp 2 2 Comp(G 2 ) satisfying (1) 8u 2 O(tp 1 j i1 ), tp 1 j i1:u a constructor, which implies tp 1 j i1 (u)=tp 2 j i2 (u) (2) and 8u 2 O(tp 1 j i1 ), tp 1 j i1:u =( X 1 ;ct 1 ), which implies 2 j i2:u =( X 2 ;ct 2 ), then there exists tp 3 2 Comp(G 3 ) such that (A) 8j 2 [1;i 1 1] [ [i 1 +1 ;n 1 ] tp 3 j j l tp 1 j j and (B) 8j 2 [n 1 +1;n 1 +i 2 1] tp 3 j j r tp 2 j j n1 and (C) 8j 2 [n 1 + i 2 ;n 1 +n 2 ] tp 3 j j r tp 2 j j+1 n1 and (D) 8u 2 O(tp 1 j i1 ) s.t. tp 1 j i1:u is a constructor, tp 1 j i1 (u)=tp 3 j i1 (u) and 8u 2 O(tp 1 j i1 ) such that tp 1 j i1:u =( X 1 ;ct 1 )and tp 2 j i2:u =( X 2 ;ct 2 )then tp 3 j i1:u =( X 1 X 2 ;ct 1 ct 2 )

It is proved by induction on the total number of productions used to generate tp 1 and tp 2 . The basic case is obvious because the axiom of G 3 is constructed to respect these properties.

For the induction step, let tp 1 2 Comp(G 1 ) and tp 2 2 Comp(G 2 ) such that tp 1 j i1 and tp 2 j i2 satisfy (1) and [START_REF] Baader | Unification theory[END_REF]. By the induction hypothesis, we suppose that there exists tp 3 2 Comp(G 3 ) such that tp 3 verifies (A) (B) (C) and (D):

If the next production applied on tp 1 does not affect any occurrence of tp 1 j i1 , we obtain tp 0 1 and tp 0 1 and tp 2 verifies (1) and ( 2). tp 3 ) tp 0 3 with the same production at the same occurrence because PP 1 PP 3 . Moreover, tp 0 3 verifies (A) (B) (C) and (D).

If the next production applied on tp 2 does not affect any occurrence of tp 2 j i2 , we obtain the same result.

If the production applied on tp 1 is a pack of productions fX 1 ) X 0 1 ;:::;X n )X 0 n g k that affects the occurrences u 1 ;:::u n of tp 1 , where one of them, say v,isi 1 :v 0 , 8i 2 [1;n],w e have tp 1 j ui =( X i ;ct i ),l e ttp 0 1 the computation obtained by the application of the pack. tp 0 1 and tp 2 verifies (1) and ( 2), because the synchronized productions do not produce any new constructor. Moreover, 8i 2 [1;n]we have tp 3 j ui =( X i ;ct i (?;:::;?)), except v,forwhichwehavetp 3 j v = (X j Y;ct j ct 0 ). By construction of G 3 , the pack fX 1 ) X 0 1 ;:::;X j Y )X 0 j Y;:::;X n )X 0 n g k is in PP 3 , therefore it can be applied on tp 3 , and we obtain tp 0 3 that verifies (A) (B) (C) and (D).

If the production applied on tp 2 is a pack of productions with similar reasoning as above, we get the same result.

If the production applied on tp 2 is a free production that affects one occurrence of tp 2 j i2 :L e tX 2 ) c(Y 2;1 ;:::;Y 2;n ) be the production, v the occurrence in tp 2 j i2 ,andtp 0 2 the computation obtained. If there exists tp 00 1 2 Comp(G 1 ) such that tp 1 ) tp 00 1 and tp 00 1 j i1 (v)=tp 0 2 j i2 (v)=c , then there ex- ists tp 0 1 in Comp(G 1 ) such that tp 1 ) tp 0 1 and tp 0 1 j i1 = tp 1 j i1 [v c((Y 1;1 ;ct 1 );:::;(Y 1;n ;ct 1 ))] and a free production in PP 1 X 1 ) c(Y 1;1 ;:::;Y 1;n ). Indeed, the i 1 th component of G 1 is externally synchronized, therefore each branch of this component can be generated independently from the others. Moreover, every free production generates one and only one constructor, so tp 0 1 and X 1 ) c(Y 1;1 ;:::;Y 1;n ) do exist. Now, tp 0 1 and tp 0 2 verifies (1) and [START_REF] Baader | Unification theory[END_REF]. Notice that all the productions but X 1 ) c(Y 1;1 ;:::;Y 1;n ) in tp 1 ) tp 0 1 do not affect any occurrence of tp 1 j i1 or are synchronized productions, therefore from the second and the fourth point of this proof we can deduce that tp 3 ) tp 00 3 and tp 00 3 j i1 (v)=( X 1 X 2 ;ct 1 ct 2 ). From the construction of G 3 , we know that X1X2 ) c(Y 1;1 Y 2;1 ;:::;Y 1;n Y 2;n ) is in PP 3 , therefore this production can be applied on tp 00 3 at occurrence v, and we obtain 0 3 that verifies (A) (B) (C) and (D). To conclude this part of the proof we can see that if tp 1 2 Rec(G 1 ) and tp 2 2 Rec(G 2 ), then there exists tp 3 2 Rec(G 3 ) that verifies (A) (B) (C) and (D). This means that tp 3 is the intersection over one component of tp 1 and tp 2 . 2. Conversely, we have to prove that if tp 3 2 Rec(G 3 ), then there exists tp 1 2 Rec(G 1 ) and tp 2 2 Rec(G 2 ), such that tp 3 = tp 1 (tp 2 n i2 ). To prove that, we prove that if tp 3 2 Comp(G 3 ) then there exist tp 1 2 Comp(G 1 ) and tp 2 2 Comp(G 2 ) such that tp 3 verifies (A), (B), (C) and (D) wrt tp 1 and tp 2 .

It is proved by induction on the number of productions applied to obtain tp 3 . The case n =0is obvious from the construction of G 3 . For the induction step we will suppose that the lemma is true for a given tp 3 , and we prove that if a new production is applied on tp 3 obtaining tp 0 3 , we can find tp 0 1 2 Comp(G 1 ) and tp 0 2 2 Comp(G 2 ) such that tp 0 3 verifies (A), (B), (C) and (D) wrt tp 0 1 and tp 0 2 .

If the next production applied on tp 3 does not affect any occurrence of tp 3 j i1 , then it is a production either of PP 1 or of PP 2 , therefore the same production can be applied at the same occurrence (modulo a shift for tp 2 ) on either tp 1 or tp 2 . Therefore, we prove the induction step.

If the next production applied on tp 3 is a free one, say X1X2 ) c(Y 1;1 Y 2;1 ;:::;Y 1;n Y 2;n )

applied at an occurrence v of tp 3 j i1 , from the construction of G 3 we have X1 ) c(Y 1;1 ;:::;Y 1;n ) 2 PP 1 and X2 ) c(Y 2;1 ;:::;Y 2;n ) 2 PP 2 , therefore we can apply the first one at the occurrence v of tp 1 j i1 and the other at the occurrence v of tp 2 j i2 , and the resulting computations allow us to verify the induction step.

If the next production applied on tp 3 is a pack of productions that affects at least one occurrence of tp 3 j i1 , then from the construction of PP 3 , the corresponding pack of productions exists in PP 1 or in PP 2 (depending on whether the pack belongs to Sync 1 or Sync 2 ). Therefore, the corresponding pack of productions can be applied on either tp 1 or tp 2 , and we get the tuples that prove the induction step.

2

The point now is to prove that if one component (different from i 2 )ofG 2 is externally synchronized, then the corresponding component of G 3 keeps this property. This is necessary to be able to compute incrementally several intersections using the previous algorithm.

Lemma 7.11

Let G 1 be a TTSG whose i 1 th component is externally synchronized and G 2 another TTSG whose j 2 th component is also externally synchronized. Let G be a one component i 1 ;i 2 intersection (i 2 6 = j 2 )ofG 1 and G 2 . The component that corresponds to j 2 (i.e. n 1 + j 2 if j 2 <i 2 and n 1 + j 2 1, otherwise) in G 3 still externally synchronized. Proof. Point (1) of Definition 7.5 is obvious. For point [START_REF] Baader | Unification theory[END_REF], when building G 3 , the only possible merging between two TransClasses of G 2 might come from the intersection component, due to an internal synchronization on the i 1 th component of G 1 . However, it is assumed to be externally synchronized. 2

To end Example 1.1, let us see the grammars obtained by intersection. We have had three grammars:

Gr l 1 , whose axiom is (G l 1 ;X l ). Gr l , whose axiom is (G l ;A l 1 ).

Gr r

, whose axiom is (G r ).

For the sake of simplicity, only new productions are given. ' ' represents any non-terminal allowed by Theorem 7.9.

We have Reach(G l 1 )=f G l 1 ;R 4 ;R 4 1 ;R 5 g, Reach(A l 1 )=f A l 1 ;L1 1 ;L 1 1:1 ;X 1 ;L 2 1 ;X 2 ;L 3 1 g,and Reach(G r )=f G r g. So the intersection of Gr l 1 with Gr l gives the grammar Gr lef t with the following new productions:

f R 4 L 1 1 ) s(R 4 1 L 1 1:1 );R 4 L 1 1:1 )s(R 4 1 X 1 );R 5 L 3 1
)0; fR 4 1 )R 4 ;X 4 )L 4 1 g 1 ;fR 4 1 )R 5 ;X 4 )L 5 1 g 1 ; fG l 1 )R 4 ;X l )L 4 1 g 1 ;fG l 1 )R 5 ;X l )L 5 1 g 1 ; fR 1 )R 1 ; X 1 ) L 1 1 g 2 ;fR 1 )R 2 ; X 1 ) L 2 1 g 2 ; fR 1 )R 3 ; X 1 ) L 3 1 g 2 ;fR 2 )R 1 ; X 2 ) L 1 1 g 2 ; fR 2 )R 2 ; X 2 ) L 2 1 g 2 ;fR 2 )R 3 ; X 2 ) L 3 1 g 2 ; fG l )R 1 ; A l 1 ) L 1 1 g 2 ;fG l )R 2 ; A l 1 ) L 2 1 g 2 ; fG l )R 3 ; A l 1 ) L Proof. This is proved by induction on n.

If no intersection has been done, i.e. n =0 , we can see that the TransClasses are in fact the Classes. From the previous lemma, the size of any Class cannot be greater than the number of non-terminals of G, i.e. card(NT).

For the induction step we consider the TTSG G 1 (resp. G 2 ), made thanks to n 1 intersections (resp. n 2 ), whose TransClass Size not greater than card(NT) n1+1 (resp. card(NT) n2+1 ) ,a n dw ea l s oa s s u m e that the i 1 th component of G 1 is externally synchronized. Let G 3 be the i 1 ;i 2 intersection over one component of G 1 and G 2 .

When building G 3 , the only possible merging between two TransClasses of G 2 may come from the intersection component, due to an internal synchronization on the i 1 th component of G 1 . This is impos- sible, since it is assumed to be externally synchronized. Therefore, if c 3 is a TransClass of G 3 ,t h e ni t comes from the merger of some TransClass c 2 of G 2 with some TransClasses c 1 1 ;:::;c k 1 of G 1 ,wherek is the number of occurrences of c 2 that belong to the 2 th component of G 2 . From the induction hypothesis, we get Size(c 3 ) = Size(c 1 1 )+:::+Size(c k 1 )+Size(c 2 ) k k:card(NT) n1+1 + card(NT) n2+1 k = k:(card(NT) n1+1 1) + card(NT) n2+1

This expression is maximal when k is, i.e. k = card(NT) n2+1 . This case appears when the size of c 2 is maximal and all the occurrences of c 2 belong to the i 2 th component. Therefore,

Size(c 3 ) card(NT) n2+1 card(NT) n1+1 = card(NT) n1+n2+2
Since the number of intersections for building G 3 is n = n 1 + n 2 +1,wege tSize(c 3 ) card(NT) n+1 . 2

We introduce now the notion of an NT-TransClass. Intuitively, an NT-TransClass is composed by the non-terminals appearing at the occurrences of a given TransClass. But this is not sufficient, because the subtrees derived by applying productions from an NT-TransClass also depend upon the Classes appearing within the TransClass, and we want the notion of an NT-TransClass to define in a unique way the language derived from it. To make formalisation easier, we give a more general definition, in the sense that a NT-TransClass is associated with each TransClass, but the reverse is false. This means that some NT-TransClasses (as defined below) cannot really appear in a computation. The size of an NT-TransClass is defined as being the size of the multiset.

For each level i, the partition simulates the way in which the Classes are organized. Note that the values of control tuples do not matter; only the sets they define are important. Lemma 8. [START_REF] Nutt | Basic narrowing revisited[END_REF] Under the same assumptions as the previous lemma, there are finitely many NT-TransClasses whose size is not greater than card(NT) n+1 . Proof. For any p, there are finitely many NT-TransClasses of size p, because there are finitely many multisets of size p whose elements come from the finite set NT,and for each multiset, for each i 2 [START_REF] Plotkin | Building-in equational theories[END_REF]Sz]there are finitely many partitions.

2 Lemma 8. [START_REF] You | Enumerating outer narrowing derivations for constructor-based term rewriting systems[END_REF] The emptiness of languages recognized by TTSGs built from unification problems is decidable.

Proof. The reasoning is similar to that used for a regular tree grammar: if there is a derivation of the grammar giving a term whose leaves are all terminals (i.e. the recognized language is not empty), then there is a derivation that does not contain several times of the same non-terminal in the same branch, and that gives a term whose leaves are all terminals. So to test emptiness, only derivations that do not apply more than n (n being the number of non-terminals of the grammar) at comparable occurrences have to be generated.

For a TTSG, we use the same reasoning on NT-TransClasses instead of single non-terminals. From Lemma 8.2, the size of TransClasses is bounded by card(NT) n+1 . So is the size of NT-TransClasses.

Then from the previous lemma, there are finitely many NT-TransClasses. Moreover, given two different TransClasses of a given computation, their associated NT-TransClasses are next derived independently. Then, as for regular tree languages, only derivations that do not contain several times the same NT-TransClass in the same sub-derivation must be generated to test emptiness. So, only derivations whose depth is less than the number of NT-TransClasses are needed. define the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in previous work [START_REF] Hullot | Canonical forms and unification[END_REF][START_REF] Mitra | Semantic Unification for Convergent Rewrite Systems[END_REF][START_REF] Comon | Syntacticness, cycle-syntacticness and shallow theories[END_REF][START_REF] Nieuwenhuis | Basic paramodulation and decidable theories[END_REF][START_REF] Kapur | Matching, unification and complexity[END_REF][START_REF] Christian | Some termination criteria for narrowing and E-unification[END_REF][START_REF] Kaji | Solving a unification problem under constrained substitutions using tree automata[END_REF][START_REF] Faßbender | A strict border for the decidability of E-unification for recursive functions[END_REF], but does satisfy ours. Therefore, we are able to solve linear equations modulo this theory.

Example 8.8 Let r 1 : f(c(x; x 0 );c(y; y 0 )) ! c(f(x; y 0 );f(x 0 ;y)) r 2 : f(0; 0) ! 0

This system provides an idea of the expressiveness of TTSGs, because when solving the equation f(x; y)= z, the set of possible instantiations of x and y are the binary trees such that the instance of x is the symmetric of that of y. For example, if we consider the following narrowing derivation issued from fx; y: fx; y ; [;r1;x7 c(x1;x 0 1 );y7 c(y1;y 0 1 )] cfx 1 ;y 0 1 ;fx 0 1 ;y 1 ; [1;r1;x17 c(x2;x 0 2 );y 0 1 7 c(y2;y 0

2 )] ccfx 2 ;y 0 2 ;fx 0 2 ;y 2 ;fx 0 1 ;y 1 ;

[r2] cc0; 0; 0 the generated substitution is x 7 cc0; 0; 0;y 7 c0;c0; 0. Since this rewrite system satisfies all our restrictions, our method will be able to compute a TTSG that recognized the solutions, i.e. the symmetric trees.

Conclusion

We have presented an original approach using Tree Tuple Synchronized Grammars (TTSGs) to solve linear equations modulo theories given as rewrite systems satisfying some restrictions. This approach allows us to represent infinite sets of solutions in a finite way, and provides a decision procedure for unifiability. Moreover, we have shown that each restriction is needed to decide unifiability. future, it would be nice to use TTSGs to deal with equational disunification [START_REF] Fernández | Narrowing based procedures for equational disunification[END_REF][START_REF] Comon | Complete axiomatizations of some quotient term algebras[END_REF], i.e. finding substitutions that are not the solution of a given equation. This may be achieved if it is possible to compute the set minus between two languages recognized by TTSGs.

TTSG productions look like regular tree language productions because non-terminals are of arity 0. However, they enforce synchronization constraints as well as constraints due to control. control tuples contain non-bounded integers, a tree automata that can recognize the language defined by a TTSG need an infinite memory. The question is: What is the place of TTSGs in the known hierarchies of tree grammars?

TTSGs can define infinite sets of (tuples of) ground terms. In automated deduction, several authors have studied recurrent schematizations of infinite sets of terms, like !-terms, I-terms, R-terms and primal grammars (see elsewhere [START_REF] Hermann | Overview of Existing Recurrent Schematizations[END_REF][START_REF] Amaniss | Classification, extension and applications of some schematization methods of infinite sets of terms[END_REF][START_REF] Amaniss | Méthodes de schématisation pour la démonstration automatique[END_REF] for an overview). A language like f n a :::f n a | {z } p ;n ;p2I N can be defined both by a primal grammar and by a TTSG that does not come from a unification problem. On the other hand, the symmetric trees cannot be defined by a primal grammar, whereas they are defined by a TTSG coming from a unification problem, as shown in Example 8.8. It would be interesting to study the possible links between recurrent schematizations and TTSGs.

Example 1 . 1 1 !

 111 Consider the TRS that defines the functions f and g f (s(s(x)))

Theorem 4 . 2

 42 There exists no uniform algorithm for solving the Post correspondence problem. The problem remains undecidable when and 0 are injective.

Lemma 4 . 3

 43 Linearity of rewrite rules is necessary to decide unifiability.

2 5 Formal

 5 Definitions of TTSGsOnly formal definitions are given here. For motivations and examples see Sects. 6 and 7.

Definition 5 . 2 ADefinition 5 . 3 A

 5253 tuple of control is a tuple of non-negative integers. TTSG is defined by a 5-tuple (Sz; C;NT;PP;TI),where

Fig. 1 :

 1 Fig. 1:

Definition 8 . 3

 83 An NT-TransClass is composed by a multiset of non-terminals, and for each i 2 [1;Sz], a partition of the multiset.

2 Thus we get: Theorem 8 . 6 Example 8 . 7

 28687 The satisfiability of linear equations in theories given as confluent, constructor-based, linear, without in (see Sect. 4), without nested functions in rhs's, rewrite systems is decidable. Moreover, the set of solutions can be expressed by a tree tuple synchronized grammar. Let R = f 0+x!x; x +0!x; s(x)+s(y)!s(s(x+y));s(x)+p(y)!x+y; p(x)+s(y) !x+y; p(x)+p(y)!p(p(x+y)) g

  T C[V are called data terms. A term is said to be linear if it does not contain several times the same variable. Let

t b eat e r m ,O(t) is the set of occurrenceso ft,tj u is the subterm of t at occurrence u,a n d t(u) is the symbol that labels the occurrence u of t. t[u s] is the term obtained by replacing in t the subterm at occurrence u by s.A substitution is a mapping from V into T [V whose domain D()=f x2Vj x 6 = xg is assumed to be finite. It is trivially extended to a mapping from T

  t narrows into s, if there exists a rule l ! r in R, a non-variable occurrence u of t, such that tj u = l where = mgu(tj u ;l)and s =( t)[u r]. We write t ; [u;lr;] s, and the relation ; is called narrowing.

	Theorem 2.1 TRS R being confluent and constructor based, the set of data substitutions such that
	there exists a narrowing derivation
	t 0 ? = t 0 0 ; [1] t 1 ? = t 0

1 ; :::; [n] t n ?

  Var gare created. The variables concerned with this new case are those appearing in a branch on a rhs of the rewrite rule which contains only constructors. For each of these variables x j and for each constructor c 2C ,t h e synchronized productions fX 0j ) ANY cRes ;X j )AN Y cVar gare created. Now consider the term f(y). If the only constructors are 0, s, the productions associated with this

	problem are fAN Y 0 f X 02 )AN Y 0 Res ;X 2 )AN Y 0 fG l ) R 2 ;Y)X 2 g ;R 2 Var g; fX 02 ) ANY s )s ( X 02 ) Res ;X 2 )AN Y s Var g Res ) 0;ANY 0 Var ) 0g; fAN Y s Res ) s(ANY 1 Res );ANY s Var )s(AN Y 1 Var )g fAN Y 1 Res ) ANY 0 Res ;ANY 1 Var )AN Y 0 Var g; fAN Y 1 Res ) ANY s Res ;ANY 1 Var ) ANY s Var g
	From the pair (G l
	1 Res ;:::;ANY n Res and Var are created. Var ;:::;ANY n Var )cAN Y 1 ANY c
	For all integers i between 1 and the maximal arity of the constructors and 8c 2C, the synchronized productions fAN Y i Res ) ANY c Res ;ANY i Var ) ANY c

  We show as in 1.2 that (t; s 1 ;:::;s n )=terms(d; d 1 ;:::;d n ). 2 n ) by productions that do not use ANY and (d; d 1 ;:::;d n ) is in simplified form, ] t,thenTI (d; d 1 ;:::;d n )by productions that do not contain ANY , (d; d 1 ;:::;d n ) is in simplified form, and (t; a 1 ;:::;a n )=terms(d; d 1 ;:::;d n ).

	then	s ; [] t and (t; a 1 ;:::;a n )=terms(d; d 1 ;:::;d n )
	Conversely, if s ;

(d;

d 1 ;:::;d n ) Lemma 6.4 (Correspondence in several steps) Let TI =( G u ;A v1 ;:::;A vn ) be the simplified form of the axiom, and let (s; a 1 ;:::;a n ) be its associated tuple of terms, where a 1 ;:::;a n are variables. If TI (d; d 1 ;:::;d [

  a 1 ;:::;a n are variables). If (d; d 1 ;:::;d n ) is a tuple recognized by the grammar, i.e. TI (d; d 1 ;:::;d n ) and d; d 1 ;:::;d n do not contain any non-terminal, and so d; d 1 ;:::;d n are ground data-terms, then s ; [] t and there exists a substitution such that d = t; d 1 = a 1 ;:::;d n = a n . Conversely, if s ; [] t where t is a data term, and there exists a data substitution such that t; a 1 ;:::;a n are ground, then there is a tuple (d; d 1 ;:::;d n ) recognized by the grammar such that d = t; d 1 = a 1 ;:::;d n = a n .

	Proof. 1. First sense.

  The size of the TransClasses of a TTSG G that comes from a unification problem is not greater than card(NT) n+1 ,whereNT is the set of non-terminals associated with the unification problem, and n is the number of intersections achieved to build G.

	Lemma 8.2
	and the axiom is ((G l	3 1 g 2 gg

;X[START_REF] Nutt | Basic narrowing revisited[END_REF] ,wegetR[START_REF] Nutt | Basic narrowing revisited[END_REF] ;L[START_REF] Nutt | Basic narrowing revisited[END_REF] 1 , which means that the unification is about to be done, and therefore so is the narrowing step, but the new constructors produced by the unification and the narrowing step have not yet appeared.

A l 1 ; (0; 0)); (X l ; (0; ?)); (G l ; (?; 0))).

Acknowledgements

We would like to thank A. Bockmayr, H. Comon, A. Despland and E. Domenjoud for helpful discussions.

Control

Synchronized grammars, as defined previously, are close to regular tree grammars (and very close to the coupled grammars of Guan et al. [START_REF] Guan | Tree Grammars with Multilinear Interpretation[END_REF]), and are easy to use, but unfortunately they cannot encode our complete problem because they do not take into account variable renamings. Indeed, consider the rewrite system ff(c(x;y)) 1 c(f (x);f(y))g and the goal f (x)=t ,w he ret is an arbitrary term. The Tree Grammar Gr l contains the productions L 1 1 c(X 1 ;Y 1 );R 1 c(R 1

2 );fR 1 1 R 1

;X 1 L 1 1 g;fR 1 2 R 1

;Y 1 L 1 1 g;fG l R 1

;X l L 1 1 gand the axiom is (G l ;X l ). A possible derivation of Gr l is:

2 );c(X 1 ;Y 1 ))

2 );R 1 2 );c(L 1

2 );R 1 2 );c(c(X 1 ;Y 1 );Y 1 ))

This encodes the narrowing derivation: The problem now is that both R 1 2 and Y 1 occur twice. One occurrence of R 1 2 corresponds to the term f (y 2 ) and the other to f (y 1 ). In the same way, one occurrence of Y 1 corresponds to y 2 and the other to y 1 . Obviously, if f (y 1 ) is narrowed, y 1 is instantiated, whereas if f (y 2 ) is narrowed, y 2 instantiated. But using the grammar, the synchronized productions fR 1 2 R 1

;Y 1 L 1 1 gcan be applied on the first occurrence of R 1 2 and the second occurrence of Y 1 . This means that f (y 2 ) is narrowed while y 1 is instantiated.

The solution to this problem consists of using an integer number, called control, to encode variable renamings. In a grammar computation, each non-terminal is coupled with an integer of control, which is set to a new fresh value when a synchronized production is applied on it. When a free production is applied, the control number is preserved. Moreover, a pack of productions will be applied only on non-terminals that have the same control number. For example, the previous derivation is transformed into:

Given a TTSG Gr, a computation tp is in simplified form if tp cannot be derived by a free production.

If it is not, the simplified form of tp, denoted by tp, is a computation in simplified form derived from tp by free productions. It is unique because, from the construction of TTSG, there is at most one free production x ) t for a given non-terminal X.

Each tuple of control ct is here a 1-tuple, i.e. an integer. Id ct r j denotes the term r j whose variable

x j is renamed into x j ct . The next definition gives the way to get terms of narrowing derivations (i.e. result of narrowing and instantiation of variables) and computations of TTSGs. Definition 6.1 Let tp be a computation in simplified form, and suppose that the goal is g ? = g 0 .T h e term (that contains no non-terminals) associated to tp is the tuple issued from tp by replacing every non-terminal of the form It is denoted by termstp.

In Example 1.1, terms(s((R 4 1 ; 1));s((X 4 ; 1))) = (s(g(x 4 1 ));s(x 4 1 )). Lemma 6.2 (Technical) Let (c; c 1 ;:::;c n ) be a computation in simplified form. If w:u =( R j u ;ct)then 8x j 2 Va r (r j j u ); (X j ;ct)appears in (c 1 ;:::;c n ). Proof. Along the derivation that has created (c; c 1 ;:::;c n )a computation like ((R j ;ct);:::)has appeared, i.e. a pack like P = fR i v ) R j ;X i )L i w ; :::ghas been used while the control number ct has been created. As there is no in , every non-terminal associated with the variables of l j appears in (L j w #;k).In the derivation, the j w #'s appeared before (or at the same time as) (c; c 1 ;:::;c n ), because (c; c 1 ;:::;c n ) is in simplified form. If x j 2 Va r (r j j u ),t h e nx j 2 Va r (l j ), so the associated non-terminal (X j ;ct) appeared before (or at the same time as) (c; c 1 ;:::;c n ). It has not disappeared because x j occurs in r j under a function (r j (u) is a function), and then only a synchronized pack containing R j u ) :::could remove it; this is impossible because (R j u ;k)would also have been removed. T ransC lasstp; u is the set of occurrences of tp that may be indirectly synchronized with u.

It is the union of the following inductively defined sets:

-E 0 = S Sz j=1 Class(tp; u; j)

-E i+1 = S Sz j=1 fvj9w 2E i such that v 2 Class(tp; w; j)g. The occurrence of X is 1:1.

Class(tp; 1:1; 2) = f1:1; 1:2g, i.e. the occurrences of X and Y . T ransClass(tp; 1:1) = f1:1; 1:2; 2:1g. Class and T ransClass contain non-terminal occurrences, i.e. occurrences of leaves. TransClass is roughly the transitive closure of Class -then two different TransClasses are disjoint.

The following lemma means that two different TransClasses can be derived independently.

Lemma 7.4

Two different TransClasses of the same computation tp cannot be merged when tp is derived further. Formally, let TC = fu 1 ;:::;u n g and TC 0 = fu 0 1 ;:::;u 0 n 0g two different TransClasses of tp 2 Comp(Gr), and let tp 0 a computation derived form tp the grammar (i.e. ) tp 0 ). Then any two non-terminal occurrences v;v 0 of tp 0 ,ofthefor mv = u i :w, v 0 = u 0 j :w 0 , do not belong to the same TransClass of tp 0 .

Proof. Obvious as packs of synchronized productions may divide Classes but never join them. 2 Definition 7.5 Let G =( Sz;C;NT;PP;TI)be a TTSG. The ith component of G is said to be externally synchronized if 8tp 2 Comp(G) and for all packs fX 1 ) Y 1 ;:::;X n )Y n g k of PP that can be applied on tp (at occurrences fu 1 ;:::;u n g)wehave 1. there is at most one v 2fu 1 ;:::;u n gsuch that v = i:w, 2. and if such v exists then the tuple tp 0 obtained by applying fX 1 ) Y 1 ;:::;X n ) Y n g k on tp satisfies T ransClass(tp 0 ;v)\fv 0 2O(tp)jv 0 = i:w 0 g = v.

Recall that the first component computes the ground instances of terms obtained by narrowing.

Lemma 7.6

The first component of every TTSG produced from the unification problem has the external synchronization property.

Proof. By construction, the first component contains only non-terminals like R ? ? or like X j ,w h e r ex j is a variable occurring only under constructors on some rhs. So X j does not appear as the lhs of any productions. Moreover, in every pack of productions there is only one production whose lhs is of the form R ? ? .

On the other hand, the control tuples of such TTSGs are 1-tuples. So the Classes and TransClasses are the same, therefore (2) is satisfied.

2

The axiom is now ((X; (0; ?); (YZ;(0; 0)); (T; (?; 0)). ? means that this level of control is not used by the non-terminal. A possible derivation for G 3 is ((X; (0; ?); (YZ;(0; 0)); (T; (?; 0)) ) ((X 0 ; (1; ?); (Y 0 Z; (1; 0)); (T; (?; 0)) Now fY 0 Z ) Y 0 Z 0 ;T )T 0 g 2 is applicable, and we get ((X 0 ; (1; ?)); (Y 0 Z 0 ; (1; 1)); (T 0 ; (?; 1))) )

[free prods:] (s((X; (1; ?)));s((Y 00 Z; (1; 1)));s(s((T; (?; 1))))) ) (s((X; (1; ?)));s((Y 00 Z 0 ; (1; 2)));s(s((T 0 ; (?; 2))))) )

[free prods:] (s((X; (1; ?)));s(s((YZ;(1; 2))));s(s(s(s((T; (?; 2))))))) ) (s((X 0 ; (2; ?)));s(s((Y 0 Z; (2; 2))));s(s(s(s((T; (?; 2))))))) ) (s((X 0 ; (2; ?)));s(s((Y 0 Z 0 ; (2; 3))));s(s(s(s((T 0 ; (?; 3))))))) )

[free prods:] (s(0);s(s(0));s(s(s(s(0)))))

The following definition is needed for Theorem 7.9. It defines the set of non-terminals that may be derived from a given non-terminal. Definition 7.8 Let PP be a set of packs of productions. ReachX; P P is inductively defined by X is in Reach(X; P P ), if Y is in Reach(X; P P ) and Y ) Z is a production that belongs to a pack of PP,t henZ is in Reach(X; P P ), if Y is in Reach(X; P P ) and there is a free production in PP such that Y ) c(Y 1 ;:::;Y n ),t hen fY 1 ;:::;Y n gReach(X;PP). Theorem 7.9 (Algorithm for intersection) Let G 1 =( Sz 1 ; C 1 ;NT 1 ;PP 1 ;TI 1 ) and G 2 =( Sz 2 ; C 2 ; NT 2 ;P P 2 ;T I 2 )be two TTSGs such that the i 1 th component of G 1 is externally-synchronized. The language recognized by the TTSG G 3 =( Sz 3 ; C 3 ;NT 3 ;PP 3 ;TI 3 )as defined below is the one component i 1 ;i 2 intersection of G 1 and G 2 . (I i1 ;ct i 1 ) (resp. (I i2 ;ct i 2 )) denotes the i 1 th (resp. i 2 th) component of the axiom TI 1 (resp. TI 2 )ofG 1 (resp. G 2 ).

where -C ons = fX1X2 c(Y1;1 Y2;1 ;:::;Y1;n Y2;n ) such that X1 2 Reach(Ii 1 ;PP1) and X1 c(Y1;1 ;:::;Y1;n ) 2 PP1 and X2 2 Reach(Ii 2 ;PP2) and X2 c(Y2;1 ;:::;Y2;n ) 2 PP2g -Sync1 = ffX1X2 Y1X2;Z 1 Z 0 1 ;:::;Zn Z 0 n gksuch that X1 2 Reach(Ii 1 ;PP1) and fX1 Y1 ;Z1 Z 0 1 ;:::;Zn Z 0 n gk 2PP1and X2 2 Reach(Ii 2 ;PP2)g

We have Reach(G l )=f G l ;R 1 ;R 2 ;R 3 g. So the intersection of Gr lef t with Gr r

gives the final grammar with the following new productions:

) 0; fR 1 ) R 1 ; X 1 ) L 1 1 g 2 ; fR 1 ) R 2 ; X 1 ) L 2 1 g 2 ; fR 1 ) R 3 ; X 1 ) L 3 1 g 2 ; fR 2 ) R 1 ; X 2 ) L 1 1 g 2 ; fR 2 ) R 2 ; X 2 ) 2 1 g 2 ; fR 2 ) R 3 X 2 ) L 3 1 g 2 ; fG l ) R 1

; A l 1 ) L 1 1 g 2 ; fG l ) R 2

; A l 1 ) L 2 1 g 2 ; fG l ) R 3

; A l 1 ) L 3 1 g 2 gg and the axiom is ((G l 1 A l 1 ; (0; 0; ?));(X l ; (0; ?;?));(G l G r ; (?; 0; 0))).

A possible derivation of this TTSG is ) (s(s(0));s(s(0)); 0)

This derivation illustrates how the synchronizations enforce two applications r 4 for one application of r 1 .

Decidability

This section shows how unifiability can be decided thanks to TTSGs. First, we give a bound on the size of the TransClasses that is used to limit the length of the derivations. At the end of this section, two examples of problems we can solve with our technique are given.

In the following lemmas, a Class (resp. TransClass) of a given TTSG G denotes any Class (resp. TransClass) in any computation of G. Proof. This is true for the axiom, since the goal is linear. Actually, linearity of each side of the goal, considered independently of each other, suffices.

When applying a pack of synchronized productions f:::)R j ; ::: )L j v1 ;::: )L j vn g, the newly generated non-terminals belong to the same Class, but they are different to each other. After that, they are reduced into a simplified form (this notion was defined at the beginning of Sect. 6.6) by free productions.

However, the non-terminals appearing in the simplified form of R j e psilon come from the rhs of rewrite rule j, and are then of the form R j ? , X 0j , Y 0j ,... . The same X 0j cannot appear twice because of the linearity of the rhs's. On the other hand, L j v1 ;:::;L j vn are replaced by independent subterms of the rhs l j that contain non-terminals like L j ? , X j , Y j ,... . So the same X j cannot appears twice because of the linearity of the lhs's.

2