Thomas Place

Luc Segoufin

A DECIDABLE CHARACTERIZATION OF LOCALLY TESTABLE TREE LANGUAGES

Keywords: 1998 ACM Subject Classification: F.4.3 Regular Tree Languages, Locally Testable, Characterization

A regular tree language L is locally testable if membership of a tree in L depends only on the presence or absence of some fix set of neighborhoods in the tree. In this paper we show that it is decidable whether a regular tree language is locally testable. The decidability is shown for ranked trees and for unranked unordered trees.

Introduction

This paper is part of a general program trying to understand the expressive power of first-order logic over trees. We say that a class of regular tree languages has a decidable characterization if the following problem is decidable: given as input a finite tree automaton, decide if the recognized language belongs to the class in question. Usually a decision algorithm requires a solid understanding of the expressive power of the corresponding class and is therefore useful in any context where a precise boundary of this expressive power is crucial. In particular we do not possess yet a decidable characterization of the tree languages definable in FO(≤), the first-order logic using a binary predicate ≤ for the ancestor relation.

We consider here the class of tree languages definable in a fragment of FO(≤) known as Locally Testable (LT). A language is in LT if membership in the language depends only on the presence or absence of neighborhoods of a certain size in the tree. A closely related family of languages is the class LTT of Locally Threshold Testable languages. Membership in such languages is determined by counting the number of neighborhoods of a certain size up to some threshold. The class LT is the special case where no counting is done, the threshold is 1. In this paper we provide a decidable characterization of the class LT over trees.

The standard approach for deriving a decidable characterization is to first exhibit a set of closure properties that hold exactly for the languages in the class under investigation and then show that these closure properties can be automatically tested. This requires a formalism for expressing the desired closure properties but also some tools, typically induction mechanisms, for proving that the properties do characterize the class, and for proving the decidability of those properties.

Over words one formalism turned out to be successful for characterizing many classes of regular languages. The closure properties are expressed as identities on the syntactic monoid or syntactic semigroup of the regular language. The syntactic monoid or syntactic semigroup of a regular language is the transition monoid of its minimal deterministic automaton including or not the transition induced by the empty word. For instance the class of word languages definable in FO(≤) is characterized by the fact that the syntactic monoid of any such languages is aperiodic. The latter property corresponds to the identity = +1 where is the size of the monoid. This equation is easily verifiable automatically on the syntactic monoid. Similarly, the classes LTT and LT have been characterized using decidable identities on the syntactic semigroup [START_REF] Brzozowski | Characterizations of locally testable languages[END_REF][START_REF] Mcnaughton | Algebraic decision procedures for local testability[END_REF][START_REF] Beauquier | Factors of words[END_REF][START_REF] Thérien | Graph congruences and wreath products[END_REF].

Over trees the situation is more complex and right now there is no formalism that can easily express all the known closure properties for the classes for which we have a decidable characterization. The most successful formalism is certainly the one introduced in [START_REF] Bojańczyk | Forest algebras[END_REF] known as forest algebras. For instance, these forest algebras were used for obtaining decidable characterizations for the classes of tree languages definable in EF+EX [START_REF] Bojańczyk | Characterizing EF and EX tree logics[END_REF], EF+F -1 [Boj07b, Pla08], BC-Σ 1 (<) [START_REF] Bojańczyk | Piecewise testable tree languages[END_REF][START_REF] Place | Characterization of logics over ranked tree languages[END_REF], Δ 2 (≤) [START_REF] Bojańczyk | Tree languages defined in first-order logic with one quantifier alternation[END_REF][START_REF] Place | Characterization of logics over ranked tree languages[END_REF]. However it is not clear yet how to use forest algebras in a simple way for characterizing the class LTT over trees and a different formalism was used for obtaining a decidable characterization for this class [START_REF] Benedikt | Regular languages definable in FO and FOmod[END_REF].

We were not able to obtain a reasonable set of identities for LT either by using forest algebras or the formalism used for characterizing LTT. Our approach is slightly different.

There is another technique that was used on words for deciding the class LT. It is based on the "delay theorem" [START_REF] Straubing | Finite semigroup varieties of the form V * D[END_REF][START_REF] Tilson | Categories as algebra: an essential ingredient in the theory of monoids[END_REF] for computing the required size of the neighborhoods: Given an automaton recognizing the language , a number can be computed from that automaton such that if is in LT then it is in LT by investigating the neighborhoods of size . Once this is available, deciding whether is indeed in LT or not is a simple exercise. On words, a decision algorithm for LT (and also for LTT) has been obtained successfully using this approach [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF]. Unfortunately all efforts to prove a similar delay theorem on trees have failed so far.

We obtain a decidable characterization of LT by combining the two approaches mentioned above. We first exhibit a set of necessary conditions for a regular tree language to be in LT. Those conditions are expressed using the formalism introduced for characterizing LTT. We then show that for languages satisfying such conditions one can compute the required size of the neighborhoods. Using this technique we obtain a characterization of LT for ranked trees and for unranked unordered trees.

Other related work. There exist several formalisms that have been used for expressing identities corresponding to several classes of languages but not in a decidable way. Among them let us mention the notion of preclones introduced in [START_REF] Esik | Algebraic characterization of regular tree languages[END_REF] as it is close to the one we use in this paper for expressing our necessary conditions.

Finally we mention the class of frontier testable languages, not expressible in FO(<), that was given a decidable characterization using a specific formalism [START_REF] Wilke | An algebraic characterization of frontier testable tree languages[END_REF].

Organization of the paper. We start with ranked trees and give the necessary notations and preliminary results in Section 2. Section 3 exhibits several conditions and proves they are necessary for being in LT. In Section 4 we show that for the languages satisfying the necessary conditions the required size of the neighborhoods can be computed, hence concluding the decidability of the characterization. Finally in Section 5 we show how our result extends to unranked trees.

Notations and preliminaries

We first investigate the case of binary trees. The case of unranked unordered trees will be considered in Section 5.

Trees. We fix a finite alphabet Σ, and consider finite binary trees with labels in Σ. All the results presented here extend to arbitrary ranks in a straightforward way. In the binary case, each node of the tree is either a leaf (has no children) or has exactly two children, the left child and the right child. We use the standard terminology for trees. For instance by the descendant (resp. ancestor) relation we mean the reflexive transitive closure of the child (resp. inverse of child) relation and by distance between two nodes we refer to the length of the shortest path between the two nodes. A language is a set of trees.

Given a tree and a node of the subtree of rooted at , consisting of all the nodes of that are descendant of , is denoted by | . A context is a tree with a designated (unlabeled) leaf called its port which acts as a hole. Given contexts and ′ , their concatenation ⋅ ′ is the context formed by identifying the root of ′ with the port of . A tree ⋅ can be obtained similarly by combining a context and a tree . Given a tree and two nodes , of such that is a descendant (not necessarily strict) of , the context of between and , denoted by [ , ], is defined by keeping all the nodes of that are descendants of but not descendants of and by placing the port at . We say that a context occurs in if is the context of between and for some nodes and of .

Types. Let be a tree and be a node of and be a positive integer, the -type of is the (isomorphism type of the) restriction of | to the set of nodes of at distance at most from . When will be clear from the context we will simply say type. A -type occurs in a tree if there exists a node of of type . If is the context [ , ] for some tree and some nodes , of , then the -type of a node of is the -type of the corresponding node in . Notice that the -type of a node of depends on the surrounding tree , in particular the port of has a -type, the one of in .

Given two trees and ′ we denote by ≼ ′ the fact that all -types that occur in also occur in ′ . Similarly we can speak of ≼ when is a tree and is ′ [ , ] for some tree ′ and some nodes , of ′ . We denote by ≃ ′ the property that the root of and the root of ′ have the same -type and and ′ agree on their -types: ≼ ′ and ′ ≼ . Note that when is fixed the number of -types is finite and hence the equivalence relation ≃ has a finite number of equivalence classes. This property is no longer true for unranked trees and this is why we will have to use a different technique for this case.

A language is said to be -locally testable if is a union of equivalence classes of ≃ . A language is said to be locally testable (is in LT) if there is a such that it is -locally testable. In other words, in order to test whether a tree belongs to it is enough to check for the presence or absence of -types in , for some big enough .

Regular Languages. We assume familiarity with tree automata and regular tree languages. The interested reader is referred to [CGJ + 07] for more details. Their precise definitions are not important in order to understand our characterization. However pumping arguments will be used in the decision algorithms.

The problem. We want an algorithm deciding if a given regular language is in LT. When the complexity is not an issue, we can assume that the language is given as a MSO formula. Another option would be to start with a bottom-up tree automaton for or, even better, the minimal deterministic bottom-up tree automaton that recognize . We will come back to the complexity issues in Section 7. The main difficulty is to compute a bound on , the size of the neighborhood, whenever such a exists.

The word case is a special case of the tree case as it corresponds to trees of rank 1. A decision procedure for LT was obtained in the word case independently by [START_REF] Brzozowski | Characterizations of locally testable languages[END_REF] and [START_REF] Mcnaughton | Algebraic decision procedures for local testability[END_REF]. A language is in LT if and only if its syntactic semigroup satisifies the equations = and = , where is an arbitrary idempotent ( = ) while and are arbitrary elements of the semigroup. The equations are then easily verified after computing the syntactic semigroup.

In the case of trees, we were not able to obtain a reasonably simple set of identities for characterizing LT. Nevertheless we can show: Theorem 2.1. It is decidable whether a regular tree language is in LT.

Our strategy for proving Theorem 2.1 is as follows. In a first step we provide necessary conditions for a language to be in LT. In a second step we show that if a language verifies those necessary conditions then we can compute from an automaton recognizing a number such that if is in LT then is -locally testable. The last step is simple and show that once is fixed, it is decidable whether a regular language is -locally testable. This last step follows immediately from the fact that once is fixed, there are only finitely many -locally testable languages and hence one can enumerate them and test whether is equivalent to one of them or not.

Given a regular language , testing whether is in LT is then done as follows: (1) compute from the of the second step and (2) test whether is -locally testable using the third step. The first step implies that this algorithm is correct.

Before starting providing the proof details we note that there exist examples showing that the necessary conditions are not sufficient. Such an example will be provided in Section 6. We also note that the problem of finding whenever such a exists is a special case of the delay theorem mentioned in the introduction. When applied to LT, the delay theorem says that if a finite state automaton recognizes a language in LT then this language must be -locally testable for a computable from . The delay theorem was proved over words in [START_REF] Straubing | Finite semigroup varieties of the form V * D[END_REF] and can be used in order to decide whether a regular language is in LT as explained in [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF]. We were not able to prove such a general theorem for trees.

Necessary conditions

In this section we exhibit necessary conditions for a regular language to be in LT. These conditions will play a crucial role in our decision algorithm. These conditions are expressed using the same formalism as the one used in [START_REF] Benedikt | Regular languages definable in FO and FOmod[END_REF] for characterizing LTT.

Guarded operations. Let be a tree, and , ′ be two nodes of such that and ′ are not related by the descendant relationship. The horizontal swap of at nodes and ′ is the tree ′ constructed from by replacing | with | ′ and vice-versa, see Figure 1

(left).

A horizontal swap is said to be -guarded if and ′ have the same -type.

Let be a tree and , , be three nodes of such that , , are not related by the descendant relationship and such that | = | . The horizontal transfer of at , , is the tree ′ constructed from by replacing | with a copy of | , see Figure 1 (right). A horizontal transfer is -guarded if , , have the same -type. Let be a tree of root , and , , be three nodes of such that is a descendant of and is a descendant of . The vertical swap of at , , is the tree ′ constructed from by swapping the context between and with the context between and , see Figure

| | ′ ′ ⇐⇒ | ′ | ′ | | | ⇐⇒ | | |
(left). More formally let = [ , ], Δ 1 = [ , ], Δ 2 = [ , ] and = | . We then have = ⋅ Δ 1 ⋅ Δ 2 ⋅ . The tree ′ is defined as ′ = ⋅ Δ 2 ⋅ Δ 1 ⋅ . A vertical swap is -guarded if , , have the same -type.
Let be a tree of root , and , , be three nodes of such that is a descendant of and is a descendant of such that Δ = [ , ] = [ , ]. The vertical stutter of at , , is the tree ′ constructed from by removing the context between and , see Figure (right). A vertical stutter is -guarded if , , have the same -type. Let be a tree language and be a number. If X is any of the four constructions above, horizontal or vertical swap, or vertical stutter or horizontal transfer, we say that is closed under -guarded X if for every tree and every tree ′ constructed from using -guarded X then is in iff ′ is in . Notice that being closed under -guarded X implies being closed under ′ -guarded X for ′ > . An important observation is that each of the -guarded operation does not affect the set of ( + 1)-types occurring in the trees. If is closed under all the -guarded operations described above, we say that is -tame. A language is said to be tame if it is -tame for some .

Δ 1 Δ 2 ⇐⇒ Δ 2 Δ 1 Δ Δ ⇐⇒ Δ
The following simple result shows that tameness is a necessary condition for LT.

Proposition 3.1. If is in LT then is tame.

Proof. Assume is in LT. Then there is a such that is -locally testable. We show that is -tame. This is a straightforward consequence of the fact that all the -guarded operations above preserve ( + 1)-types and hence preserve -types.

A simple pumping argument shows that if is tame then it is -tame for bounded by a polynomial in the size of the minimal deterministic bottom-up tree automaton recognizing .

Proposition 3.2. Given a regular language and the minimal deterministic bottom-up tree automaton recognizing , we have is tame iff is 0 -tame for 0 = | | 3 + 1.

Proof. We prove that if is one of the four operations that defines tameness, then if is closed under -guarded for > 0 , then is closed under 0 -guarded . This will imply that if is -tame then it is 0 -tame.

Consider the case of -guarded horizontal transfer and assume is closed underguarded horizontal transfers. We show that is closed under 0 -guarded horizontal transfers. Let be a tree and , , three nodes of having the same 0 -type and not related by the descendant relation such that | = | . We need to show that replacing | by a copy of | does not affect membership in .

We do this in three steps, first we transform by pumping in parallel in the subtrees of , and until , , have the same -type, then we use the closure of under -guarded horizontal transfer in order to replace | by a copy of | , and finally we backtrack the initial pumping phase in order to recover the initial subtrees.

We let 1 = | and 2 = | and we assume for now on that 1 ∕ = 2 . By position we denote a string of {0, 1} * . A position is realized in a tree if there is a node of such that if 1 , ⋅ ⋅ ⋅ , = is the sequence of nodes in the path from the root of to then for all ≤ the ℎ bit of is zero if is a left child and it is one if is a right child. We order positions by first comparing their respective length and then using the lexicographical order.

By hypothesis 1 and 2 are identical up to depth at least 0 . Let be the first position such that 1 and 2 differ at that position. That can be either because is realized in 1 but not in 2 , or vice versa, or is realized in both trees but the labels of the corresponding nodes differ. We know that the length of is strictly greater than 0 . If > , we are done with the first phase. We assume now that ≤ .

Consider the run of on . The run assigns a state to each node of . From we assign to each position ′ < a pair of states ( , ′ ) such that is the state given by at the corresponding node in 1 while ′ is the state given by at the corresponding node in

2 . Because > 0 > | | 2 ,
there must be two prefixes 1 and 2 of that were assigned the same pair of states. Consider the context 1 = 1 [ 1 , 2 ] where and ′ are the nodes of 1 at position 1 and 2 and the context

2 = 2 [ ′ 1 , ′ 2 ]
where and ′ are the nodes of 2 at position 1 and 2 . Without affecting membership in , we can therefore at the same time duplicate 1 in the two copies of 1 rooted at and and 2 in the copy of 2 rooted at .

Let ′ 1 and ′ 2 be the subtrees of the resulting tree, rooted respectively at and . The reader can verify that ′ 1 and ′ 2 now differ at a position strictly greater than . Performing this repeatedly, we eventually arrive at a situation where the subtree ′ 1 rooted at and agree up to depth with the subtree rooted at . We can now apply -guarded horizontal transfer and replace one occurrence of ′ 1 by a copy of ′ 2 . We can then replace ′

1 by 1 and both copies of ′ 2 by 2 without affecting membership in . The other operations are done similarly. For the horizontal swap, we pump the subtrees at positions and ′ simultaneously, which is possible because 0 > | | 2 . For vertical swap, we pump the subtrees at the positions , and simultaneously, and that requires 0 > | | 3 . Finally, for vertical stutter, we pump the subtrees at the positions , and simultaneously, which again requires 0 > | | 3 .

Once is fixed, a brute force algorithm can check whether is -tame or not. Indeed, as is regular, when testing for closure under -guarded , it is enough to consider all relevant states and appropriate transition functions of the automata instead of all trees and all contexts. See for instance Lemma 12 and Lemma 13 in [START_REF] Benedikt | Regular languages definable in FO and FOmod[END_REF].

Therefore Proposition 3.2 implies that tameness is decidable. However for deciding LT we will only need the bound on 0 given by the proposition.

Deciding LT

In this section we show that it is decidable whether a regular tree language is in LT. This is done by showing that if a regular language is in LT then there is a computable from an automaton recognizing such that is in fact -locally testable. Recall that once this is computed the decision procedure simply enumerates all the finitely many -locally testable languages and tests whether is one of them.

Assume is in LT. By Proposition 3.1, is tame. Even more, from Proposition 3.2, one can effectively compute a such that is -tame. Hence Theorem 2.1 follows from the following proposition.

Proposition 4.1. Assume is a -tame regular tree language then is in LT iff is -locally testable where is computable from .

Recall that for each the number of -types is finite. Let be this number. Proposition 4.1 is an immediate consequence of the following proposition.

Proposition 4.2. Let be a -tame regular tree language. Set = + + 1. Then for all > and any two trees , ′ if ≃ ′ then there exist two trees , ′ with

(1)

∈ iff ∈ (2) ′ ∈ iff ′ ∈ (3) ≃ ′
Proof of Proposition 4.1 using Proposition 4.2. Assume is -tame and let be defined as in Proposition 4.2. We show that is in LT iff is -locally testable. Assume is in LT. Then is -locally testable for some ∈ ℕ. We show that is actually -locally testable. For this it suffices to show that for any pair of trees and ′ , if

≃ ′ then ∈ iff ′ ∈ . Let
and ′ be the trees constructed for from and ′ by Proposition 4.2. We have ≃ ′ and therefore ∈ iff ′ ∈ . As we also have ∈ iff ∈ and ′ ∈ iff ′ ∈ , the proposition is proved.

Before proving Proposition 4.2 we need some extra terminology. A non-empty context occurring in a tree is a loop of -type if the -type of its root and the -type of its port is . A non-empty context occurring in a tree is a -loop if there is some -type such that is a loop of -type . Given a context we call the path from the root of to its port the principal path of . Finally, the result of the insertion of a -loop at a node of a tree is a tree such that if = ⋅ | then = ⋅ ⋅ | . Typically an insertion will occur only when the -type of is and is a loop of -type . In this case the -types of the nodes initially from and of the nodes of are unchanged by this operation.

Proof of Proposition 4.2. Suppose that is -tame. We start by proving two lemmas that will be useful in the construction of and ′ . Essentially these lemmas show that even though being -tame does not imply being ( + 1)-locally testable (recall the remark after Theorem 2.1) some of the expected behavior of ( + 1)-locally testable languages can still be derived from being -tame. The first lemma shows that given a tree , without affecting membership in , we can replace a subtree of containing only ( + 1)-types occurring elsewhere in by any other subtree satisfying this property and having the same -type as root. The second lemma shows the same result for contexts by showing that a -loop can be inserted in a tree without affecting membership in as soon as all the ( + 1)-types of the -loop were already present in . After proving these lemmas we will see how to combine them for constructing and ′ . Lemma 4.3. Assume is -tame. Let = be a tree where is a subtree of . Let ′ be another tree such that the roots of and ′ have the same -type.

If

≼ +1 and ′ ≼ +1 then ∈ iff ′ ∈ .
Proof. We start by proving a special case of the Lemma when ′ is actually another subtree of . We will use repeatedly this particular case in the proof.

Claim 4.4. Assume is -tame. Let be a tree and let , be two nodes of not related by the descendant relationship and with the same -type. We write = | , ′ = | and the context such that =

. If ≼ +1 then ∈ iff ′ ∈ .
Proof. The proof is done by induction on the depth of and makes crucial use of -guarded horizontal transfer. Assume first that is of depth less than . Since and have the same -type, we have = ′ and the result follows.

Assume now that is of depth greater than . Let be the ( + 1)-type of . We assume that is a tree of the form ( 1 , 2 ). Notice that the -type of the roots of 1 and 2 are completely determined by . Since ≼ +1 , there exists a node in of type . We write ′′ = | .

We consider several cases depending on the relationship between , and . We first consider the case where and are not related by the descendant relationship, then we reduce the other cases to this case.

Assume that and are not related by the descendant relationship. Since ′′ is of type , it is of the form ( ′′ 1 , ′′ 2 ) where the roots of ′′ 1 and ′′ 2 have the same -type as respectively the roots of 1 and 2 . By hypothesis all the ( + 1)-types of 1 and 2 already appear in and hence we can apply the induction hypothesis to replace 1 by ′′ 1 and 2 by ′′ 2 without affecting membership in . Notice that the resulting tree is ′′ , that = ∈ iff ′′ ∈ , and that ′′ contains two copies of the subtree ′′ , one at position and one at position . We now show that we can derive ′ from ′′ using -guarded operations.

Since is -tame it will follow that that ′′ ∈ iff ′ ∈ and thus ∈ iff ′ ∈ . Let ′′ = ′′ and we distinguish between three cases depending on the relationship between and in ′′ :

(1) If is a descendant of , let = ′′ [ , ] and notice that ′ = ′′ . Since , and have the same -type, we use -guarded vertical stutter to duplicate and a -guarded horizontal swap to move the new copy of at position (see the picture below). The resulting tree is ′ as desired.

′′ ′′ =⇒ Vertical Stutter ′′ ′′ =⇒ Horizontal Swap ′′ ′′
(2) If is an ancestor of , let = ′′ [ , ] and notice that ′′ = ′ . Since and have the same -type, we use -guarded horizontal swap followed by a -guarded vertical stutter to delete the copy of (see the picture below). The resulting tree is ′ as desired. This concludes the case where and are not related by the descendant relationship in . We are left with the case where is a descendant of (recall that is outside and therefore not a descendant of ). We reduce this problem to the previous case by considering two subcases:

• If , are not related by the descendant relationship, we use a -guarded horizontal swap to replace by ′ and vice versa. This reverses the roles of and and as and are not related by the descendant relationship and position now has ( + 1)-type we can apply the previous case.

′ =⇒ Horizontal Swap ′ =⇒ Previous Case ′ ′
• If is an ancestor of both and we use -guarded vertical stutter to duplicate the context between and . This introduces a new node ′ of type that is not related to by the descendant relationship and we are back in the previous case.

′ =⇒ Vertical Stutter ′ ′ ′ ′ =⇒ Previous Case ′ ′ ′ ′ ′ =⇒ Vertical Stutter ′ ′
We now turn to the proof of Lemma 4.3. The proof is done by induction on the depth of ′ . The idea is to replace with ′ node by node.

Assume first that ′ is of depth less than . Then because the -type of the roots of and ′ are equal, we have = ′ and the result follows.

Assume now that ′ is of depth greater than . Let be the node of corresponding to the root of . Let be the ( + 1)-type of the root of ′ . We assume that ′ is a tree of the form ( ′ 1 , ′ 2 ). Notice that the -type of the roots of ′ 1 and ′ 2 are completely determined by . By hypothesis ′ ≼ +1 , hence there exists a node in of type . We consider two cases depending on the relationship between and .

• If is an ancestor of , let be [ , ] and notice that and have the same -type. This case is depicted below. Hence applying a -guarded vertical stutter we can duplicate obtaining the tree . Because is -tame, ∈ iff = ∈ . Now the root of in is of type and therefore of the form ( 1 , 2 ) where the roots of 1 and 2 have the same -type as respectively the roots of ′ 1 and ′ 2 . By construction all the ( + 1)-types of 1 and 2 already appear in and hence we can apply the induction hypothesis to replace 1 by ′ 1 and 2 by ′ 2 without affecting membership in . Altogether this gives the desired result. • Assume now that and are not related by the descendant relationship. This case is depicted below. Let ′′ be the subtree of rooted at . By hypothesis all the ( + 1)-types of are already present in and the roots of and ′′ have the same -type. Hence we can apply Claim 4.4 and we have ∈ iff ′′ ∈ . Now the root of ′′ is by construction of type . Hence ′′ is of the form ( 1 , 2 ) where 1 and 2 have all their ( + 1)-types appearing in and their roots have the same -type as respectively ′ 1 and ′ 2 . Hence by induction 1 can be replaced by ′ 1 and 2 by ′ 2 without affecting membership in . Altogether this gives the desired result. We now prove a similar result for -loops.

Lemma 4.5. Assume is -tame. Let be a tree and a node of of -type . Let ′ be another tree such that ≃ +1

′ and be a -loop of type in ′ . Consider the tree constructed from by inserting a copy of at . Then ∈ iff ∈ .

Proof. The proof is done in two steps. First we use the -tame property of to show that we can insert a -loop ′ at in such that the principal path of is the same as the principal path of ′ . By this we mean that there is a bijection from the principal path of ′ to the principal path of that preserves the child relation and ( + 1)-types. In a second step we replace one by one the subtrees hanging from the principal path of ′ with the corresponding subtrees in .

First some terminology. Given two nodes , ′ of some tree , we say that ′ is a l-ancestor of if is a descendant of the left child of ′ . Similarly we define r-ancestorship.

Consider the context occurring in ′ . Let 0 , ⋅ ⋅ ⋅ , be the nodes of ′ on the principal path of and 0 , ⋅ ⋅ ⋅ , be their respective ( + 1)-type. For 0 ≤ < , set to l if +1 is a left child of and r otherwise.

From we construct using -guarded swaps and -vertical stutters a tree 1 such that there is a sequence of nodes 0 , ⋅ ⋅ ⋅ , in 1 with for all 0 ≤ < , is of type and is an -ancestor of +1 . The tree 1 is constructed by induction on (note that this step do not require that is a -loop). If = 0 then this is a consequence of ≃ +1 ′ that one can find in a node of type 0 . Consider now the case > 0. By induction we have constructed from a tree ′ 1 such that 0 , ⋅ ⋅ ⋅ , -1 is an appropriate sequence in ′ 1 . By symmetry it is enough to consider the case where is the left child of -1 . Because all -guarded operations preserve ( + 1)-types, we have ≃ +1 ′ 1 and hence there is a node ′ of ′ 1 of type . If -1 is a l-ancestor of ′ then we are done. Otherwise consider the left child ′′ of -1 and notice that because is a child of -1 and -1 has the same ( + 1)-type as -1 then ′′ , and ′ have the same -type. We know that ′ is not a descendant of ′′ . There are two cases. If ′ and ′′ are not related by the descendant relationship then by -guarded swaps we can replace the subtree rooted in ′′ by the subtree rooted in ′ and we are done. If ′ is an ancestor of ′′ then the context between ′ and ′′ is a -loop and we can use -guarded vertical stutter to duplicate it. This places a node having the same ( + 1)-type as ′ as the left child of -1 and we are done.

This concludes the construction of 1 . From 1 we construct using -guarded swaps and -guarded vertical stutter a tree 2 such that there is a path 0 , ⋅ ⋅ ⋅ , in 2 with is of type for all 0 ≤ < .

Consider the sequence 0 , ⋅ ⋅ ⋅ , obtained in 1 from the previous step. Recall that the -type of 0 is the same as the -type of . Hence using -guarded vertical stutter we can duplicate in 1 the context rooted in 0 and whose port is . Let ′ 1 the resulting tree. We thus have two copies of the sequence 0 , ⋅ ⋅ ⋅ , that we denote by the top copy and the bottom copy. Assume is not a child of -1 . By symmetry it is enough to consider the case where -1 is a l-ancestor of . Notice then that the context between the left child of -1 and is a -loop. Using -guarded vertical swap (see Figure 3) we can move the top copy of this context next to its bottom copy. Using -guarded vertical stutter this extra copy can be removed. We are left with an instance of the initial sequence in the bottom copy, while in the top one is a child of -1 . This construction is depicted in figure 3. Repeating this argument yields the desired tree 2 . Consider now the context ′ = 2 [ 0 , ]. It is a loop of -type . Let ′ be the tree constructed from by inserting ′ at .

Claim 4.6. ′ ∈ iff ∈ . Proof. Consider the sequence of -guarded swaps and -guarded vertical stutter that was used in order to obtain 2 from . Because is -tame, ∈ iff 2 ∈ . We can easily identify the nodes of with the nodes of ′ outside of ′ . Consider the same sequence of -guarded operations applied to ′ . Observe that this yields a tree 2 corresponding to 2 with possibly several extra copies of ′ . As ′ is a -loop, each of the roots and the ports of these extra copies have the same -type. Hence, using appropriate vertical -swaps or appropriate horizontal -swaps, depending on whether two copies are related or not by the descendant relation, they can be brought together. Two examples of such operation is given in Figure 4.

Then, using -guarded vertical stutter all but one copy can be eliminated resulting in 2 . Hence ′ ∈ iff 2 ∈ and the claim is proved. See figure 5. It remains to show that ′ ∈ iff ∈ . By construction of ′ we have ′ ≼ +1 . Consider now a node in the principal path of ′ . Let be the subtree branching out the principal path of at and ′ be the subtree branching out the principal path of ′ at . By construction and are of ( + 1)-type . Therefore the roots of and ′ have the same -type. Because ′ ≼ +1 all the ( + 1)-types of ′ already appear in the part of ′ outside of ′ . By hypothesis we also have ≼ +1 . Hence we can apply Lemma 4.3 and replacing ′ with does not affect membership in . A repeated use of that lemma eventually shows that ′ ∈ iff ∈ . We return to the proof of Proposition 4.2. Recall that we have two trees , ′ such that ≃ ′ for = + + 1. For > , we want to construct , ′ such that:

(1) ∈ iff ∈ (2) ′ ∈ iff ′ ∈ (3) ≃ ′
Recall that the number of -types is . Therefore, by choice of , in every branch of a -type one can find at least one -type that is repeated. This provides many -loops that can be used using Lemma 4.5 for obtaining bigger types.

Take > , we build and ′ from and ′ by inserting -loops in and ′ without affecting their membership in using Lemma 4.5. Let = { 0 , ..., } be the set of -types such that there is a loop of -type in or in ′ . For each ∈ we fix a context as follows. Because ∈ there is a context in or ′ that is a loop of -type . For each ∈ , we fix arbitrarily such a and set as ⋅ . . . ⋅ , concatenations of the context . Notice that the path from the root of to its port is then bigger than . We now describe the construction of from . The construction of ′ from ′ is done similarly. The tree is constructed by simultaneously inserting, for all ∈ , a copy of the context at all nodes of of type . We now show that and ′ have the desired properties. The first and second properties, ∈ iff ∈ and ′ ∈ iff ′ ∈ , essentially follow from Lemma 4.5. We only show that ∈ iff ∈ , the second property is proved symmetrically. We view as if it was constructed from using a sequence of insertions of some context for ∈ . We write 0 , ..., the sequence of intermediate trees with 0 = and = . We call the context inserted to get +1 from . We show by induction on that (i) ≃ +1 and (ii) ∈ iff +1 ∈ . This will imply ∈ iff ∈ as desired. (i) is clear for = 0. We show that for all (i) implies (ii). Recall that is the concatenation of copies of a -loop present either in or in ′ . We suppose without generality that the -loop is present in . Let be the tree constructed from by duplicating the -loop times. Hence is a tree containing and by construction ≃ +1 . Because ≃ ′ with > + 1 and ≃ +1 we have ≃ +1 . By Lemma 4.5 this implies that +1 ∈ iff ∈ . By construction we also have +1 ≃ +1 and the induction step is proved.

We now show the third property:

Lemma 4.7. ≃ ′ Proof. We need to show that ≼ ′ , ′ ≼ and that the roots of and ′ have the same -type. It will be convenient for proving this to view the nodes of as the union of the nodes of plus some nodes coming from the -loops that were inserted. To do this more formally, if is a node of of -type not in , then is identified with the corresponding node of . If is a node of whose -type is in then is identified in with the port of the copy of that was inserted at node . We start with the following claim.

Claim 4.8. Take two nodes in and ′ in ′ , such that and ′ have the same -type. Let and ′ be the corresponding nodes in and ′ . Then and ′ have the same -type.

Proof. Let the -type of and ′ . Consider a branch of of length . By the choice of we know that in this branch one can find two nodes and ′ with the same -types , with an ancestor of ′ and such that the -type of is determined by ( is at distance ≥ from the leaves of ). Hence is in . Note that because the -type of is included in , the presence of a node of type induces the presence of a node of type at the same relative position than . Hence a copy of is inserted simultaneously at the same position relative to and ′ during the construction of and ′ . Because this is true for all branches of and because all have depth at least , then and ′ have the same -type.

From claim 4.8 it follows that the roots of and ′ have the same -type. By symmetry we only need to show that ≼ ′ . Let be a node of and be its -type. We show that there exists ′ ∈ ′ with type . We consider two cases:

• is not a node of a loop inserted during the construction of . Let be the corresponding position in and let be its -type. Since ≃ ′ , there is a node ′ of ′ of type . Let ′ be the node of ′ corresponding to ′ . By Claim 4.8 and ′ have the same -type.

• is a node inside a copy of inserted to construct . Let be the node of where this loop was inserted. Let be the -type of (the -type of is ). Since ≃ ′ , there is a node ′ of ′ of type . Since > , and ′ have the same -type, a copy of was also inserted in ′ at position ′ during the construction of ′ . From Claim 4.8, and ′ , when viewed as nodes of and ′ have the same -type. Let ′ be the node of ′ in the copy of inserted at ′ that corresponds to the position . Since and ′ are ancestors of and ′ that have the same -type, and since the context from to is the same as the context from ′ to ′ , then and ′ must have the same -type. This concludes the proof of Proposition 4.2.

Unranked trees

In this section we consider unranked unordered trees with labels in Σ. In such trees, each node may have an arbitrary number of children but no order is assumed on these children.

In particular even if a node has only two children we can not necessarily distinguish the left child from the right child.

Our goal is to adapt the result of the previous section and provide a decidable characterization of locally testable languages of unranked unordered trees.

In this section by regular language we mean definable in the logic MSO using only the child predicate and unary predicates for the labels of the nodes. There is also an equivalent automata model that we briefly describe next. A tree automaton over unordered unranked trees consists essentially of a finite set of states = { 1 , ⋅ ⋅ ⋅ , }, an integer denoted as the counter threshold in the sequel, and a transition function associating a unique state to any pair consisting of a label and a tuple ( 1 , 1 ) ⋅ ⋅ ⋅ ( , ) where ∈ {= | < } ∪ {≥ }. The meaning is straightforward via bottom-up evaluation: A node of label a get assigned a state if for all , the number of its children, up to threshold , that were assigned state is as specified by . In the sequel we assume without loss of generality that all our tree automata are deterministic.

In the unranked tree case, there are several natural definitions of LT. Recall the definition of -type: the -type of a node is the isomorphism type of the subtree induced by the descendants of at distance at most from . With unranked trees this definition generates infinitely many -types. We therefore introduce a more flexible notion of type, ( , )-type, based on one extra parameter restricting the horizontal information. It is defined by induction on . Consider an unordered tree and a node of . For = 0, the ( , )-type of is just the label of . For > 0 the ( , )-type of is the label of together with, for each ( -1, )-type, the number, up to threshold , of children of of this type. The reader can verify that over binary trees, the ( , 2)-type and the -type of always coincide. As in the previous section we say that two trees are ( , )-equivalent, and denote this using ≃ ( , ) , if they have the same occurrences of ( , )-types and their roots have the same ( , )-type. We also use ≼ ( , )

′ to denote the fact that all ( , )-types of also occur in ′ .

Based on this new notion of type, we define two notions of locally testable languages. The most expressive one, denoted ALT (A for Aperiodic), is defined as follows. A language is in ( , )-ALT if it is a union of ( , )-equivalence classes. A language is in ALT if there is a and a such that is in ( , )-ALT.

The second one, denoted ILT in the sequel (I for Idempotent), assumes = 1: A language is in ILT if there is a such that is a union of ( , 1)-equivalence classes.

The main result of this section is that we can decide membership for both ILT and ALT.

Theorem 5.1. It is decidable whether a regular unranked unordered tree language is ILT. It is decidable whether a regular unranked unordered tree language is ALT.

Tameness. The notion of -tame is defined as in Section 3 using the same -guarded operations requiring that the swapped nodes have identical -type. We also define a notion of ( , )-tame which corresponds to our new notion of ( , )-type. Consider the four operations of tameness defined in Section 3. A horizontal swap is said to be ( , )-guarded if and ′ have the same ( , )-type, a horizontal transfer is ( , )-guarded if , , have the same ( , )-type, a vertical swap is ( , )-guarded if , , have the same ( , )-type and a vertical stutter is ( , )-guarded if , , have the same ( , )-type. Let be a regular unranked unordered tree language and let be the counting threshold of the minimal automaton 5.1. Decision of ALT. We now turn to the proof of Theorem 5.1. We begin with the proof for as both the decision procedure and its proof are obtained as in the case of binary trees. Assuming tameness we obtain a bound on and such that a language is in ALT iff it is in ( , )-ALT. Once and are known, it is easy do decide if a language is ( , )-ALT since the number of such languages is finite. The bounds on and are obtained following the same proof structure as in the binary cases, essentially replacing -tame by ( , )-tame, but with several technical modifications. Therefore, we only sketch the proofs below and only detail the new technical material. Our goal is to prove the following result.

Proposition 5.5. Assume is a ( , )-tame regular tree language and let be its minimal automaton. Then is in ALT iff is in ( , )-ALT where and are computable from , and .

Notice that for each , the number of ( , )-types is finite, let , be this number. Proposition 5.5 is now a simple consequence of the following proposition.

Proposition 5.6. Let be a ( , )-tame regular tree language and let be the minimal automaton recognizing . Set = | | + 1 and = , + + 1. Then for all ′ > , all ′ > and any two trees , ′ if ≃ ( , ) ′ then there exists two trees , ′ with (1)

∈ iff ∈ (2) ′ ∈ iff ′ ∈ (3) ≃ ( ′ , ′ ) ′ .
Before proving Proposition 5.6 we adapt the extra terminology we used in the proof of Proposition 4.2 to the unranked setting. A non-empty context occurring in a tree is a loop of ( , )-type if the ( , )-type of its root and the ( , )-type of its port is . A non-empty context occurring in a tree is a ( , )-loop if there is some ( , )-type such that is a loop of ( , )-type . Given a context we call the path from the root of to its port the principal path of . Finally, the result of the insertion of a ( , )-loop at a node of a tree is a tree such that if = ⋅ | then = ⋅ ⋅ | . Typically an insertion will occur only when the ( , )-type of is and is a loop of ( , )-type . In this case the ( , )-types of the nodes initially from and of the nodes of are unchanged by this operation.

Proof of Proposition 5.6. Suppose that is ( , )-tame. As we did for the proof of the binary case we first prove two lemmas that are crucial for the construction of and ′ . They show that subtrees can be replaced and contexts can be inserted as long as this does not change the ( + 1, )-equivalence class of the tree. They are direct adaptations of the corresponding lemmas for the ranked setting: Lemmas 4.3 and 4.5. We start with subtrees.

Lemma 5.7. Assume is ( , )-tame. Let = be a tree where is a subtree of . Let ′ be another tree such that the roots of and ′ have the same ( , )-type.

If ≼ ( +1, ) and ′ ≼ ( +1, ) then ∈ iff ′ ∈ .

Proof sketch. As in the binary setting the proof is done by first proving a restricted version where ′ is actually another subtree of . Before doing that, we state a new claim, specific to the unranked setting, that will be useful later in the induction bases of our proofs. In the binary setting, two trees that had the same -type at their root and were of depth smaller than were equal. This obviously does not extend to unranked trees and ( , )types. However it is simple to see that equality can be replaced by indistinguishability by the minimal tree automaton recognizing .

Claim 5.8. Let be a tree automaton and be its counting threshold. Let and ′ be two trees of depth smaller than and whose roots have the same ( , )-type. Then and ′ evaluate to the same state of .

Proof. This is done by induction on . If = 0, and ′ are leaves, it follows from their (0, )-type that = ′ .

Otherwise we know that and ′ have the same ( , )-type at their root therefore they have the same root label. Let and ′ be two trees that are children of the root of or of ′ and have the same ( -1, )-type at their root. The depth of and ′ is smaller than -1, therefore by induction hypothesis and ′ evaluate to the same state of . Now, because the roots of and ′ have the same ( , )-type, for each ( -1, )-type , they have the same number of children of type up to threshold . From the previous remark this implies that for each state of , they have the same number of children in state up to threshold . It follows from the definition of that and ′ evaluate to the same state of .

We are now ready to state and prove the lemma in the restricted case.

Claim 5.9. Assume is ( , )-tame. Let be a tree and let , be two nodes of not related by the descendant relationship and with the same ( , )-type. We write = | , ′ = | and the context such that = . If ≼ ( +1, ) then ∈ iff ′ ∈ .

Proof sketch. This proof only differs from its binary tree counterpart Claim 4.4 in the details of the induction step. It is done by induction on the depth of . Assume first that is of depth less than . Since and have the same ( , )-type and since ≥ it follows from Claim 5.8 that and ′ evaluate to the same state on the automaton recognizing . Hence we can replace with ′ without affecting membership in .

Assume now that is of depth greater than . Let be the ( + 1, )-type of . We write 1 , ..., for the children of and the label of its root. Since ≼ ( +1, ) , there exists a node in of type . We write ′′ = | .

We now do a case analysis depending on the descendant relationships between , and . As for binary trees, all cases reduce to the case when and are not related by the descendant relationship by simple ( , )-tameness operations. Therefore we only consider this case here.

Assume that and are not related by the descendant relationship. We show only that ∈ iff ′′ ∈ . The proof that ′ ∈ iff ′′ ∈ is then done exactly as for binary trees.

Since and are of same ( + 1, )-type , the roots of ′ and ′′ have the same label . Let ′′ 1 , . . . , ′′ ′ be the children of the root of ′′ . As in the binary case we want to replace the trees 1 , . . . , with these children by induction since the depth of the trees 1 , . . . , is smaller than the depth of . Unfortunately for each ( , )-type , the number of trees whose root has type among the children of and among the children of might not be the same. However we know that in this case both numbers are greater than . We overcome this difficulty in two steps, first we modify the children of , without affecting membership in , so that if and have the same ( , )-type then = , then we use the fact that > in order to delete or duplicate children of until for each ( , )-type the number of trees of root of type among the children of and among the children of is the same. By definition of , this does not affect membership in . Finally we replace the by the ′′ by induction as in the binary case.

• ′ ∈ iff ′ 1 ∈ • 1 ≃ ( ′ , ) ′ 1
This construction is the same as in the binary tree setting so we only briefly describe it. Let = { 0 , ..., } be the set of ( , )-types such that there is a loop of ( , )-type in or in ′ . For each ∈ we fix a context as follows. Because ∈ there is a context in 1 or ′ 1 that is a loop of ( , )-type . For each ∈ , we fix arbitrarily such a and set as ⋅ . . . ⋅ ′ , ′ concatenations of the context . Notice that the path from the root of to its port is then bigger than ′ .

1 is constructed from as follows (the construction of ′ 1 from ′ is done similarly). The tree 1 is constructed by simultaneously inserting, for all ∈ , a copy of the context at all nodes of of type . By Lemma 5.10 it follows that ∈ iff 1 ∈ and ′ ∈ iff ′ 1 ∈ . Using the same proof as that of Proposition 4.2 for the binary tree setting, we obtain 1 ≃ ( ′ , ) ′ 1 . We now describe the construction of from 1 , the construction of ′ from ′ 1 is done similarly. It will be convenient for us to view the nodes of 1 as the union of the nodes of plus some extra nodes coming from the loops that were inserted.

Let be the maximum arity of a node of 1 or of ′ 1 . We duplicate subtrees in 1 and ′ 1 as follows. Let be a node of 1 , that is not in a loop we inserted when constructing 1 from . For each ( ′ -1, )-type , if has more than children of type we duplicate one of the corresponding subtrees until has exactly children of type in total. This is possible without affecting membership in because > | |. Indeed, because > | |, for at least one state of , there exists more than subtrees of of type for which assigns that state at their root, and by definition of any of these subtrees can be duplicated without affecting membership in . The tree is constructed from 1 by repeating this operation for any node of 1 coming from . By construction we have 1 ∈ iff ∈ and therefore ∈ iff ∈ . The same construction starting from ′ 1 yields a tree ′ such that ′ ∈ iff ′ ∈ .

We now show that ≃ ′ ′ , it follows that ≃ ( ′ , ′ ) ′ and this concludes the proof.

Lemma 5.11. ≃ ′ ′ Proof. We need to show that ≼ ′ ′ , ′ ≼ ′ and that the roots of and ′ have the same ′ -type.

Recall that in 1 we distinguished between two kinds of nodes, those coming from and those coming from the loops that were inserted during the construction of 1 from . We make the same distinction in by assuming that a node generated after a duplication gets the same kind as its original copy.

Recall the definition of and of for ∈ that was used for defining 1 and ′ 1 from and ′ . As for the binary tree case it suffices to show that for any node of coming from there is a node of ′ coming from ′ and having the same ′ -type. Hence the result follows from the claim below that is an adaptation of Claim 4.8. Claim 5.12. Take two nodes in and ′ in ′ , such that and ′ have the same ( , )type. Let and ′ be the corresponding nodes in and ′ . Then and ′ have the same ′ -type.

Proof. Let and ′ be two nodes of and ′ with the same ( , )-type. Let 1 and ′ 1 be the corresponding nodes in 1 and ′ 1 . The same proof as Claim 4.8 for the binary tree case shows that 1 and ′ 1 have the same ( ′ , )-type. Let be a child of . Let 1 be the node corresponding to in 1 . Notice now that the ( ′ , )-type of 1 in 1 is completely determined by the ( -1, )-type of in . Indeed, by choice of , during the construction of 1 , a loop of type ∈ will be inserted between and any descendant of at distance at most ( , ) -1 from . As > ( , ) + , the relative positions below where such a is inserted can be read from . As the depth of any is greater than ′ , from we can compute exactly the descendants of 1 in 1 up to depth ′ . Hence determines the ( ′ , )-type of 1 .

It follows that two children of 1 or of ′ 1 have the same ( ′ , )-types iff they had the same ( -1, )-types in or in ′ .

We now construct an isomorphism between the ′ -type of and the one of ′ . Let be the maximal distance between and a node that is a descendant of where a loop was inserted during the construction of from . We construct our isomorphism by induction on .

If = 0 then the ( , )-type of is in and as and ′ have the same ( ′ , )-type with ′ > , the ( , )-type of ′ is the same as the one of ′ . Therefore the subtrees rooted at and ′ are equal up to depth ′ as they all start with a copy of and we are done. Otherwise, as and ′ have the same ( ′ , )-type their roots must have the same labels. Consider now a ( ′ -1, )-type . By construction of and ′ , and ′ must have the same number of occurrences of children of type . Indeed from the type these numbers must match if one of them is smaller than and by construction they are equal to otherwise. Hence we have a bijection from the children of of type and the children of ′ of type . From the text above we know that the ( ′ , )-type of these nodes is determined by the ( -1, )-type of their copy in or in ′ . Because and ′ have the same ( , )-type, the corresponding ( -1, )-types are all equal and hence all the nodes of type actually have the same ( ′ , )-type. By induction they are isomorphic up to depth ′ and we are done.

From Claim 5.11 the lemma follows as in the proof of Lemma 4.7 for binary trees. This concludes the proof of Proposition 5.6.

Decision of ILT.

In the idempotent case we can completely characterize ILT using closure properties. We show that membership in ILT corresponds to tameness together with an extra closure property denoted horizontal stutter reflecting the idempotent behavior. A tree language is closed under horizontal stutter iff for any tree and any node of , replacing | with two copies of | does not affect membership in . Theorem 5.1 for ILT is a consequence of the following theorem.

Theorem 5.13. A regular unordered tree language is in ILT iff it is tame and closed under horizontal stutter.

Proof. It is simple to see that tameness and closure under horizontal stutter are necessary conditions. We prove that they are sufficient. Take a regular tree language and suppose that is tame and closed under horizontal stutter. Then there exists and such that is ( , )-tame. We show that if ≃ ( +1,1)

′ then ∈ iff ′ ∈ . It follows that is in ILT. We first show a simple lemma stating that if two trees contain the same ( + 1, 1)-types,

ℎ 1 ℎ 2 ′ ℎ 3 ∈ ≃ ′ / ∈ ℎ 1 ′ ℎ 2 ′ ℎ 3

Discussion

We have shown a decidable characterization for the class of locally testable regular tree languages both for ranked trees and unranked unordered trees.

Complexity. The decision procedure for deciding membership in LT as described in this paper requires a time which is a tower of several exponentials in the size of the deterministic minimal automaton recognizing . This is most likely not optimal. In comparison, over strings, membership in LT can be performed in polynomial time [START_REF] Pin | The expressive power of existential first order sentences of Büchi's sequential calculus[END_REF]. Essentially our procedure requires two steps. The first step shows that if a regular language is in LT then it is -locally testable for some computable from the minimal deterministic automaton recognizing . The obtained in Proposition 4.1 is doubly exponential in the size of . In comparison, over strings, this can be shown to be polynomial. For trees we did not manage to get a smaller but we have no example where even one exponential would be necessary.

Our second step tests whether is -locally testable once is fixed. This was easy to do using a brute force algorithm requiring several exponentials in . It is likely that this can be optimized but we didn't investigate this direction.

However for unranked unordered trees we have seen in Theorem 5.13 that in the case of ILT it is enough to test for tameness. The naive procedure for deciding tameness is exponential in the size of . But the techniques presented in [START_REF] Benedikt | Regular languages definable in FO and FOmod[END_REF] for the case of LTT, easily extend to the closure properties of tameness, and provide an algorithm running in time polynomial in the size of . Hence membership in ILT can be tested in time polynomial in the size of the minimal deterministic bottom-up tree automaton recognizing the language.

Logical characterization. There is a logical characterization of languages that are locally testable. It corresponds to those languages definable by formulas containing the temporal predicates G and X where G stands for "everywhere in the tree" while X stands for "child". In the binary tree case, we also require two predicates distinguishing the left child from the right child. In the unranked unordered setting the logic above is closed under bisimulation and therefore corresponds to ILT. This shows that in a sense ILT is the natural extension of LT to the unranked setting.

Open problem. It would be interesting to obtain a different characterization of LT based on a finite number of conditions such as the ones characterizing tameness. This would be a more satisfying result and would most likely provide a more efficient algorithm for deciding LT.

Figure 1 :

 1 Figure 1: Horizontal Swap (left) and Horizontal Transfer (right)

Figure 2 :

 2 Figure 2: Vertical Swap (left) and Vertical Stutter (right)

  If and are not related by the descendant relation, then , and have the same -type and ′′ | = ′′ | . We use -guarded horizontal transfer to replace ′′ | with ′′ | as depicted below.

Figure 3 :

 3 Figure 3: The construction of 2 , eliminating the context between -1 and

Figure 4 :

 4 Figure 4: Bringing copies of the -loop ′ together in Claim 4.6

Figure 5 :

 5 Figure 5: Relation with 2

recognizing , we say that is ( , )-tame iff it is closed under ( , )-guarded horizontal swap, horizontal transfer, vertical swap and vertical stutter and > (we assume > in order to make the statements of the results similar to those used in the binary setting). We first prove that over unordered trees being -tame is the same as being ( , )-tame.

Proposition 5.2. Let be an unordered unranked regular tree language, then for all integers , is -tame iff there exists such that is ( , )-tame. Furthermore, such an can be computed from any automaton recognizing .

Proof. If there exists such that is ( , )-tame then is obviously -tame. Suppose that is -tame, and let be the counting threshold of the minimal automaton recognizing . We show that there exists ′ such that is closed under ( , ′ )-guarded operations. This implies the result as one can then take = ( + 1, ′ ). We need to show that is closed under ( , ′ )-guarded vertical swap, vertical stutter, horizontal swap and horizontal transfer. The proof is similar to the proof of Proposition 1 in [START_REF] Benedikt | Regular languages definable in FO and FOmod[END_REF]. We will use the following claim which is proved in [BS10] using a simple pumping argument:

Claim 5.3. [BS10] For every tree automaton there is a number ′ , computable from , such that for every if a tree 1 is ( , ′ )-equivalent to a tree 2 , then there are trees ′ 1 , ′

2

with ′ 1 and ′ 2 -equivalent such that reaches the same state on ′ as on for = 1, 2. We use this claim to prove that is closed under horizontal transfer. Let ′ be the number computed from by Claim 5.3. We prove that is closed under ( , ′ )-guarded horizontal transfer. Consider a tree and three nodes , , of not related by the descendant relationship and such that | = | and such that , and have the same ( , ′ )-type. Let ′ be the horizontal transfer of at , , . Let 1 = | and 2 = | and ′ 1 , ′ 2 obtained from 1 , 2 using Claim 5.3. Let be the tree obtained from by replacing | and | with ′ 1 and | with ′ 2 , and let ′ be the tree obtained from ′ by replacing ′ | with ′ 1 and ′ | and ′ | with 2 . From Claim 5.3 it follows that ∈ iff ∈ and ′ ∈ iff ′ ∈ . Since is -tame, it is closed under -guarded horizontal transfer, therefore we have ∈ iff ′ ∈ , it follows that ∈ iff ′ ∈ .

The closure under horizontal swap is proved using the same claim. The proofs for vertical swap and vertical stutter uses a claim similar to Claim 5.3 but for contexts: For every tree automaton there is a number computable from such that for every if the context 1 is ( , )-equivalent to the context 2 (by this we mean that their roots have the same ( , )-type), then there are contexts ′ 1 , ′ 2 with ′ 1 -equivalent to ′ 2 such that ′ induces the same function on the states of as for = 1, 2.

From this lemma we know that a regular language over unranked unordered trees is tame iff it is -tame for some iff it is ( , )-tame for some , . Moreover, as in the binary setting, if a regular language is tame then it is ( , )-tame for some and computable from an automaton recognizing . The bound on can be obtained by a straightforward adaptation of Proposition 3.2. The bound on then follows from Proposition 5.2. Hence we have: Proposition 5.4. Let be a regular language and let be its minimal deterministic bottomup tree automaton, we have is tame iff is ( 0 , 0 )-tame for 0 = | | 3 + 1 and some 0 computable from .

For the first step notice that any of the is by definition of depth smaller than therefore by the induction hypothesis we can replace it with any of its siblings having the same ( , )-type at its root without affecting membership in .

We now turn to the proof of Lemma 5.7 in its general statement. The proof is done by induction on the depth of ′ . The idea is to replace with ′ node by node.

Assume first that ′ is of depth smaller than . Then because the ( , )-types of the roots of and ′ are the same we are in the hypothesis of Claim 5.8 and it follows that and ′ evaluate to the same state of . The result follows.

Assume now that ′ is of depth greater than . Let be the node of corresponding to the root of . Let be the ( + 1, )-type of the root of ′ . In the binary tree case we used a sequence of tame operations to reduce the problem to the case where has ( + 1, )-type . Using the same operations we can also reduce the problem to this case in the unranked setting. Then we use the induction hypothesis to replace the children of by the children of the root of ′ . As in the proof of Claim 5.9, the problem is that the number of children might not match but this is solved exactly as in the proof of Claim 5.9.

As in the binary tree case, we now prove a result similar to Lemma 5.9 but for ( , )loops.

Lemma 5.10. Assume is ( , )-tame. Let be a tree and a node of of ( , )-type . Let ′ be another tree such that ≃ ( +1, )

′ and be a ( , )-loop of type in ′ . Consider the tree constructed from by inserting a copy of at . Then ∈ iff ∈ .

Proof sketch. The proof is done using the same structure as Lemma 4.5 for the binary case. First we use the ( , )-tame property of to show that we can insert a ( , )-loop ′ at in such that the principal path of is the same as the principal path of ′ . By this we mean that there is a bijection from the principal path of ′ to the principal path of that preserves the child relation and ( + 1, )-types. In a second step we replace one by one the subtrees hanging from the principal path of ′ with the corresponding subtrees in .

Let ′ be the tree resulting from inserting ′ at position . We do not detail the first step as it is done using exactly the same sequence of tame operations we used for this step in the proof of Lemma 4.5. This yields: ∈ iff ′ ∈ . We turn to the second step showing that ′ ∈ iff ∈ .

By construction of ′ we have ′ ≼ ( +1, ) . Consider now a node ′ in the principal path of ′ and the corresponding node in . As in the binary tree case we replace the subtrees branching out of the principal path of ′ with the corresponding trees branching out of the principal path of using Lemma 5.7. As in the previous proof, the problem is that the numbers of children might not match. This is solved exactly as in the proof of Lemma 5.7.

We now turn to the construction of and ′ and prove Proposition 5.6. The construction is similar to the one we did in the binary tree case. We insert ( , )loops in and ′ using Lemma 5.10 for obtaining bigger types. However inserting loops only affects the depth of the types. Therefore we need to do extra work in order to also increase the width of the types.

Assuming ≃ ( , ) ′ we first construct two intermediate trees 1 and ′ 1 that have the following properties:

• ∈ iff 1 ∈ then we can pump them without affecting membership in into two trees that contain the same ( + 1, )-types.

Lemma 5.14. Let closed under horizontal stutter and let and ′ two trees such that ≃ ( +1,1)

′ . Then there exist two trees and ′ such that:

′

Proof. is constructed from via a bottom-up procedure. Let be a node of . For each subtree rooted at a child of , we duplicate it times using horizontal stutter. This does not affect membership in . After performing this for all nodes of we obtain a tree with the desired properties.

Let and ′ be constructed from and ′ using Lemma 5.14. Let 1 , . . . , the children of the root of and ′ 1 , . . . , ′ ′ the children of the root of ′ . Let ′′ be the tree whose root is the same as and ′ and whose children is the sequence of trees 1 , . . . , , ′ 1 , . . . , ′ ′ . We show that ′′ ∈ iff ∈ and ′′ ∈ iff ′ ∈ . It will follow that ∈ iff ′ ∈ and by Lemma 5.14 that ∈ iff ′ ∈ which ends the proof.

To show that ′′ ∈ iff ∈ we use horizontal stutter and Lemma 5.7. As the roots of and ′ have the same ( + 1, )-type, for each ′ , there exists a tree such that its root has the same ( , )-type as ′ . Fix such a pair ( , ). Let be the tree obtained by duplicating in . By closure under horizontal stutter ∈ iff ∈ . But now = for some context such that ≼ ( +1, ) . Altogether we have that: the roots of ′ and have the same ( , )-type (by choice if and ), ′ ≼ ( +1, )

(as ′ ≼ ( +1, ) ′ and ≃ ( +1, ) ′ ) and ≼ ( +1, ) (as is part of hence of ). We can therefore apply Lemma 5.7 and ′ ∈ iff ∈ . Repeating this argument for all eventually yields the tree ′′ . This proves that ′′ ∈ iff ∈ . By symmetry we also have ′′ ∈ iff ′ ∈ which concludes the proof.

Tameness is not sufficient

Over strings tameness characterizes exactly LT as vertical swap and vertical stutter are exactly the extensions to trees of the known equations for LT (recall Section 2). Over trees this is no longer the case. In this section we provide an example of a language that is tame but not . For simplifying the presentation we assume that nodes may have between 0 and three children; this can easily be turned into a binary tree language. All trees in our language have the same structure consisting of a root of label a from which exactly three sequences of nodes with only one child (strings) are attached. The trees in have therefore exactly three leaves, and those must have three distinct labels among {h 1 , h 2 , h 3 }. The labels of two of the branches, not including the root and the leaf, must form a sequence in the language b * cd * . The third branch must form a sequence in the language b * c'd * . We assume that b, c, c' and d are distinct labels. Note that the language does not specify which leaf label among {h 1 , h 2 , h 3 } is attached to the branch containing c'.

The reader can verify that is 1-tame. We show that is not in LT. For all integer , the two trees and ′ depicted below are such that ∈ , ′ / ∈ , while ≃ ′ .


Mehri Houda
email: mehri.houda@enim.rnu.tn

D Taoufik
email: djemal.taoufik@fsegs.rnu.tn

QUEUES IN CINEMAS

Queues in Tunisia

Not only all cinemas have their operating cost, they do have to bear the cost of keeping customers waiting because impatient customers may turn away and go to competitors' hands.so cinema operators have to minimize the sum of the operating cost and the waiting cost in order to maintain their competitiveness in the industry.

Although queuing is unavoidable, technology followers are getting ways to reduce queuing time. Consequently, the company images of the cinema operators will be enhanced and the proportion of balking and reneging customers will be lowered. The way to have less queuing time is achieved by means of computerizing the ticketing system. Because of the inherent inflexibility of pre-printed tickets used in the traditional manual ticketing system, the manual method cannot provide emergency facilities (to open additional ticket selling counters) to relieve heavy demand from sudden inflows of customers; mainly occur on weekends or public holidays. By computerization, the tickets are printed after customers' confirmation of the bookings. Therefore there are no limitations on opening additional ticket selling counters. The resulting strategy is to open additional ticket selling counters during rush periods in order to shorten customers' queuing time.

Besides, the computerized ticketing system also fulfils the increasing reporting requirements by management. The data captured at the point of sales provide a very resourceful database. Management information can be requested any time to reflect the most current situation of the cinema operation.

Both the single channel and the multiple channels queuing models are discussed to illustrate queuing conditions in cinema ticketing. By appropriate queue design, queuing can be a pleasant waiting environment that is acceptable to the customers. Keywords: Service; FIFO; M/M/s; Poisson distribution; Queue ; Service cost; Unlimited or Infinite Population ; Utilisation Factor; Waiting cost ; Waiting Time, Landing, agents , the approach control, estimated time of arrival .

Introduction:

When "JCI" was on show in Tunisia, long queues were seen to appear in every cinema that showed film. Cinema operators were glad to see those long waiting lines. However, most of them were unable to serve the queues faster due to the inflexibility created by the pre-printed tickets (under the traditional manual ticketing system). Impatient audience had given up waiting and left the queues. They were dissatisfied of the services provided by the cinemas.

Queues in cinemas arise because of the sudden arrival of customers while the service processes are comparatively steady. There is not only a cost associated with providing service, but also a cost associated with keeping customers waiting ( impatient customers may turn away). So it will be a cost minimization problem for the cinema operators. While many cinema operators who use the pre-printed tickets system are unable to reduce the total of service cost and waiting cost; some are taking advantages of computer technology which allow opening of additional service counters during rush periods to capture additional revenue at a much lesser marginal cost.

Film watching is one of the most favourite means of entertainment in Tunisia, especially during the hot summer. People enjoy the air-conditioned environment inside the cinemas.

Besides, film producers are so creative that bring in all sorts of technological, situational, historical or imaginative stories to the audience at a relatively low price of 5 DT ( average estimate of all cinemas) only. However, the box office takings in the past 2 years have been declining.

One may argue, the per capita attendance rate is not an appropriate measure of the attractiveness of films because films are divided into 3 categories that have different age groups of audience. But an audience's attendance to a film or not is a very complicated matter which takes into consideration the quality of the film (e.g. script story of the film, status of the producer, status of the director, who are the cast, amount of the production cost, etc.), the showing season (whether it is shown during long public holidays or during normal weekdays), and the comments on the film by the media and those people who have watched the film. The per capita attendance rate thus gives us a general indication of the overall acceptance of the film by the audience.

One of the reasons for the drop in box office takings is due to the early release of films in the forms of video tapes and laser disc, especially those illegal copies. In recent years, film producers are keen to market the video tape and laser disc formats just after the end of the he movies. People have to wait for only 6 months after the end of the first run of a movie in the cinemas, then they can rent/buy the movie in the form of video tape/laser disc. The situation is even worsened by those copy cats who record films by using video cameras during prereleases or mid-night shows. Therefore, people may wait till the release of these much cheaper media ( 1DT -3 DT) and then hire them for home entertainment by all family members, instead of paying 5 DT per person in the cinemas.

Another reason for the drop in box office takings is because of the increasing acceptance of cable TV in Tunisia. Cable Cineplex, a product introduced by Wharf Cable TV, brings to TV subscribers a reality cinema at home. On a yearly basis, 500-600 movies will be shown, which are double the numbers screened at cinemas in Tunisia. People can enjoy their favourite movies at home, any times (if they pre-set recording of the movies).

Nevertheless, queues are still found in cinemas when there is a superb film on show, or when it is weekend/public holidays, especially JCI.

CHAPTER 1 CRITERIA OF SERVICE LEVEL IN CINEMA TICKETING

Although audience the cinema environment, they dislike waiting for a long time to buy tickets, despite Tunisian people have accustomed to wait since they were born (e.g. waiting for bus, waiting at clinic, and waiting for school admission, etc.). if they can be served better (i.e. with less waiting time), they are more satisfied with the money they have spent on the tickets.