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

Tuyêt Trâm Dang

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

Untyped XQuery Canonization

Keywords: XQuery evaluation, canonization of XQuery, XQuery processing

XQuery is a powerful language defined by the W3C to query XML documents. Its query functionalities and its expressiveness satisfy the major needs of both the database community and the text and documents community. As an inconvenient, the grammar used to define XQuery is thus very complex and leads to several equivalent query expressions for one same query. This complexity often discourages XQuery-based software developers and designers and leads to incomplete XQuery handling. Works have been done in [DPX04] and especially in [Che04] to reduce equivalent forms of XQuery expressions into identified "canonical forms". However, these works do not cover the whole XQuery specification. We propose in this paper to extend these works in order to canonize the whole untyped XQuery specification.

Introduction

The XQuery [W3C05] query language defined by the W3C has proved to be an expressive and powerful query language to query XML data both on structure and content, and to make transformation on the data. In addition, its query functionalities come from both the database community, and the text community. From the database languages, XQuery has inherited from all data manipulation functionalities such as selection, join, ordering, set manipulation, aggregation, nesting, unnesting, ordering and navigation in tree structure. From the document community, functions as text search, document reconstruction, structure and data queries have been added.

The XQuery query language is expressed using the famous FLWOR (FOR ...exp... LET ...exp... WHERE ...exp... ORDER ...exp... RETURN...exp... ) expression form. But this simple form is not so simple: thus, any expression exp can also be recursively a FLWOR expression but also a full XPath expression.

In Table 1, Query A is a complex XQuery expression that defines a function that selects books with constraints on price, keywords and comments and that returns price and isbn depending on the number of returned titles. This query contains XPath Constraint, Filter, Quantifier, Document construction, Nesting, Aggregate, Conditional and Set operation, Ordering, Sequence and Function. However, by using XQuery specifications, some expressions are found to be equivalents (ie. give the same result independently of the set of input documents). Thus, the Query B in Table 1 is an equivalent form of the previous Query A. Query let $l1 := for $f1 in doc("rev.xml")/review for $f2 in doc("$doc")/catalog return ($f1 | $f2) for $f3 in $l1 for $x in $f3/book let $l2 := for $y in $x/comments where contains ($y, "Excellent") return $y let $l3 := orderby ($x, $x/@isbn) for $ordered in $l3 let $l4 := count ($ordered/title) let $l5 := for $z in doc("books.xml")/book let $l6 := $z/title where $z/@isbn = $ordered/@isbn and $z/position () == 3 return <title>{$l6}</title> where contains($f3, "Robin Hobb") and $x//price > 15 and count ($l2) > 0 return <book> {$ordered/@isbn} <price>{$ordered//price/text()}</price>

{ if ($l4 > 2) then {$l5} else <title/> } </book> } Table 1.
Two equivalent XQuery queries XQuery can generate a large set of equivalent queries. In order to simplify XQuery queries studies, it is useful to identify sets of equivalent queries and associate them with a unique XQuery query called : Canonical query. This decomposition is used in our evaluation model called TGV [START_REF] Travers | TGV: an Efficient Model for XQuery Evaluation within an Interoperable System[END_REF][START_REF] Travers | TGV : a Tree Graph View for Modelling Untyped XQuery[END_REF] in which each canonized expression generates a unique pattern tree. This paper aims at allowing all XQuery representation by adding missing canonization rules (not studied in [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF] and [START_REF] Olteanu | XPath : Looking Forward[END_REF]).

The rest of this paper is organized as follows. The next section describes related works, especially canonical XQuery introduced by [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF]. Section 3 focuses on our extension of [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF]'s work to the canonization of the full untyped XQuery. Section 4 reports on validation of our canonization rules and finally, section 5 concludes.

Related Work

2.1 GALAX GALAX [FSC + 03] is a navigation-based XQuery processing system. It has first propose a full-XQuery support by rewriting XQuery expression in the XQuery core using explicit operation. The major issue of the navigational approach is to evaluate a query as a series of nested loops, whereas a more efficient evaluation plan is frequently possible. Moreover, the nested loop form is not suitable in a system using distributed sources and for identifying dependencies between the sources.

XPath

[OMFB02] proposes some equivalence between XPath axes. Those equivalences define XPaths in a single form with child and descendant expressions. Each "orself " axis is bound to a union operator. A "Parent " or "Ancestor " axis is bound to a new variable with an "exist()" function a child/descendant. Table 2

NEXT

Transformation rules suggested by [START_REF] Deutsch | The NEXT Framework for Logical XQuery Optimization[END_REF] are based on queries minimization of [START_REF] Amer-Yahia | Minimization of Tree Pattern Queries[END_REF] and [START_REF] Ramanan | Efficient Algorithms for Minimizing Tree Pattern Queries[END_REF] in NEXT. They take as a starting point the group-by used in the OQL language, named OptXQuery. In order to eliminate redundancies while scanning elements, NEXT restructures the requests more efficiently to process nested queries. We do not take into account those transformation rules since [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF] proposes transformation rules that create "let " clauses (and not a group by from OQL).

GTP

Works on GTP [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF] propose transformation rules for XQuery queries. Aiming at structuring queries, XQuery queries are transformed in a canonical form of XQuery. The grammar of canonical queries is presented in table 3. This form is more restricted than XQuery specifications, but it allows us to cover a consequent subset of XQuery.

expr ::= ( for $f v1 in range1, ... , $f vm in rangem )? ( let $lv1 := "(" expr1 ")", ... , $lvn := "(" exprn ")" )? ( where ϕ )? return <result> < tag1 >{arg1}< /tag1 > ... < tagn >{argn}< /tagn > < /result> Table 3. Canonical XQuery in GTPs Thus, we obtain a specific syntax that enables us identifying XQuery main properties. These canonized queries must match the following requirements:

-XPath expressions should not contain building filters.

expr expressions are XPaths or canonical XQuery queries.

-Expression ϕ is a Boolean formula created from a set of atomic conditions with XPaths and constants values. -Each range expression must match the definition of a field of value.

-Each range expression is an XPath or an aggregate function.

-Each aggregate function can be only associated to a let clause.

In [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF], it is shown that XQuery queries can always be translated into a canonical form. Lemmas enumerated below show canonical transformation rules.

XPath expressions can contain restrictions included in filters (between "[ ]").

With XQuery specifications, those filters can be replaced by defining new variables that are associated with predicate(s) (within the filter) into the where clause. Table 4 illustrates a transformation of a filter.

XQuery query Canonized form

for $i in doc("cat.xml")/catalog/book [@isbn="12351234"]/title return {$i} for $j in doc("cat.xml")/catalog/book for $i in $j/title where $i/@isbn = "12351234" return {$i} Table 4. Query with filters 2. A FLWR expression with nested queries can be rewritten into an equivalent expression in which FLWR expressions are declared in let clauses. The new declared variable is used instead of the nested query. An example given in table 5 redefined a nested query in the let clause: "let $l: = (...)", and the return value becomes $t.

XQuery query Canonized form

for $i in doc("cat.xml")/catalog/book return <book> {for $j in $i/title return {$j}} </book> for $i in doc("cat.xml")/catalog/book let $l := (for $j in $i/title return {$j}) return <book>{$l}</book> Table 5. Nested queries transformation 3. A FLWR expression with a quantifier "every" can be transformed into an equivalent one using an expression of quantity. XQuery syntax defines quantifiers every as a predicate associated to the Boolean formula ϕ. The quantifier checks if each selected tree verifies the predicate. Table 6 returns all books for which all prices which are strictly higher than 15 euros. In order to simplify and to canonize this query, the "let" clause is created, containing books whose prices are lower or equal than 15 euros. If the number of results is higher than 0, then the selected tree ($i) does not satisfy the quantifier "every" and is not returned.

XQuery query Canonized form

for $i in doc("cat.xml")/catalog/book where every $s in $i/price satisfies $s > 15 return {$i} for $i in doc("cat.xml")/catalog/book let $l :=(for $j in $i/price where $j <= 15 return {$j}) where count($l) = 0 return {$i} Table 6. Transformation of a quantifier "every" 4. In the same way, a FLWR expression, containing a quantifier "some", can be transformed. It is the same transformation, but the tree is selected if there is at least a tree that checks the condition (in the "let" clause). 5. Aggregates functions defined in FLWR expressions can be rewritten in "let" clauses, associated to a new variable. This variable replaces the aggregate function at the previous location.

Table 7 shows transformation of a nested query, an aggregate and a filter.

XQuery query Canonized form

for $y in doc("rev.xml")/review [. contains ("daulphin")]/book where $y/price > 15 return <result> {$y/@isbn} {$y/price} <nb titles>{ for $z in collection ("books")/book where $z/@isbn = $y/@isbn return {count ($z/title)} }</nb titles> </result> for $x in doc("rev.xml")/review, $y in $x/book let $l1 := ( for $z in collection ("books")/book let $l2 := count ($z/title) where $z/@isbn = $y/@isbn return {$l2} ) where $x contains ("dauphin") and $y/price > 15 return <result> {$x/@isbn} {$y/price} <nb titles>{$l1}</nb titles> </result> Thus, we propose some more canonization rules in order to handle those XQuery requirements, making it possible to cover a more consequent set of the XQuery queries. Those new canonization rules will allow us to integrate those expressions in our XQuery representation model: TGV [START_REF] Travers | TGV : a Tree Graph View for Modelling Untyped XQuery[END_REF] (Tree Graph View).

Canonisation

As said in the previous section, transformation rules transform a query into a canonical form. Since, it covers a subset of XQuery; we propose to cover much more XQuery queries. Thus, we add new canonization rules that handle all untyped XQuery queries.

In [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF], five categories of expression are missing: ordering operators, set operators, conditional operators, sequences and function declaration. We thus propose to add canonization rules for each of those expressions.

Ordering (Order by)

Ordering classifies XML trees according to one or more given XPaths. The order of the trees is given by nodes ordering on values, coming from XPaths. This operation takes a set of trees and produces a new ordered set.

Lemma 3.1 : Ordering

An XQuery query containing an Order By clause can be transformed into an equivalent query without this clause. It is declared in a let clause with an aggregate function orderby() whose parameters are ordering fields with XPaths, and the ascending/descending sorting information. The orderby function results a set of sorted trees. The new linked variable replaces original used variables into the return clause. To keep the XML trees flow, a for clause is added on the given variable.

To obtain a canonical query, the order by clause must be transformed into a let clause. In fact, ordering is applied after for, let and where clauses, and before the return clause. Thus, results of preceding operations can be processed by the aggregate function: orderby(). This function orders each XML trees with a given XPath. Then, this aggregate function is put into a let clause, as specified in the canonical form. The new variable replaces all variables contained into the return clause.

Proof: Take a query Q. If Q does not contain an orderby clause, it is then canonical (for the order criteria).

Let us suppose that Q has n orderby clauses: order by $var 1 /path 1 , $var n /path n . Using the transformations lemmas on XPaths, path x are in a canonical form. The query Q is said to be canonical if the orderby clause is replaced by a let clause with an aggregate function orderby, and each transformed corresponding variable.

It is then necessary to study 3 cases of orderby clause:

1. If a variable is declared: order by $var 1 /path 1 return $var 1 /path 2 , then: let $t: = orderby ($var 1 , $var 1 /path 1 ) return $t/path 2 ; 2. If two variables (or more) are declared, but identical: order by $var 1 /path 1 , $var 1 /path 2 return $var 1 /path 3 , then: let $t: = orderby ($var 1 , $var 1 /path 1 , $var 1 /path 2 ) return $t/path 3 ; 3. If two variables (or more) are declared, but different: order by $var 1 /path 1 , $var 2 /path 2 return {$var 1 /path 3 , $var 2 /path 4 }, then: let $t 1 : = orderby ($var 1 , $var 1 /path 1 ), $t 2 : = orderby ($var 2 , $var 2 /path 2 ) return {$t 1 /path 3 , $t 2 /path 4 }.

Then, the (n + 1) th orderby expressions in query Q can be written with n orderby expression, since a query with no orderby expression is canonical, then recursively, Q can be written without orderby clause.

Here is a example of an orderby clause canonization:

XQuery query Canonized form

for $i in /catalog/book order by $i/title return $i/title for $i in /catalog/book let $j := orderby ($i, $i/title) for $k in $j return $k/title In table 8, the f or clause selects a set of book elements contained in catalog. Then, it is sorted by values of the title element, and linked to the $j variable. The orderby clause canonization gives a let clause: $j, whose ordering function orderby() takes the variable $i for the input set, and $i/title to sort. The result set is then defined into the f or clause ($k), in order to build a flow of XML trees. This new variable is used in the return clause by modifying XPaths ($k/title instead of $i/title).

Then, we obtain a canonized query without orderby clauses. This let clause creates a step of evaluation that would be easily identified in the evaluation process.

Set operators

Set operators express unions, differences or intersections on sets of trees. It takes two or more sets of trees to produce a single set. A union operator gathers all sets of trees, a difference operator removes trees of the second set from the first one and an intersection operator keeps only trees that exist in the two sets.

Lemma 3.2 : Set Operator

An XQuery query containing a set operator can be transformed into an equivalent query where the expression is decomposed and contains a let clause with two canonized expressions. The return clause contains the set operator between the two expressions.

Proof: Let's take a query Q. If the query Q does not contain a set operator between two FLWR expressions, then it is known as canonical.

When a query Q contains n + 1 set operators between two expressions (other than variables), using canonization lemmas, we can say that this expressions are canonical. Let's take ξ, the set operator defined as {union, intersect, except} (union, intersection, difference), then the table 9 illustrates the four possibilities of transformation:

Set expression

Canonized expression Comments (expr1 ξ expr2) let $t3 := for $t1 in expr1 each expression is defined by for $t2 in expr2 a new variable. Those are return ($t1 ξ $t2) linked by the operator. (expr1 ξ expr2)/P let $t3 := for $t1 in expr1

The expression is broken up. for $t3 in expr2 1) the set operator return ($t1 ξ $t2) 2) the expression is replaced by ... $t3/P the variable. $XP (P1 ξ P2) for $tx in XP A new variable is created. let $t3 := for $t1 in $tx/P1

Apply the set operator (rule 1) for $t2 in $tx/P2 on the new variable return ($t1 ξ $t2) $XP (P1 ξ P2)/P3

for $tx in XP Use the second and third let $t3 := for $t1 in $tx/P1 decomposition rule on set for $t2 in $t2/P2 expressions between XP et P3 return ($t1 ξ $t2) ... $t3/P 10, the f or clause contains a union "|" between two sets. The first set is /catalog and the second one /review. On each one, the book element is selected. The title is then projected for each book. The canonization of the union operator (shortened "|") gives a let clause ($i 3 ) containing two expressions $i 1 and $i 2 . Each one is defined by a f or clause on expected paths. The let clause $i 3 returns the union of the two variables. Then, the XML trees flow is rebuilt by the f or clause i 3 on the book element. We then obtain a canonized query where set operators are decomposed to detail each step of the procedure.

Conditional operators

Conditional operators bring operational processing on XML documents. Indeed, results of conditional operators depend on a given predicate. Then, the first result is returned if the constraint is true, the second one else. In the possible results, we can find XPath expressions, nested queries, tags or strings. In the case of nested queries, it is then necessary to canonize them to create a single canonized form.

Lemma 3.3 : Conditional Operators

An XQuery query containing a conditional operator (if/then/else) and a nested query, this one can be transformed into an equivalent query where the nested query will be declared in a clause let.

This lemma can be demonstrated in the same way of unnested queries [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF] (section 2.4). Thus, recursively, we are being able to show that any query containing a nested query in a conditional operator can be canonized.

Here is a canonization example of a query with a conditional operator:

XQuery query Canonized form

for $i in /catalog/book return {if contains ($i/author, "Hobb") then ( for $j in $i//title return $j ) else ( $i/author )} for $i in /catalog/book let $l := for $j in $i//title return $j return {if contains ($i/author, "Hobb") then ( $l ) else ( $i/author )} Table 11. Canonization example of conditional operators In table 11, a conditional operator is declared in the return clause with a constraint on the author's name that must contain the word Hobb. If the word is contained, the nested query $j returns the title(s) of book else the author is returned. We obtain a canonized query where nested queries in conditional operators are set in a let clause.

In this paper, we have extended the works of [START_REF] Olteanu | XPath : Looking Forward[END_REF] and [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF] in order to recognize the full untyped XQuery specification.

We claim that thanks to our canonization rules, all works that aim to manipulate XQuery could handle the full untyped XQuery specification with only a minimal XQuery subset to recognize. Especially for our TGV model [START_REF] Travers | TGV: an Efficient Model for XQuery Evaluation within an Interoperable System[END_REF][START_REF] Travers | TGV : a Tree Graph View for Modelling Untyped XQuery[END_REF] which is a simple translation from canonized XQuery queries [START_REF] Travers | An extensible rule transformation model for xquery optimization[END_REF].

Adding typing to the canonized form needs some works using typing consideration [START_REF] Gottlob | The complexity of XPath query evaluation and XML typing[END_REF] on validated XML document. We are currently working on this issue.

This work has been implemented as a module in the XLive mediation system that evaluates any XQuery query on distributed heterogeneous sources.

  illustrates some canonization of XPath axis.

	XPath with specific axis	Canonized XPath
	for $i in //a/parent::b	for $i in //b
		where exists ($i/a)
	for $i in //a/ancestor::b	for $i in //b
		where exists ($i//a)
	for $i in //a/descendant-or-self::b	for $i in //a(//b | /. )
	for $i in //a/ancestor-or-self::b	for $k1 in //b
		for $k2 in $k1//a
		for $i in ($k1 | $k2)

Table 2 .

 2 XPath canonization

Table 7 .

 7 Canonization of a nested query, an aggregate Function and a filter As we can see, rules minimization[START_REF] Deutsch | The NEXT Framework for Logical XQuery Optimization[END_REF] and canonization[START_REF] Olteanu | XPath : Looking Forward[END_REF] [Che04] helps at transforming XQuery queries into a canonical form. The[START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF] approach is more likely to deal with our needs, but it does not handle: Ordering operators, Set operators, Conditional operators, Sequences and Functions declaration.

Table 8 .

 8 Orderby canonization example

Table 9 .

 9 Transformation of different set expressionsThus, a query Q that contains n + 1 set operators between two expressions can be rewritten with n set operators. If there are no set operators, it is canonical. Then, recursively, any query Q can be canonized without set operators.Here a canonization example of a set expression:

	XQuery query	Canonized form
		let $i3 :=
		for $i1 in /catalog
	for $i in (/catalog | /review)/book	for $i2 in /review
	return $i/title	return ($i1 | $i2)
		for $i in $i3/book
		return $i/title

Table 10 .

 10 Canonization of a set expressionIn table

Acknowledgement This work is supported by the ACI Semweb and the ANR PADAWAN projects. The research prototype XLive system is an Open Source software and can be downloaded on : http : //www.prism.uvsq.f r/users/ntravers/xlive

Sequences are sets of elements on which operations are applied. Indeed, when a constraint is applied on a sequence using brackets (XPath), the constraint is applied on the set of the trees defined by XPath (and not on each one). This operation gathers sets of trees in order to produce a unique set one which we apply the given constraint.

Lemma 3.4 : Sequences An XQuery query containing a sequence can be rewritten in an equivalent query without sequences. Each sequence is translated in a let clause on which operations are put.

Sequences' filters behave like on current XPaths. They applied on results of the sequence. So, the proof is similar to the filter's one in lemma (2.3.1) of [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF]. Sequences are built by grouping information. Thus any sequence expression is declared in a let clause, generating a new variable that could be used in the remaining query.

XQuery query

Canonized form 12, a sequence is defined in the f or clause. The catalog's book set is aggregated. Then the second book element is selected (and not the second element of each set). Then, its title is projected. The canonization step produces a let clause in which the f or clause is declared on required elements. Then, the new variable is used in the f or clause $i with a constraint on position. Finally, the title is returned.

Functions

Function definition is useful to define a query that could be re-used many times, or to define queries with parameters. In XQuery, functions take parameters in input and a single set in output. Inputs and output are typed.

Lemma 3.5 : Functions

An XQuery function containing an XQuery expression can be rewritten in an equivalent function containing a canonical expression.

In Table 13, a function is defined (local: section) with a parameter in input. This input is defined by the f or clause: for $f in doc("catalog.xml")/catalog, which set of trees will be used in the called function: local:section ($f ). In the function, each book element returns its title, and the set of all the titles contained in the sections ($/section/title). As we can see, the function contains a nested query. The unnesting canonization step transforms the query into a canonized form inside the function.

XQuery query

Canonized form

Canonical XQuery

Thus, using the previous lemmas and those proposed by [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On Efficient Evaluation of XQuery[END_REF], we can cover a broad set of expressions over XQuery. We can now cover: 1 XPath expressions with filters 2 f or, let and return clauses 3 Predicates in the where clause 4 Nested queries 5 Aggregate functions 6 Quantifiers 7 Ordering operators 8 Set operators 9 Conditional operators 10 Sequences 11 Definition of functions. The only part of XQuery we do not consider yet is typing. Adding typing to the canonized form needs some works using XQuery/XPath typing consideration [START_REF] Gottlob | The complexity of XPath query evaluation and XML typing[END_REF] on validated XML document.

Table 14 summarizes the additional canonization rules we propose. Those rules allow us to cover all untyped XQuery queries.

Expressions

Canonical Form R1 order by var/xp ⇒ let $l1 := orderby(var, var/xp) R2 (expr1 union expr2)

⇒ let $i3 := for $i1 in expr1, $i2 in expr2 return ($i1 union $i2) (expr1 intersect expr2) ⇒ let $i3 := for $i1 in expr1, $i2 in expr2 return ($i1 intersect $i2) (expr1 except expr2) ⇒ let $i3 := for $i1 in expr1, $i2 in expr2 return ($i1 except $i2) R3 if expr1 let $l1 := expr2, $l2 := expr3 then expr2

⇒ if expr1 then $l1 else $l2 else expr3

(if each expr2 and expr3 are nested queries) R4 (expr1)/expr2

⇒ let $l1 := expr1 ... $l1/expr2 With all previous lemmas, we can infer theorem 3.1 that defines a grammar for canonical XQuery queries (Table 15). We can see that canonical queries start with a FLWR expression Expr and zero or more functions. The canonical form of Expr is composed of nested queries, aggregate functions, XPaths and non-aggregate functions. Moreover, set operators are integrated in these expressions, while the conditional operations are integrated into ReturnClause. The Declaration has also a canonical form that prevents any nested expressions. XPaths do not contained anymore filters, sequences, nor set operators, since those are canonized.

XQuery ::= (F unction)* FLWR; FLWR ::= ( "for" "$" STRING " in " Declaration (, "$" STRING " in " Declaration)* | "let" "$" STRING "::=" "(" Expr ")" (, "$" STRING "::=" "(" Expr ")")* )+ ("where" P redicate ( ( "and" | "or" ) P redicate )*)? "return " ReturnClause ; ReturnClause ::= "{" CanonicExpr "}"

| "{" "if" P redicate "then" "(" Expr ")" "else" "(" Expr ")" "}" | "<" STRING ">" ( ReturnClause )* "</" STRING ">" ; "@" QN ame; QName ::= (STRING ":")? STRING; Function ::= "declare function" QName "(" "$" STRING "as" "element" ("," "$" STRING "as" "element")* ")" "as" "element" "{" FLWR "}";

Table 15. Untyped Canonical XQuery

Validation

The use cases listed in Table 16 were created by the XML Query Working Group to illustrate important applications for an XML query language. Each use case is focused on a specific application area. Each use case specifies a set of queries that might be applied to the input data, and the expected results for each query. They are designed to cover the most part of XQuery specification. We have already implemented the XQuery canonization in our XML-based mediation system: XLive [START_REF] Travers | XLive : Integrating Source With XQuery[END_REF]. With the canonization, the XQuery processor has been easier to design and implement, and any untyped XQuery can be evaluated with XLive.


Luca Aceto

Arnaud Carayol

Zoltán Ésik

Anna Ingólfsdóttir

Algebraic Synchronization Trees and Processes ⋆

We study algebraic synchronization trees, i.e., initial solutions of algebraic recursion schemes over the continuous categorical algebra of synchronization trees. In particular, we investigate the relative expressive power of algebraic recursion schemes over two signatures, which are based on those for Basic CCS and Basic Process Algebra, as a means for defining synchronization trees up to isomorphism as well as modulo bisimilarity and language equivalence. The expressiveness of algebraic recursion schemes is also compared to that of the low levels in the Caucal hierarchy.

Introduction

The study of recursive program schemes is one of the classic topics in programming language semantics. (See, e.g., [START_REF] De Bakker | Recursive Procedures[END_REF][START_REF] Courcelle | Fundamental Properties of Infinite Trees[END_REF][START_REF] Guessarian | Algebraic Semantics[END_REF][START_REF] Scott | The Lattice of Flow Diagrams[END_REF] for some of the early references.) In this paper, we study recursion schemes from a process-algebraic perspective and investigate the expressive power of algebraic recursion schemes over the signatures of Basic CCS [START_REF] Milner | Communication and Concurrency[END_REF] and of Basic Process Algebra (BPA) [START_REF] Baeten | Process Algebra: Equational Theories of Communicating Processes[END_REF] as a way of defining possibly infinite synchronization trees [START_REF] Milner | A Calculus of Communicating Systems[END_REF], which are essentially edge-labelled trees with a distinguished exit label ex. As depicted here, this exit label can only occur on edges whose target is a leaf. Both these signatures allow one to describe every finite synchronization tree and include a binary choice operator +. The difference between them is that the signature for Basic CCS, which is denoted by Γ in this pa- per, contains a unary action prefixing operation a. for each action a, whereas the signature for BPA, which we denote by ∆, has one constant a for each action that may label the edge of a synchronization tree and offers a full-blown sequential composition, or sequential product, operator. Intuitively, the sequential product t • t ′ of two synchronization trees is obtained by appending a copy of t ′ to the leaves of t that describe successful termination of a computation. In order to distinguish successful and unsuccessful termination, both the signatures Γ and ∆ contain constants 0 and 1, which denote unsuccessful and successful termination, respectively. An example of a regular recursion scheme over the signature ∆ is

• • • • • • • • • • a a
X = (X • a) + a, (1)
and an example of an algebraic recursion scheme over the signature Γ is

F 1 = F 2 (a.1), F 2 (v) = v + F 2 (a.v). (2)
The synchronization tree defined by these two schemes is depicted on page 1. In the setting of process algebras such as CCS [START_REF] Milner | Communication and Concurrency[END_REF] and ACP [START_REF] Baeten | Process Algebra: Equational Theories of Communicating Processes[END_REF], synchronization trees are a classic model of process behaviour. They arise as unfoldings of labelled transition systems (LTSs) that describe the operational semantics of process terms and have been used to give denotational semantics to process description languages-see, for instance, [START_REF] Abramsky | A Domain Equation for Bisimulation[END_REF]. Regular synchronization trees over the signature Γ are unfoldings of processes that can be described in the regular fragment of CCS, which is obtained by adding to the signature Γ a facility for the recursive definition of processes. On the other hand, regular synchronization trees over the signature ∆ are unfoldings of processes that can be described in Basic Process Algebra (BPA) [START_REF] Baeten | Process Algebra: Equational Theories of Communicating Processes[END_REF] augmented with constants for the deadlocked and the empty process as well as recursive definitions. For example, the tree that is defined by (1) is ∆-regular.

As is well known, the collection of regular synchronization trees over the signature ∆ strictly includes that of regular synchronization trees over the signature Γ even up to language equivalence. Therefore, the notion of regularity depends on the signature. But what is the expressiveness of algebraic recursion schemes over the signatures Γ and ∆? The aim of this paper is to begin the analysis of the expressive power of those recursion schemes as a means for defining synchronization trees, and their bisimulation or language equivalence classes.

In order to characterize the expressive power of algebraic recursion schemes defining synchronization trees, we interpret such schemes in continuous categorical Γ -and ∆-algebras of synchronization trees. Continuous categorical Σalgebras are a categorical generalization of the classic notion of continuous Σalgebra that underlies the work on algebraic semantics [START_REF] Goguen | Initial algebra semantics and continuous algebras[END_REF][START_REF] Guessarian | Algebraic Semantics[END_REF], and have been used in [START_REF] Bloom | The Equational Theory of Regular Words[END_REF][START_REF] Bloom | A Mezei-Wright Theorem for Categorical Algebras[END_REF][START_REF] Ésik | Continuous Additive Algebras and Injective Simulations of Synchronization Trees[END_REF] to give semantics to recursion schemes over synchronization trees and words. (We refer the interested reader to [START_REF] Milius | The Category-Theoretic Solution of Recursive Program Schemes[END_REF] for a recent discussion of category-theoretic approaches to the solution of recursion schemes.) In this setting, the Γ -regular (respectively, Γ -algebraic) synchronization trees are those that are initial solutions of regular (respectively, algebraic) recursion schemes over the signature Γ . ∆-regular and ∆-algebraic synchronization trees are defined in similar fashion.

Our first contribution in the paper is therefore to provide a categorical semantics for first-order recursion schemes that define processes, whose behaviour is represented by synchronization trees. The use of continuous categorical Σalgebras allows us to deal with arbitrary first-order recursion schemes; there is no need to restrict oneself to, say, 'guarded' recursion schemes, as one is forced to do when using a metric semantics (see, for instance, [START_REF] Van Breugel | An Introduction to Metric Semantics: Operational and Denotational Models for Programming and Specification Languages[END_REF] for a tutorial introduction to metric semantics), and this categorical approach to giving semantics to first-order recursion schemes can be applied even when the order-theoretic framework either fails because of the lack of a 'natural' order or leads to undesirable identities.

As a second contribution, we provide a comparison of the expressive power of regular and algebraic recursion schemes over the signatures Γ and ∆, as a formalism for defining processes described by their associated synchronization trees up to isomorphism, bisimilarity [START_REF] Milner | Communication and Concurrency[END_REF][START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF] and language equivalence. Moreover, we compare the expressiveness of those recursion schemes to that of the low levels in the Caucal hierarchy. (As a benefit of the comparison with the Caucal hierarchy, we obtain structural properties and decidability of Monadic Second-Order Logic [START_REF] Thomas | Constructing Infinite Graphs with a Decidable MSO-theory[END_REF].) In the setting of language equivalence, the notion of Γ -regularity corresponds to the regular languages, the one of ∆-regularity corresponds to the context-free languages and ∆-algebraicity corresponds to the macro languages [START_REF] Fischer | Grammars with Macro-like Productions[END_REF], which coincide with the languages generated by Aho's indexed grammars [START_REF] Aho | Indexed Grammars -an Extension of Context-Free Grammars[END_REF]. We present a pictorial summary of our expressiveness results on Figure 1. Moreover, we prove that the synchronization tree that is the unfolding of the bag (also known as multiset) over a binary alphabet depicted on Figure 2 is not Γ -algebraic, even up to language equivalence, and that it is not ∆-algebraic up to bisimilarity. These results are a strengthening of a classic theorem from the literature on process algebra proved by Bergstra and Klop in [START_REF] Bergstra | The Algebra of Recursively Defined Processes and the Algebra of Regular Processes[END_REF].

In order to obtain a deeper understanding of Γ -algebraic recursion schemes, as a final main contribution of the paper, we characterize their expressive power by following the lead of Courcelle [START_REF] Courcelle | A Representation of Trees by Languages I and II[END_REF][START_REF] Courcelle | Fundamental Properties of Infinite Trees[END_REF]. In those references, Courcelle proved that a term tree is algebraic if, and only if, its branch language is a deterministic context-free language. In our setting, we associate with each synchronization tree with bounded branching a family of branch languages and we show that a synchronization tree with bounded branching is Γ -algebraic if, and only if, the family of branch languages associated with it contains a deterministic contextfree language (Theorem 2). In conjunction with standard tools from formal language theory, this result can be used to show that certain synchronization trees are not Γ -algebraic.

The paper is organized as follows. In Section 2, we recall the notion of continuous categorical Σ-algebra. Synchronization trees are defined in Section 3, together with the signatures Γ and ∆ that contain the operations on those trees that we use in this paper. We introduce regular and algebraic recursion schemes,

Γ -alg. = Tree2 = ∆-reg. Tree3 = ∆-alg. Tree1 = Graph1 = Γ -reg. (a) ∆-reg. Γ -alg. = Tree2 ∆-alg. Graph 3 Tree1 = Graph1 = Γ -reg. (b) Tree2 ∆-reg.
Γ -alg.

∆-alg.

Graph 3 Tree1 = Graph1 = Γ -reg. (c)
Fig. 1. The expressiveness hierarchies up to language equivalence (a), up to bisimilarity (b) and up to isomorphism (c) as well as their initial solutions, in Section 4. Section 5 studies the expressive power of regular and algebraic recursion schemes over the signatures Γ and ∆. In Section 6, following Courcelle, we characterize the expressive power of Γalgebraic recursion schemes by studying the branch languages of synchronization trees whose vertices have bounded outdegree.

Continuous Categorical Algebras

In this section, we recall the notion of continuous categorical Σ-algebra. Continuous categorical Σ-algebras were used in [START_REF] Bloom | The Equational Theory of Regular Words[END_REF][START_REF] Bloom | A Mezei-Wright Theorem for Categorical Algebras[END_REF][START_REF] Ésik | Continuous Additive Algebras and Injective Simulations of Synchronization Trees[END_REF] to give semantics to recursion schemes over synchronization trees and words.

Let Σ = n≥0 Σ n be a ranked set (or 'signature'). A categorical Σ-algebra is a small category A equipped with a functor σ A :

A n → A for each σ ∈ Σ n , n ≥ 0. A morphism between categorical Σ-algebras A and B is a functor h : A → B such that, for each σ ∈ Σ n , the diagram B n B σ B / / A n B n h n A n A σ A / / A B h commutes up to a natural isomorphism π σ .
Here, the functor h n : A n → B n maps each object and morphism (x 1 , . .

. , x n ) in A n to (h(x 1 ), . . . , h(x n )) in B n .
A morphism h is strict if, for all σ ∈ Σ, the natural isomorphism π σ is the identity. Suppose that A is a categorical Σ-algebra. We call A continuous if A has a distinguished initial object (denoted ⊥ A or 0 A ) and colimits of all ω-diagrams (f k : a k → a k+1 ) k≥0 . Moreover, each functor σ A is continuous, i.e., preserves colimits of ω-diagrams. Thus, if σ ∈ Σ 2 , say, and if

x 0 f0 → x 1 f1 → x 2 f2 → . . . and y 0 g0 → y 1 g1 → y 2 g2 → . . . are ω-diagrams in A with colimits (x k φ k → x) k and (y k ψ k → y) k , respectively, then σ A (x 0 , y 0 ) σ A (f0,g0) → σ A (x 1 , y 1 ) σ A (f1,g1) → σ A (x 2 , y 2 ) σ A (f2,g2) → . . . has colimit (σ A (x k , y k ) σ A (φ k ,ψ k ) → σ A (x, y)) k .
A morphism of continuous categorical Σ-algebras is a categorical Σ-algebra morphism that preserves the distinguished initial object and colimits of all ωdiagrams. Below we will often write just σ for σ A , in particular when A is understood.

For later use, we note that if A and B are continuous categorical Σ-algebras then so is

A × B. Moreover, for each k ≥ 0, the category [A k → A] of all continu- ous functors A k → A is also a continuous categorical Σ-algebra, where, for each σ ∈ Σ n , σ [A k →A] (f 1 , . . . , f n ) = σ A • f 1 , . . . , f n , with f 1 , . . . , f n standing for the target tupling of the continuous functors f 1 , . . . , f n : A k → A. On natural transformations, σ [A k →A] is defined in a similar fashion. In [A k → A], colimits of ω-diagrams are formed pointwise.

Synchronization Trees

A synchronization tree t = (V, v 0 , E, l) over an alphabet A of 'action symbols' consists of a finite or countably infinite set V of 'vertices' and an element v 0 ∈ V (the 'root'), a set E ⊆ V × V of "edges" and a 'labelling function' l : E → A ∪ {ex}. These data obey the following restrictions.

-(V, v 0 , E) is a rooted tree: for each u ∈ V , there is a unique path v 0 ; u.

-If e = (u, v) ∈ E and l(e) = ex, then v is a leaf, and u is called an exit vertex.

A morphism φ : t → t ′ of synchronization trees is a function V → V ′ that preserves the root, the edges and the labels, so that if (u, v) is an edge of t, then (φ(u), φ(v)) is an edge of t ′ , and l ′ (φ(u), φ(v)) = l(u, v). Morphisms are therefore functional simulations [START_REF] Milner | An Algebraic Definition of Simulation Between Programs[END_REF][START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF]. It is clear that the trees and tree morphisms form a category. The tree that has a single vertex and no edges is initial. It is known that the category of trees has colimits of all ω-diagrams, see [START_REF] Bloom | Iteration Theories[END_REF]. (It also has binary coproducts.) In order to make the category of trees small, we may require that the vertices of a tree form a subset of some fixed infinite set.

The category ST(A) of synchronization trees over A is equipped with two binary operations: + (sum) and • (sequential product or sequential composition), and either with a unary operation or a constant associated with each letter a ∈ A.

The sum t + t ′ of two trees is obtained by taking the disjoint union of the vertices of t and t ′ and identifying the roots. The edges and labelling are inherited. The sequential product t • t ′ of two trees is obtained by replacing each edge of t labelled ex by a copy of t ′ . With each letter a ∈ A, we can either associate a constant, or a unary prefixing operation. As a constant, a denotes the tree with vertices v 0 , v 1 , v 2 and two edges: the edge (v 0 , v 1 ), labelled a, and the edge (v 1 , v 2 ), labelled ex. As an operation, a(t) is the tree a • t, for any tree t. Let 0 denote the tree with no edges and 1 the tree with a single edge labelled ex. On morphisms, all operations are defined in the expected way. For example, if h : t → t ′ and h ′ : s → s ′ , then h + h ′ is the morphism that agrees with h on the nonroot vertices of t and that agrees with h ′ on the nonroot vertices of s. The root of t + s is mapped to the root of t ′ + s ′ .

In the sequel we will consider two signatures for synchronization trees, Γ and ∆. The signature Γ contains +, 0, 1 and each letter a ∈ A as a unary symbol. In contrast, ∆ contains +, •, 0, 1 and each letter a ∈ A as a nullary symbol. It is known that, for both signatures, ST(A) is a continuous categorical algebra. See [START_REF] Bloom | Iteration Theories[END_REF] for details.

Two synchronization trees t = (V, v 0 , E, l) and t ′ = (V ′ , v ′ 0 , E ′ , l ′ ) are bisimilar or bisimulation equivalent [START_REF] Milner | Communication and Concurrency[END_REF][START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF] if there is some symmetric relation R ⊆ (V × V ′ ) ∪ (V ′ × V ) that relates their roots, and such that if (v 1 , v 2 ) ∈ R and there is some edge (v 1 , v ′ 1 ), then there is an equally-labelled edge

(v 2 , v ′ 2 ) with (v ′ 1 , v ′ 2 ) ∈ R.
The path language of a synchronization tree is composed of the words in A * that label a path from the root to the source of an exit edge. Two trees are language equivalent if they have the same path language.

Algebraic Objects and Functors

When n is a non-negative integer, we denote the set {1, . . . , n} by [n].

Definition 1. Let Σ be a signature. A Σ-recursion scheme, or recursion scheme over Σ, is a sequence E of equations

F 1 (v 1 , . . . , v k1 ) = t 1 , . . . , F n (v 1 , . . . , v kn ) = t n ,
where each t i is a term over the signature Σ Φ = Σ ∪Φ in the variables v 1 , . . . , v ki , and Φ contains the symbols F i (sometimes called 'functor variables') of rank

k i , i ∈ [n]. A Σ-recursion scheme is regular if k i = 0, for each i ∈ [n].
Suppose that A is a continuous categorical Σ-algebra, and consider a Σ-recursion scheme of the form given above. Define

A r(Φ) = [A k1 → A] × • • • × [A kn → A].
Then A r(Φ) is a continuous categorical Σ-algebra, as noted in Section 2.

When each F i , i ∈ [n], is interpreted as a continuous functor f i : A ki → A, each term over the extended signature Σ Φ = Σ ∪ Φ in the variables v 1 , . . . , v m induces a continuous functor A m → A that we denote by t A (f 1 , . . . , f n ). In fact, t A is a continuous functor t A : A r(Φ) → [A m → A]. More precisely, we define t A as follows. Let f i , g i denote continuous functors A ki → A, i ∈ [n], and let α i be a natural transformation f i → g i for each i ∈ [n]. When t is the variable v i , say, then t A (f 1 , . . . , f n ) is the ith projection functor A m → A, and t A (α 1 , . . . , α n ) is the identity natural transformation corresponding to this projection functor. Suppose now that t is of the form σ(t 1 , . . . , t k ), where σ ∈ Σ k and t 1 , . . . , t k are terms. Then

t A (f 1 , . . . , f n ) = σ A • h 1 , . . . , h k and t A (α 1 , . . . , α n ) = σ A • β 1 , . . . , β k , where h j = t A j (f 1 , . . . , f n ) and β j = t A j (α 1 , . . . , α n ) for all j ∈ [k].
(Here, we use the same notation for a functor and the corresponding identity natural transformation.) Finally, when t is of the form F i (t 1 , . . . , t ki ), then t A (f 1 , . . . , f n ) = f i • h 1 , . . . , h ki , and the corresponding natural transformation is α i • β 1 , . . . , β ki , where the h j and β j , j ∈ [k i ], are defined similarly as above.

Note that if each α i : f i → f i is an identity natural transformation (so that

f i = g i , for all i ∈ [n]), then t A (α 1 , . . . , α n ) is the identity natural transformation t A (f 1 , . . . , f n ) → t A (f 1 , . . . , f n ).
In any continuous categorical Σ-algebra A, by target-tupling the functors t A i , we obtain a continuous functor

E A : A r(Φ) → A r(Φ) .

Indeed, we have that t

A i : A r(Φ) → [A ki → A], for i ∈ [n], so that E A = t A 1 , . . . , t A n : A r(Φ) → A r(Φ) .
Thus, E A has an initial fixed point in A r(Φ) , unique up to natural isomorphism, that we denote by

|E A | = (|E| A 1 , . . . , |E| A n ), so that, in particular, |E| A i = t A i (|E| A 1 , . . . , |E| A n ), at least up to isomorphism, for each i ∈ [n].
Definition 2. Suppose that A is a continuous categorical Σ-algebra. We say that f : A m → A is Σ-algebraic, if there is a recursion scheme E such that f is isomorphic to |E| A 1 , the first component of the above-mentioned initial solution of E. When m = 0, we identify a Σ-algebraic functor with a Σ-algebraic object. Last, a Σ-regular object is an object isomorphic to the first component of the initial solution of a Σ-regular recursion scheme.

In particular, we get the notions of Γ -algebraic and Γ -regular trees, and ∆algebraic and ∆-regular trees.

Example 1. The ∆-regular recursion scheme (1) and the Γ -algebraic one (2) have the infinitely branching tree i≥1 a i depicted on page 1 as their initial solutions. That tree is therefore both ∆-regular and Γ -algebraic. So ∆-regular and Γ -algebraic recursion schemes can be used to define infinitely branching trees that have an infinite number of subtrees, even up to language equivalence.

Comparing the Expressiveness of Classes of Recursion Schemes

In this section, we interpret recursion schemes over the continuous categorical algebra ST(A), viewed either as a Γ -algebra or as a ∆-algebra, and study the expressive power of classes of recursion schemes over the signatures Γ and ∆. It is clear that every Γ -regular tree is ∆-regular and that the inclusion is proper, since every Γ -regular tree has, up to isomorphism, only a finite number of subtrees, see [START_REF] Bloom | Iteration Theories[END_REF][START_REF] Milner | A Calculus of Communicating Systems[END_REF], while there exist ∆-regular and Γ -algebraic trees that do not have this property (see Example 1). The strict inclusion also holds with respect to strong bisimulation equivalence or language equivalence. It is well-known that the languages of synchronization trees defined by Γ -regular schemes are the regular languages. On the other hand, modulo language equivalence, ∆-regular schemes are nothing but context-free grammars and have the same expressive power as Γ -algebraic schemes (see Theorem 1(1) and ( 4) below).

The ∆-regular trees that can be defined using regular ∆-recursion schemes that do not contain occurrences of the constants 0 and 1 correspond to unfoldings of the labelled transition systems denoted by terms in Basic Process Algebra (BPA) with recursion, see, for instance, [START_REF] Baeten | Process Algebra: Equational Theories of Communicating Processes[END_REF][START_REF] Bergstra | The Algebra of Recursively Defined Processes and the Algebra of Regular Processes[END_REF]. Indeed, the signature of BPA contains one constant symbol a for each action as well as the binary + and • operation symbols, denoting nondeterministic choice and sequential composition, respectively. (Below, we write BPA for 'BPA with recursion'.) Alternatively, following [START_REF] Moller | Infinite Results[END_REF], one may view BPA as the class of labelled transition systems associated with context-free grammars in Greibach normal form in which only leftmost derivations are permitted. The class of Basic Parallel Processes (BPP) is a parallel counterpart of BPA introduced by Christensen [START_REF] Christensen | Decidability and decomposition in process algebras[END_REF]. We refer the interested readers to [START_REF] Moller | Infinite Results[END_REF] for the details of the formal definitions, which are not needed to appreciate the results to follow, and further pointers to the literature.

In the results to follow, we will compare the expressiveness of recursion schemes to that of the low levels in the Caucal hierarchy [START_REF] Radhakrishnan | On Infinite Terms Having a Decidable Monadic Theory[END_REF]. For the sake of completeness, following [START_REF] Carayol | The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-order Pushdown Automata[END_REF], we recall that Tree 0 and Graph 0 denote the collections of finite, edge-labelled trees and graphs, respectively. Moreover, for each n ≥ 0, Tree n+1 stands for the collection of unfoldings of graphs in Graph n , and the graphs in Graph n+1 are those that can be obtained from the trees in Tree n+1 by applying a monadic interpretation (or transduction). It is well known that Graph 1 is the class of all prefix-recognizable graphs [START_REF] Rytter | On Infinite Transition Graphs Having a Decidable Monadic Theory[END_REF].

The following theorem collects our main results on the expressiveness of recursion schemes over the signatures ∆ and Γ . A pictorial summary of all our expressiveness results may be found on Figure 1. All the inclusions on that figure are strict, with the possible exception of the inclusion of the collection of the ∆algebraic trees in Graph 3 up to bisimilarity and up to isomorphism. To the best of our knowledge, it is open whether those inclusions are strict. The fact that the path language of every synchronization tree in Tree 3 (respectively, Tree 2 ) is an indexed language (respectively, context-free language) is known from [START_REF] Carayol | The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-order Pushdown Automata[END_REF]Theorem 4].

Theorem 1.

1. Every ∆-regular tree is Γ -algebraic. 2. There is a Γ -algebraic synchronization tree that is not bisimilar to any ∆regular tree. Moreover, there is a Γ -algebraic synchronization tree that is neither definable in BPA modulo bisimilarity nor in BPP modulo language equivalence. 3. Each synchronization tree in Tree 2 is Γ -algebraic, but there is a ∆-regular (and hence Γ -algebraic) synchronization tree that is not in Tree 2 . 4. Every Γ -algebraic synchronization tree is bisimilar to a tree in Tree 2 . Therefore, modulo bisimilarity, the Γ -algebraic synchronization trees coincide with those in Tree 2 . Moreover, each Γ -algebraic synchronization tree is language equivalent to a ∆-regular one. 5. Each ∆-algebraic synchronization tree is in Graph 3 and hence has a decidable monadic second-order theory. Moreover, there is a ∆-algebraic synchronization tree that does not belong to Tree 3 . 6. The synchronization tree t bag associated with the bag over a binary alphabet depicted on Figure 2 has an undecidable monadic second-order theory (even without the root being the source of an exit edge). Hence, it is not in the Caucal hierarchy and is therefore not ∆-algebraic, even up to bisimilarity. Moreover, t bag is not Γ -algebraic up to language equivalence. 7. There exists a Γ -algebraic synchronization tree whose minimization with respect to bisimilarity does not have a decidable monadic second-order theory and hence is not in the Caucal hierarchy. Statement 6 in the above theorem is a strengthening of a classic result from the literature on process algebra proved by Bergstra and Klop in [START_REF] Bergstra | The Algebra of Recursively Defined Processes and the Algebra of Regular Processes[END_REF]. Indeed, in Theorem 4.1 in [START_REF] Bergstra | The Algebra of Recursively Defined Processes and the Algebra of Regular Processes[END_REF], Bergstra and Klop showed that the bag over a domain of values that contains at least two elements is not expressible in BPA, and the collection of synchronization trees that are expressible in BPA is strictly included in the ∆-algebraic synchronization trees. Thomas showed in [START_REF] Thomas | A Short Introduction to Infinite Automata[END_REF]Theorem 10] that the monadic second-order theory of the infinite two-dimensional grid is undecidable. However, we cannot use that result to prove that the synchronization tree t bag has an undecidable monadic second-order theory. Indeed, the unfolding of the infinite two-dimensional grid is the full binary tree, which has a decidable monadic second-order theory.

• • • b o o '&%$ !"# d O O a / / c '&%$ !"# d O O a / / b o o c '&%$ !"# d O O a / / b o o c '&%$ !"# d O O c a / / b o o • • • b o o '&%$ !"# d O O a / / c '&%$ !"# d O O a / / b o o c '&%$ !"# d O O a / / b o o c '&%$ !"# d O O a / / b o o c • • • b o o . . . d O O . . . d O O . . . d O O . . . d O O . . .
Finally, we remark that Theorem 1 [START_REF] Bloom | Iteration Theories[END_REF] yields that the collection of synchronization trees in the Caucal hierarchy is not closed under quotients with respect to bisimilarity. Indeed, there is a Γ -algebraic tree whose quotient with respect to bisimilarity is not in the Caucal hierarchy. Nevertheless the result is sort of folklore.

Branch Languages of Bounded Synchronization Trees

Call a synchronization tree bounded if there is a constant k such that the outdegree of each vertex is at most k. Our aim in this section is to offer a language-theoretic characterization of the expressive power of Γ -algebraic recursion schemes defining synchronization trees. We shall do so by following Courcelle-see, e.g., [START_REF] Courcelle | Fundamental Properties of Infinite Trees[END_REF]-and studying the branch languages of bounded synchronization trees. More precisely, we assign a family of branch languages to each bounded synchronization tree over an alphabet A and show that a bounded tree is Γ -algebraic if, and only if, the corresponding language family contains a deterministic context-free language (DCFL). Throughout this section, we will call Γ -algebraic trees just algebraic trees, and similarly for regular trees. Definition 3. Suppose that t = (V, v 0 , E, l) is a bounded synchronization tree over the alphabet A. Denote by k the maximum of the outdegrees of the vertices of t. Let B denote the alphabet A × [k]. A determinization of t is a tree t ′ = (V, v 0 , E, l ′ ) over the alphabet B which differs from t only in the labelling as follows. Suppose that v ∈ V with outgoing edges (v, v 1 ), . . . , (v, v ℓ ) labelled a 1 , . . . , a ℓ ∈ A ∪ {ex} in t. Then there is some permutation π of the set [ℓ] such that the label of each (v, v i ) in t ′ is (a i , π(i)).

Consider a determinization t ′ of t. Let v ∈ V and let v 0 , v 1 , . . . , v m = v denote the vertices on the unique path from the root to v. The branch word corresponding to v in t ′ is the alternating word

k 0 (a 1 , i 1 )k 1 . . . k m-1 (a m , i m )k m
where k 0 , . . . , k m denote the outdegrees of the vertices v 0 , . . . , v m , and for each j ∈ [m], (a j , i j ) is the label of the edge (v j-1 , v j ) in t ′ . The branch language L(t ′ ) corresponding to a determinization t ′ of t consists of all the branch words of t ′ . Finally, the family of branch languages corresponding to t is: L(t) = {L(t ′ ) : t ′ is a determinization of t}.

By way of example, consider the LTS depicted in Figure 2. The synchronization tree t bag that is obtained by unfolding this LTS from its start state is bounded. In fact, the outdegree of each non-leaf node is three. The branch words corresponding to the nodes of any determinization of the tree t bag have the form 3(a 1 , i 1 )3 . . . 3(a m , i m )k m ,

where k m is either 3 or 0, i 1 , . . . , i m ∈ [3] and a 1 . . . a m is a word with the property that, in any of its prefixes, the number of occurrences of the letter a is greater than, or equal to, the number of occurrences of the letter b, and the number of occurrences of the letter c is greater than, or equal to, the number of occurrences of the letter d. Moreover, for each j ∈ [m], a j = ex if and only if j = m and k m = 0. (Note that, when a m = ex, the number of a's in a 1 . . . a m-1 equals the number of b's, and similarly for c and d.)

Theorem 2.

1. A bounded synchronization tree t is algebraic (respectively, regular) if, and only if, L(t) contains a DCFL (respectively, regular language). 2. The bounded synchronization trees in Tree 2 are the bounded Γ -algebraic synchronization trees.

Using statement 2 in the above theorem, we can show that Figure 1(b) also applies for bounded synchronization trees. The language-theoretic characterization of the class of bounded algebraic synchronization trees offered in Theorem 2 can be used to prove that certain trees are not algebraic. For example, consider the following ∆-algebraic scheme:

F 0 = F (1), F (v) = a • F (b • v) + v • c • v • 0.
Given any determinization of the synchronization tree t defined by this scheme, the non-context-free language {a n b n cb n : n ≥ 0} is a homomorphic image of the intersection of its branch language with a regular language. Thus t is not Γ -algebraic.

Fig. 2 .

 2 Fig. 2. An LTS whose unfolding is not a ∆-algebraic synchronization tree

  Luca Aceto and Anna Ingólfsdóttir have been partially supported by the project 'Meta-theory of Algebraic Process Theories' (nr. 100014021) of the Icelandic Research Fund. Arnaud Carayol has been supported by the project AMIS (ANR 2010 JCJC 0203 01 AMIS). Zoltán Ésik has been partially supported by the project T ÁMOP-4.2.1/B-09/1/KONV-2010-0005 'Creating the Center of Excellence at the University of Szeged', supported by the European Union and co-financed by the European Regional Fund, and by the National Foundation of Hungary for Scientific Research, grant no. K 75249. Zoltán Ésik's work on this paper was also partly supported by grant T10003 from Reykjavik University's Development Fund and a chair from the LabEx Bézout.

	a
	ex a	a
	ex	a
	ex

⋆ A full version of this paper may be found at http://www.ru.is/faculty/luca/ PAPERS/algsynch.pdf.


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

Tuyêt Trâm Dang

AN EXTENSIBLE RULE TRANSFORMATION MODEL FOR XQUERY OPTIMIZATION Rules Pattern for XQuery Tree Graph View

Keywords:

-has extended the Tree Pattern representation in order to make it more intuitive, respect full XQuery specification and got support to be manipulated, optimized and then evaluated. For optimization, a search strategy is needed. It consists in generating equivalent execution plan using extensible rules and estimate cost of plan to find the better one. We propose the specification of extensible rules that can be used in heterogeneous environment, supporting XML and manipulating Tree Patterns.

INTRODUCTION

Efficient evaluation of XML Query Languages has become a crucial issue for XML exchanges and integration [START_REF] Abiteboul | Querying Semistructured Data[END_REF]. XQuery (W3C, 2005) has proved to be an expressive and powerful language to query XML data both on structure and content, and to make transformation on data. In addition, its query functionalities come from both database community (filtering, join, selection, aggregation), and text community (supporting and defining function as text search). However, such functionalities provided by the XQuery language imply complexity that makes its evaluation very difficult.

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.

In previous work [START_REF] Dang-Ngoc | Tree graph view : On efficient evaluation of xquery in an xml mediator[END_REF][START_REF] Travers | TGV : a Tree Graph View for Modelling untyped XQuery[END_REF][START_REF] Travers | TGV : a Tree Graph View for Modelling untyped XQuery[END_REF], we have defined the TGV model that extends the Tree Pattern representation in order to make it intuitive, have full XQuery support and got support to be manipulated, optimized and then evaluated. XQuery queries are modeled with TGV to generate execution plan that will be used to evaluate the XQuery query.

We are interested in providing an extensible framework to optimize XQuery queries' evaluation. Optimizing query evaluation can have different meaning depending on what the user or the application expects. The most popular and important aspect is efficiency or cost. Mainly, cost models referred to time cost (time for evaluating the whole request and provide the result), but also resource cost, energy cost, money cost, etc. But depending on the context, other aspects can be considered instead for an optimized query evaluation, as accuracy on the evaluation as introduced in weighted patterns (Damiani and Tanca, 2000), fuzzy (Damiani et al., 2000) or flexible [START_REF] Calmès | Requêtes flexibles et données semi-structurées -quelques éléments de discussion et d'implémentation[END_REF] queries or right access.

Extensible optimizer were studied in Exodus [START_REF] Carey | The EXODUS Extensible DBMS Project : An Overview[END_REF], Starburst [START_REF] Widom | The Starburst Active Database Rule System[END_REF], Volcano [START_REF] Graefe | The Volcano Optimizer Generator : Extensibility and Efficient Search[END_REF] and OPT++ [START_REF] Kabra | OPT++ : an objectoriented implementation for extensible database query optimization[END_REF]). An extensible optimizer aims at generating a query optimizer by integrating new transformation rules. These rules transform algebraic plans into alternative ones. Extensible optimizers need search strategies to order transformation rules for queries execution. It often relies on cost information as with introduced expected cost factor in [START_REF] Carey | The EXODUS Extensible DBMS Project : An Overview[END_REF] and [START_REF] Graefe | The Volcano Optimizer Generator : Extensibility and Efficient Search[END_REF].

However, these works are designed to relational or object contexts. And as far as we know, those solutions could not be applied on semi-structured data with tree pattern matching queries. So, we define a model for designing transformation rules that would be applied on TGV, to optimize XQuery evaluation.

In this article, we briefly recall the TGV model and annotations on which transformation rules rely on (section 2). In section 3, we present the goal of this article which defines a new model, the rule patterns, which would be integrated in our extensible optimizer. And, finally we conclude.

TREE GRAPH VIEW (TGV)

XQuery is a rich language on XML documents. It defines complex operations such as aggregation, ordering, nesting/unnesting, document construction, conditional cases, sets, sequences, quantifiers, and XPath filter. To handle such functionalities, a canonical form using simple sequences of FOR...LET...WHERE...RETURN (FLWR) expressions equivalent to any XQuery expression can be retrieved (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 | Full Untyped XQuery Canonization[END_REF]).

The canonized XQuery evaluation process relies on our TGV model. Since we focus on TGV transformation rules, we briefly recall the TGV model. Details and Abstract Data Type formalization of the TGV model can be found in [START_REF] Travers | Extensible Optimization in an XML Mediatior[END_REF][START_REF] Travers | TGV : a Tree Graph View for Modelling untyped XQuery[END_REF]. A TGV implementation is downloadable on http://www.prism.uvsq.fr/˜ntravers/xlive/

The TGV model

To manipulate XQuery expressions, a tree logical structure is needed. (Amer-Yahia et al., 2001) has introduced the TPQ model that expresses a single FOR-WHERE-RETURN (FWR) query by a Pattern Tree and a formula. Then, [START_REF] Chen | From Tree Patterns to Generalized Tree Patterns : On efficient Evaluation of XQuery[END_REF] proposes the GTP model that are a generalization of the TPQ model. In this model, each LET clauses generates a Tree Pattern, and one predicate that contains all constraints. The representation acts as a pattern applicable on data sources. However, GTPs do not capture well all XQuery expressiveness and cannot be used in a mediation context. Moreover, it does not support extensible optimization.

We have proposed the TGV model [START_REF] Dang-Ngoc | Tree graph view : On efficient evaluation of xquery in an xml mediator[END_REF][START_REF] Travers | Extensible Optimization in an XML Mediatior[END_REF][START_REF] Travers | TGV : an Efficient Model for XQuery Evaluation within an Interoperable System[END_REF] -Set Hyperlinks (SH) : a set operation between two tree patterns. All these elements are connected together to form a TGV that represents an XQuery query. They are formalized in [START_REF] Travers | Extensible Optimization in an XML Mediatior[END_REF].

Table 1 illustrates an XQuery query which contains a FOR clauses ($x) with a constraint predicate defined in a filter (between "[]"). This constraint selects all documents containing the word "XML". Then, the book attribute "isbn" must not exceed "1526". Finally, the result includes the title of the book and authors if only there is more then two authors (aggregation and a join on "isbn" with another collection).

This query is represented by a TGV in figure 1. We can see Tree Patterns represented by ovals (STP) and rectangles (ATP, RTP). The first STP defines the collection filter for "reviews". It is associated to a "contains" function, the tree representation is composed of two branches with a title and an isbn (linked to a constraint). The second STP filters the collection where $x/@isbn > 1526 return <books> {$x/title} { for $y in collection("books")/book where $x/@isbn = $y/@isbn and count($y/author) > 2 return $y/author } </books> TAB. 1: XQuery Example "books". The isbn is linked to the previous isbn node with a Join Hyperlink. The author node is linked to two ATPs by Projection Hyperlinks. The ATP on the right corresponds to the aggregate constraint that requires more than two authors by book. The ATP on the left nests results for each book (defined by its isbn), this result is put in the RTP by a Generalized Hyperlink. The RTP represents the XML document creation, with tags (nodes relation) and values (hyperlinks).

The TGV logical structure recognizes the full untyped-XQuery specification and covers 8 of 9 use cases of the W3C. The use-cases category not covered by our TGV model is the STRONG category that includes query type information.

Annotations

Our TGV logical model can be extended by annotating its elements with physical information, produ-cing an annotated TGV (which is then a physical model). Annotations add new information to a TGV model in order to indicate for example, execution costs, localization information, or some others constraints as accuracy, access right, etc.

We introduce a generic annotation model, which allows us annotating subsets of TGV elements with information. The motivation for annotating a TGV is to give, for each arbitrary granularity (i.e. subset size), some additional information such as cost information, system performance information, source localization, etc. Our annotation model is generic and allows any type of information. The set of annotation based on the same annotation type is called an annotated view. There can be several annotation view for the same TGV, eg. time-cost annotated view, algorithm annotated view, source-localization annotated view, etc.

For example, we can annotate the execution cost on a hyperlink ; it's also possible to annotate all elements of a source all together by adding an execution cost and some localization information.

Figure 2 illustrates an annotated TGV with algorithms annotations. This physical TGV represents a view of the possible algebraic evaluation of the TGV with given operators. We can see XSources that selects and filters data on sources s1 and s2 (we can notice that aggregate functions are embedded in the source s2). An XJoin will join data provided by s1 and s2 with a left outer join. Then, an XConstruct will build an XML document with specific projections on data.

Figure 3 shows a cost annotated TGV. Several TGV elements are linked to cost annotations. This view gives an estimate cost of each step of the evaluation. We can see the use of cardinality, selectivity, projection, and aggregation in formulas. The final cost formula (8) provides the evaluation global cost. "reviews" left Outer-join

(1)

(2)

(2) (4)

(2) XSource :

query on source s2

(1) XSource :

EXTENSIBLE OPTIMIZATION

Now we have recall TGV characteristics, we present the optimization framework. TGV are modified by the optimizer to generate more efficient evaluations.

The optimization framework takes several transformations to manipulate TGVs and generates new ones. We now introduced the optimization process, and then focus on transformations we call Rule Patterns. We present a model to create new transformation rules in order to extend our optimizer. We propose a model to represent and create rules ; we do not focus on which rule we add to our optimizer (or proving them). Some classical transformation rules can be found in [START_REF] Cherniack | Changing the Rules : Transformations for Rule-Based Optimizers[END_REF][START_REF] Lohman | Grammar-like Functional Rules for representing Query Optimization Alternatives[END_REF][START_REF] Ali | Minimization of Tree Pattern Queries[END_REF].

Optimization framework

Since TGV is an intuitive representation model for XQuery, we aim at defining a representation model for transformation rules on TGV. Then, rules definition could be easier to create, according to existing equivalence rules on object-oriented queries [START_REF] Cherniack | Changing the Rules : Transformations for Rule-Based Optimizers[END_REF][START_REF] Lohman | Grammar-like Functional Rules for representing Query Optimization Alternatives[END_REF][START_REF] Ali | Minimization of Tree Pattern Queries[END_REF].We present rules specification applicable on the TGV model.

Two TGV are said to be equivalent if they do have the same evaluation (i.e. same resulting document) independently of the XML documents sources : eval(T GV 1 , τ) = eval(T GV 2 , τ). eval is the evaluation function for a T GV and τ an XML document set. Then, a transformation rule φ keeps equivalence if the T GV modified by φ is equivalent to T GV : eval(φ(T GV ), τ) = eval(T GV, τ).

Equivalence Rules (or shortly Rules) define that under specified conditions, the result of the TGV after the transformation is equivalent (i.e. same results).

Rule Patterns

We propose a rule presentation model for this rule language : a Rule Pattern Model (RP Model). Like TGV mappings on XML documents with Tree Patterns, we represent rules in intuitive manners in order to build a pattern to map visually on TGV representations. Since TGV representation is a translation from ADT formalization, we can naturally use this transformation process and extract parts of the TGV.

The given rule pattern for the transformation rule is a part of a TGV in which is represented only concerned elements. Two rule patterns are necessary to represent a transformation rule. In fact, the first rule pattern is called Condition Rule Pattern and represents the rule condition. The second rule pattern is called Conclusion Rule Pattern and represents the rule conclusion (i.e. the final pattern after applying transformations using condition pattern's variables).

Then, the framework given in Figure 4 defines transformation rules. Rx is the transformation name identifier. The condition rule pattern represents which TGV elements a TGV must have to be applied. The conclusion rule pattern represents the pattern transformation when applied. Differences between the two rule patterns correspond to the transformation.

Transformation rules defined by the Rule Language allow us to improve optimizer's knowledge with new transformations which would modify TGV representations and reach an optimal representation. The two first categories include well-known equivalence rules : logical rules and physical rules. Those categories are detailed in following sub-sections with illustrating examples (figure 5 and6).

Condition

$n $c => = $H 1 1 = $H 1 $n 2 $n $c 1 $n $c 2 R1: FIG. 5: Logical Rule Pattern Example $n => = $H 1 1 $n 2 R2: (1) (2) (3) (3) Algorithm : : left Outer-join (1) (2) Cardinality () Cardinality () (1) (2) << $n = $H 1 1 $n 2 (1) (2) (3) (3

Logical Pattern Rules

Thus, Logical Equivalent Transformations correspond to logical knowledge on TGV. Those rules deal with topology improvements on TGV without annotations requirements.

Figure 5 illustrates a transformation rule R1. This rule takes care of nodes which are linked to both a constraint and a join hyperlink. Since the equal ope-rator is distributive, we can infer that the constraint will be cloned to the linked node. This figure shows a Condition Rule Pattern on the left, in which a join hyperlink $H 1 links $n 1 and $n 2 . $n 1 is also linked to a constraint $c. We notice that the join hyperlink is equality joint. Then, the Conclusion Rule Pattern represents the same pattern with a single modification. The constraint $c is cloned on $n 2 .

When we apply R1 on our example (figure 1), a join hyperlink is present with a linked constraint. Then the transformation is applied and we obtain a new TGV (figure 7) and the constraint is cloned to the other node isbn.

Physical Pattern Rules

Physical Equivalent Transformations use physical information that sources can provide like algorithms, cost information, function capabilities, systems statistics. These transformations are based on sources information annotated on TGV (see section 2.2).

Figure 6 illustrates a physical transformation rule.

"reviews"

Bind left Outer-join (1) (2)
(2)

(

(2) XSource : query on source s2

(1) XSource : query on source s1

(4) XConstruct :

($x, $y) >1526

FIG. 8: Physical transformation on TGV

This physical rule uses two types of annotation. In fact, some annotations from the algorithm-annotated view showed in figure 2 and the cost-annotated view in figure 3 are used in Rule Patterns. We can see a join hyperlink on which annotations must be present (XJoin for the join hyperlink with a left outer join) and cardinality annotations for Tree Patterns (cardinality are given by formulas). The Condition Rule Pattern verifies if the cardinality of source s1 is quite lower than source s2's one. Then the transformation modifies the algorithm annotation by a Bind left outer join.

The cardinality comparison is carried out by the optimizer (theoretical cardinalities are given by the cost model).

When the rule pattern is applied on the TGV, the join algorithm is modified has expected. The result is showed in figure 8.

Extensibility

User-define Transformations are rules provided by a user or an administrator that have knowledge on sources or data behavior. It could be used to create a specific rule.

Since we have categorized transformations, a search-strategy push the information into the optimizer proposed in [START_REF] Travers | Extensible Optimization in an XML Mediatior[END_REF]. This strategy relies on rule valuation with a coefficient of improvement [START_REF] Carey | The EXODUS Extensible DBMS Project : An Overview[END_REF]. This coefficient is directed by information provided by our cost model. Transformation rules, like cost model, need an annotation support on parts of the TGV model in order to manage external information on Tree Graph Views.

The extensibility of the optimizer is then given by new added rules. Each of these rules are added to the optimizer and can potentially improve performances.

EXPERIMENTAL EVALUATION

The purpose of this section is to validate the better performance of a query evaluation after having integrated previous defined optimization rules. Thus, we evaluate a query on the benchmark defined by [START_REF] Dragan | Benchmarking an xml mediator[END_REF] within the mediator XLive (Travers et al., 2007a). We load the extensible optimizer with rule patterns that are applied if the rule condition matches. We use XML documents with various sizes and information distribution, and calculate their execution time after having applied optimization rules. Tests have been realized on an AMD Athlon 1.8GHz, with 1024Mo RAM under Windows XP SP2, sources were handled by a Pentium 2.65GHz, with 512Mo de RAM under Windows XP SP2 with a 10Mbps connection.

The transformation rules integrated into the optimizer are physical rules transformation as they use annotation information (functional capacities of the sources for the functions, cardinality for the algorithm of joint).

Thus, these three optimization rules are used successively :

-delegate function contains to sources ; -delegate the aggregate operation to sources ; -change the join algorithm (nested loop to hash).

On Figure 9, we report the time used by the XLive mediator to evaluate the XQuery shown in our previous example, applied on documents with different size. Of course, as the document data size increase, the execution time linearly increase too.

The objective is to validate the extensible optimizer and show that the more matching pattern rules there are, the faster is the evaluation.

Measurement are made with sets of rules that are loaded successively in the optimizer. In each additio-nal set that is provided, one rule pattern match the request.

FIG. 9: Time execution depending on the data size

RELATED WORK

Using transformation rules, a given execution plan will be transformed into an equivalent execution plan (i.e. that give the same result when evaluated). Transformation rules can be logical (i.e. based on the algebraic properties of the operators), physical (i.e. based on the hardware, system and data statistics) or userdefined (i.e. defined arbitrarily by the user).

EXODUS [START_REF] Carey | The EXODUS Extensible DBMS Project : An Overview[END_REF]) was the first system to include a query optimizer generator based on a rule language that specifies transformation of query trees. The EXODUS optimizer uses a best-first search strategy for rule-application based on the excepted benefit of applying a rule to a query. The Volcano [START_REF] Graefe | The Volcano Optimizer Generator : Extensibility and Efficient Search[END_REF] optimizer generator improves EXO-DUS generator through its use of heuristics and semantics to guide the search for transformations, its ability to learn optimization heuristics, its extensible support for physical properties of data, and its support for flexible costs models that can be used to generate plans for partially specified queries. Starburst [START_REF] Pirahesh | Extensible/rule based query rewrite optimization in Starburst[END_REF] optimizer is divided in two phases, each one having its own rules language. The query rewrite rules is written in C. Esprit EDS [START_REF] Finance | A rule-based query optimizer with multiple search strategies[END_REF] defines an unified rules language for expressing query transformations in an extensible query optimizer.

However, all these works are designed to relational or object contexts. And as far as we know, those solutions could not be applied on a semi-structured context with tree pattern matching queries. So, our model defines transformation rules that would be ap-plied on TGV, to optimize XQuery evaluation and bring adaptability to the mediator with specific rules.

CONCLUSION

In this paper, we propose a rule-based optimizer for XQuery. Rule-based optimizers are extensible as they consist in modifiable sets of rules. Sets of rules can be defined in two categories :

-Logical rules that rely on logical operators used by the query -Physical rules that rely on physical information got from sources and from the system. Rules are applied on the XQuery model called TGV designed for heterogeneous distributed sources, which supports full non-typed XQuery specification. A logical rules suite is provided using theorems deduced from the definition of the Abstract Data Type TGV. In order to define the physical rules suite, physical information on sources and system must be provided. User-defined rules provided by the user or the administrator based on her/his knowledge of data and systems. Moreover, the search strategy is all the more efficient since transformation rules are based on annotated information. This leads to a better execution plan. A generic annotation is defined to annotate the TGV and that can be used when defining rules. This generic annotation can support any type of information, mainly cost information, but also information as accuracy, access, preferences, etc.

Many systems relying on rules-based optimizer have been defined for relational sources [START_REF] Pirahesh | Extensible/rule based query rewrite optimization in Starburst[END_REF][START_REF] Graefe | The Volcano Optimizer Generator : Extensibility and Efficient Search[END_REF][START_REF] Carey | The EXODUS Extensible DBMS Project : An Overview[END_REF][START_REF] Mitchell | Extensible query processing in an object-oriented database[END_REF] and object-oriented sources [START_REF] Kabra | OPT++ : an objectoriented implementation for extensible database query optimization[END_REF][START_REF] Finance | A rule-based query optimizer with multiple search strategies[END_REF]. But as far as we know, nothing has been done yet for semi-structured systems and a fortiori on heterogeneous distributed XQuery queries. For those reasons, our work on rules-based optimizer for XQuery is a new axis.

Our system based on the mediator/wrappers architecture is called XLive and already supports full XQuery evaluation on heterogeneous distributed sources, using TGV with annotation support (a poster presentation has also been submitted to the conference).

  FIG. 2: Algorithm-annotated TGV view

  FIG. 4: Transformation rules's framework

  FIG. 6: Physical Rule Pattern Example

  FIG. 7: Logical transformation on TGV

ACKNOWLEDGEMENTS

The XLive is supported by the ACI Semweb project. Part of this work is also supported by the ANR PADAWAN project.