Arnaud Carayol

Christof Loeding

Damian Niwinski

Igor Walukiewicz

Damian Niwiński

Choice functions

published or not. The documents may come

Introduction

The main goal of this paper is to present a simple proof for the fact (first shown by Gurevich and Shelah in [START_REF] Gurevich | Rabin's uniformization problem[END_REF]) that there is no MSO-definable choice function on the infinite binary tree t 2 . A choice function on t 2 is a mapping assigning to each nonempty set of nodes of t 2 one element from this set, i.e., the function chooses for each set one of its elements. Such a function is MSO-definable if there is an MSO-formula with one free set variable X and one free element variable x such that when X is interpreted as a nonempty set U then there is exactly one possible interpretation u ∈ U for x making the formula satisfied.

The question of the existence of an MSO-definable choice function over the infinite binary tree can be seen as a special instance of the more general uniformization problem, which asks, given a relation that is defined by a formula with free variables, whether it is possible to define by another formula a function that is compatible with this relation. More precisely, given a formula φ(X, Y ) with vectors X, Y of free variables, such that the formula ∀X∃Y φ(X, Y ) is true over the infinite binary tree, uniformization asks for a formula φ * (X, Y ) such that 1. φ * implies φ (each interpretation of X, Y making φ * true also makes φ true), 2. and φ * defines a function in the sense that for each interpretation of X there is exactly one interpretation of Y making φ * true.

The question of the existence of a choice function is the uniformization problem for the formula φ(X, Y ) := X = ∅ → (Y is a singleton ∧ Y ⊆ X).

The infinite line, i.e., the structure consisting of natural numbers equipped with the successor relation, is known to have the uniformization property for MSO [START_REF] Siefkes | The recursive sets in certain monadic second order fragments of arithmetic[END_REF], even when adding unary predicates [START_REF] Rabinovich | On decidability of monadic logic of order over the naturals extended by monadic predicates[END_REF]. On the infinite binary tree MSO is known to be decidable [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF] but it does not have the uniformization property. This was conjectured in [START_REF] Siefkes | The recursive sets in certain monadic second order fragments of arithmetic[END_REF] and proved in [START_REF] Gurevich | Rabin's uniformization problem[END_REF] where it is shown that there is no MSO-definable choice function on the infinite binary tree. The proof in [START_REF] Gurevich | Rabin's uniformization problem[END_REF] uses complex set theoretical arguments, whereas it appears that the result can be obtained by much more basic techniques. We show that this is indeed true and present a proof that only relies on the equivalence of MSO and automata over infinite trees and otherwise only uses basic techniques from automata theory. Besides its simplicity, another advantage of the proof is that we provide a concrete family of sets (parametrized by natural numbers) such that each formula fails to make a choice for those sets with the parameters chosen big enough. We use this fact when we discuss two applications of the result.

At first, we show an example of a tree game with an MSO-definable winning condition, where the winner has no MSO-definable winning strategy. The second application concerns the existence of inherently ambiguous tree languages. An unambiguous automaton is an automaton which has exactly one accepting run on every tree it accepts. On finite words and trees it is clear that every regular language can be accepted by an unambiguous automaton because deterministic automata are unambiguous. The regular languages of infinite words are accepted by unambiguous Büchi automata [START_REF] Arnold | Rational ω-languages are non-ambiguous[END_REF]. For regular languages of infinite trees, we show that the language of infinite trees labeled by {0, 1} having at least one node labeled by 1 is not accepted by any unambiguous parity tree automaton. Using the counter-example sets introduced previously, we strengthen this result by giving a regular tree language and a tree in this language such that any automaton accepting the language has at least two accepting runs on the tree.

The subject of MSO-definability of choice functions on trees has been studied in more depth in [START_REF] Lifsches | Uniformization, choice functions and well orders in the class of trees[END_REF], where the authors consider more general trees and not only the infinite binary tree. They show the following dichotomy: for a tree it is either not possible to define a choice function in MSO even with additional predicates, or it is possible to define a well-ordering on the domain of the tree with additional predicates.

Note that it is very easy to define a choice function if one has access to a well-ordering of the domain: for each set one chooses the minimal element according to the well-ordering. The same result remains true if we only have access to a partial well-ordering: we pick the left-most element of the finite set of minimal elements instead of the minimal element. The non-existence of an MSO-definable choice function on the infinite binary tree implies that there is no MSO-definable partial well-ordering on the infinite binary tree. We strengthen this result by showing that extending the infinite binary tree by any partial well-ordering leads to a structure with an undecidable MSO-theory. As a consequence we obtain that each structure in which we can MSO-define a partial well-ordering and MSO-interpret the infinite binary tree must have an undecidable MSO-theory.

The paper is structured as follows. In Section 2 we introduce notations and basic results for automata on infinite trees and monadic second-order logic. The proof of the undefinability of choice functions over the infinite binary tree is presented in Section 3, where we also discuss the first application concerning the definability of winning strategies in infinite games. In Section 4 we prove that there are regular languages of infinite trees that are inherently unambiguous. Section 5 is on the undecidability of the monadic second-order theory of the infinite binary tree extended with a partial well-ordering. We conclude in Section 6 and give some possible directions of future research.

This paper is a full version of the conference publication [START_REF] Carayol | MSO on the infinite binary tree: Choice and order[END_REF].

Preliminaries

In this section we first introduce some general notations and then give some background on automata and logic.

The set of natural numbers (non-negative integers) is denoted by N. A finite interval {i, . . . , j} of natural numbers is written as [i, j].

An alphabet is a finite set of symbols, called letters. Usually, alphabets are denoted by Σ. The set of finite words over Σ is written as Σ * and the set of infinite words as Σ ω . The length of a finite word w ∈ Σ * is denoted by |w| and ε is the empty word.

For all words

w 1 , w 2 ∈ Σ * , w 1 is a prefix of w 2 (written w 1 ⊑ w 2 ) if there exists w ∈ Σ * such that w 2 = w 1 w. If w ∈ Σ + then w 1 is a strict prefix of w 2 (written w 1 ⊏ w 2 ).
The greatest common prefix of two words w 1 and w 2 (written w 1 ∧ w 2 ) is the longest word which is a prefix of w 1 and w 2 .

Automata on infinite trees

We view the set {0, 1} * of finite words over {0, 1} as the domain of an infinite binary tree. The root is the empty word ε, and for a node u ∈ {0, 1} * we call u0 its left successor (or 0-successor), and u1 its right successor (or 1-successor). A branch π is an infinite sequence u 0 , u 1 , u 2 . . . of successive nodes starting with the root, i.e., u 0 = ε and u i+1 = u i 0 or u i+1 = u i 1 for all i ≥ 0.

An (infinite binary) tree labeled by a finite alphabet Σ is a mapping t : {0, 1} * → Σ. We denote by T ω Σ the set of all trees labeled by Σ. In a tree t, a branch π induces an infinite sequence of labels in Σ ω . We sometimes identify a branch with this infinite word. It should always be clear from the context to which meaning of a branch we are referring to.

In connection with logic, the labels of the infinite tree are used to represent interpretations of set variables. This motivates the following definitions. For a set U ⊆ {0, 1} * , we write t[U ] ∈ T ω {0,1} for the characteristic tree of U , i.e., the tree which labels all nodes in U with 1 and all the other nodes with 0. This notation is extended to the case of several sets. The characteristic tree of U 1 , . . . , U n ⊆ {0, 1} * is the tree labeled by {0, 1} n written t[U 1 , . . . , U n ] and defined for all u ∈ {0, We now turn to the definition of automata for infinite trees. A parity tree automaton (PTA) on Σ-labeled trees is a tuple A = (Q, Σ, q i , ∆, c) with a finite set Q of states, an initial state

1} * by t[U 1 , . . . , U n ](u) := (b 1 , . . . , b n ) where for all i ∈ [1, n], b i = 1 if u ∈ U i
q i ∈ Q, a transition relation ∆ ⊆ Q × Σ × Q × Q, and a priority function c : Q → N. A run of A on a tree t ∈ T ω Σ from a state q ∈ Q is a tree ρ ∈ T ω
Q such that ρ(ε) = q, and for each u ∈ {0, 1} * we have (ρ(u), t(u), ρ(u0), ρ(u1)) ∈ ∆. We say that ρ is accepting if the parity condition is satisfied on each branch of the run, i.e., on each branch the minimal priority appearing infinitely often is even. If we only speak of a run of A without specifying the state at the root, we implicitly refer to a run from q i . A tree t is accepted by A if there is an accepting run of A on t. The language recognized by A is the set of all accepted trees:

T (A) = {t ∈ T ω Σ | t accepted by A}.
A tree language is called regular if it is recognized by some PTA.

For two trees t and t ′ we say that they are A-equivalent, written as t ≡ A t ′ , if for each state q of A there is an accepting run from q on t if and only if there is an accepting run from q on t ′ . Intuitively, this means that A cannot distinguish the two trees.

Monadic second-order logic

A signature is a ranked set τ of symbols, where for all R ∈ τ , |R| denotes the arity (which is ≥ 1) of the symbol R. A relational structure S over τ is given by a tuple (D, (R S ) R∈τ ) where D is the domain (or the universe) of S and where for all R ∈ τ , R S (which is also called the interpretation of R in S) is a subset of D |R| . When S is clear from the context, we simply write R instead of R S .

We use ∼ = to denote that two structures are isomorphic. Usually, we do not distinguish isomorphic structures but sometimes we refer to different representations of structures over specific domains, and in these cases we use ∼ = instead of =.

To every tree t labeled by Σ = {a 1 , . . . , a n }, we associate a canonical structure over the signature {E 0 , E 1 , P a1 , . . . , P an } where E 0 and E 1 are binary symbols and the P ai are predicates, i.e., unary symbols. The universe of this structure is {0, 1} * . The symbols E 0 and E 1 are respectively interpreted as

{(w, w0) | w ∈ {0, 1} * } and {(w, w1) | w ∈ {0, 1} * }. Finally for all i ∈ [1, n], P ai is interpreted as {u ∈ Σ * | t(u) = a i }.
In the following, we do not distinguish between a tree and its canonical relational structure.

The unlabeled binary tree, i.e., the structure ({0, 1} * , {E 0 , E 1 }) with the above interpretation of E 0 and E 1 is denoted by t 2 . The structure with N as domain and the successor relation on N can be viewed as a tree with unary branching. Hence we denote it by t 1 .

We are mainly interested in monadic second-order logic (MSO) over relational structures with the standard syntax and semantics (see e.g. [START_REF] Ebbinghaus | Finite Model Theory[END_REF] for a detailed presentation). MSO-formulas use first-order variables, which are interpreted by elements of the structure, and monadic second-order variables, which are interpreted as sets of elements. First-order variables are usually denoted by lower case letters (e.g. x, y), and monadic second-order variables are denoted by capital letters (e.g. X, Y ). First-order logic (FO) is the fragment of MSO that does not use quantifications over set variables. Atomic MSO-formulas are of the form • R(x 1 , . . . , x |R| ) for a relation symbol R from the signature and first-order variables x 1 , . . . , x |R| , or

• x = y, X = Y , or x ∈ X for first-order variables x, y, and monadic second-order variables X, Y with the obvious semantics. Complex formulas are built as usual from atomic ones by the use of boolean connectives, and quantification. We write φ(X 1 , . . . , X n , y 1 , . . . , y m ) to indicate that the free variables of the formula φ are among X 1 , . . . , X n (monadic second-order) and y 1 , . . . , y m (firstorder) respectively. A formula without free variables is called a sentence.

For a relational structure S and a sentence φ, we write S |= φ if S satisfies the formula φ. The MSO-theory of S is the set of sentences satisfied by S. For every formula φ(X 1 , . . . , X n , y 1 , . . . , y m ), all subsets U 1 , . . . , U n of the universe of S and all elements v 1 , . . . , v m of the universe of S, we write S |= φ[U 1 , . . . , U n , v 1 , . . . , v m ] to express that φ holds in S when X i is interpreted as U i for all i ∈ [1, n] and y j is interpreted as v j for all j ∈ [1, m].

Given a structure S, we calla relation R ⊆ D n , for some n ≥ 1, MSOdefinable in S if there is an MSO-formula φ(x 1 , . . . , x n ) with n free first-order variables such that (u 1 , . . . ,

u n ) ∈ R iff S |= φ[u 1 , . . . , u n ].
A single element u of a structure is MSO-definable if so is the unary relation {u}, i.e., if there is a formula φ(x) such that u is the only element with S |= φ[u].

We are particularly interested in MSO logic over the infinite binary tree t 2 , which we refer to as MSO[t 2 ]. The MSO-theory of the infinite binary tree t 2 is also referred to as S2S, the second-order theory of two successors [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. Correspondingly, we refer to the MSO-theory of t 1 , the natural numbers with successor, as S1S [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF].

An MSO[t 2 ]-formula φ(X 1 , . . . , X n ) with n free variables defines a tree language T (φ) ⊆ T ω {0,1} n as follows:

T (φ) = {t[U 1 , . . . , U n ] | t 2 |= φ[U 1 , . . . , U n ]}.
It is often convenient to consider the binary tree t 2 along with a sequence of sets U 1 , . A theorem of Rabin states that the tree languages definable by MSO[t 2 ]formulas are precisely those that can be accepted by tree automata [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. An analogous fact for MSO[t 1 ]-definable languages of infinite words (also called ωregular) was proved previously by Büchi [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF]. The acceptance condition used by Rabin in [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] differs from the parity condition but it can be transformed into a parity condition (see e.g. [START_REF] Thomas | Languages, automata, and logic[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games[END_REF]). Parity tree automata have first been used in [START_REF] Mostowski | Regular expressions for infinite trees and a standard form of automata[END_REF] where they are shown to be equivalent to the automata used in [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF].

We state here the difficult direction of the theorem, the proof of which is based on the closure properties of PTAs.

Theorem 2.1 ( [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF][START_REF] Mostowski | Regular expressions for infinite trees and a standard form of automata[END_REF]) For every MSO[t 2 ]-formula φ(X 1 , . . . , X n ) there is a parity tree automaton A φ such that T (A φ ) = T (φ). This result can be used to show the decidability of the satisfiability problem for MSO[t 2 ], i.e., the question whether for a given MSO[t 2 ] formula there is an interpretation of the free variables such that the formula is satisfied in t 2 . Furthermore, one can even construct a satisfying assignment:

Theorem 2.2 ([20]) Let φ(X 1 , . . . , X n ) be a satisfiable MSO[t 2 ]-formula. There are regular sets U 1 , . . . , U n such that t 2 [U 1 , . . . , U n ] |= φ.
Above we have introduced the notion of MSO-definability. We conclude from Theorem 2.2 that on t 2 each MSO-definable set is regular: Starting from a formula φ(x) defining a set, we construct the formula φ ′ (X) = ∀x. x ∈ X ↔ φ(x).

Then there is exactly one set satisfying φ ′ and this set is regular according to Theorem 2.2. Conversely, each regular set can be defined in MSO by describing an accepting run of the DFA defining the set.

Proposition 2.3 A set U ⊆ {0, 1} * is definable in MSO[t 2 ] iff it is regular.
As a consequence we can add regular predicates to t 2 without affecting the decidability result for MSO. An MSO-formula having access to regular predicates P 1 , . . . , P n can be turned in a standard MSO-formula over t 2 by using formulas φ P1 , . . . , φ Pn defining these predicates.

The notion of interpretation that is introduced in the following generalizes this idea.

Let τ and τ be two signatures. An MSO-interpretation from τ -structures to τ -structures is given as a list I = φ dom , (φ R) R∈τ of MSO-formulas over the signature τ . The formula φ dom has one free first-order variable and is called the domain formula. For each R ∈ τ the formula φ R has | R| many free first-order variables.

Applied to a τ -structure S = (D, (R S ) R∈τ ), the interpretation defines a τstructure I(S) = ( D, ( RI(S) ) R∈τ ), where the domain formula defines the domain of the new structure (all elements of S satisfying φ dom ), and the formulas φ R define the relations of I(S):

• D = {u ∈ D | S |= φ dom [u]}, • RI(S) = {(u 1 , . . . , u | R| ) ∈ D| R| | S |= φ R[u 1 , . . . , u n ]}.
Now assume that we are given an MSO-formula over I(S) and we want to know whether it is satisfiable in I(S). We can replace each atomic formula R(x 1 , . . . , x | R| ) by its definition φ R(x 1 , . . . , x n ), and restrict the range of all variables to the set D defined by φ dom . In this way we obtain an MSO-formula over S that is satisfiable in S iff the original formula is satisfiable in I(S). Applying this technique to MSO-sentences (without free variables), we can transfer the decidability of the MSO-theory as stated in the following proposition.

Proposition 2.4 If I is an MSO-interpretation and if the MSO-theory of S is decidable, then the MSO-theory of I(S) is decidable.

MSO-definable choice functions

As already described in the introduction, an MSO-definable choice function is given by an MSO-formula φ(X, x) such that: for every non-emptyset U , there is precisely one u ∈ U such that

t 2 |= φ[U, u].
This section is devoted to the proof of the following theorem of Gurevich and Shelah.

Theorem 3.1 ([11]

) There is no MSO-definable choice function on the infinite binary tree.

The technical formulation of the result we prove is given in Theorem 3.5 (on page 12), where we concretely provide counter examples for which a given formula cannot choose a unique element. As a machinery for the proof we use tree automata, that are easier to manipulate (at least for our purpose) than formulas. In the following we present a slight modification of the standard automaton model that we use in the proof.

An MSO[t 2 ]-formula with free variables defines a relation between subsets of {0, 1} * . In this section we consider formulas with two free variables, and a natural view in the context of choice functions is that the first variable represents the input, and the second variable represents the output. A choice function is the special case that the second variable is an element and not a set, and that for each nonempty input set there is a unique output which is inside the input set. To adapt this general view of inputs and outputs on the automata theoretic level we introduce automata with output, called transducers. These transducers are very simple: An output symbol is associated to each transition, which gives a natural correspondence between runs and output trees.

A parity tree automaton with output is a tuple A = (Q, Σ, q i , ∆, c, λ), where (Q, Σ, q i , ∆, c) is a standard PTA, and λ : ∆ → Γ is an output function assigning to each transition a symbol from the output alphabet Γ. When ignoring the output function we can use the terminology of standard PTAs, in particular the notion of accepting run and the notion of A-equivalence (see page 4).

In general, a PTA with output defines for each input tree t ∈ T ω Σ a set of output trees A(t) ⊆ T ω Γ defined by

A(t) = {λ(ρ) | ρ is an accepting run of A on t},
where λ(ρ) denotes the tree in T ω Γ that is obtained by taking at each node u the output produced by λ applied to the transition used at u in ρ.

As already indicated above we are interested in such transducers for representing formulas with two free variables, i.e., the input and the output alphabets are both equal to {0, 1}. The following theorem can easily be shown by a simple argument based on Theorem 2.1.

Theorem 3.2 For each MSO[t 2 ]-formula φ(X, Y ) there is a PTA with output A φ such that t 2 [U, U ′ ] |= φ iff t 2 [U ′ ] ∈ A(t 2 [U ]).
We are interested in PTAs with output that represent possible candidates for choice formulas. i.e., the case where the second free variable of the formula represents a single element. This motivates the following definition.

A weak choice automaton is a PTA with output such that the input and the output alphabet are equal to {0, 1}, and for each U ⊆ {0, 1} * there is at most one output tree in A(t 2 [U ]), and this output tree is of the form t 2 [u] for some u ∈ U . We say that A chooses u in U . A weak choice automaton chooses for each set U at most one element from this set. It is called weak because it does not have to choose an element. A weak choice automaton that chooses one element from each nonempty set represents a choice formula. Our goal is to show that such an automaton cannot exist. Note that there are weak choice automata: for example the automaton that rejects all inputs is a weak choice automaton because it does not choose an element for any set.

We show in Lemma 3.4 that for each weak choice automaton A we can find a set that is complex enough such that A cannot choose an element of U . If A had a run choosing an element of U , we could construct another run choosing a different element, contradicting the property of a weak choice automaton. More precisely, we define a family (U M,N ) M,N ∈N of sets such that for each weak choice automaton A we can find M and N such that A cannot choose an element of U M,N . To achieve this, we "hide" the elements of the set very deep in the tree so that weak choice automata up to a certain size are not able to uniquely choose an element.

For M, N ∈ N the set U M,N ⊆ {0, 1} * is defined by the following regular expression

U M,N = {0, 1} * (0 N 0 * 1) M {0, 1} * .
In Figure 1 a deterministic finite automaton for the set U M,N is shown, where the dashed edges represent transitions for input 1 that lead back to the initial state x M . The chains of 0-edges between x k+1 and x k have length N . The final state is x 0 . It is easy to verify that x 0 is reachable from x M by exactly those paths whose sequence of edge labels is in the set U M,N . Let t M,N = t[U M,N ] and let t k,M,N = t 2 [U k,M,N ], where U k,N,M is the set that we obtain by making x k the initial state. We now fix a weak choice automaton A = (Q, {0, 1}, q 0 , ∆, c, λ) on {0, 1}labeled trees and take M = 2 |Q| +1 and N = |Q|+1. For these fixed parameters we simplify the notation by letting t k = t k,M,N . In particular, t M = t M,M,N = t M,N . We say that a subtree (of some tree t) that is isomorphic to t k for some k is of type t k .

Our aim is to trick the automaton A to show that it cannot choose a unique element from the set U M,N . This is done by modifying a run that outputs an element u of U M,N such that we obtain another run outputting a different element from the same set.

To understand the general idea, consider the path between x k+1 and x k for some k. If we take a 1-edge before having reached the end of the 0-chain, i.e., one of the dashed edges leading back to the initial state x M , then we reach a subtree of type t M . But if we walk to the end of the 0-chain and then move to the right using a 1-edge, then we arrive at a subtree of type t k . If we show that there is ℓ < M such that t M and t ℓ are A-equivalent, then this means that A has no means to identify when it enters the part where taking a 1-edge leads to a subtree of type t ℓ . We then exploit this fact by pumping the run on this part of the tree such that we obtain another run with a different output. Proof. We consider for each tree t ∈ T ω {0,1} the function f t : Q → {a, r} with f t (q) = a if there is an accepting run of A from q on t, and f t (q) = r otherwise. By definition, two trees t, t ′ are A-equivalent if f t = f t ′ . There are at most 2 |Q| different such functions. By the choice of M there are 1

x M • • • x M -1 • • • x M -2 . . . x 1 • • • x 0 1 0 0 0 0 1 0 0 0 0 1 0 1 0 0 0 0 1 0, 1 N 0-edges
≤ k 1 < k 2 ≤ M such that t k1 ≡ A t k2 .
We now show that t k1 ≡ A t k2 implies t k1+1 ≡ A t k2+1 (in case k 2 < M , otherwise we choose ℓ = k 1 ). This allows us to lift the equivalence step by step to t ℓ and t M for ℓ = k 1 + (Mk 2 ).

If we only look at the left-most branches and the types of the trees going off to the right, then t k1+1 and t k2+1 look as shown in Figure 2. From this picture it should be clear that t k1+1 ≡ A t k2+1 because an accepting run on t k1+1 can easily be turned into an accepting run on t k2+1 , and vice versa, using the equivalence of t k1 and t k2 .

2

The following lemma states that it is impossible for A to choose an element of U M,N (and hence the set of outputs computed by A on t M,N is empty).

Lemma 3.4 The weak choice automaton

A cannot choose an element from U M,N , i.e., A([t M,N ]) = ∅.
Proof. Assume that there is an accepting run ρ of A on t M = t M,N . Since A is a weak choice automaton this means that the output of this run must be an element of U M,N , i.e., λ(ρ) = t[u] for some u ∈ U M,N .

From ρ we construct another accepting run with a different output tree, contradicting the definition of weak choice automaton.

Since u is in U M,N , we know that the path from the root to u must end with the pattern as defined by the automaton in Figure 1. Hence we can make the following definitions. For 0 ≤ k ≤ M let u k denote the maximal prefix of u such that the subtree at u k is of type t k . Let ℓ be as in Lemma 3.3. For i ≥ 0 let v i = u ℓ+1 0 i and v ′ i = v i 1. Note that v 0 = u ℓ+1 and that for 0 ≤ i < N the subtree at v ′ i is of type t M , and for i ≥ N the subtree at v ′ i is of type t ℓ . From Lemma 3.3 we know that t ℓ ≡ A t M . Hence, for each accepting run ρ q of A from q on t M we can pick an accepting run ρ ′ q of A from q on t ℓ . By the choice of N (recall that N = |Q| + 1) there are 0 ≤ j < j ′ < N such that ρ(v j ) = ρ(v j ′ ). For the moment, consider only the transitions taken in ρ on the sequence v 0 , v 1 , . . ., i.e., on the infinite branch to the left starting from v 0 . We now simply repeat the part of the run between v j and v j ′ once. The effect is that some of the states that were at a node v ′ i for i < N are pushed to nodes v ′ i for i ≥ N , i.e., the states are moved from subtrees of type t M to subtrees of type t ℓ . But for those states q we can simply plug the runs ρ ′ q that we have chosen above.

More formally, we define the new run ρ ′ of A on t M as follows. On the part that is not in the subtree below v 0 the run ρ ′ corresponds to ρ. In the subtree at v 0 we make the following definitions, where h = j ′j.

• For i < j ′ let ρ ′ (v i ) = ρ(v i ) and ρ ′ (v ′ i ) = ρ(v ′ i ). • For i ≥ j ′ let ρ ′ (v i ) = ρ(v i-h ) and ρ ′ (v ′ i ) = ρ(v ′ i-h ). • For the subtrees at v ′ i for i < j ′ we take the subrun of ρ at v ′ i . • For the subtrees at v ′ i for j ′ ≤ i < N or i ≥ N + h we take the subrun of ρ at v ′ i-h . This is justified because in these cases ρ ′ (v ′ i ) = ρ(v ′ i-h
) and the subtrees at v ′ i and v ′ i-h are of the same type (both of type t M or both of type t ℓ ).

• For the subtrees at v ′ i for N ≤ i < N +h we take the runs ρ ′ qi for q i = ρ ′ (v ′ i ). This is justified as follows. From q i = ρ ′ (v ′ i ) and the definition of ρ ′ we know that ρ(v ′ i-h ) = q i . Hence, there is an accepting run of A from q i on t M . Thus, ρ ′ qi as chosen above is an accepting run of A from q i on t ℓ . This run ρ ′ is accepting. Furthermore, the transition producing output 1 in ρ has been moved to another subtree: There are n ≥ N and w ∈ {0, 1} * such that u = u ℓ+1 0 n w. In ρ ′ the transition that is used at u in ρ is used at u ′ = u ℓ+1 0 n+h w. Hence, we have constructed an accepting run whose output tree is different from t[u], a contradiction. 2

Of course, the statement is also true if we increase the value of M or N , e.g., if we take N = M = 2 |Q|+1 . Thus, combining Theorem 3.2 and Lemma 3.4 we obtain the following.

Theorem 3.5 Let φ(X, x) be an MSO-formula. There exists m ∈ N such that for all n ≥ m and for each u

∈ U n,n with t 2 |= φ[U n,n , u] there is u ′ = u with t 2 |= φ[U n,n , u ′ ].
Proof. Consider the formula

φ * (X, x) := φ(X, x) ∧ x ∈ X ∧ ¬∃y(y = x ∧ y ∈ X ∧ φ(X, y)).
Applying Theorem 3.2 to this formula yields a weak choice automaton A. Choose n = 2 |Q|+1 and assume that there is u ∈ U n,n such that t 2 |= φ[U n,n , u]. According to Lemma 3.4 we have A(t n,n ) = ∅. Hence, because A and φ * are equivalent,

t 2 |= φ * [U n,n , u]
. By definition of φ * this means that there must be

u ′ = u such that t 2 |= φ[U n,n , u ′ ]. 2
A direct consequence is the theorem of Gurevichand Shelah (Theorem 3.1). The advantage of our proof is that we obtain a rather simple family of counter examples (the sets U M,N ).

An easy reduction allows us to extend the non-existence of an MSO-definable choice function to the case where we allow a finite number of fixed predicates as parameters. This result has already been shown in [START_REF] Lifsches | Uniformization and Skolem functions in the class of trees[END_REF] in an even more general context, but again relying on the methods employed in [START_REF] Gurevich | Rabin's uniformization problem[END_REF].

Corollary 3.6 Let P 1 , . . . , P n ⊆ {0, 1} * be arbitrary predicates. There is no MSO-formula φ(X, x) such that for each nonempty set U there is exactly one

u ∈ U with t 2 [P 1 , . . . , P n ] |= φ[U, u].
Proof. Suppose that there are P 1 , . . . , P n ⊆ {0, 1} * and an MSO[t 2 ]-formula φ(X 1 , . . . , X n , X, x) such that for each nonempty set U there is exactly one u ∈ U with t 2 [P 1 , . . . , P n ] |= φ[U, u], where the symbols X 1 , . . . , X n are interpreted by P 1 , . . . , P n , respectively. Then the formula ∃X 1 , . . . , X n ∀X = ∅ ∃x ∈ X : φ(X 1 , . . . , X n , X, x) ∧ ∀y φ(X 1 , . . . , X n , X, y) → x = y holds in t 2 . Hence, there are regular predicates P ′ 1 , . . . , P ′ n (see Theorem 2.2 on page 6) such that

t 2 [P ′ 1 , . . . , P ′ n ] |= ∀X = ∅ ∃x ∈ X : φ(X 1 , . . . , X n , X, x) ∧ ∀y φ(X 1 , . . . , X n , X, y) → x = y.
Regular predicates are MSO-definable (see Proposition 2.3), and therefore we can find formulas ψ 1 (z), . . . , ψ n (z) defining P ′ 1 , . . . , P ′ n , respectively. Then the formula φ ′ (X, x) defined as

∃X 1 , . . . , X n : φ(X 1 , . . . , X n , X, x) ∧ n i=1 (∀z : z ∈ X i ↔ ψ i (z))
describes a choice function, contradicting Theorem 3.5.

2

We point out here that this method only relies on the fact that the property of being a choice function is MSO-definable. This way of reducing the case with parameters to the parameter free case can be applied whenever the properties of the object under consideration are MSO-definable (in Proposition 5.7 on page 25 we also use this technique).

MSO-definable winning strategies

In this section we use Theorem 3.1 to study the definability of winning strategies in infinite games. For a general introduction to games of infinite duration we refer the reader to [START_REF] Grädel | Automata, Logics, and Infinite Games[END_REF]. The logical definability of winning regions in parity games has been studied in [START_REF] Dawar | The descriptive complexity of parity games[END_REF]. To express that a vertex of a game graph belongs to the winning region of one player it is sufficient to express that there exists a winning strategy from this vertex. Here we study the question whether it is possible to define a single winning strategy. In the following we show that there exist tree games (games with a tree as underlying game graph) that do not admit MSO-definable winning strategies.

A game tree is a tuple Γ = (U 1 , U 2 , Ω) where U 1 , U 2 ⊆ {0, 1} * form a partition of {0, 1} * , and Ω : {0, 1} * → {0, . . . , n} maps each node to a number in a finite initial segment of N. A tree game (Γ, W ) is given by a game tree Γ and a winning condition W ⊆ {0, . . . , n} ω . A play in this game starts in ε. If the play is currently in u ∈ {0, 1} * , then Player 1 or Player 2, depending on whether u ∈ U 1 or u ∈ U 2 , chooses b ∈ {0, 1}, and the next game position is ub. In the limit, such a play forms an infinite word in {0, 1} ω ; we identify the play with this word. This infinite word corresponds to an infinite sequence over {0, . . . , n} by applying Ω to each prefix. If this sequence is in W then Player 1 wins, and otherwise Player 2 wins.

A strategy for Player i is a function f i : U i → {0, 1}. A play γ is played according to f i if, for each prefix u ∈ U i of γ, Player i uses the strategy to determine the next move, i.e., uf i (u) is again a prefix of γ. A strategy f i is winning for Player i if each play γ played according to f i is won by Player i.

If W ⊆ {0, . . . , n} ω is a regular ω-language, then for each tree game (Γ, W ) one of the players has a winning strategy [START_REF] Büchi | Solving sequential conditions by finitestate strategies[END_REF].

A strategy f i for Player i can be represented by two sets of nodes S 0 and S 1 of the game tree: the set of nodes where the value of f i is 0 and 1, respectively. We are interested in MSO-definability of strategies in the game tree. To this end, we represent a game tree Γ = (U 1 , U 2 , Ω) as the binary tree t 2 extended by monadic predicates U 1 , U 2 , Ω 0 , . . . , Ω n , where each Ω i ⊆ {0, 1} * corresponds to the set of nodes mapped to i by Ω. Let us abbreviate t

2 [U 1 , U 2 , Ω 0 , . . . , Ω n ] = t 2 [Γ].
We say that a strategy represented by S 0 and S 1 is MSO-definable in the game tree Γ if these sets are definable in t 2 [Γ], i.e., if there exists two MSOformulas φ 0 (x) and φ 1 (x) determining the sets S 0 and S 1 :

S 0 ={u : t 2 [Γ] |= φ 0 [u]} S 1 ={u : t 2 [Γ] |= φ 1 [u]}.
Finite-state strategies (i.e. strategies implementable by a finite-state automaton) are a particular case of MSO-definable strategies.

Note that the above formulas φ 0 (x) and φ 1 (x) may depend on the game tree Γ. The question whether such formulas exist for a particular game tree Γ and a player i should not be confused with the fact that the family of all winning strategies for player i is definable in MSO in a uniform way. More precisely, whenever the condition W is ω-regular then it is not difficult to write an MSO-formula ψ W (X 1 , X 2 , Y 0 , . . . , Y n , Z 0 , Z 1 ), such that, for any game tree Γ = (U 1 , U 2 , Ω) with Ω : {0, 1} * → {0, . . . , n}, and any S 0 , S 1 ⊆ {0, 1} * ,

t 2 |= ψ W [U 1 , U 2 , Ω 0 , . . . , Ω n , S 0 , S 1 ]
iff S 0 and S 1 represent a winning strategy for Player i in (Γ, W ). Thus, we can express the existence of a winning strategy for Player i in the game (Γ, W ) by an MSO-formula interpreted in t 2 [Γ]. If t 2 [Γ] has decidable MSO-theory, we can therefore decide who wins the game (Γ, W ) for any ω-regular winning condition W . This however does not imply the existence of an MSO-definable winning strategy. In fact, we show in the following that there is a fixed tree game (with a decidable MSO-theory) for which there are no MSO-definable winning strategies.

It is well-known that there exists a recursive tree game where Player 1 has a winning strategy but no recursive one. In [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF], an example of such a tree game is given that has moreover an MSO-definable winning condition. Nevertheless this example cannot be used to prove the following theorem as both players admit MSO-definable strategies. Theorem 3.7 There is a game tree Γ = (U 1 , U 2 , Ω) with decidable MSO-theory, and an MSO-definable winning condition W , such that Player 1 has a winning strategy in the game (Γ, W ), but no winning strategy for Player 1 is MSOdefinable in t 2 [Γ].

Proof. Consider the following {0, 1, 2}-labeled tree t such that for each n ∈ N the subtree at the node 1 n 0 is isomorphic to t n,n , and all nodes of the form 1 n are labeled by 2. The labeling of t defines the mapping Ω, i.e., Ω(u) = t(u). We let

U 2 = {1 n | n ∈ N} and U 1 = {0, 1} * \ U 2 .
Consider Γ = (U 1 , U 2 , Ω) and let the winning condition W (for Player 1) contain all infinite words over {0, 1, 2} that do not contain 0 or that contain a 1.

Intuitively, Player 2 can move along the right branch of the game tree. If he continues like this forever then he loses because only nodes labeled 2 are visited during the play. Otherwise, he moves to the left at some position, that is, to the root of a subtree t n,n . Now Player 1 chooses all the following moves and wins if a node labeled 1 is reached eventually. As each subtree t n,n contains a node labeled 1 it is obvious that Player 1 has a winning strategy.

Assume that there is a winning strategy f 1 for Player 1 that is MSO-definable in t 2 [Γ] by formulas φ 0 (x) and φ 1 (x). Let S f1 be the set of all nodes that occur in a play that is played according to f 1 . (This set can be seen as an alternative way of coding the strategy f 1 .) From φ 0 and φ 1 we can easily derive an MSO

[t 2 ]- formula φ(X 1 , X 2 , Y 0 , Y 1 , Y 2 , X), such that t 2 |= φ[U 1 , U 2 , Ω 0 , Ω 1 , Ω 2 , S]
holds precisely when S = S f1 .

The formula φ is equivalent to a parity automaton over alphabet {0, 1} 6 , but using the definition of our Γ (constructed from the tree t), we can simplify it to an automaton A over the alphabet {0, 1, 2} × {0, 1}, where the 1 on the second component should be read as "marked". This automaton reads trees over {0, 1, 2}, where some nodes are marked, and whenever it reads our tree t, it accepts it only in the case when the marking coincides with S f1 .

Using A we can construct a formula φ * (X, x) that chooses exactly one u ∈ U n,n for each n ∈ N, contradicting Theorem 3.5. For this we fix an arbitrary order on the states of A. For each n there is at least one state q of A such that A accepts from q exactly one winning strategy on the subtree t n,n of t (namely the state assumed at the root of the subtree t n,n in an accepting run for the unique winning strategy on Γ that is accepted by A). The formula φ * is designed to select the smallest state q with this property and then chooses the element of U n,n that is described by the unique winning strategy accepted by A from q on t n,n . It is not difficult to verify that the formalization is indeed possible in MSO.

2

One should note here that the tree constructed in the proof of Theorem 3.7 (and also the one from Theorem 4.3) is not too complicated: it belongs to the Caucal hierarchy1 [START_REF] Radhakrishnan | On infinite terms having a decidable monadic theory[END_REF]. This means that it can be obtained from a regular tree by a finite number of applications of MSO-interpretations and unfoldings, or equivalently, it is the transition graph of a higher-order pushdown automaton [START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF].

In [START_REF] Löding | Automata and Logics over Infinite Trees[END_REF] it is shown that the tree belongs to the fourth level of the hierarchy. The possibility of constructing such rather simple examples is one of the advantages of our new proof of Theorem 3.1.

In the tree games that we consider we do not require that there is a strict alternation between the moves of the two players. However, by inserting additional nodes in the tree games, it is always possible to obtain a game with strict alternation.

Unambiguous automata

In this section, we show that unambiguous parity tree automata do not accept all regular tree languages. For the proof we use the non-existence of a MSOdefinable choice function.

Unambiguous automata have been introduced on finite words because they allow more efficient algorithms for equivalence and inclusion testing [START_REF] Stearns | On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata[END_REF]. This has been generalized to automata on finite trees in [START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF]. On finite words and trees it is clear that every regular language can be accepted by an unambiguous automaton because deterministic automata are unambiguous.

For Büchi automata on infinite words the situation is more difficult. Although determinization is possible ( [START_REF] Mcnaughton | Testing and generating infinite sequences by a finite automaton[END_REF][START_REF] Safra | On the complexity of omega-automata[END_REF]), it requires the model of deterministic parity (or Muller) automata with acceptance conditions that are more powerful than Büchi conditions. However, from the determinization result one can infer that all regular languages of infinite words can be accepted by an unambiguous Büchi automaton [START_REF] Arnold | Rational ω-languages are non-ambiguous[END_REF]. In [START_REF] Kähler | Complementation, disambiguation, and determinization of Büchi automata unified[END_REF] a construction for unambiguous automata is presented that does not rely on deterministic automata.

In this section we show that the situation is different for infinite trees: There are regular languages that cannot be accepted by an unambiguous automaton. The proof is based on the main result from the previous section: the undefinability of a choice function in MSO. The underlying idea is rather simple. We consider the language

T ∃1 = {t ∈ T ω {0,1} | ∃u ∈ {0, 1} * : t(u) = 1}
of trees with at least one node labeled 1. Each tree in T ∃1 can be viewed as the set of nodes labeled 1. Intuitively, an automaton accepting T ∃1 has to verify that the input tree contains a 1, i.e., an accepting run has to identify some position labeled by 1. If the automaton is unambiguous, then there is exactly one run for each tree in T ∃1 , and hence the automaton identifies exactly one position from the set coded by the 1-positions. This can be turned into a formula defining a choice function.

We show the following more technical result because it can be used to prove different statements on the ambiguity of automata. Lemma 4.1 Let A be a parity tree automaton over the alphabet {0, 1} not accepting the tree that is completely labeled by 0. Then there is a formula ψ A (X, x) such that for each U ⊆ {0, 1} * for which there is a unique accepting run of A on t 2 [U ], there is a unique element u ∈ U such that

t 2 |= ψ A [U, u].
Proof. We consider the following game which can be seen as the emptiness game2 for the automaton A intersected with the trivial automaton that accepts only the tree t[∅] (i.e., the tree labeled 0 everywhere). This intersection corresponds to removing all transitions that use a letter different from 0 from the standard emptiness game for A.

Formally, the game is played between two players Eva and Adam who move in alternation. The positions of Eva are the states of A, and the positions of Adam are the transitions of A that use input letter 0. The initial position is the initial state of A. Then the players move in alternation as follows:

• From a position q Eva chooses a transition (q, 0, q 0 , q 1 ) of A.

• From position (q, 0, q 0 , q 1 ) Adam chooses a state q 0 or q 1 . Eva wins a play if she can always choose a transition and if the resulting sequence of states chosen in the play satisfies the acceptance condition of A. Since the acceptance condition of A is a parity condition, we obtain a parity game (for basic facts on parity games see [START_REF] Thomas | Languages, automata, and logic[END_REF]).

We have already mentioned that the presented game is an emptiness game for the subautomaton of A in which all transitions with label 1 have been removed.

A winning strategy of Eva in this game would yield an accepting run of A on the tree t[∅], contradicting the assumption t[∅] / ∈ T (A). We can conclude that Adam has a winning strategy, and since we are working with a parity game, Adam even has a positional3 winning strategy f that picks for each transition of the form (q, 0, q 0 , q 1 ) one of the states q 0 , q 1 (see [START_REF] Thomas | Languages, automata, and logic[END_REF] for a proof of the positional determinacy of parity games).

We now construct the formula ψ A (X, x) based on this strategy f . Evaluated on t[U, u] the formula states that there exists an accepting run of A on t[U ] such that the path leading to node u corresponds to the choices of Adam according to the strategy f . Note that if we apply the strategy of Adam to the transitions in an accepting run, then this results in a path ending in a node labeled 1 because otherwise the resulting infinite play would be winning for Eva.

Assuming that the states of A are {1, . . . , n} the formula ψ A (X, x) looks as follows:

∃X 1 , . . . , X n : AccRun(X 1 , . . . , X n , X) ∧ X(x) ∧ ∀y ⊏ x : strat f (X, x, X 1 , . . . , X n , y)
where

• the formula AccRun expresses that X 1 , . . . , X n describe an accepting run of A on the characteristic tree of X (the construction of such a formula is standard, see e.g. [START_REF] Thomas | Languages, automata, and logic[END_REF]), and

• strat f states that the strategy f applied at node y in the run coded by X 1 , . . . , X n moves into the direction of x. In case the strategy allows to move to both directions (when the states q 0 and q 1 are the same), the formula picks the left move: ¬X(y) ∧ q,q0,q1∈{1,...,n} X q (y) ∧ X q0 (y0) ∧ X q1 (y1) → f (q, 0, q 0 , q 1 ) = q 0 ↔ (y0 ⊑ x)

If we fix the interpretations for X and X 1 , . . . , X n , then there is exactly one interpretation of x such that ∀y ⊏ x.strat f (X, x, X 1 , . . . , X n , y) is satisfied (if there are two positions, then we obtain a contradiction when interpreting y as the greatest common ancestor of these two positions). Now assume that there is exactly one accepting run of A on t[U ]. Then the interpretations of X 1 , . . . , X n are fixed by U and hence the formula ψ A (X, x) has the claimed property.

2

Using this lemma it is easy to obtain the following theorem.

Theorem 4.2 There is no unambiguous parity tree automaton accepting the language T ∃1 consisting of exactly those {0, 1}-labeled trees in which at least one node is labeled 1.

Proof. Assume A is an unambiguous automaton for T ∃1 and consider the formula ψ A (X, x) from Lemma 4.1. As there is a unique accepting run of A on t[U ] for each non-empty set U , ψ A (X, x) defines a choice function. This contradicts Theorem 3.1. 2

Using Lemma 4.1 we can also show that there are regular languages whose ambiguity is witnessed by a single tree. Theorem 4.3 There is a regular language T ⊆ T ω {0,1} and a tree t ∈ T such that there is no parity automaton accepting T that has a unique accepting run for t.

Proof. Consider the language T of trees with the property that each subtree rooted at a node of the form 1 * 0 contains a node labeled 1. Obviously this is a regular language.

The tree t is defined to have all nodes of the form 1 * labeled 0, and for each n we plug the tree t n,n as the subtree rooted at the node 1 n 0 (as in the proof of Theorem 3.7.) As each t n,n contains a node labeled 1, we have t ∈ T .

Assume that there is parity automaton A accepting T that has a unique run on t. Let q be a state of A that occurs at infinitely many nodes of the form 1 * 0 in this run. Let A ′ be the automaton A with initial state q. As A accepts T it is clear that A ′ does not accept the tree t[∅]. Furthermore, as the run of A on t is unique, there are infinitely many n such that A ′ has a unique run on t n,n . For the formula ψ A ′ (X, x) from Lemma 4.1 this yields a contradiction to Theorem 3.5. 2

Well-orderings

A well-ordering is a total order relation with the property that there are no infinite descending chains or, equivalently, every non-empty subset of the domain of the relation has a smallest element. A simple example is the natural ordering on the set of natural numbers N. The natural ordering on the set of integers Z is not a well-ordering because, e.g., the whole set Z does not have a minimal element w.r.t. to this ordering. If we define an ordering on Z by first comparing the absolute values of the numbers and in case of equality letting the negative one be smaller, i.e., n m iff |n| < |m|, or |n| = |m| and n ≤ m, then we obtain a well-ordering. A partial well-ordering is a partial order relation with no infinite descending chains and with no infinite sets of pairwise incomparable elements. Equivalently a partial well-ordering is a partial order in which any non-empty set admits a non-empty finite set of minimal elements. Another useful equivalent property is that for every infinite sequence (a i ) i∈N there are two indices k < l such that a k ≤ a l . For two elements u and v of the partial well-ordering, we write u | v if u and v are incomparable for the order.

A well-ordering is a particular case of partial well-ordering. If we partially order the integers in Z by comparing their absolute values if they have the same sign, we obtain a partial well-ordering on Z.

In this section we are interested in well-orderings and partial well-orderings on the tree domain {0, 1} * . A typical ordering of {0, 1} * is the lexicographic ordering ≤ lex defined by

u 1 ≤ lex u 2 if u 1 is a prefix of u 2 , or u 1 = u0u ′ 1 and u 2 = u1u ′ 2 for some u, u ′ 1 , u ′ 2 ∈ {0, 1} * .
From the definition of ≤ lex one can easily see that it is MSO-definable in t 2 . But it is not a well-ordering because, e.g., the set of nodes of the form 0 * 1 does not have a minimal element.

In a similar way as we changed the standard ordering on Z into a wellordering, we can obtain a well-ordering on {0, 1} * by first comparing the length of the elements and in case of equality take the lexicographic ordering. We obtain the length-lexicographic ordering ≤ llex formally defined by

u 1 ≤ llex u 2 iff |u 1 | < |u 2 |, or |u 1 | = |u 2 | and u 1 ≤ lex u 2 .
This defines a well-ordering but its definition requires to compare the length of the elements. From the fact that the MSO-theory of t 2 extended with the equal length predicate is undecidable (see [START_REF] Thomas | Automata on infinite objects[END_REF]) one can easily derive that ≤ llex is not MSO-definable in t 2 .

A partial well-ordering < len on {0, 1} * is obtained by only comparing the length of the words (i.e. u ≤ len v if u = v or |u| < |v|). In fact, as there are only finitely many words of a given length, any non-empty subset of {0, 1} * has a non-empty set of minimal elements for < len . Again < len is not MSO-definable in t 2 .

More generally, as a direct consequence of Theorem 3.1 we obtain that there exists no MSO-definable partial well-ordering on the nodes of the infinite binary tree. In fact, from an MSO-formula φ ≤ (x, y) defining a partial well-ordering in t 2 , a choice function choosing x in X is easily defined by taking the smallest element for ≤ lex of the finite set of minimal elements of X (for the partial well-ordering):

ψ choice (X, x) := ∃Y ⊆ X. x ∈ Y ∧ (∀y ∈ Y. x ≤ lex y)∧ ∀z ∈ X. z ∈ Y ↔ ¬(∃z ′ ∈ X φ < (z ′ , z))
This naturally raises the question whether there is a partial well-ordering that we can add to t 2 while preserving the decidability of MSO. In this section, we prove the following negative result.

Theorem 5.1 The MSO-theory of the full-binary tree together with an arbitrarypartial well-ordering is undecidable.

In the particular case of t llex , the infinite binary tree with length-lexicographic order, i.e., the structure t llex = ({0, 1} * , E 0 , E 1 , ≤ llex ), this result is well-known. It easily follows from the undecidability of t 2 extended with the equal length predicate (see [START_REF] Thomas | Automata on infinite objects[END_REF]).

We show that t llex can be MSO-interpreted in the infinite binary tree with any partial well-ordering. Theorem 5.2 There exists an MSO-interpretation I such that for every partially well-ordered infinite binary tree t, I(t) is isomorphic to t llex .

As MSO-interpretations preserve the decidability of MSO (see Proposition 2.4), Theorem 5.1 follows from the undecidability of the MSO-theory of t llex . The rest of this section is dedicated to the proof of Theorem 5.2.

Partially well-ordered trees

We consider structures over the binary signature τ = {E 0 , E 1 , ≤}. A canonical well-ordered tree has the universe {0, 1} * where E 0 and E 1 are respectively interpreted as {(u, u0) | u ∈ {0, 1} * } and {(u, u1) | u ∈ {0, 1} * }, and ≤ is interpreted as a well-ordering on {0, 1} * . We say that a τ -structure t is a wellordered (infinite binary) tree if it is isomorphic to a canonical well-ordered tree. Similarly, if ≤ is a partial well-order we talk about partially well-ordered trees.

Up to isomorphism, a well-ordered tree is entirely characterized by the wellordering on the set of words over {0, 1}. Above, we have already defined t llex to be the well-ordered tree with ≤ llex as ordering relation.

The key property of t llex is that it is MSO-definable (up to isomorphism) in the class of partially well-ordered trees4 . Proposition 5.3 There exists an MSO-sentence φ llex such that a partially wellordered tree t is isomorphic to t llex iff t |= φ llex .

Proof. We describe the properties that we need to express by φ llex to ensure that partially well-ordered t is isomorphic to t llex . In the description, for a node v1 ∈ 1 + we denote by Bubble(v1) the set {u : v < u ≤ v1}. Note that if ≤ equals ≤ llex , then Bubble(v1) consists of all nodes that are on the same level as v1. The formula φ llex expresses the following properties:

1. Bubble(1) = {0, 1}, and for all v ∈ 1 * , Bubble(v1) is the set of all the children of nodes in Bubble(v).

2. The root of the tree is the least element for the order ≤, and on Bubble(v) the relation ≤ agrees with the lexicographic order for all v ∈ 1 + .

These properties can be defined in MSO. It is easy to see that t llex satisfies the formula φ llex . It remains to show that for every well-ordered tree t satisfying φ llex is isomorphic to t llex .

Let t be a partially well-ordered tree satisfying φ llex . First observe that for v ∈ 1 * the first condition assures that Bubble(v) = {u : |u| = |v|}, i.e., the set of all the nodes that are on the same level as v.

We write Succ llex (u) for the successor of u for the order ≤ llex . To prove the proposition it is enough to show that every node u has exactly one successor in <-ordering, and it is Succ llex (u); in other terms, the set of minimal elements of {v : u < v} is exactly {Succ llex (u)}.

Assume by contradiction that this property is not satisfied. Let ū be the smallest in the ≤ llex ordering node violating this property. By the first condition, ū is not the root. If ū ∈ 1 + then the minimal elements of {v : ū < v} are contained in Bubble(ū1). By the second condition the only minimal element is 0 |ū|+1 = Succ llex (ū). If ū ∈ 1 + then all its potential successors are in Bubble(v) where v ∈ 1 * has the same length as ū. Once again the second condition allows us to conclude. 2

Interpreting t llex

We now define the notion of induced partially well-ordered tree. Consider a canonical partially well-ordered tree t with partial well-ordering ≤ t and a set U ⊆ {0, 1} * of nodes that

• is closed under greatest common prefix (u ∈ U ∧ v ∈ U → u ∧ v ∈ U ),
• has the property that for all u ∈ U , u0{0, 1} * ∩U = ∅ and u1{0, 1} * ∩U = ∅, i.e., from every node we can go to the left and to the right and find another element of U below.

The partially well-ordered tree t| U induced by U in t has universe U .

To interpret its relations we use a formula ψ greatest (X, x) stating that x is the greatest common prefix of the set X:

E t| U 0 = {(u, v) ∈ U × U | t |= ψ greatest [u0{0, 1} * ∩ U, v]} E t| U 1 = {(u, v) ∈ U × U | t |= ψ greatest [u1{0, 1} * ∩ U, v]} ≤ t| U = {(u, v) ∈ U × U | u ≤ t v}.
The plan is to show that in each partially well-ordered tree we can find a subset U inducing a well-ordered tree that is isomorphic to t llex . As a first step we show that we can express each MSO-property φ of t| U by an MSO-formula φ * on t that takes U as a parameter. Lemma 5.4 For every MSO-formula φ over τ there exists a formula φ * (X) such that for every canonical partially well-ordered tree t and set U , t |= φ * [U ] iff the set U induces a partially well-ordered tree t| U on t, and t| U |= φ.

Proof. Consider an MSO-formula φ over τ . Let φ ind (X) be an τ -formula expressing that X satisfies the conditions to induce a full binary tree and let φ ′ (X) be the formula obtained from φ by relativizing the quantifications to X and by replacing E i (x, y) with ψ choice (xi{0, 1} * ∩X, y), for i ∈ {0, 1}. It is easy to check that the formula φ * (X) := φ ind (X) ∧ φ ′ (X) satisfies the property stated in the lemma.

2

Applying this lemma to the formula φ llex from Proposition 5.3 yields that t |= φ * llex [U ] iff U induces a well-ordered tree isomorphic to t llex . We now show that for every canonical partially well-ordered tree t there exists a subset U ⊆ {0, 1} * such that t| U is isomorphic to t llex . We even show a stronger result: there is in fact an MSO-definable such set (Lemma 5.6). To construct such a set U we built up a sequence of nodes indexed by the elements from {0, 1} * . We start with a node u ε representing the root of t| U . Then we define u 0 to be a node in the left subtree of u ε such that u ε < u 0 . We continue by finding a node u 1 in the right subtree of u ε such that u 0 < u 1 . Then we take a node u 00 in the left subtree of u 0 such that u 1 < u 00 , and so on. This construction is illustrated in Figure 3, where the dashed arrows represent the order relation < on the sequence u ε , u 0 , u 1 , u 00 , . . . by always pointing to the next bigger element from this sequence.

u ε • • u 0 u 1 • u 00
For this construction to work we need to ensure that we always can find nodes as required, e.g., that there is a node u 00 in the left subtree of u 0 such that u 1 < u 00 . For this purpose we make the definition of a mixed node and later choose u ε to be a node with this property. We call a node u ∈ {0, 1} * of a canonical partially well-ordered tree t mixed if the ordering relation "jumps" between all different subtrees below u in the following sense: for all v, v ′ ⊒ u there exists w ∈ {0, 1} * such that v < v ′ w. We show that we can indeed find a node with this property. Lemma 5.5 Every canonical partially well-ordered tree t contains a mixed node.

Proof. Let t be a canonical partially well-ordered tree. Assume by contradiction that t does not have any mixed nodes. We are going to construct a sequence (u n ) n∈N of nodes such that for no i < j, u i < u j . This is in contradiction with the fact that < is a well partial ordering.

We construct the sequence (u n ) n∈N by induction on n together with another sequence of nodes (v n ) n∈N such that for all n ≥ 0:

• v n ⊑ u n+1 and v n ⊑ v n+1 ,
• there is no v > u n in the subtree rooted in v n .

Note that these conditions imply that for no i < j, u i < u j because u j is in the subtree rooted in v i .

As ε is not mixed there exist two nodes u and v such that there is no node in the subtree of v that is greater (with respect to <) than u. We take u 0 = u and

(3) for all x ′ = x 0 ∈ U 0 with predecessor x in U 0 (according to ≤), father x ′′ in U 0 (according to the binary tree structure induced by U 0 ), and i ∈ {0, 1} such that x ′′ i ⊑ x ′ , we have that x ′ is the element chosen by ψ in the set of elements of U 0 which are below x ′′ i and greater than x (below according to the prefix relation, and greater according to <).

It follows from the first part of the proof that such a set exists. Moreover there exists at most one set satisfying properties (1), ( 2) and (3). It remains to verify that the above properties can be expressed in MSO-logic. For property [START_REF] Arnold | Rational ω-languages are non-ambiguous[END_REF], it is enough to take the formula φ * llex (X) obtained by applying Lemma 5.4 to the formula φ llex of Proposition 5.3. For property (2), we simply need to remark that the property of being a mixed node can be expressed in MSO. For property (3) the translation is immediate.

2

Note that we can now already derive Theorem 5.1: For every formula φ over τ , consider the formula φ * (X) obtained from φ by Lemma 5.4 and φ * llex (X) obtained from the formula φ llex of Proposition 5.3. By Lemma 5.6, for every partially well-ordered tree t:

t llex |= φ iff t |= ∃X : φ * llex (X) ∧ φ * (X).
As the formula φ * (X) can be effectively constructed from the formula φ, it follows that the MSO-theory of t llex is recursive in the MSO-theory of any partially well-ordered tree t.

Using the previous results it is easy to prove Theorem 5.2. Proof(of Theorem 5.2). The interpretation I = (φ dom , φ E0 , φ E1 , φ ≤ ) such that I(t) ∼ = t llex for each well-ordered tree t is defined as follows. As domain formula φ dom we take the formula ψ defining the set U 0 from Lemma 5.6. The formulas φ E0 , φ E1 , and φ ≤ just define the induced successor relations and the induced ordering from the definition of induced well-ordered tree.

2

An immediate consequence of this result is that the infinite binary tree cannot be MSO-interpreted in t 1 (the natural numbers with successor). Based on this we can use the same technique as in Corollary 3.6 to obtain the same result for t 1 extended with unary predicates. Proposition 5.7 Let P 1 , . . . , P n be unary predicates for t 1 . There is no interpretation I such that I(t 1 [P 1 , . . . , P n ]) ∼ = t 2 .

Proof. As already mentioned there is no interpretation I such that I(t 1 ) ∼ = t 2 . Otherwise we could extend this interpretation by a formula transferring the ordering on t 1 to t 2 , thus obtaining a well-ordered tree with decidable MSO-theory (contradicting Theorem 5.1). Now assume that there is an interpretation I such that I(t 1 [P 1 , . . . , P n ]) ∼ = t 2 . We first construct a formula φ tree (X 1 , . Such a formula only needs to express that the formulas from the interpretation describe a structure in which all nodes have exactly one E 0 successor, exactly one E 1 successor, and exactly one predecessor except for one node which is the root. This can easily be done by an MSO-formula. The formula ∃X 1 , . . . , X n : φ tree (X 1 , . . . , X n ) is true in t 2 (interpreting X 1 , . . . , X n by P 1 , . . . , P n ). Hence, there are regular interpretations U 1 , . . . , U n of X 1 , . . . , X n such that t 1 |= φ tree [U 1 , . . . , U n ] (see Theorem 2.2). By construction of φ tree this means that I(t 1 [U 1 , . . . , U n ]) ∼ = t 2 . Since regular sets can be defined in MSO we can directly refer to U 1 , . . . , U n in the interpretation and obtain in interpretation I ′ such that I ′ (t 1 ) = t 2 , which is not possible. 2

Note that Proposition 5.7 does not make any assumption on the predicates P 1 , . . . , P n . Another consequence of Theorem 5.1 is that t 2 is not MSO-interpretable in any structure that has a decidable MSO-theory and admits an MSO-definable well-ordering because otherwise one could also MSO-interpret t 2 extended with a well-ordering in a structure with decidable MSO-theory.

Consider, for example, the function flip on the natural numbers. It maps a natural number n to the number that is obtained by changing the least significant bit that is 1 in the binary representation of n to 0. The graph of the flip function is shown in Figure 4. The structure (t 1 , flip) of the natural numbers with successor extended by the flip function has a decidable MSO-theory [START_REF] Monti | Systolic tree omega-languages: the operational and the logical view[END_REF]. We conclude that t 2 cannot be MSO-interpretable in this structure because otherwise we could also interpret a well-ordered tree in it. Proposition 5.8 There is no MSO-interpretation I with I(t 1 , flip) ∼ = t 2 .

Conclusion

In this paper we have studied questions on MSO-definability in the binary tree and on decidability of MSO in extensions of the binary tree by well-orderings. As a result we obtain a rather simple and elementary proof of the theorem of Gurevich and Shelah stating that there is no MSO-definable choice function on the infinite binary tree. A simple consequence is that there is also no MSOdefinable well-ordering on the domain of the infinite binary tree. We obtain the even stronger result that adding any partial well-ordering to the infinite binary tree yields a structure with undecidable MSO-theory. These two results can be used to derive non-definability results for MSO, as we have illustrated with some examples.

One natural question that remains open is whether there exists a choice function that can be added to the infinite binary tree such that the resulting structure has a decidable MSO-theory.

As mentioned in the introduction, MSO-definability of a choice function is a very special instance of the uniformization problem, namely for the formula φ(X, y) = y ∈ X. The result from Section 3 shows that uniformization is not possible in general on the infinite binary tree. This leaves the question whether there are other types of formulas that allow uniformization. In [START_REF] Semenov | Decidability of monadic theories[END_REF] it is mentioned that uniformization is possible for formulas of the form φ(x, Y ). Here, uniformization means that the relation between elements and sets defined by φ(x, Y ) can be turned into an MSO-definable function associating to each element exactly one set from the relation. 5Another type of question related to this is the one of decidability, as for example in Church's synthesis problem [START_REF] Church | Logic, arithmetic and automata[END_REF] (see also [START_REF] Thomas | Church's problem and a tour through automata theory[END_REF]). An instance of this problem is given by an MSO-formula φ(X, Y ) over the infinite line t 1 such that for each input sequence X there is at least one output sequence Y . A solution is a very specific function compatible with this relation: It should be implementable by a finite state automaton that reads the input sequence and produces in each step one element of the output sequence. The task is now to decide if such an automaton exists (and to construct one if possible). Similarly, one can study the decision variant of uniformization on the binary tree: Given an MSO-formula φ(X, Y ) over t 2 , does there exist an MSO-formula φ * (X, Y ) that defines a function compatible with φ(X, Y ). In its full generality this question seems to be too difficult but one could study specific instances of it for simple classes of formulas.

  and b i = 0 otherwise. For a singleton set U = {u} we simplify notation and write t[u] instead of t[{u}].

Figure 1 :

 1 Figure 1: A DFA accepting U M,N . Dashed edges are labeled by 1. The tree t M,N is obtained by unraveling this DFA.

Figure 3 :

 3 Figure 3: Construction of a set inducing t llex

Figure 4 :

 4 Figure 4: Graph of the flip function

  . . , U n ⊆ {0, 1} * , as a new logical structure over the signature extended by n fresh predicate symbols interpreted by U 1 , . . . , U n . We denote this structure by t 2 [U 1 , . . . , U n ]. Given a formula φ(X 1 , . . . , X n ), we clearly havet 2 |= φ[U 1 , . . . , U n ] iff t 2 [U 1 , . . . , U n ] |= φ,where in the latter case φ is considered as a sentence with the predicate symbols X 1 , . . . , X n interpreted by U 1 , . . . , U n , respectively. This correspondence extends to formulas with additional free variables, say φ(X 1 , . . . , X n , Z 1 , . . . , Z k , y 1 , . . . , y m ). That is,t 2 |= φ[U 1 , . . . , U n , W 1 , . . . , W k , v 1 , . . . , v m ] if and only if t 2 [U 1 , . . . , U n ] |= φ[W 1 , . . . , W k , v 1 , . . . , v m ],for any W 1 , . . . , W k ⊆ {0, 1} * , and v 1 , . . . , v m ∈ {0, 1} * . We will often use this correspondence implicitly in the sequel. Note that in general there may be more relations definable in t 2 [U 1 , . . . , U n ] than in t 2 .

  . . , X n ) such that t 1 |= φ tree [U 1 , . . . , U n ] iff I(t 1 [U 1 , . . . , U n ]) ∼ = t 2 .

	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16 • • •

In particular, as all graphs in the Caucal hierarchy have a decidable MSO-theory, the tree constructed in the proof of Theorem 3.7 also has a decidable MSO-theory.

For a description of the emptiness game for parity tree automata see[START_REF] Thomas | Languages, automata, and logic[END_REF].

The moves of a positional strategy only depend on the current vertex and not on the entire history of the play.

The class of well-ordered trees and the class of partially well-ordered trees are themselves MSO-definable in the class of τ -structures.

Such a result can be shown by transforming the formula into an equivalent automaton and then constructing a formula that selects for each x a unique run that accepts the tree annotated with x and some set Y . For this purpose it is enough to select a (say lexicographically) smallest run on the path to the element x that can be completed to an accepting run. In this finite part of the run we can plug for each 'dangling' state a fixed MSO-definable run. The details of this construction are left to the reader.

Acknowledgements. We would like to thank the anonymous referees for their helpful comments.

* Supported by the Polish government Grant N206 008 32/0810.

v 0 = v. If v 0 is not mixed then we can apply the same argument to the subtree rooted in v 0 obtaining u 1 and v 1 . We get the desired sequence by induction. 2

Now we can formalize the construction of the set U inducing t llex as indicated above and in Figure 3.

Lemma 5.6 For every canonical partially well-ordered tree t, there exists a set of nodes U inducing a well-ordered tree t| U isomorphic to t llex . Moreover there exists an MSO-formula ψ(X) which uniquely defines one such set (i.e. there exists a unique set

Proof. Let t be a canonical partially well-ordered tree. We construct a sequence of nodes (u w ) w∈{0,1} * indexed by the set of words over {0, 1} * such that:

• and for all w ∈ {0, 1} * and i ∈ {0, 1}, u wi ∈ u w i{0, 1} * .

If we assume that this sequence has been constructed and we take U := {u w | w ∈ {0, 1} * }, it is easy to check that U is closed by greatest common prefix and hence U induces a full binary tree on t. Furthermore the mapping from {0, 1} * to U associating w to u w is an isomorphism from t llex to t| U .

We now construct the sequence (u w ) w∈{0,1} * by induction on the lengthlexicographic order ≤ llex . By Lemma 5.5, the tree t has a mixed node. We take u ε to be a mixed node of t.

Assume that the sequence has been constructed up to w ∈ {0, 1} * . Let w ′ be the successor of w in the length-lexicographic order. Note that as w ′ is not empty, it can uniquely be written as w ′ = w ′′ i for some w ′′ ≤ llex w and i ∈ 0, 1. To construct u w ′ , we need to find an element of u w ′′ i{0, 1} * which greater than u w . As u ε is mixed and u w and u w ′′ i are below u ε (below according to the prefix relation), there exists z ∈ {0, 1} * such that u w ′′ iz > u w . We take u w ′ equal to u w ′′ iz.

This establishes the first part of the lemma. The construction of the set U presented above leaves several choices: namely the mixed node we take for u ε and the element of {u w ′′ iz|z ∈ {0, 1} * ∧ u w ′′ iz > u w } we take for u w ′ for each w ′ ∈ {0, 1} + . We have already remarked (on page 20) that we can define a choice function on t by means of an MSO-formula ψ(x, X). The formula states that x is the left-most minimal element of X (minimal with respect to <).

We will show that if for each of the choices in the construction of U we use the choice function defined by ψ we obtain a set U 0 which is MSO-definable in t.

Consider a set U 0 satisfying the following properties:

(1) U 0 induces a well-ordered tree which is isomorphic to t llex ,

(2) the smallest element x 0 of U 0 is chosen by ψ in the set of mixed nodes of t,


Nicolas Travers
email: nicolas.travers@prism.uvsq.fr

Tuyêt-Trâm Dang-Ngoc
email: tuyet-tram.dang-ngoc@u-cergy.fr

Tianxiao Liu
email: tianxiao.liu@u-cergy.fr

XLIVE: INTEGRATING SOURCES WITH XQUERY An efficient XQuery evaluation prototype with TGV

Keywords:

 proposal to rewrite XQuery expressions in "canonical XQuery" in order to support the full XQuery specification. The XQuery expressiveness makes difficulties to obtain an exclusive internal representation within a system. Models based on Tree Patterns have been proposed, and we have extended the tree pattern model to a model called TGV that (a) integrates the whole functionalities of XQuery (b) uses an intuitive representation that provides a global visualization of the request in a mediation context and (c) provides a support for optimization and for cost information. Our paper is based on the XLive mediation system. XLive integrates sources in a uniform view. It is a running research vehicle designed at PRiSM Laboratory for assessing the integration system at every stage of the process starting from sources extraction to the user interface and is already used in several projects. This paper presents XLive, an efficient XQuery processing in a heterogeneous distributed system.

XLIVE ARCHITECTURE

The XLive prototype is designed to be a light mediation system with high modularity and extension capabilities. It is a running research vehicle designed for assessing the integration system at every stage of the process starting from sources extraction to the user interface, including query parsing and modeling, optimization and evaluation, and also benchmarking.

As most mediation systems [START_REF] Wiederhold | Mediators in the Architecture of Future Information Systems[END_REF], XLive is composed of three layers: Presentation, Integration and Sources.

Figure 1 shows the integration system. On the Source Layer, there are multiple heterogeneous data sources (relational/object/XML data sources, webservices, files, etc.) These sources are queryable by the XLive system via wrappers. The Wrapper is a component for accessing a specific Source for query-

Presentation

Source

Integration

Figure 1: XLive Architecture ing and retrieving result. As sources have specific access methods, the role of the wrapper is to translate the wrapper specificity to a common access method. The Integration Layer is the heart of the medi-ation system as it process XQuery requests according to sources and send by the result in XML form. The Wrapper Information Manager is for integrating information about wrapped sources. It provides to the mediator sources metadata, capabilities, and costs statistics on source data. The XQuery Evaluator parses the XQuery query, make logical plans then physical plans by using optimization rules, choose the best execution plan, and then evaluates the execution plan by querying relevant sources and merging results

The XLive system is provide a public API that process an XQuery query and evaluates it on sources, and then return the result as an XML document. Some clients using the XLive API have been implemented on the Presentation Layer: The Console is a graphical interface for managing and querying XLive. The Web service provides services for managing/querying XLive from the Web. And finally, the Benchmark is designed to test the XLive mediator and other sources in order to make comparisons.

More details on the XLive architecture can be found on [START_REF] Dang-Ngoc | Federating Heterogeneous Data Sources with XML[END_REF][START_REF] Dang-Ngoc | XLive: An XML Light Integration Virtual Engine[END_REF]. The TGV model used for XQuery evaluation has been described in [START_REF] Travers | Tree graph view (tgv)[END_REF][START_REF] Travers | Tgv: an efficient model for xquery evaluation within an interoperable system[END_REF]. And a paper describing the TGV annotation method and extensible optimization rules has been submitted to this conference in the paper session.

XQUERY EVALUATION

XQuery is a rich and complex language. Its powerful expression capabilities provide a large range of queries over XML documents. However the richness of the language makes the evaluation of XQueries inefficient in several cases.

Figure 2 describes the evaluation process: (1) XQuery is canonized into a canonical form of XQuery (2) then the canonized XQuery is modeled in the internal structure TGV which can (3) be restructured into equivalent structures using equivalence rules. (4) Then the TGV is annotated with information for evaluation such as the data sources location, cost models information, sources functional capabilities, etc. The optimal annotated TGV is then selected and (5) the logical TGV is transformed into an execution plan using a physical algebra. We have chosen the XAlgebra [START_REF] Dang-Ngoc | Federating Heterogeneous Data Sources with XML[END_REF], an extension of the relational algebra to XML. (6) Finally, the execution plan is evaluated and produces an XML result.

The whole process is implemented in the XLive ( [START_REF] Dang-Ngoc | XLive: An XML Light Integration Virtual Engine[END_REF] system and validates all usecases defined by the W3C that do not imply strong typing consideration (our system recognize 8 of the 9 categories of XQuery).

Table 1 gives an XQuery query example supported by our XQuery processor. It is the query XMP-6 defined in the W3C use-cases document. This query expresses the following request: "For each book that has at least one author, list the title and first two authors, and an empty "et-al" element if the book has additional authors."

XQuery Canonization

XQuery defines complex operations such as aggregation, ordering, nesting/unnesting, document construction, conditional cases (if-then-else), and XPath filter.

To handle such functionalities, a canonical form using simple sequences of FOR...LET...WHERE...ORDER-BY...RETURN (FLWOR) expressions can be used (the demonstration begin in [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns: On efficient Evaluation of XQuery[END_REF] and achieved in [START_REF] Travers | Xquery canonization[END_REF]).

In order to optimize the evaluation of such queries, we propose to structure the language declaration by canonizing it using some transformation rules. These transformation rules keep the semantic of queries and make them more convenient to manipulate.

Table 2 gives the canonized XQuery form of query shown of the example presented in table 1. The following canonization rules have been used:

• Each FLWR-type queries nested in the return clause is redefined in a let clause and is assigned to a variable. In the return clause, the nested queries are replaced by their assigned variable.

• Each aggregate function is redefined in a let clause and is assigned to a variable that replaces the aggregate function in the main expression.

• Each quantifier functions (every and some) is redefined in a let clause and is assigned to a variable that replaces the quantifier functions in the main expression.

• Nested expressions in conditional expressions

If/Then/Else are declared in let clauses with new variables. The conditional expression is rewritten using those variables.

TGV

XQuery modeling is a difficult goal since it provides a large set of functionalities. Its canonization in a canonical form helps us defining a more simple model. Moreover, mediation purpose directs our reflection for modeling in specific Tree Patterns in which all XQuery operations are represented in a single expressive form. Each set of trees defined in canonized queries generates a particular representation. Tree Pattern Queries [START_REF] Sihem | Tree Pattern Query Minimization[END_REF][START_REF] Jagadish | TAX: A Tree Algebra for XML[END_REF] are now well admitted for modeling parts of XML Queries. Works as GTP [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns: On efficient Evaluation of XQuery[END_REF] use the Tree Pattern Query as a basis to model a part of the XQuery specification.

We propose the TGV (Tree Graph View) model which is implemented in the XLive mediator to process XQuery. The TGV model [START_REF] Travers | Tree graph view (tgv)[END_REF][START_REF] Travers | Tgv: an efficient model for xquery evaluation within an interoperable system[END_REF] extends the Tree Pattern representation in order to make it intuitive and full non-typed XQuery support. XQuery queries are modeled in TGV, then optimized, translated to an execution plan and evaluated.

The TGV model allows us to cover 8 of 9 use cases of the W3C (unless strong typing). In fact, specific XQuery characteristics have been integrated into the TGV model by canonization or specific elements. The TGV proposed in figure 3 illustrates the canonized query (table 2). We can identify tree patterns for source document, return document and intermediate structures. On tree patterns are represented by labels, constraints and ascendant-descendant links (simple line for descendant axis, double link otherwise), and a variable is bound. Between trees, hyperlinks represent aggregation, join, projection or condition. More description on TGV are given in [START_REF] Travers | Tree graph view (tgv)[END_REF][START_REF] Travers | Extensible Optimization in an XML Mediator[END_REF].

THE XLIVE SYSTEM

The whole XLive architecture with TGV support and full untyped-XQuery implementation has been released as an Open-Source software 1 .

In the figure 4, we show a XLive screenshot where we see 1 data sources management 2 global schema management 3 an XQuery query 4 the associated logical TGV 5 the associated XAlgebra execution plan and 6 the XML result document.

A benchmark [START_REF] Dragan | Benchmarking an XML Mediator[END_REF] has been created in the context of distributed semistructured model on heterogeneous sources. It has been specified and applied to XLive. It performs comparisons between queries evaluated on single sources and queries evaluated through the mediator. Mediator performance is shown in Figure 5 for a set of representative queries (Selection, projection, join, reconstruction). We use two kinds of XML data in our There is an overhead due to the mediation process compared to single source evaluation. The execution is 1.4 to 2 times slower.

Figure 2 :

 2 Figure 2: XQuery evaluation process <bib>{ for $b in doc("http://bstore1.example.com/bib.xml")//book where count ($b/author) > 0 return <book> {$b/title} {$b/author[position() <= 2]} {if (count ($b/author) > 2) then <et-al/> else ()} </book> }</bib>

  let $r_1 := for $b in doc("http://bstore1.example .com/bib.xml")//book let $r_2 := for $a in $b/author where position

Figure

  Figure 3: TGV

  Figure 4: XLive execution scenarios, data oriented and structure oriented. XLive stores those data in different systems: native XML repositories (XHive, Xyleme), relational systems (Oracle, MySQL) and web sources (Google, Amazon).There is an overhead due to the mediation process compared to single source evaluation. The execution is 1.4 to 2 times slower.

Figure

  Figure 5: Benchmark

Table 1 :

 1 An XQuery query example

Table 2 :

 2 Canonized XQuery query

ACKNOWLEDGEMENTS

The XLive is supported by the ACI Semweb project. The cost model is supported by the ANR PADAWAN project and XCalia S.A.