Learning More about XQuery

We start by describing the formal model of XML values and XML Schema types used in XQuery, which is necessary to understand the rest of the chapter. Then the next section, "Matching and Subtyping," expands on our definition of matching to include matching of complex XML values with complex types. Since FLWOR expressions are the workhorse of XQuery, we cover their normalization and static and dynamic semantics in the section entitled "FLWOR Expressions." The normalization of path expressions into FLWOR expressions is covered next in " Path Expressions." The normalization of arithmetic and comparison operators into function calls is covered next , under "Implicit Coercions and Function Calls." We conclude with a section dealing with node identity and element constructors.

Values and Types

In the "Getting Started" section, we only had Boolean and integer values and types. To define XQuery formally , we first need to define XML values and types.

Values

We start with the formal notation for values. Recall from Chapter 4 that a value is a sequence of zero or more items . Sequences are central to XQuery's semantics ”so much so that one item and a sequence containing that item are indistinguishable. We write () for the empty sequence, and Item 1 , . . . , Item n for a sequence of n items. An item is either an atomic value or a node value.

graphics/05equ82.gif

We also write Value 1 , Value 2 for the value that is the concatenation of two values.

An atomic value is either an integer, Boolean, string, or date.

graphics/05equ83.gif

Here we use the value-constructor functions to be explicit about the type attached to data. The arguments to xs:integer(), xs:boolean(), and xs:date() must be strings in the lexical space of integer and date , as defined by XML Schema Part 2 [SCHEMA]. (XML Schema specifies nineteen primitive data types. The full XQuery data model has the same, and also gives special status to integer , which is derived from decimal . Here we consider only the subset above.)

We write unadorned strings and integers as abbreviations for the corresponding cases above. Thus, "Red bicycle" is short for xs:string("Red bicycle") and 42 is short for xs:integer("42") . We also use fn:true() and fn:false() in lieu of xs:boolean("true") and xs:boolean("false") .

A node is either an element or text. An element has an element name (which is a qualified name ), a type annotation, and a value. A text node has a text string. We do not discuss attributes, as their semantics is largely similar to that of elements.

graphics/05equ84.gif

We may omit the type annotation on an element, in which case the annotation xs:anyType is assumed. Thus,

graphics/05equ85.gif

is equivalent to

graphics/05equ86.gif

(The full data model also has document, comment, and processing instruction nodes. Here we consider only the subset above.)

Types

Chapter 4 introduced XML Schema, briefly explained its relationship to the XQuery type system, and presented some examples of XQuery types. Here is an example just to refresh your memory. Suppose that we have the schema shown in Listing 5.1, in which an article element contains a name element and zero or more reserve_price elements, and a reserve_price contains zero or more decimal values:

Listing 5.1 XML Schema for the article Element
 <xs:element name="article" type="Article"/> <xs:complexType name="Article">    <xs:sequence>       <xs:element name="name" type="xs:string"/>       <xs:element name="reserve_price" type="PriceList"                   minOccurs="0" maxOccurs="unbounded"/>    </xs:sequence> </xs:complexType> <xs:simpleType name="PriceList">    <xs:list itemType="xs:decimal"/> </xs:simpleType> 

This schema is represented in the XQuery type notation as shown in Listing 5.2:

Listing 5.2 XQuery Type Definitions for the article Element
 define element article of type Article define type Article {   element(name,xs:string),   element(reserve_price,PriceList) * } define type PriceList restricts xs:anySimpleType { xs:decimal * } 

We refer to this example in the following sections. We refer you to the XQuery Formal Semantics [XQ-FS] for the complete mapping from XML Schema into the XQuery type system.

We start with an item type , which is a node type or an atomic type. A node type is an element type or a text type. Element types are explained below. All text nodes have the same type, which is text() . An atomic type is given by its name.

graphics/05equ87.gif

Every AtomicTypeName is also a TypeName .

An element type gives an optional name, followed by an optional type name. A name alone refers to a global declaration (e.g., element(article) ). A name followed by a type name is a local declaration (e.g., element(name,xs:string) ). The wildcard name * can be used to match any name (e.g., element(*,xs:string) ). The expression element() alone refers to any element.

graphics/05equ88.gif

A type is either the nil choice ( none() ), the empty type ( empty() ), an item type, or composed by sequence ( , ), choice ( ), or an occurrence indicator ”either optional ( ? ), one or more ( + ), or zero or more ( * ).

graphics/05equ89.gif

A simple type is composed from atomic types by choice or occurrence. Every simple type is a type.

graphics/05equ90.gif

At the top level one can define elements and types. A global element declaration, like a local element declaration, consists of an element name and a type annotation. A global type declaration consists of a type name and a type derivation. A type derivation either restricts an atomic type or a named type and specifies the restricted type.

graphics/05equ91.gif

All complex types are derived from xs:anyType , thus the shorthand definition

graphics/05equ92.gif

is equivalent to

graphics/05equ93.gif

Remember that all element types are assumed to have a type annotation. In the case of an XML Schema anonymous type, an implementation-defined name is computed. This property is required by the semantics of matching given next.

Matching and Subtyping

Since XQuery is a strongly typed language, matching values to types is central to its dynamic semantics. We have already seen that matching is used in the semantics of type declarations, which occur in let , for , some , and every expressions and function signatures. Matching for Boolean and integer values only was defined in the previous section entitled "Matching Values and Types." In this section, we extend the definition of matching to relate complex XML values with complex types. After matching, the next most important judgment on types is subtyping. Subtyping is used during static analysis to check whether a type is a subtype of another type. Both matching and subtyping are used extensively in this section.

Types in XML differ in some ways from types used elsewhere in computing. Traditionally, a value matches a type ”given a value and a type, either the value belongs to the type or it does not. In XML, a value can also validate against a type ”given an (external) value and a type, validation produces an (internal) value or it fails. After validation, one can safely talk about type matching.

For instance, consider the simple type PriceList , defined in the XML Schema in Listing 5.1, and the following unvalidated element value:

 <reserve_price> 10.00 20.00 25.00 </reserve_price> 

Before validation, this element is represented by the following untyped XML value.

 element reserve_price { text { " 10.00 20.00 25.00 " }} 

After validation, this element is represented by the following typed XML value:

 element reserve_price of type PriceList {10.0 20.0 25.0} 

(As in Chapter 4, we use this formal notation to illustrate the type labels of validated elements and attributes ”it is not a valid XQuery expression.) Validation has annotated the element with its type, PriceList . If we extract the typed value of this node by applying the fn:data function, the result is the sequence of decimals (10.0, 20.0, 25.0) .

Unvalidated data may not match against a type; therefore, the following does not hold :

 element reserve_price { text { " 10.00 20.00 25.00 " }}  matches  element(reserve_price) 

Recall that the sequence type element reserve_price refers to the globally declared reserve_price element. After validation, matching succeeds, so the following does hold:

 element reserve_price of type PriceList {10.0 20.0 25.0}  matches  element(reserve_price) 

In practice, an XQuery processor does not necessarily need to implement validation itself, but can rely on a third-party XML Schema validator. An XQuery processor, however, must implement matching. Thus, we focus on matching in this section and refer the reader to the XML Schema specification [SCHEMA], or to the formal treatment of validation in the XQuery Formal Semantics [XQ-FS], or to the more gentle introduction to validation in The Essence of XML [ESSENCE].

Now we are ready to give the rule for matching elements against element types. The rule uses three new judgments yields, substitutes for , and derives from , which we define next.

graphics/05equ94.gif

First the content of the element type is examined to yield a base element name ElementName 1 and a base type name TypeName 1 . Then the given element matches the element type if three things hold: the element name must be able to substitute for the base element name, the type name must derive from the base type name, and the value must match the type. This is a mouthful, but it will make sense once we define the three ancillary judgments.

Yields

The judgment

graphics/05equ95.gif

takes an element type and yields an element name and a type name. We assume that the element names include a special wildcard name * , which is returned if the element type does not specify an element name. For example,

 element(article)  yields  element(article,Article) element(reserve_price,PriceList)  yields  element(reserve_price,PriceList) element(  *  ,PriceList)  yields  element(  *  ,PriceList) element()  yields  element(  *  ,xs:anyType) 

If the element type is a reference to a global element, then it yields the name of the element and the type annotation from the element declaration. The first hypothesis is a global element definition; this is an abbreviation for stating that the given definition appears in the element declarations in the static environment.

graphics/05equ96.gif

If the element type contains an element name with a type annotation, then it yields the given element name and type name in the type annotation.

graphics/05equ97.gif

If the element type has a wildcard name followed by a type name, then it yields the wildcard name and the type name.

graphics/05equ98.gif

If the element type has no element name and no type name, then it yields the wildcard name and the type name xs:anyType .

graphics/05equ99.gif

Substitution

The judgment

graphics/05equ100.gif

holds when the first element name may substitute for the second element name. This happens when the two names are equal, or when the second name is the wildcard element name * . For example article substitutes for article and article substitutes for * . (We do not discuss element substitution groups here, but the judgment generalizes neatly to handle these.)

An element name may substitute for itself.

graphics/05equ101.gif

And an element name may substitute for the distinguished element name * .

graphics/05equ102.gif

Derives

The judgment

graphics/05equ103.gif

holds when the first type name derives from the second type name. For example, recall our example from Chapter 4:

graphics/05equ105.gif

Every type name derives from the type that it is declared to derive from by restriction.

graphics/05equ106.gif

This relation is a partial order: It is reflexive and transitive by the rules below, and it is asymmetric because no cycles are allowed in derivation by restriction.

graphics/05equ107.gif

Matches

Now we're back to matches again, but this time, we define it for all types, not just for the atomic and element types. The judgment

graphics/05equ108.gif

holds when the given value matches the given type. For example,

 (element name of type xs:string { "Tom" },    element name of type xs:string { "Mary" })  matches  element(name,xs:string)+ 

and

 (10.0, 20.0, 25.0)  matches  xs:decimal * 

Here are the rules for matching against any type. The empty sequence matches the empty sequence type.

graphics/05equ109.gif

An integer value matches an atomic type name if the atomic type name derives from xs:integer .

graphics/05equ110.gif

Similar rules apply to all the other atomic types (e.g., strings, dates, and Booleans).

If two values match two types, then their sequence matches the corresponding sequence type.

graphics/05equ111.gif

If a value matches a type, then it also matches a choice type where that type is one of the choices.

graphics/05equ112.gif

A value matches an optional occurrence of a type if it matches either the empty sequence or the type.

graphics/05equ113.gif

A value matches one or more occurrences of a type if it matches a sequence of the type followed by zero or more occurrences of the type.

graphics/05equ114.gif

Lastly, a value matches zero or more occurrences of a type if it matches an optional one or more occurrences of the type.

graphics/05equ115.gif

Subtyping

Finally, the judgment

graphics/05equ116.gif

holds if every value that matches the first type also matches the second. For example,

 element(article) +  subtype  element(article)  *  element(*,NewUser)  subtype  element(*,User) 

All the judgments we have seen in this chapter are defined using inference rules over the structure of values and types. Subtyping is the only judgment that we do not define by using inference rules, because it is not possible to give a complete definition in this way. Imagine trying to define rules that prove the following three types are equivalent:

 (element(), text())*, element(), text() (element(), text())+ element(), text(), (element(), text())* 

Instead, subtyping is defined by a logical equivalence. We have

graphics/05equ117.gif

if and only if

graphics/05equ118.gif

for every Value .

Subtyping can be checked by straightforward modification of well-known algorithms that check for inclusion between the languages generated by two regular expressions [ALGORITHMS].

FLWOR Expressions

The FLWOR expression is the workhorse of XQuery: It allows a user to iterate over sequences of values, compute intermediate results, conditionally filter values, and construct new values. In essence, it is the XQuery analog of SQL's select-from-where expression, and its syntax was designed so that it looks familiar to database programmers.

In its full generality, the FLWOR expression contains one or more for and let clauses, followed by optional where and order by clauses, followed by a return clause. Each for and let clause may bind one or more variables . Listing 5.3 shows the grammar for the FLWR expression (i.e., a FLWOR minus the order by clause):

Listing 5.3 Grammar for the FLWR Expression
  Expr  :=  . . . previous expressions . . .  FLWRExpr   FLWRExpr  :=  Clause+ return Expr   Clause  :=  ForExpr  LetExpr  WhereExpr   ForExpr  :=  for ForBinding (, ForBinding)  *    LetExpr  :=  let LetBinding (, LetBinding)  *    WhereExpr  :=  where Expr   ForBinding  :=  $Var TypeDeclaration? PositionalVar? in Expr   LetBinding  :=  $Var TypeDeclaration? := Expr   TypeDeclaration  :=  as SequenceType   PositionalVar  :=  at $Var   SequenceType  :=  ItemType Occurrence  

The optional type declaration in a for or let clause refers to the SequenceType production, which is used in XQuery to refer to a type. The optional position variable associated with the for clause is bound to the integer index of the current item bound to Var in the input sequence.

Normalization

It is easier to define the static and dynamic semantics of an expression if it is small and doesn't do too much. Trying to define the semantics of a complete FLWR expression would be difficult, but luckily a FLWR expression can always be defined in terms of multiple, simpler for , let , and if expressions. For example, the FLWR expression

 for $i in $I, $j in $J let $k := $i + $j where $k >= 5 return ($i, $j) 

normalizes to the following equivalent expression:

 for $i in $I return   for $j in $J return     let $k := $i + $j return       if ($k >= 5) then ($i, $j)       else () 

Normalization of a FLWR expression with more than one clause turns each clause into a separate nested FLWR expression, and normalizes the result. Here's the rule to normalize two or more clauses:

graphics/05equ119.gif

Normalization of a for or let clause with more than one binding turns each binding into a separate nested for or let expression and normalizes the result.

graphics/05equ120.gif

Normalization of a for or let clause with a single binding just normalizes the subexpressions .

graphics/05equ121.gif

Finally, a where clause is normalized into an if expression that returns the empty sequence if the condition is false, and normalizes the result:

graphics/05equ122.gif

(The normalization rule for if expressions is discussed in the later section "Implicit Coercions and Function Calls.") After normalization, we are left with only for and let expressions each with a single variable binding and with if expressions.

Dynamic Semantics

We have already seen the dynamic semantics of the let expression in the earlier section "Environments." The dynamic rule for a for expression is similar to the rule for let , except instead of binding the variable to the entire sequence, it is bound once to each item in the sequence and the resulting values are concatenated together.

graphics/05equ123.gif

The sequence operator " ," concatenates two item sequences.

Users new to XQuery sometimes expect one evaluation of the body of a for expression to affect later evaluations, as is possible in imperative programming languages such as C or Java. This rule makes clear that each evaluation is independent of every other evaluation, that is, the evaluation when Var is mapped to Item 1 has no effect on the evaluation when Var is mapping to Item n .

Unlike the normalization rules of the previous section, there is no restriction n > 0 in the above rule. In the case that n = 0, the above rule simplifies to the following:

graphics/05equ124.gif

In this case, there is no need to evaluate the body of the for expression, because the input sequence is empty.

For a for expression that includes a position variable, the iteration variable is bound to an item in the sequence, and the position variable is bound to the item's position. The body of the for expression is evaluated in the environment dynEnv extended with these two variable bindings:

graphics/05equ125.gif

Finally, the dynamic rule for a for expression that includes a type declaration is similar to the dynamic for a let expression with a type declaration, except that every item must match the declared type. If any Item 1 , . . . , Item n does not match the declared type, a type error is raised.

We refer you to the XQuery Formal Semantics for the dynamic semantics of the FLWOR expression that includes the order by clause [XQ-FS].

Static Semantics and Factored Types

In addition to for expressions, many constructs in XQuery iterate over the items in a sequence. If the type iterated over is a factored type , that is, it consists of an item type and an occurrence indicator, then the result type can be computed in a way similar to the let expression. Here is a static typing rule that assumes the type of the input sequence is already factored:

graphics/05equ126.gif

In general, the type of the input sequence may not be factored. Here are some examples of types and their factorizations:

graphics/05equ126a.gif

and

graphics/05equ126b.gif

Factoring in this way may lose information. In the first example, we lose the fact that a string is always preceded by an integer, and in the second example, we lose the fact that there is only one title and that it precedes all the authors. But for typing iteration, the information yielded by factoring is usually good enough.

Before defining factorization, we define its result type, which is the product of a prime type and a quantifier and is written Prime Quantifier . A prime type is a choice among zero or more item types.

graphics/05equ127.gif

A quantifier just represents an occurrence indicator. We can combine an arbitrary type with a quantifier, and get the expected type.

graphics/05equ128.gif

Given an arbitrary type Type , we want to factor it into a Prime and Quantifier such that

graphics/05equ129.gif

Here is how to compute prime types:

graphics/05equ130.gif

Both sequence types ( , ) and choice types ( ) are converted into the choice type. Similarly, both the empty sequence empty() and the nil choice none() are converted into the nil choice, since that is identity for choice (that is, Type none() = Type , for all types). Occurrence operators are dropped.

Here is how to compute quantifiers:

graphics/05equ131.gif

We combine quantifiers by applying the rules in the following symmetric tables. The tables formalize the approximate arithmetic required to compute occurrence indicators. This will also be used in the section entitled "Path Expressions."

graphics/05equ132.gif

For example, (?,+) = + , that is, zero-or-one item followed by one-or-more items is one-or-more items; and ?+ yields * , that is, zero-or-one item or one-or-more items is zero-or-more items.

If we apply the prime and quant functions to the types given above, we get the factorings given above:

graphics/05equ133.gif

The following theorem states that the above rules always correctly factor a type, and always find the smallest (i.e., most precise) factorization. To characterize smallest, we define a partial ordering on quantifiers as follows : 1 ?, 1 +, ? *, + * .

Theorem 5.3 Factorization

For all types we have

graphics/05equ134.gif

Further if

graphics/05equ135.gif

then

graphics/05equ136.gif

The first part of the theorem guarantees that every value that belongs to the original type also belongs to its factorization, as we require, and the second part guarantees that the factorization is in some sense optimal. This theorem has practical implications: If factorization did not compute the smallest (i.e., most precise) type possible, the user would have to clutter queries with calls to the occurrence functions one-or-more and one , which would give the more precise type.

Now that we have factorization, it is easy to write the typing rule for for when applied to an expression with an arbitrary type. We compute the type of the first subexpression and then factor that type into a prime type and quantifier. We extend the static environment so that Var has the prime type and then compute the type of the body of the for expression. The result type is the type of the body combined with the quantifier. Here is the rule:

graphics/05equ137.gif

For example, if

 $kseq : ((xs:integer, xs:string)  xs:integer)* 

then

 for $k in $kseq return typeswitch($k) case xs:integer return $k<1                    case xs:string return $k : (xs:boolean  xs:string)* 

It would be sound to give this expression the more precise type ((xs:boolean, xs:string) xs:boolean)* , but finding a type algorithm that is so precise is difficult. In practice, the loss of information implied by factoring is usually acceptable, and when it is not, the extra information can be recovered by using a treat as expression.

The static semantics of the functions fn:unordered , fn:distinct-nodes , fn: distinct-values , the operators union , except , and intersect , and the expressions some and every all factor the type of their input sequences. Now that you understand what a factored type is and how it is computed, you should be able to read and understand the static typing rules for all these constructs.

Path Expressions

In this section, we focus on how the implicit and sometimes complex semantics of path expressions is revealed through normalization.

The notion of defining some expressions in terms of others was put to good use in the XPath 1.0 specification, and this has carried over into XPath 2.0 and XQuery. For instance, the expression book/isbn is an abbreviation for child::book/child::isbn . In general, QName is an abbreviation for child:: QName , which returns all element children of the context node with the name QName . The context node itself is referred to as ".", which is an abbreviation for self::node() . Similarly, the parent of the context node is referred to as "..", which is an abbreviation for parent::node() . Finally, the expression Expr 1 // Expr 2 is an abbreviation for Expr 1 / descendant-or-self::node() / Expr 2 . Thus, Expr // QName translates to Expr / descendant-or-self::node()/child:: QName rather than (as you might have expected) Expr / descendant:: QName , though these last two expressions turn out to be exactly equivalent.

Though simple and uniform, this translation of " // " has consequences that may not be appreciated even by seasoned XPath users (although this trick goes back to XPath 1.0). For example, Expr // . translates to Expr /descendant-or-self::node()/self::node() and not to, say, Expr / descendant::* as one might have guessed. The former includes the nodes in Expr itself, the latter does not.

The XQuery formal semantics expresses the translations such as those above by means of normalization rules. Just as in the earlier section "Normalization" we wrote [ Expr ] Expr for the normalization operator on expressions, here we write [ PathExpr ] Path for the normalization operator on path expressions.

Here are the rules corresponding to the cases discussed above:

graphics/05equ138.gif

A comparison of the text above with the rules above shows that the rules are more compact, which is exactly why we use formal notation. Note that the last rule recursively applies normalization to its right-hand side. This is because the definition of " / " is also expanded out by normalization, as described in the next section.

Although they serve quite different purposes from a user point of view, XPath expressions using " / " and XQuery expressions using for have some common semantics: both iterate over sequences. They differ in that " / " binds an implicit focus of iteration known as the context node, written " .", while for binds an explicit iteration variable. Similarly, " / " binds an implicit position for the context node, written position() , while for permits binding an explicit position variable with an expression such as for $x at $i . Finally, " / " returns nodes sorted in document order with duplicates removed, while for returns items in the order they are generated with duplicates retained.

This similarity suggests that the " / " connective and "[ ]" predicates of XPath are closely related to the for and if expressions of XQuery. In fact, the former can be precisely defined in terms of the latter. We show this by giving the normalization rules for the subset of XPath expressions given in Listing 5.4. As usual, the normalization of the complete grammar is in the [ XQuery Formal Semantics ] .

Listing 5.4 Normalization Rules for a Subset of XPath Expressions
  Expr  ::=  . . .  previous expressions  . . .  PathExpr   PathExpr  ::=  /   / RelativePathExpr   RelativePathExpr   RelativePathExpr  ::=  StepExpr / RelativePathExpr   StepExpr  ::= (  ForwardStep  ReverseStep  )  Predicates   ForwardStep  ::=  ForwardAxis NodeTest   ReverseStep  ::=  ReverseAxis NodeTest   ForwardAxis  ::= child::  descendant::  self::                       descendant-or-self::  ReverseAxis  ::= parent::  Predicates  ::= ([  Expr  ])*  NodeTest  ::= text()  node()  *  QName  :* 

We start with the rule relating normalization of expressions to normalization of path expressions.

graphics/05equ139.gif

This rule guarantees that every path expression returns a sequence of nodes sorted in document order with duplicates removed by applying the function fs:distinct-doc-order . (The namespace fs is defined in the formal semantics and is used by functions defined only within the formal semantics.)

The normalization rules for absolute path expressions are straightforward.

graphics/05equ140.gif

Here the built-in variable $fs:dot represents the context node. An absolute path expression just refers to the root of the XML tree that contains the context node.

Now things get more interesting, as we consider the rule for composing steps using " / ":

graphics/05equ141.gif

This rule binds four built-in variables: $fs:sequence , $fs:last , $fs:dot , and $fs:position , which represent, respectively, the context sequence, context size, context node, and context position. The first let binds $fs:sequence to the context sequence (the value of StepExpr ), which is sorted in document order with duplicates removed. The second let binds $fs:last to its length. Given this context, the for expression binds fs:dot (and fs:position ) once for each item (and its position) in the context sequence and then evaluates RelativePathExpr once for each binding. The bindings of the built-in variables make explicit the implicit semantics of " / ".

The normalization rule for a "[ ]" predicate is similar to the rules above, but a bit more subtle. It defines the fs:sequence , fs:last , fs:dot , and fs:position variables, evaluates the predicate expression in this context, and if the predicate expression evaluates to true, returns the context node; otherwise , it returns the empty sequence.

Here is the normalization rule for a ForwardStep expression, followed by zero or more intermediate Predicates , and then a final predicate expression [ Expr ] . It returns each context node in the forward step expression that satisfies the predicates in Expr :

graphics/05equ142.gif

XPath distinguishes between step expressions in the "forward" axes (e.g., child and descendant) and those in the "reverse" axes (e.g., parent and ancestor ), because the meaning of the context position depends on the axis direction. For the forward axes, the context position increases with the document order of nodes in the context sequence; for the reverse axes, it decreases with document order. The rule for reverse axes defines $fs:position so that it corresponds to reverse document order:

graphics/05equ143.gif

The meaning of an individual predicate expression depends on the type of its value. If the predicate value is a numeric, the predicate is true if the numeric value is equal to the context position; if the predicate value is not a numeric, the function fn:boolean converts the value to a Boolean.

graphics/05equ144.gif

Finally, a simple step expression (an axis and node test expression with no other predicates) just normalizes to itself:

graphics/05equ145.gif

The rule for ReverseAxis is similar.

Putting this all together, here is the normalization of the expression $article/child::reserve_price:

graphics/05equ163.gif

You may notice that the variables $fs:last and $fs:position are defined but are not used in the bodies of the let and for expressions, and therefore are redundant. We can simplify the expression above to the following:

graphics/05equ164.gif

You might ask why define these variables if they are never used? The answer is that, in general, a relative path expression may refer to position() or last() , and therefore require fs:position and fs:last to be defined. An XQuery implementation is free to make the simplification shown above, but the normalization rules are defined for the most general case. Predicate expressions illustrate how these variables are used. Extending the example above, here's the normalization of ($article/child::reserve_price)[1] :

graphics/05equ165.gif

And the normalization of [ 1 ] Predicates is

 typeswitch (1)   case numeric $v return      op:numeric-equal(fn:round($v), $fs:position)   default $v return fn:boolean($v) 

Note that $fs:position is used in the normalization of the predicate expression but defined in the previous rule. These examples illustrate the convenience of XPath's syntax by revealing the complexity of its semantics.

You may have noticed that normalization rules give a complete , but not necessarily minimal , definition of XQuery expressions.

Some simplifications , such as removing definitions of unused variables, are well known and simple. Others, such as eliminating redundant sorts by document order, may require some query analysis ”Chapter 3 discusses some optimizations for XPath. General rules for simplifying core expressions are outside the scope of this chapter, but we note that many techniques for simplifying expressions in functional languages apply to XQuery [FUNC-LANG].

Implicit Coercions and Function Calls

One important characteristic of XML is its ability to represent irregular data. Suppose that we have the schema shown in Listing 5.5, in which an article element may contain zero or more reserve_price elements, and a reserve_price may contain zero or more decimal values:

Listing 5.5 Schema Containing Irregular Data
 <xs:element name="article" type="Article"/> <xs:complexType name="Article">   <xs:sequence>     <xs:element name="name" type="xs:string"/>     <xs:element name="reserve_price "type="PriceList"                 minOccurs="0" maxOccurs="unbounded"/>   </xs:sequence> </xs:complexType> <xs:simpleType name="PriceList"> <xs:list itemType="xs:decimal"/> </xs:simpleType> 

This schema is represented in the XQuery formal type notation as follows:

 define element article of type Article define type Article {   element(name,xs:string),   element(reserve_price,PriceList) *, } define type PriceList { xs:decimal * } 

XQuery accommodates this flexibility by introducing certain implicit coercions. An arithmetic expression is well defined on any item sequence that can be coerced to zero or one atomic value. For example, the path expression $article/reserve_price evaluates to a sequence of zero or more reserve_price elements , but in the expression $article/reserve_price * 0.07 , its typed content is extracted automatically. A comparison expression is well defined on any item sequence that can be coerced to a sequence of atomic values. For example, in the expression $article/reserve_price < 100.00 , the typed context of $article/reserve_price is extracted automatically. Finally, XPath's predicate expressions are well defined on any item sequence. For example, the expression $article[reserve_price] returns each node in $article that has at least one reserve_price child. The expression reserve_price evaluates to a sequence of zero or more reserve_price elements, but in the expression $article[reserve_price] , the sequence is treated as a Boolean value.

Such flexibility is permitted in almost every XQuery expression: in path expressions, in arithmetic and comparison expressions, in conditional expressions, in function calls and returns, and in cast expressions. The normalization rules for these expressions make this flexibility explicit by coercing the values of subexpressions to values whose types are required by the expression. We describe two such coercions next.

The first coercion is applied to expressions that require a Boolean value (e.g., in if expressions, where clauses, and XPath predicate expressions). It simply maps the Expr argument to a core expression and applies the function fn:boolean to the result. The fn:boolean function evaluates to false if its argument is the empty sequence, the Boolean value false , the empty string, the singleton numeric value zero, or the singleton double or float value NaN; otherwise, fn:boolean returns true . For example, applying fn:boolean to 0.0 yields false , and applying it to the sequence (false, true, 0.0) yields true .

Here's the normalization rule for if , which applies the fn:boolean function to the conditional expression. The then and else branches are normalized by recursively applying the rule for expression normalization.

graphics/05equ146.gif

The second coercion is applied to an expression when used in a context that requires a sequence of atomic values. The coercion is known as atomization , because it coerces any sequence of items to a sequence of atomic values. It simply maps the Expr argument to a core expression then applies the function fn:data to the result. The fn:data function takes any item sequence, applies the following two rules to each item in the sequence, and concatenates the results:

  • If the item is an atomic value, it is returned.

  • Otherwise, the item is a node, and its typed value is returned.

For example, applying the function fn:data to this sequence of items, each of which is validated as element reserve_price ,

 (<reserve_price> 10.00 </reserve_price>, <reserve_price> 20.00 25.00 </reserve_price>) 

yields the sequence of decimal values (10.0, 20.0, 25.0) .

The typed value of every kind of node is defined in the XQuery data model[XQ-DM]. For this discussion, there are only two cases of interest. If the element is validated against a simple type or a complex type with simple content, the typed value is the sequence of atomic values that results from validating the element's content. (The same rule applies to attribute nodes that are validated against a simple type). If the element is validated against a complex type with complex content, fn:data raises a type error, because it is not sensible to try to extract atomic values from an element with complex content.

We put atomization to use in the normalization of arithmetic and comparison expressions. Because values are often optional or repeated in XML documents, the arithmetic and comparison operators are well defined on item sequences that can be atomized, that is, coerced to atomic values. This permits users to apply arithmetic and comparison expressions to empty sequences or node sequences. Arithmetic and comparison operators are also overloaded. This permits users to apply them to a variety of value types. Comparison is defined on every XML Schema data type, and arithmetic is defined on numerics, dates, and durations.

We start with the normalization rule for the plus ( + ) operator. The rules for other arithmetic operators are similar.

graphics/05equ147.gif

The normalization rule for plus first atomizes each argument expression and then applies the overloaded internal function fs:plus to each atomized argument.

As you can see, much of the semantics of the plus operator boils down to a call to the overloaded function fs:plus function, which may be applied to numerics or dates and durations, among others. An overloaded function is resolved to a non-overloaded function based on the types of its arguments. Table 5.2 specifies how fs:plus is resolved when applied to the types empty , numeric , xs:date , and xdt:yearMonthDuration .

The semantics of a function call raises a type error if the values of arguments do not match one of the permissible combinations of types specified in the function's resolution table. For example, fs:plus applied to numeric and string would raise a type error because numeric and string is not a permissible combination of types for fs:plus . Moreover, if the query is evaluated by a processor that supports static typing, all type errors raised must be detected and reported at query-analysis time; otherwise, they must be detected and reported at query-evaluation time.

When dynamic typing is in effect, function resolution must be handled dynamically ”that is, the function's resolution table would be queried at run-time to determine the specific function to call. Implementers should note that when static typing is supported, it is often possible to resolve an overloaded function to a specific function after static analysis. For example, the function call fs:plus ( Expr 1 , Expr 2 ) can be resolved to op:numeric ( Expr 1 , Expr 2 ) statically under the following assumptions:

graphics/05equ148.gif

Table 5.2. Resolution of Overloaded Function fs:plus on empty , numeric , xs:date , and xdt:yearMonthDuration

Type of A

Type of B

Resolves to

empty

T

()

T

empty

()

numeric

numeric

op:numeric-add(A,B)

xs:date

xdt:yearMonthDuration

op:add-yearMonthDuration-to-date(A,B)

xdt:yearMonthDuration

xs:date

op:add-yearMonthDuration-to-date(B,A)

Where T = empty numeric xs:date xdt:yearMonthDuration.

In addition to resolving overloaded functions, the semantics of function calls applies rules to promote values to required types. We refer the reader to the XQuery Formal Semantics [XQ-FS] for the complete semantics of function calls.

Here's an example that illustrates the flexibility of the arithmetic operators. Assume we have the following expression:

 $article/reserve_price * 0.07 

Assume also that $article/reserve_price may evaluate to one of the following four values, all of which are validated against element reserve_price :

 (<reserve_price/>) (<reserve_price> 10.00 </reserve_price>) (<reserve_price> 10.00 </reserve_price>, <reserve_price/>) (<reserve_price> 10.00 </reserve_price>, <reserve_price> 20.00 25.00</reserve_price>) 

When applied to the first value, the expression returns the empty sequence, because <reserve_price/> is empty. When applied to the second and third values, the expression returns 0.7 , because in both cases, the atomized value is the decimal 10.0 . When applied to the fourth value, a type error is raised, because the atomized value is the sequence of decimals (10.0, 20.0, 25.0) , which is neither the empty sequence nor one atomic value.

The general comparison operators (i.e., = , != , < , > , <= , >=) are existentially quantified over sequences of atomic values, after atomization. This permits general comparison operators to be applied to any item sequence that can be atomized. The normalization rule makes the atomization and existential quantification explicit. We give the rule for the < operator:

graphics/05equ149.gif

The some expression evaluates to true if some value in the atomized value of Expr 1 is less than some value in the atomized value of Expr 2 . The function fs: less-than , like fs:plus , is overloaded and can be applied to numerics, Booleans, or dates, among others.

Node Identity and Element Constructors

Element constructors are among the most complex expressions in XQuery. In Chapter 4, we saw how elements are constructed , validated, and typed. To review, at evaluation time, an element constructor creates a new element node with a new identity distinct from all other nodes, and it implicitly validates the element using the validation context and mode determined by the lexical scope of the constructor expression. At static-analysis time, an element constructor checks that the type of the element's content is appropriate for the type of element being constructed and raises a type error if it is not. In this way, static typing prevents some validation errors that would occur when the element's content could never be validated successfully.

We begin with the formal definition of node identity and conclude with the dynamic and static semantics of node constructors.

Node Identity

An element constructor always creates new nodes with new identities. For example, consider the following expression:

 let $name := <name>Red Bicycle</name> return <article>{$name, $name}</article> 

This expression first constructs a new name element containing one text node with contents Red Bicycle . The expression in the return clause constructs a new article element containing two copies of the name element ”that is, the element bound to the variable $name and the two elements contained in the article element have distinct identities. For example, the following expression:

 let $name := <name>Red Bicycle</name>,     $article := <article>{$name, $name}</article> return (     $name is $article/name[1],     $name is $article/name[2],     $article/name[1] is $article/name[2]) 

evaluates to the sequence ( false , false , false ), because each name element has a distinct identity. This should not be a surprise, as we know from the study of path expressions that nodes can be distinguished by their order within the document; thus, node identity and document order are closely related.

To capture node identity, we introduce the notion of a store into the dynamic environment. The store is a mapping from node identifiers to node values. In our case, the store is immutable ”the node associated with a node identifier never changes. The same notion of store can also be used for mutable nodes, if one wishes to model an extension of XQuery with update.

We use NodeId to range over node identifiers. The syntax of node identifiers is not specified further. The definition of Item given earlier is modified to take node identity into account. Instead of

graphics/05equ150.gif

we now have

graphics/05equ151.gif

Before we can see how this affects our semantics, we need to introduce a notation for defining stores. The notation is similar to that used for varValue and varType , except that we write dynEnv store ( NodeId NodeValue ), with in place of + , to indicate that dom ( dynEnv . store ) may not include NodeId . This guarantees that we never change the node value associated with a node identifier; that is, the store is immutable.

Here's an example that we first saw in Chapter 4:

 <article>   <name>Red Bicycle</name>   <start_date>1999-01-05</start_date>   <end_date>1999-01-20</end_date>   <reserve_price>40</reserve_price> </article> 

When we are explicit about node identity, this corresponds to the node identifier N 1 and the store shown in Listing 5.6.

Listing 5.6 The Store for the <article> Example
  store  (  N   1   element article of type Article {  N   2   , N   3   , N   4   , N   5  }  ,   N   2   element name of type xs:string { "Red Bicycle" }  ,   N   3   element start_date of type xs:date { "1999-01-05" }  ,   N   4   element end_date of type xs:date { "1999-02-20" }  ,   N   5   element reserve_price of type xs:decimal {"40.0"} ) 
Evaluation and the Store

Constructor expressions create new nodes in the store, and we need a new evaluation judgment that specifies how evaluation affects the store. Here is how we write it:

graphics/05equ152.gif

This is read, "Given old store Store and dynEnv , evaluation of expression Expr yields value Value with new store Store 1 ." Note we have separated the store from the dynamic environment. If Expr does not construct new nodes, then Store and Store 1 will be identical.

The XQuery expressions considered so far, including arithmetic, path expressions, and iteration, do not modify the store. But any of these expressions might include as a subexpression an element constructor that does modify the store. To be rigorous , all of the dynamic inference rules of the preceding sections must be rewritten with the new judgment to make the effect upon the store explicit. But all of these rules treat the store in the same way, so to rewrite them in full would achieve little other than to increase length and decrease clarity.

Instead, we introduce a simple abbreviation, by which a rule that uses the old judgment can be expanded into a rule that uses the new judgment. Every inference rule of the following form:

graphics/05equ153.gif

is considered an abbreviation for an expanded rule of the following form:

graphics/05equ154.gif

graphics/05equ155.gif

Note that each new store computed through a given judgment is passed as input to the next judgment.

For example, here is the inference rule for dynamic evaluation of let expressions:

graphics/05equ156.gif

It is considered as an abbreviation for the following rule:

graphics/05equ157.gif

In this way, most rules treat the store implicitly. We only mention the store explicitly in those rules that depend upon it, such as the rule for element construction considered in the next section.

Dynamic Semantics of Element Construction

Naively, one might expect element construction to look like this:

graphics/05equ158.gif

One first evaluates the expression for the contents. One then allocates a fresh node identity, not already allocated in the store. Then one extends the store by binding the new node identity to an element node with the given name and contents. Finally, one returns the node identity for the new node with the new store.

This naive form of element construction is too naive, because it ignores key aspects of the XQuery data model. In the XQuery data model, all elements are labeled with a type name, and the content of the element must correspond to that type name. Therefore, in keeping with XML tradition, each element is validated as it is constructed.

XML Schema validation is only defined on unvalidated documents ”recall that validation takes an untyped document, validates it against some schema, and produces a new document in which all nodes have an associated type annotation. So to apply validation, we must first erase any type annotations resulting from previous validation.

We introduce two judgments to capture this process. The judgment

graphics/05equ159.gif

holds when erasing the type information in Value yields UntypedValue . The judgment

graphics/05equ160.gif

holds when validating the UntypedValue results in Value . Formal definitions of erasure and validation can be found in the XQuery Formal Semantics [XQ-FS] and in "The Essence of XML" [ESSENCE]. Note that the second of these judgments is responsible for allocating the new typed element nodes in the store, which is done in much the same way as in the untyped naive element construction rule above.

Given these auxiliary rules, the basic rule for element construction is quite simple.

graphics/05equ161.gif

This evaluates the expression to yield a value, erases all type information in the value, constructs the untyped element node, and then validates it to yield the final typed value.

These inference rules might suggest a rather expensive implementation that requires erasing type information before validating a new element, but implementers certainly can employ more clever strategies for implementing element constructors that do not erase existing type annotations. Again, the formal rules say what to do, but not how to do it.

Static Semantics of Element Construction

We conclude with the static semantics for element constructors, which is an appropriate place to end, because it stresses one of XQuery's biggest strengths ”the ability of the static type system to perform a conservative analysis that catches errors early, during static analysis rather than dynamic evaluation.

In particular, the static semantics of element construction errs on the side of safety, insisting that the type of the data must statically match the type declared for the element. For instance, if the element is declared to have type xs:integer then the type of its contents must be xs:integer (or one of its subtypes ). It cannot be, say, xs:string , even though the string might contain only digits, and thus successfully validate as an integer.

We give the rule for globally declared elements; the rule for locally declared elements is similar.

graphics/05equ162.gif

This rule checks that the type inferred for the element's content is indeed appropriate for the element that is being constructed. In particular, the fourth judgment checks that the content type ( Type 1 ) is indeed a subtype of the type against which validation is to be performed ( Type 2 ).



XQuery from the Experts(c) A Guide to the W3C XML Query Language
Beginning ASP.NET Databases Using VB.NET
ISBN: N/A
EAN: 2147483647
Year: 2005
Pages: 102

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net