XQuery 1.0 Formal Semantics

A new element's content does not refer directly to
the given children nodes, but to
copies
of these nodes.
For example, the following expression constructs
an element with name
newbook
and content
$book0/author
$book0/title
LET $book1 :=

{ $book0/author, $book0/title }

RETURN $book1
==>
Abiteboul
Buneman
Suciu


: ELEMENT newbook (
(ELEMENT author (xs:string))+,
ELEMENT title (xs:string)
The
newbook
element contains copies of the nodes in the sequence
$book0/author
$book0/title
not the original nodes in
$book0
Copying guarantees that a node is always the
parent of its child nodes and a node is always
the child of its parent; these constraints are invariants of
[XQuery 1.0 and XPath 2.0 Data Model]
For example, we would expect that
the following expression is always true:
$book1/author/.. == $book1
If the element constructor did not copy its arguments,
anomalies such as the following could occur:
$book1/author/.. == $book0
that is, the parent of
book1
's child node
is not
book1
, and
this would violate the XML Query Data Model's parent-child invariant.
Sometimes it is useful to construct elements that do
preserve the identity of its child nodes, for example,
when constructing a
view
of one or more XML documents.
In this case,
we want the new element to
contain
references
to, not copies of,
the original nodes.
The
ref
operator constructs a reference
to a node. For example,
book2
below
contains references to the nodes in
$book0
LET $book2 :=

{ (FOR $a IN $book0/author RETURN ref($a)),
ref($book0/title)

RETURN $book2
==>
Abiteboul
Buneman
Suciu


: ELEMENT newbook (
(REFERENCE (ELEMENT author (xs:string)))+,
REFERENCE (ELEMENT title (xs:string))
Ed. Note:
MF : Issue - serialized representation of Data Model
reference nodes.
Note that the type of the expression contains reference types.
The
deref
operator dereferences a reference value.
In the following, it returns the elements in
$book0
FOR $v IN $book2/* RETURN deref($v)
==> (Abiteboul,
Buneman,
Suciu,
)
: (ELEMENT author (xs:string))+,
ELEMENT title (xs:string)
For convenience, the expression above can be also be written as
$book2/deref()
2.11 Restructuring and grouping
Often it is useful to regroup elements in an XML document. For example,
each
book
element in
$bib0
groups one title with multiple authors. This expression groups each author
with the titles of his/her publications.
FOR $a IN distinct-value($bib0/book/author/data()) RETURN

{ $a }
{ FOR $b IN $bib0/book, $a2 IN $b/author/data()
WHERE $a = $a2 RETURN
$b/title

==> (
Abiteboul

,

Buneman

,

Suciu


,

Fernandez

)
: (ELEMENT biblio (
ELEMENT author (xs:string),
(ELEMENT title (xs:string))*)
)*
Readers may recognize this expression as a self-join of books on authors.
The expression
distinct-value($bib0/book/author/data())
produces a
sequence of author names whose values are all distinct.
The outer
for
expression binds
$a
to the name of each
author element, and the inner
for
expression selects the
title of each book that has some author whose name equals
$a
Here
distinct-value
is an example of a built-in function.
It produces a sequence of nodes whose values are all distinct,
i.e., there are no duplicate values; the order of the
resulting sequence is not defined.
The builtin function
distinct-node
produces a sequenc of nodes whose
identities
are all distinct.
The type of the result expression may seem surprising:
each
biblio
element may contain
zero
or more
title
elements,
even though in
$bib0
every
author
co-occurs with a
title
. Recognizing such a constraint is
outside the scope of the type system, so the resulting type is not as precise
as we would like.
2.12 Querying order
Ed. Note:
MF: Clearly, the following example of index is not
appropriate for a tutorial -- it is only used to define RANGE.
Often it is useful to query the order of elements in an sequence or a
document. There are two kinds of order among elements:
local
order and
document
(or global) order. XQuery supports querying of local and
global order.
Local order refers to the order among sibling elements in an sequence.
To query local order, the
index
function pairs an integer
index with
each element in an sequence:
index($book0/author)
==> (1
Abiteboul,
2
Buneman
3
Suciu)
: (ELEMENT q:pair(
ELEMENT q:fst (xs:integer),
ELEMENT q:snd (REFERENCE (ELEMENT author (xs:string))))
)+
The
index
function uses reference in order to preserve node identity
when accessing local order. Note that the result type takes into
account that at least one pair exists in the result, as
$book0/author
always contains one or more authors.
Once we have paired authors with an integer index, we can select the
first two authors:
FOR $p IN index($book0/author)
WHERE ($p/q:fst/data() <= 2) RETURN
$p/q:snd/deref()
==> (Abiteboul,
Buneman)
: (ELEMENT author (xs:string))*
The
for
expression iterates over all pair elements produced by the
index
expression. It selects elements whose index value in the
q:fst
element is between one and two inclusive, and it returns the original
content by dereferencing the content of the
q:snd
element.
The result type may be surprising, because the
Book
type
guarantees that each book has at least one author. However, the type
system cannot determine that the conditional
where
expression will always
succeed, so the inner expression may produce zero results. (A
sophisticated analysis might improve type precision, but is likely to
require much work for little benefit.)
Document (or global) order refers to the total order among all
elements in a document. Global order is defined as the order of
appearance of the element nodes when performing a
pre-order, depth-first traveral of a tree.
This corresponds to the order of appearance of their
opening tags in the XML serialization. This is equivalent to the
definition used in
[XPath]
To query global order, the
xfo:node-before
function
can be applied to two nodes.
It returns true
if the first node is before (and
different from) the second node in document order. It returns false if
the first node is equal to or after the second node in document
order. It raises an error if the nodes are in different documents.
For example, the nodes
bib0
and
review0
are unrelated therefore comparing their order raises an error:
xfo:node-before($bib0, $review0)
==> ERROR
: 0
The
xfo:node-after
function is defined
similiarly.
Using global order, the following expression returns all author nodes
appearing after a book written in 2001:
FOR $b IN $bib0/book
WHERE $b/@year/data() = 2001 RETURN
(FOR $a IN $bib0/book/author
WHERE $b before $a RETURN $a)
==> (Fernandez,
Suciu)
: (ELEMENT author (xs:string))*
Note that the root element of a document is before any other
element. More generally, an element is before all of its children.
For example, the set of elements that are before
$bib0
is
empty:
empty(FOR $b IN $bib0/book
WHERE $b before $bib0 $b RETURN
$b)
==> true
: xs:boolean
XQuery supports global order only for elements within the same
document. Support for global order among elements in distinct
documents is discussed in
Issue-0003:
Global Order
2.13 Sorting
To sort a sequence, XQuery provides a sort
expression, whose form is:
Expr
sortby
Expr
The built-in variable '
', called dot, ranges over the items in the sequence
Expr
and sorts those items using the key value
defined by
Expr
For example, this expression sorts
book
elements in
$review0
by their titles.
$review0/book SORTBY ./title/data()
==> (

This is great!
,


This is pretty good too!
)
: (ELEMENT book (
ELEMENT title (xs:string),
ELEMENT review (xs:string))
)*
The
sort
expression is a restricted
form of
higher-order
function, i.e., it takes a function as an argument.
In this case,
sort
takes a single function, which
extracts the key value from each element.
The
sort
expression requires that the less-than
inequality,
, be defined for
the type of
Expr
2.14 Aggregation
We have already seen two built-in
functions:
index
and
distinct-value
In addition to these
functions, XQuery has five built-in aggregation
functions:
avg
count
max
min
, and
sum
This expression selects books that have more than two authors:
FOR $b IN $bib0/book
WHERE count($b/author) > 2 RETURN
$b
==>

Abiteboul
Buneman
Suciu

: Book*
All the aggregation functions take a sequence with repetition type and return
an integer value;
count
returns the number of elements
in the sequence.
2.15 Expanded names
So far, all our examples
of attributes and elements use unqualified
local
names
, i.e., names that do not include an explicit namespace
URI.
It is also possible to specify and match on the
expanded
name
of an attribute or element.
The expanded name
Namespace
LocalName
consists of a namespace URI
Namespace
and a local name
LocalName
Consider an inventory of books that contains data from
both
and
In this example, the first element contains values whose names are
defined in the
BooksRUs.com
namespace, and the second element
contains values whose names are defined in the
cheapBooks.com
namespace:
NAMESPACE booksRus = "http://www.BooksRUs.com/books.xsd"
NAMESPACE cheapBooks = "http://www.cheapBooks.com/ourschema.xsd"
TYPE Inventory = InvBook*
LET $inventory :=


Data on the Web
Abiteboul
Buneman
Suciu


XML Query
Fernandez
Suciu
1-XXXXX-YYY-Z

: Inventory
RETURN ...
In this example, elements imported from existing schemas each refer
to a single namespace, thus the definition of
InvBook
is:
TYPE BooksRUBook =
ELEMENT booksRus:book (
ATTRIBUTE year (xs:integer) &
ATTRIBUTE isbn (xs:string),
ELEMENT booksRus:title(xs:string)
(ELEMENT booksRus:author(xs:string))+
TYPE CheapBooksBook =
ELEMENT cheapBooks:book (
ATTRIBUTE year (xs:integer),
ELEMENT cheapBooks:title (xs:string),
(ELEMENT cheapBooks:author(xs:string))+
ELEMENT cheapBooks:isbn (xs:string)
TYPE InvBook = BooksRUBook | CheapBooksBook
Here vertical bar (
) is used to indicate a
choice between types: each
InvBook
is either a
BooksRUBook
or
CheapBooksBook
We have already seen how to project on the constant name of an attribute or
element.
It is also useful to project on
wildcards
, which
are used to match names with any namespace and/or any local name.
For example, this expression matches elements
with any local name and with
namespace URI
$inventory/booksRus:*
==>
Data on the Web
Abiteboul
Buneman
Suciu

: ELEMENT booksRus:book (
ATTRIBUTE year (xs:integer) &
ATTRIBUTE isbn (xs:string),
ELEMENT booksRus:title (xs:string)
(ELEMENT booksRus:author (xs:string))+
Similarly, this expression first projects elements
in any namespace whose local name is
book
and then projects on their
year
attributes:
$inventory/*:book/@year
==> (ATTRIBUTE year (1999), ATTRIBUTE year (2001))
: (ATTRIBUTE year (xs:integer))*
Ed. Note:
MF: Open issue whether *:localname will be supported.
The expression
Expr
is shorthand for
Expr
ns
, where
ns
is the default namespace.
Similarly,
is shorthand for
ns
, i.e., any name in the default namespace.
2.16 Comments and processing instructions
In an XML document, comments and processing instructions may
appear anywhere outside other markup
[XML]
. Processing
instructions permit documents to contain instructions for
applications. Comments and processing instructions are not part of the document's
character data. An XML processor may, but need not, make the text of
comments available to an application, but it must pass processing instructions to the
application. The processing instruction begins with a target used to identify
the application to which the instruction is directed.
XQuery supports comments and processing instructions
in types and expressions.
The type expression
PIC
) denotes
a value in which zero or more processing instructions and comments may be interleaved
arbitrarily with the nodes in type
For example, the two element types
BibPIC
and
BookPIC
permit PIs and comments to be interleaved
with their content:
TYPE BibPIC = ELEMENT bib (pic(BookPIC*))
TYPE BookPIC =
ELEMENT book (
ATTRIBUTE year (xs:integer) &
ATTRIBUTE isbn (xs:string),
PIC (ELEMENT title (xs:string), (ELEMENT author(xs:string))+)
Note that in the
book
element, the
PIC
operator is only applied to its element content, not its attribute content,
because comments and processing instructions may not occur in
attributes.
We can construct processing instruction and comment values using the
built-in constructors
processing_instruction
and
comment
LET $bibpc0 :=

{ comment("Canonical XQuery example.") }

{ comment("First book example"),
processing_instruction("Publisher.asp",
"publisher=http://www.mkp.com") }

Abiteboul
Buneman
Suciu



{ comment("Second book example") }
Fernandez
Suciu

: BibPIC
RETURN ...
Finally, we can project on processing instructions and comments, in
the same way we project on children, attributes, and simple content:
$bibpc0/book/comment()
==> (comment("First book example"), comment("Second book example"))
: Comment*

$bibpc0/book/processing_instruction()
==> processing_instruction("Publisher.asp", "publisher=http://www.mkp.com")
: ProcessingInstruction*
Comments and processing instructions may be ignored by an XML
processor, in which case they would not even be accessible to a query
processor.
If they are not ignored, however, comments and processing
instructions are typed values and are treated like any
other value in an XQuery expression.
2.17 Mixed Content
An element type has mixed content when elements of that type may
contain character data, optionally interspersed with child
elements
[XML]
The type expression
mixed
) denotes
a value in which zero or more
xs:string
values may be interleaved
arbitrarily with the nodes in type
For example, the content of the
review
element
contains a
reviewer
element, which may be interleaved
with string values:
TYPE ReviewsMixed =
ELEMENT reviews (
(ELEMENT book (
ELEMENT title (xs:string),
ELEMENT review (MIXED (ELEMENT reviewer(xs:string)))))*
Here are two examples of mixed content, in which
the text of the book review may be interleaved with
the name of the reviewer:
LET $reviewmix0 :=



A darn fine book: XML On-line


,
The publisher says 'This is great!'

: ReviewsMixed
RETURN ...
It is often useful to
concatenate all the string values of a mixed-content element to
recover
its complete text value.
We use the builtin function
string_value
as defined in XPath
[XPath]
the string value of a node is determined by its kind,
e.g., element, attribute, etc.
FOR $b IN $reviewmix0/book RETURN
string_value($b/review)
==> ("A darn fine book : XML On-line",
"The publisher says 'This is great!'")
: xs:string*
2.18 Functions
Functions can make queries more modular and concise. Recall that we used the
following query to find all books that do not have "Buneman" as an
author.
FOR $b IN $bib0/book
WHERE EVERY $a IN $b/author SATISFIES NOT($a/data() = "Buneman") RETURN
$b
==>

Fernandez
Suciu

: Book*
A different way to formulate this query is to first define a function that
takes a string
and a book
as arguments, and returns true if book
does not have
an author with name
DEFINE FUNCTION notauthor (xs:string $s, Book $b) RETURNS xs:boolean {
EVERY $a IN $b/author SATISFIES NOT($a/data() = $s)
The query can then be re-expressed as follows.
FOR $b IN bib0/book
WHERE notauthor("Buneman", $b) RETURN
$b
==>

Fernandez
Suciu

: Book*
Note that a function declaration includes the types of all its arguments and
the type of its result. This is necessary for the type system to guarantee that
applications of functions are type correct.
In general, any number of functions may be declared at the top-level. The
order of function declarations does not matter, and each function may refer to
any other function. Among other things, this allows functions to be recursive
(or mutually recursive), which supports structural recursion, the subject of
the next section.
Functions make XQuery extensible. We have seen examples of built-in
functions (
sort
and
distinct-value
) and examples of user-defined functions (
notauthor
).
In addition to built-in and user-defined
functions, XQuery could support externally defined functions, i.e.,
functions that are not defined in XQuery itself, but in some external
language. This would make special-purpose implementations of, for example,
full-text search functions available in XQuery. We discuss support for
externally defined functions in
Issue-0009:
Externally defined functions
2.19 Structural recursion
XML documents can be recursive in structure, for example, it is possible to
define a
part
element that directly or indirectly
contains other
part
elements. In XQuery, we use
recursive types to define documents with a recursive structure, and we use
recursive functions to process such documents. (We can also use mutually
recursive functions for more complex recursive structures.)
For instance, here is a recursive type defining a part hierarchy.
TYPE Part = Basic | Composite
TYPE Basic =
ELEMENT basic (
ELEMENT cost (xs:integer)
TYPE Composite =
ELEMENT composite (
ELEMENT assembly_cost(xs:integer)
ELEMENT subparts (Part+)
And here is some sample data.
LET $part0 :=

12


22

33


7

: Part
RETURN ...
Here vertical bar (
) is used to indicate a
choice between types: each part is either basic (no subparts), and has a cost,
or is composite, and includes an assembly cost and subparts.
We might want to translate to a second form, WHERE every part has a total
cost and a list of subparts (for a basic part, the list of subparts is
empty).
TYPE Part2 =
ELEMENT part (
ELEMENT total_cost (xs:integer),
ELEMENT subparts (Part2*)
Here is a recursive function that performs the desired transformation. It
uses a new construct, the
typeswitch
expression.
DEFINE FUNCTION convert(Part $p) RETURNS Part2 {
TYPESWITCH ($p) AS $x
CASE Basic RETURN

{ $x/cost/data() }


CASE Composite RETURN
LET $s := (FOR $y IN $x/subparts/* RETURN convert($y))
RETURN


{ $q/assembly_cost/data() +
sum($s/total_cost/data()) }

{ $s }

DEFAULT RETURN ERROR
Each branch of the typeswitch expression is labeled with a type,
Basic
or
Composite

The evaluator checks the type of the value of
$p
at
query-evaluation time, i.e., run time,
and evaluates the corresponding branch.
If the first branch is taken then
$x
is bound to the
value of
$p
, and the branch returns a new part with total cost the
same as the cost of
$x
, and with no subparts. If the second
branch is taken, then
$x
is bound to the value of
$p
. The
function is recursively applied to each of the subparts of
$x
giving a sequence of new subparts
$s
. The branch returns a new part
with total cost computed by adding the assembly cost of
$x
to the
sum of the total cost of each subpart in
$s
, and with subparts
$s
One might wonder why
$x
is required,
since it has the same value as
$p
. The reason why is
that
$p
and
$x
have different
types.
$p : Part
$x : Basic -- in the first branch
$x : Composite -- in the second branch
The type of
$x
is more precise than
the type of
$p
, because which branch is taken depends upon
the type of value in
$p
Applying the query to the given data gives the following result.
convert($part0)
==>
74


55


33





7




: Part2
Of course, a
typeswitch
expression may be used in any
query, not just in a recursive one.
2.20 Functions for all well-formed documents
[XML Schema : Formal Description]
defines a ``root'', or most general
type, for the four kinds of schema components: elements, attributes,
simple types, and complex types.
They are named
xs:AnyElement
xs:AnyAttribute
xs:AnySimpleType
and
xs:AnyComplexType
, respectively.
The type
xs:AnySimpleType
stands
for the most general simple type. All built-in primitive types
(like
xs:integer
or
xs:string
and lists of simple types are subtypes of it.
The built-in simple types are listed in
3.4 Atomic simple types
The remaining schema components are defined as follows:
TYPE xs:AnyTree = xs:AnySimpleType
| xs:AnyElement
| xs:AnyAttribute
TYPE xs:AnyAttribute = ATTRIBUTE *:* (xs:AnySimpleType)
TYPE xs:AnyElement = ELEMENT *:* (xs:AnyComplexType)
TYPE xs:AnyComplexType = xs:AnyAttribute*,
((xs:AnyElement | xs:string)* | xs:AnySimpleType)
TYPE xs:AnyType = (xs:AnyTree)*
The type
xs:AnyTree
denotes any simple type, element, or attribute.
The type
xs:AnyAttribute
stands for the most general attribute type, which
may have any name, and its content must have type
xs:AnySimpleType
, i.e., it may contain simple values,
but no elements.
The type
xs:AnyElement
stands for the most general element type,
which may have any name, and its content must be a
complex type.
The type
xs:AnyComplexType
stands for the most
general complex
type,
which is any sequence of attributes followed by any sequence of
elements or strings or by any simple type.
Strings are permissible in a complex type because an element may
contain
mixed
content, i.e., character data interleaved
with other elements.
Finally,
xs:AnyType
is a sequence of
any tree.
In particular, our earlier data also has type
xs:AnyElement
$book0 : xs:AnyElement
==>

Abiteboul
Buneman
Suciu

: xs:AnyElement
A specific type can be indicated for any expression in the query language,
by writing a colon and the type after the expression.
As an example
of a function that can be applied to all well-formed documents,
we define a recursive function that converts any XML data
into HTML. We first give a simplified definition of HTML.
TYPE HTML_body =
( xs:AnySimpleType
| ELEMENT b(HTML_body)
| ELEMENT ul ((ELEMENT li (HTML_body))*)
) *
An HTML body consists of a sequence of zero or more items, each of which is
either a simple value, or a
element, where the content is
an HTML body, or an
ul
element, where the children
are
li
elements, each of which has as content an HTML
body.
Now, here is the function that performs the conversion.
DEFINE FUNCTION html_of_xml( xs:AnyTree $x ) RETURNS HTML_Body {
TYPESWITCH ($x) AS $z
CASE xs:AnySimpleType RETURN $z
CASE xs:AnyAttribute RETURN
{ name($z) } ,

{ FOR $y IN $z/data() RETURN
• { html_of_xml($y) }
}

{ FOR y IN $z/@* RETURN
• { html_of_xml($y) }
• }

{ FOR y IN $z/* RETURN
• { html_of_xml($y) }
}

• year
  • 1999


• isbn
  • 1-55860-622-X


• title
  • Data on the Web


• author
  • Abiteboul


• author
  • Buneman


• author
  • Suciu

For a textbook introduction to type systems, see, for
example,
[Mitchell]
In inference notation, when all judgements above the line
hold, then the judgement below the line holds as well. Here is an example
of a rule used later on:
|-
Data
|-
Data
|-
Data
Data
Data
is the subset of expressions that consists only of
literal constant, attribute,
element, sequence, and empty-sequence expressions.
Data
::=
Literal
literal constant
attribute
NCName
Data
attribute
NCName
/>
empty element
NCName
> {
Data
} <
NCName
element
Data
Data
sequence
()
empty sequence
The judgement "|-
Data
is read as "in the empty environment, the value
Data
has type
."
The symbol |- is called a
turnstyle
, and is usually preceded by an
environment symbol, which represents
a mapping from variables to values.
In this example, there is no environment symbol,
which means the judgement holds in the empty environment.
In
4.4 Expressions
, we will see examples of rules that
have non-empty environments.
The rule states that if both
Data
and
Data
hold, then
Data
Data
holds as well.
For instance, take
Data
{ 1
}
Data
{ "two" }
ELEMENT a
(xs:integer)
ELEMENT b (xs:string)
Then since both these hold:
{ 1 } : ELEMENT a (xs:integer)
{ "two" } : ELEMENT b (xs:string)
we may conclude that the following holds:
{ 1 }, { "two" }
: ELEMENT a (xs:integer), ELEMENT b (xs:string)
4.1 Relating data to types
The following type rules relate
Data
values to types.
The next rule rules states that a literal
NCName
has the type
xs:NCName
The following three rules are analogous for strings and
double precision numbers.
|-
NCName
xs:NCName
|-
StringLiteral
xs:string
|-
NumericLiteral
xs:double
Ed. Note:
MF: Analogous rules are necessary for all the functions that construct Schema simple-typed values.
The next three rules are for attribute and element construction.
The first rule states that if
Data
has type
, then the attribute expression
attribute
NCName
Data
has type
ATTRIBUTE
NCName
). The subsequent rules are
analogous for element expressions.
|-
Data
|-
attribute
NCName
Data
ATTRIBUTE
NCName
|-

NCName
/> :
ELEMENT
NCName
()
|-
Data
|-

NCName
Data
NCName
> :
ELEMENT
NCName
The next rule states that the empty sequence value always has the empty
sequence type:
|-
()
()
This rule was described above:
|-
Data
|-
Data
|-
Data
Data
The rules above associate the most specific type possible with a
Data
value.
The remaining rules in this section associate more general types
with a
Data
value, which are necessary when the type
system must determine whether a
Data
value with
most specific type
is permissible when a value of type
t'
is expected.
This occurs during type checking of a query.
The next two rules are also for attribute and element construction,
but these rules specify more general types.
The first rule states that if
Data
has type
, and
NCName
is in the set of names defined
by the wildcard expression
NameSet
then the given attribute expression also
has type
ATTRIBUTE
NameSet
). The subsequent rules are analogous for element expressions.
|-
Data
NCName
<:
Wild
NameSet
|-
attribute
NCName
Data
ATTRIBUTE
NameSet
NCName
<:
Wild
NameSet
|-

NCName
/> :
ELEMENT
NameSet
()
NCName
<:
Wild
NameSet
|-
Data
|-

NCName
Data
NCName
> :
ELEMENT
NameSet
The next rule states that the sequence of one value with type
followed by a value with repetition type
min
max
has repetition type
min
+1
max
+1.
|-
Data
|-
Data
min
max
|-
Data
Data
min
+1)
max
+1)
The next rule states that the empty sequence is a repetition of any type
with lower bound 0:
|-

():
min
max
4.2 Equivalences and subtyping
The symbol <: denotes the subtype relation.
We write
<:
if
for every data
Data
such that |-
Data
, it
is also the case that |-
Data
, i.e.,
is
is a subtype
of
The subtyping relation is used in many of the type rules that follow.
It is easy to see that the subtype relation <: is
a partial order, i.e., it is reflexive,
<:
, and it is transitive, if
<:
and
<:
then
<:
Here are some of the inequalities that hold:
<:
<:
xs:AnyType
<:
xs:AnySimpleType
<:
<:
Further, if
QName
<:
wild
NameSet
and
<:
', then
ELEMENT
QName
<:
ELEMENT
NameSet
')
If
<:
and
>=
' and
<=
' then
min
max
<:
t'
min
max
If
<:
and
<:
then
<:
',
<:
' &
<:
' &
We
write
if
<:
and
<:
Here are some of the equalities that hold:
min
max
),
, ()
(),
, Ø
Ø,
| Ø
Ø |
) |
),
) |
) &
& ()
() &
& Ø
Ø &
ELEMENT
NameSet
ELEMENT
NameSet
ELEMENT
NameSet
ELEMENT
NameSet
) |
ELEMENT
*:* (
ELEMENT
*:* (
min
max
+1
min
max
min
max
+1
() |
, (
min
max
min
max
()
min
max
Ø,
if
or
We also have
that
<:
if
and only if
We define the
intersection
/\
of two types
and
to be the largest type
that is smaller than both
and
That is,
/\
if
<:
and
<:
and if for any
t'
such that
t'
<:
and
t'
<:
we have
t'
<:
4.3 Environments
The type rules use an environment
comprised of a type environment and a namespace environment,
defined in
Figure 6
in
TypeEnv = (
Variable
->
Type
Type environment
QName
->
QName
Type
, ...,
Type
returns
Type
NS
in
NamespaceEnv =
NCName
->
anyURI
Namespace environment
in
Env = TypeEnv
NamespaceEnv
Static environment
Figure 6: Environments used in type-inference rules
The type environment T is a finite map from
variables and function names to types.
Part of an attribute or element's type is its tag name, which
is a
QName
. A
QName
contains
a namespace prefix, whose meaning depends on the namespace
environment NS, which is a finite map from namespace prefixes (NCNames)
to namespace URIs.
The namespace environment is modified by namespace declarations
and by element constructors that contain namespace declarations.
To select the type-environment component of an environment, we use
the notation T of
; similarly, we use
NS of
to select the namespace
environment.
We retrieve type information from the environment by
writing
T (
Variable
)=
to look up a
variable, or by writing
T(
QName
) = (
QName
, ...,
returns
to look up a function type.
We write
NS(
NCName
) =
anyURI
to look up a namespace prefix.
It is often necessary to modify an environment, for example, when
defining variables or functions.
The modification of one environment
by another
is written
' and it denotes:
' = ((T of
),
(T' of
'); (NS of
),
(NS' of
'))
The finite map
is the finite map with domain Dom
Dom
and values
)(a) = if a in Dom
then
(a) else
(a)
This definition means that when ``looking up'' a variable
in the environment
', the environment
' will always be searched first.
The type checking starts with
an empty type environment.
As type checking proceeds, new
variables are added to the type environment
and new namespace prefixes are added to the namespace environment.
For instance, when typing the query
of
2.4 Iteration
variable
$b
will be typed with
Book
and
added in the
environment. This will result in a new environment:
G' = G, $b : Book
4.4 Expressions
We write
|-
Expr
if
in
environment
the
expression
Expr
has type
Below are
all the rules except those for
for
and
typeswitch
expressions, which are discussed in
later subsections.
The following rule states
that in any environment
the literal
NCName
has the type
xs:NCName
The two subsequent rules are analogous for strings and
numerical values.
For example,
|- 1 :
xs:integer
and
|- "two" :
xs:string
|-
NCName
xs:NCName
|-
StringLiteral
xs:string
|-
NumericLiteral
xs:double
The next rule simply states the variable
Variable
has type
in environment
(T of
)(
Variable
) =
|-
Variable
Part of an attribute or element's type is its tag name, which
is a
QName
Before computing the type of an attribute or element, we convert
the attribute or element's
QName
into an
expanded
QName
The inference rule below converts a
QName
into an
expanded QName
by mapping its namespace
prefix to a namespace URI. Later rules rely on this
judgement to resolve the namespace prefixes that occur in the
QNames
of elements and attributes.
QName
NCName
NCName
(NS of
)(
NCName
) =
anyURI
|-
QName
=> {
anyURI
NCName
The next two rules are for attribute and element construction with
a constant tag name.
The first rule states that if
Expr
has type
and that
QName
resolves to the given
expanded QName
then the attribute expression
ATTRIBUTE
QName
Data
has type
ATTRIBUTE
expQName
). The subsequent rules are
analogous for element expressions.
|-
Expr
|-
QName
=>
expQName
|-
ATTRIBUTE
QName
Expr
):
ATTRIBUTE
expQName
|-
QName
=>
expQName
|-

QName
/> :
ELEMENT
expQName
()
|-
Expr
|-
QName
=>
expQName
|-

QName
> {
Expr
} QName
> :
ELEMENT
expQName
Ed. Note:
MF: (08-May-2001) The above rules do not
handle namespace attributes in element constructors,
e.g.,
xmlns:foo="http://www.foo.com/foo.xsd">
These need to be added. In mapping from XQuery to core,
all namespace attributes should occur before other attributes.
The next rule is for element construction in
which the tag name is computed.
The built-in function
make-attribute
is used to construct an attribute with a computed tag; its typing rule
appears in
4.6 Built-in functions

The rule states that if
Expr
has type
then the element expression with computed tag
Expr
has type
ELEMENT
*:*
).
Ed. Note:
MF: Note that the types are less precise than in
Algebra, which supported name expressions and wildcard types.
This probably makes the 80-20 cut.
|-
Expr
xs:QName
|-
Expr
|-

<{
Expr
}> {
Expr
:
ELEMENT *:*
The following two rules are analogous to the sequence and empty
sequence rules in
4.1 Relating data to types
|-
Expr
|-
Expr
|-
Expr
Expr
|-

() : ()
Note that in the type rule for a conditional expression,
the result type is the choice (
).
|-
Expr
xs:boolean
|-
Expr
|-
Expr
|-
if
Expr
then
Expr
else
Expr
let
expression extends the type environment
by mapping
Variable
to type
Note that
Expr
the body of the
let
expression,
is typed in the extended environment, and the type of the entire
let
expression is
|-
Expr
Variable
|-
Expr
|-
let
Variable
:=
Expr
return
Expr
The next rule is for function application.
In a function application,
the type of each actual argument to the function
must be a
subtype
of the corresponding formal argument to the
function, i.e.,
it is not necessary for the actual and formal types to be equal.
(T of
)(
QName
) =
QName
, ···,
returns
|-
Expr
t'
t'
<:
···
|-
Expr
t'
t'
<:
|-
QName
Expr
, ···,
Expr
The next rule states
that it is always permissible to explicitly type an expression with a type
t'
that is a supertype of the expression's type
. In programming-language terminology,
this operation is sometimes called an ``upcast''.
|-
Expr
t'
t'
<:
|-

Expr
) :
The
cast
operator converts the type of an expression to
the given atomic simple type.
Ed. Note:
MF: the relationship between
and
p'
depends on operator work.
|-
Expr
p'
<:
|-
cast as
p'
Expr
) :
p'
The
error
expression always has the empty choice type.
|-
error
: Ø
4.5 Operators
A joint task force on operators with members from the XSLT, XML
Schema, and XML Query working groups is chartered to define
the operators for XQuery and XPath 2.0.
The complete set of operators will be
defined in a forthcoming document by that group,
so it is not possible to give the typing rules for all operators here.
(See
Issue-0056:
Operators
on Simple Types
).
In general, however, arithmetic operators will have a type rule such
as the following, in which
and
are numeric types and
appropriate type conversions exist between the two:
|-
Expr
|-
Expr
result-type
|-
Expr
Op
arith
Expr
Equality and inequality operators are typed similarly.
|-
Expr
|-
Expr
|-
Expr
Op
eq
Expr
xs:boolean
Boolean operators require that their subexpressions be boolean
expressions.
|-
Expr
xs:boolean
|-
Expr
xs:boolean
|-
Expr
Op
bool
Expr
xs:boolean
The type rules for the collection operators,
Op
coll
, are given in
4.7 Typing unordered expressions
4.6 Built-in functions
The following type rules define the input and output types for
built-in functions.
|-
Expr
|-
count
Expr
) :
xs:integer
The next two rules are for comment and processing
instruction constructors.
|-
Expr
xs:string
|-
comment
Expr
) :
COMMENT
|-
Expr
xs:NCName
|-
Expr
xs:string
|-
processing-instruction
Expr
Expr
) :
PROCESSING-INSTRUCTION
In the core syntax, all character-data
literals are expressed using
the built-in
pcdata
(parsable character data) function.
The type of PCDATA is always
xs:AnySimpleType
|-
pcdata(
StringLiteral
xs:AnySimpleType
Attributes with computed tag names are constructed by the
make-attribute
This rule states that if
Expr
has type
then the attribute expression with computed tag
Expr
has type
ATTRIBUTE
*:*
).
|-
Expr
xs:QName
|-
Expr
|-
make-attribute
Expr
Expr
) :
ATTRIBUTE *:*
The name of an attribute or element always has type
xs:QName
|-
Expr
ATTRIBUTE
NameSet
|-
name
Expr
) :
xs:QName
|-
Expr
ELEMENT
NameSet
|-
name
Expr
) :
xs:QName
The
attributes
and
children
accessors only apply to values with
element type.
|-
Expr
ELEMENT
NameSet
<:
xs:AnyAttribute
xs:AnyElement
xs:string
)*
|-
attributes
Expr
) :
|-
Expr
ELEMENT
NameSet
<:
xs:AnyAttribute
xs:AnyElement
xs:string
)*
|-
children
Expr
) :
The next two rules are for name expressions: they extract the
constituent parts of a name.
|-
Expr
|-
<:
xs:AnyElement
xs:AnyAttribute
PROCESSING-INSTRUCTION
COMMENT
|-
namespace-uri
Expr
xs:uriReference
|-
Expr
|-
<:
xs:AnyElement
xs:AnyAttribute
PROCESSING-INSTRUCTION
COMMENT
|-
local-name
Expr
) :
xs:NCName
The next rule is for the
parent
function, which may be
applied to any unit type:
|-
Expr
|-
parent
Expr
) :
xs:AnyElement
The next two rules are for the reference constructor and
dereference function. Note that
ref
requires that its argument have a unit type.
|-
Expr
|-
ref
Expr
) :
REFERENCE
|-
Expr
REFERENCE
|-
deref
Expr
) :
The next rule is for the
string-value
of
a unit value.
|-
Expr
|-
string-value
Expr
) :
xs:string
The accessor
typed-value
returns the simple typed value of an attribute or
element. An attribute always contains a simple typed value,
therefore
typed-value
simply returns the attribute's
typed content.
An element may contain a simple-typed value or a complex-typed value.
The second and third rules below distinguish between these two cases.
|-
Expr
ATTRIBUTE
NameSet
|-
typed-value
Expr
) :
|-
Expr
ELEMENT
NameSet
<:
xs:AnySimpleType
|-
typed-value
Expr
) :
|-
Expr
ELEMENT
NameSet
<:
xs:AnyComplexType
|-
typed-value
Expr
) :
()
4.7 Typing unordered expressions
The built-in functions
index
and
unordered
and the operator
sortby
disregard the relative order of components
in their input type.
For example, consider the following.
index (children (book0))
==> (1
,
2
Abiteboul,
3
Buneman,
4
Suciu,
5
1999)
By nesting the children of
book0
under
snd
the original sequence of
title, author+, year
gets lost. The
snd
element can contain
either a
title
, an
author
, or a
year
To compute a meaningful type for this expression,
we need to find a type
, and
such
that
children(book0) : q min m max n
and then the type is given by
index(children(book0)) :
ELEMENT q:pair(
ELEMENT q:fst (xs:integer),
ELEMENT q:snd (REFERENCE (ELEMENT author (q)))
) min m max n
In the case
of books, the values of
are:
ELEMENT title (xs:string) |
ELEMENT author (xs:string)
the value of
is three (because there will be
one
title
at
least one
author
, and one
year
element) and the value of
is *
(because
there may be any number of author elements).
We call a type like
prime
type. In general, it may contain scalar,
attribute, element,
choice, and empty choice types, but it will not contain repetition, sequence,
or
empty sequence types (except, perhaps, within an element or attribute type). The
definition of prime types appears in
Figure 4
factor
min
max
factor
ELEMENT
NameSet
))
ELEMENT
NameSet
min
max
factor
ATTRIBUTE
NameSet
))
ATTRIBUTE
NameSet
min
max
factor
min
max
where
min
max
factor
factor
min
max
where
min
max
factor
factor
min
(min
max
max
where
min
max
factor
factor
min
max
min
m'
max
' ·
where
min
max
' =
factor
factor
(())
min
max
factor
(Ø)
min
max
Figure 7: Definition of factoring
The
factor
function, as shown in
Figure 7
converts any type
to a type of
the form
min
max
where
<:
min
max

so that any value that has type
also has type
min
max

For example,
factor (ELEMENT title (xs:String),
ELEMENT author (xs:String) min 1 max *,
ELEMENT year (xs:integer)) =

(ELEMENT title (xs:string) |
ELEMENT author (xs:string) |
ELEMENT year(xs:integer)) min 3 max *
We can see here that the factored type is less specific than the
unfactored type.
For convenience we write
min
max
factor
), but one should
actually
think of the
function as
returning a triple consisting of a prime type
and
two
bounds
and
Just as factoring a number yields a product of prime
numbers, factoring a type yields a repetition of prime types. Further, the
result yielded by factoring is in some sense optimal. If
min
max
factor
) then
<:
min
max
and for any
',
', and
' such that
<:
min
max
' we have
that
<:
' and
>=
and
<=
'. Also, if
',
then
factor
) =
factor
'). In particular,
the
choice of the lower bound
for
factor
(Ø)
guarantees that
factor
) =
factor
Ø), since
min
Using
factor
, we can type
index
sortby
unordered
and the
union
difference
, and
intersection
operations. Note
that
factor
is only used by the type inference
rules; it is not part of XQuery expressions.
The type rule for
index
requires that
its argument be a factored type. The second expression
above the judgement line converts
into a factored type.
|-
Expr
min
max
factor
|-
index
Expr
) :
ELEMENT q:pair(ELEMENT q:fst (xs:integer),
ELEMENT q:snd (REFERENCE (
)))
min
max
The types of aggregated expressions must be factored, and their
prime type must be a numeric type.
|-
Expr
min
max
factor
<:
xs:decimal
xs:double
|-
agg
Expr
agg
is one of
avg
max
min
sum
The
sortby
operator returns the
factor
of
its input type.
|-
Expr
|-
Expr
min
max
factor
|-
Expr
sortby
Expr
ascending
descending
):
min
max
Ed. Note:
MF, Oct 23/2000: This definition assumes that the
equality operator on
is defined. An alternative is requiring
Expr
to have
xs:AnySimpleType
, but that seems too restrictive.
The
distinct-node
function removes all duplicate nodes from its input.
|-
Expr
min
max
factor
|-
distinct-node
Expr
) :
min
(1 min
max
Ed. Note:
PF (Jan 29, 2000): a more accurate lower bound may be derived by
counting the disjoint constituent types of
. But this is probably
too complex.
The
distinct-value
function removes all duplicate values from its input. The typing
rule is analogous to that of
distinct-node
except the lower bound
can be at most one.
|-
Expr
min
max
factor
' = 1 min
|-
distinct-value
Expr
) :
min
max
Similar to
distinct-value
and
distinct-node
, the
intersect
and
except
operators
need to set the lower bound of the cardinality of the input type to 0.
The upper bound of the cardinality of the intersection of two types can be at
most the minimum of upper bounds of their individual cardinalities.
|-
Expr
|-
Expr
min
max
factor
|-
Expr
union
Expr
min
max
|-
Expr
|-
Expr
min
max
factor
min
max
factor
|-
Expr
intersect
Expr
/\
min
max
min
|-
Expr
|-
Expr
min
max
factor
min
max
factor
|-
Expr
except
Expr
min
max
The
unordered
function ignores the order of the items in
its sequence argument, therefore its type is also a factored type.
|-
Expr
min
max
factor
|-
unordered
Expr
) :
min
max
4.8 Iteration expressions
The typing of
for
expressions is rather subtle. We give an intuitive
explanation first and then the detailed typing rules below.
unit
type is defined in
Figure 4
it is either an simple type,
an attribute or element type with a constant or wildcard
name, a comment, or a processing instruction. A
for
expression
for
Variable
in
Expr
return
Expr
is typed as follows. First, one finds the type of expression
Expr
Next, for each unit type in this type one assumes the variable
Variable
has the unit type and one types the body
Expr
. Note that this
means we may type the body of
Expr
several times, once for each
unit type in the type of
Expr
. Finally, the types of the body
Expr
are combined, according to how the types were combined in
Expr
That is, if the type of
Expr
is formed with sequencing, then
sequencing is used to combine the types of
Expr
, and similarly
for choice or repetition.
For example, consider the following expression, which selects all
author
elements from a book.
for $c in children($book0) return
typeswitch ($c)
case $a : ELEMENT author(xs:AnyType) return $a
default return ()
The type of
children(book0)
is
ELEMENT title(xs:String), ELEMENT year(xs:integer), ELEMENT author(xs:string)+
This is composed of three unit types, and so the
body is typed three times.
assuming
$c
has type
ELEMENT title(xs:string)
the body has type
()
ELEMENT year(xs:integer)
()
ELEMENT author(xs:string)
ELEMENT author(xs:String)
The three result types are then combined in the same way the
original unit types were, using sequencing and iteration.
(), (), ELEMENT author(xs:string)+
as the type of the iteration, and simplifying yields
ELEMENT author(xs:string)+
as the final type.
As a second example, consider the following expression, which selects all
title
and
author
elements from a book, and renames them.
for $c in $book0/* return
typeswitch ($c)
case ELEMENT title (xs:string) return
{ t/data() }
case ELEMENT year (xs:integer) return
()
case ELEMENT author (xs:string) return
{ a/data() }
default return ERROR
Again, the type of
book0/*
is
ELEMENT title(xs:string), ELEMENT year(xs:integer), ELEMENT author(xs:string)+
This is composed of three unit types, and so the
body is typed three times.
assuming
$c
has type
ELEMENT title(xs:string)
the body has type
ELEMENT titl(xs:string)
ELEMENT year(xs:integer)
()
ELEMENT author(xs:string)
ELEMENT auth(xs:string)
The three result types are then combined in the same way the
original unit types were, using sequencing and iteration.
This yields
ELEMENT titl(xs:string), (), ELEMENT auth(xs:string)+
as the type of the iteration, and simplifying yields
ELEMENT titl(xs:string), ELEMENT auth(xs:string)+
as the final type.
Note that the title occurs just once and the author occurs one or more times,
as one would expect.
As a third example, consider the following expression, which selects all basic
parts from a sequence of parts.
for $p in $part0/subparts/* return
typeswitch ($p)
case Basic return $b
case Composite return ()
default return ERROR
The type of
part0/subparts/*
is
(Basic | Composite)+
This is composed of two unit types, and so the
body is typed two times.
if
$p
has type
Basic
the body has type
Basic
Composite
()
The two result types are then combined in the same way the
original unit types were, using sequencing and iteration.
This yields
(Basic | ())+
as the type of the iteration, and simplifying yields
Basic*
as the final type.
Note that although the original type involves repetition one or
more times, the final result is a repetition zero or more times.
This is what one would expect, since if all the parts are composite
the final result will be an empty sequence.
In this way, we see that
for
expressions can be combined with
typeswitch
expressions
to select and rename elements from a sequence, and that the result is given a
sensible type.
In order for this approach to typing to be sensible, it is necessary that
the unit types can be uniquely identified. However, the type system given
here satisfies the following law.
ELEMENT a (t1 | t2) = ELEMENT a (t1) | ELEMENT a (t2)
This has one unit type on the left, but two distinct unit types on
the right, and so might cause trouble. Fortunately, our type
system inherits an additional restriction from XML Schema: we
insist that the regular expressions can be recognized by a top-down
deterministic automaton. In that case, the regular expression must
have the form on the left, the form on the right is outlawed because
it requires a non-deterministic recognizer. With this additional
restriction, there is no problem.
The method of translating projection to iteration described in
the previous section combined with the typing rules given here
yield optimal types for projections, in the following sense.
Say that variable
has type
, and the projection
x / a
has type
t'
. The type assignment is
sound
if for every value of type
, the value of
x / a
has type
t'
. The type assignment is
complete
if for every value
of type
t'
there is a value
of type
such that
x / a = y
. In symbols, we can see that
these conditions are complementary.
sound:
forall
in
exist
in
t'
x / a = y
complete:
forall
in
t'
exist
in
x / a = y
Any sensible type system must be sound, but it is rare for a type
system to be complete. But, remarkably, the type assignment given
by the above approach is both sound and complete.
The type rule for for expressions uses the following auxiliary judgement. We
write
|-
for
Variable
return
Expr
t'
, if in environment
when the bound variable
Variable
of an iteration has type
then the body
Expr
of the iteration has type
t'
Variable
|-
Expr
t'
|-
for
Variable
return
Expr
t'
|-
for
Variable
()
return
Expr
()
|-
for
Variable
Expr
t'
|-
for
Variable
Expr
t'
|-
for
Variable
return
Expr
t'
t'
|-
for
Variable
Expr
t'
|-
for
Variable
Expr
t'
|-
for
Variable
return
Expr
t'
t'
|-
for
Variable
: Ø
return
Expr
: Ø
|-
for
Variable
Expr
t'
|-
for
Variable
Expr
t'
|-
for
Variable
return
Expr
t'
t'
|-
for
Variable
Expr
t'
|-
for
Variable
: (
min
max
return
Expr
: (
t'
min
max
Given the above rules, the type rules for
for
expressions are immediate.
|-
Expr
|-
for
Variable
return
Expr
|-
for
Variable
in
Expr
return
Expr
4.9 Typeswitch expressions
The typing of
typeswitch
expressions is closely related to
the typing of
for
expressions.
Due to the typing rules of
for
expressions, it is possible that the body of an iteration is checked
many times. Thus, when a
typeswitch
expression is checked, it is possible that quite
a lot is known about the type of the expression being matched, and one can
determine that only some of the clauses of the
typeswitch
apply. The definition of
typeswitch
uses the auxiliary judgements to check whether a given
clause is applicable.
We
write
|-
case
Variable
return
Expr
t'
, if in environment
, the
Variable
of the
typeswitch
has type
then the body
Expr
of
case
has type
t'
. Note the type of the body is irrelevant if
= Ø.
¬(
= Ø)
Variable
|-
Expr
t'
|-
case
Variable
return
Expr
t'
|-
case
Variable
: Ø
return
Expr
: Ø
We write
|-
<:
t'
default return
Expr
t''
if in environment
when
<:
t'
does not hold, then
the body
Expr
of the
typeswitch
expression's
default return
clause has type
t''
. Note that
the type of the body is irrelevant if
t'
<:
t'
|-
<:
t'
else
Expr
: Ø
<:
t'
|-
Expr
t''
|-
<:
t'
else
Expr
t''
Given the above, it is straightforward to construct the typing rule for a
typeswitch
expression. Recall that we write
/\
t'
for the intersection of two types.
|-
Expr
|-
case
Variable
/\
return
Expr
t'
···
|-
case
Variable
/\
return
Expr
t'
|-
| ... |
default return
Expr
n+1
t'
n+1
|-
typeswitch
Expr
as
Variable
case
return
Expr
···
case
return
Expr
default return
Expr
n+1
t'
| ... |
t'
n+1
4.10 Typing descendent-or-self
The built-in function
DESCENDENT-OR-SELF(expr)
implements the descendent-or-self
axis of XPath, and is used to express the sematics of the
//
operator.
For example, consider the following type declaration:
TYPE Part = Basic | Composite
TYPE Basic =
ELEMENT basic (
ELEMENT cost (xs:integer)
TYPE Composite =
ELEMENT composite (
ELEMENT assembly_cost (xs:integer)
ELEMENT subparts (Part+)
If
$v
has type
Part
, the XPath expression
$v//basic
would retrieve all
basic parts. We would rewrite this query into the core language as follows:
for $x in descendent-or-self($v) return
typeswitch ($x) as $z
case ELEMENT basic(xs:AnyType) return $z
default return ()
The type of
descendent-or-self($v)
is
(ELEMENT basic (
ELEMENT cost (xs:integer)
| ELEMENT cost (xs:integer)
| ELEMENT composite (
ELEMENT assembly_cost (xs:integer)
ELEMENT subparts (Part+)
| ELEMENT assembly_cost ( xs:integer )
| ELEMENT subparts ( Part+)
| xs:integer
) min 3 max *
The lower bound of 3 indicates that
descendent-or-self($v)
returns at least
three nodes,
ELEMENT basic (...)
ELEMENT cost (...)
, and
xs:integer
, which is what happens when
$v
is bound to a single
element of type
Basic
. Based on this type, the type of
$v//basic
is
ELEMENT basic (
ELEMENT cost (xs:integer)) min 0 max *
On the other hand, the type of
$v//part
is
()
, the empty
sequence, because no
part
element appears in the type
Part
(An expression with type
()
typically indicates a programming error,
unless the expression is
()
itself.)
The typing of
descendent-or-self
loses all information about the relative
ordering of the subparts. For instance, in
descendent-or-self($v)
it
is always the case that a
basic
element is immediately followed
(in document order) by a
cost
element, but this is not
reflected in the type above.
There are two reasons why information about order is not retained.
First, there may exist two locally declared elements,
e.g.,
ELEMENT foo(type1)
and
ELEMENT foo(type2)
with the same name but different content-type. Maintaining their
relative order at type level would generate the invalid type
ELEMENT foo(type1) ... ELEMENT foo(type2)
whereas
ELEMENT foo(type1) | ELEMENT foo(type2)
can be
transformed to the valid type
ELEMENT foo( type1 | type2)
Second, for some recursive types, maintaining the relative order of
elements leads to a context-free type. For example, with
TYPE type1 = ELEMENT a (type1 min 0 max 1), ELEMENT b ()
the type of descendents would need to be the context-free type
TYPE type1' = ELEMENT a (type1 min 0 max 1), type1', ELEMENT b ()
but there is no equivalent regular type expressible in our system.
In principle,
DESCENDENT-OR-SELF(expr)
could be expressed
as a recursive user defined function:
DEFINE FUNCTION descendent-or-self (xs:AnyTree $x)
RETURNS (xs:AnyElement | xs:AnyScalar) min 0 max * {
TYPESWITCH ($x)
CASE (Comment|PI|AnyAttribute) RETURN ()
DEFAULT RETURN
($x, FOR $z IN children($x) RETURN descendent-or-self($z))
However, this loses far too much type information. With this
definition and the translation above the type of
$v//basic
is
ELEMENT basic(xs:AnyType) min 0 max *
rather than
ELEMENT basic(ELEMENT cost(xs:integer)) min 0 max *
Similarly, the type of
$v//part
is (
ELEMENT part (AnyType) min 0 max *
rather than
()
, losing the chance to uncover a type error.
The rule for typing
descendent-or-self(expr)
is as follows.
|-
Expr
type
|-
descendent-or-self
Expr
recfactor
type
; Ø)
This uses the function recfactor defined in
Figure 8
. The function
recfactor
() is similar to
factor
(), but it applies to all the descendents
of a node.
To be precise,
recfactor
) takes a type
and a choice of type variables
. The
argument
is a factoring environment: initially the empty choice Ø,
it collects all the type variables encountered so far in a recursive traversal
of the type. If
is a type in which all elements have empty content
models, then
recfactor
; Ø) =
factor
).
recfactor
min
max
recfactor
ELEMENT
NameSet
);
ELEMENT
NameSet
) |
min
+ 1
max
+ 1)
where
min
+ 1
+ 1 =
recfactor
recfactor
ATTRIBUTE
NameSet
);
min
max
recfactor
min
max
where
min
max
recfactor
recfactor
min
max
where
min
max
recfactor
recfactor
min
(min
max
max
where
min
max
recfactor
recfactor
min
max
min
m'
max
' ·
where
min
max
' =
recfactor
recfactor
(();
min
max
recfactor
(Ø;
min
max
recfactor
recfactor
def
);
if
not
<:
recfactor
factor
def
))
min
max
if
<:
Figure 8: Definition of recursive factoring
4.11 Top-level declarations and query expressions
We write
|-
QueryModule
if in environment
the query module
QueryModule
is well-typed.
Context declarations are always well typed. Below, they have the
effect of updating the namespace environment.
|-
namespace
NCName
StringLiteral
|-
default namespace
StringLiteral
A type declaration is always well typed:
|-
type
NCName
A function declaration is well-typed if in the environment
extended with the type assignments for its formal variables,
its body is well-typed.
Variable
), ···
Variable
|-
Expr
t'
t'
<:
|-
define function
QName
Variable
, ···
Variable
returns
Expr
The function
static-env
constructs an environment by extracting type assertions
and namespace mappings from top-level declarations.
It constructs a two part environment: the first part is the type
environment, T, and the second part is the namespace environment,
NS.
static-env
type
((); ())
static-env
define function
QName
Type
Variable
···,
Type
Variable
returns
Expr
((
QName
|=>
QName
···,
returns
); ())
static-env
namespace
NCName
StringLiteral
(();
NCName
|->
StringLiteral
static-env
default namespace
StringLiteral
((); '' |->
StringLiteral
Note that the default namespace is represented in the namespace
environment by the empty string.
We write |-
QueryModule
if each declaration and expression in the query module is well typed.
|-
static-env
ContextDecl
),...,
static-env
ContextDecl
),
static-env
TypeDecl
),...,
static-env
TypeDecl
),
static-env
FunctionDecl
),...,
static-env
FunctionDecl
|-
ContextDecl
...
|-
ContextDecl
|-
TypeDecl
...
|-
TypeDecl
|-
FunctionDecl
...
|-
FunctionDecl
|-
Expr
...
|-
Expr
|-
ContextDecl
...
ContextDecl
TypeDecl
...
TypeDecl
FunctionDecl
...
FunctionDecl
Expr
...
Expr
5 Dynamic Semantics : Value-Inference Rules
XQuery's dynamic, or operational,
semantics is presented as value inference rules.
The value inference rules are similar to the type
inference rules in
4 Static Semantics : Type-Inference Rules
, but they relate
expressions to values or
semantic objects
XQuery's semantic objects are defined in
the
[XQuery 1.0 and XPath 2.0 Data Model]
An operational semantics specifies the order in which an XQuery
expression is evaluated and guarantees that every expression
can be reduced to a simple semantic object.
XQuery's dynamic semantics is modeled on the dynamic semantics
presented in
[Milner]
5.1 Semantic objects
ERROR
in
SimpleValue
in
Node
in
UnitValue =
SimpleValue
Node
in
Sequence
in
Values =
Sequence
{ERROR}
sc
in
SchemaComponent
Figure 9: Semantic objects
There are five categories of values in
[XQuery 1.0 and XPath 2.0 Data Model]
error
simple values
nodes
sequences
, and
schema components
There is a single error value, named ERROR.
Simple values are the union of all the value
spaces of XML Schema simple types.
A node is one of eight node kinds: element, attribute, namespace,
comment, processing-instruction, text, and
reference.
A unit value is the union of all simple values and nodes;
a unit value is an instance of the unit type
Figure 4
A sequence is an ordered collection of nodes,
simple values, or any mixture of nodes and simple values. A
sequence cannot be a member of a sequence.
An important characteristic of the data model is there is no
distinction between a unit value (i.e., a node or a simple value) and a singleton
sequence containing that value, i.e., a unit value is equivalent to a
singleton sequence containing that value and vice versa.
Value is the class of values that includes
all sequences and ERROR.
A schema component represents the type of
element nodes, attribute nodes, and simple values.
All the above classes, except ERROR, are infinite sets.
Figure 10
lists
several basic functions from
[XQuery 1.0 and XPath 2.0 Data Model]
used in the dynamic semantics.
append
Construct a sequence
from two or more sequences
empty-sequence
Constructs the empty sequence.
empty
Returns true if argument
is empty sequence, otherwise false.
head
Returns the first node
in a non-empty sequence
tail
Returns
items in a sequence excluding its first item.
schema-component
Returns
the schema component representing its type argument
Figure 10: Functions used in dynamic semantics
Ed. Note:
MF : (Jan-15-2001)
To define the sort expression completely, we need to specify what
basic sort operators are available.
5.2 Environments
The value inference rules use an environment, defined
in
Figure 11
, comprised of a static
environment, a value environment, and a function environment.
Static environment
VE
in
ValueEnv =
Variable
->
Value
Value environment
FE
in
FuncEnv =
QName
->
Expr
Variable
*)
Function environment
in
Env = StaticEnv
ValueEnv
FuncEnv
Figure 11: Environments used in value-inference rules
The static environment
is defined by the
static type rules
4 Static Semantics : Type-Inference Rules
The value environment VE is a finite map from variables to
values.
The function environment FE
is a finite map from function names to pairs containing
an expression that is
the body of the function
and a list of free variables that are the function's formal arguments.
An environment
is a tuple containing
a static enviroment, a value environment, and
a function environment.
In the value-inference rules,
we use the same notation
to select an environment and to
lookup values in an environment
as used in
4 Static Semantics : Type-Inference Rules
To select the static-environment component of an environment, we use
the notation
of
; similarly, we use
VE of
to select the value
environment and
FE of
for the function
environment.
We look up the type of a variable by writing
of
)(
Variable
) =
, and
we write
(VE of
)(
Variable
) =
to look up the value of a variable or
(FE of
)(
QName
) =
to look up a
function.
It is often necessary to modify an environment, for example, when
defining variables or functions.
The modification of one environment
by another
is written
' and it denotes:
' = ((
of
),
' of
'); (VE of
),
(VE' of
'); (FE of
),
(FE' of
'))
The finite map
is the finite map with domain Dom
Dom
and values
)(a) = if a in Dom
then
(a) else
(a)
This definition means that when ``looking up'' a variable
in the environment
', the environment
' will always be searched first.
5.3 Expressions
Each rule of the dynamic semantics are inferences among sentences of
the form:
|-
phrase
=>
where
is an environment,
phrase
is a phrase in
the core syntax
Figure 1
, and
is a
semantic object.
As in
4 Static Semantics : Type-Inference Rules
when all judgements above the line of an inference rule
hold, then the judgement below the line holds as well.
The following three rules state that in any environment,
a string, numeric, or boolean literal
reduces to the value it denotes.
The XQuery/XPath 2.0 function library provides constructors
for all simple-typed values. Those constructors are used here:
|-
StringLiteral
=> xfo:string(
StringLiteral
|-
NumericLiteral
=> xfo:double(
NumericLiteral
|-
BooleanLiteral
=> xfo:boolean(
BooleanLiteral
The next rule determines the value of a variable,
which is simply the variable's value in the current value environment VE:
(VE of
)(
Variable
) =
|-
Variable
=>
(NS of
)(
NCName
=>
|-
NCName
NCName
=>
xfo:expanded-QName(
NCName
|-
Expr
=>
|-

Expr
} =>
The next rule constructs an attribute node from
its name and value sub-expressions.
This is the first rule that uses the static type environment:
the run-time type
schema-component
) of the
attribute is obtained from the type environment
|-
NameSpec
=>
|-
Expr
=>
of
) |-
ATTRIBUTE
NameSpec
Expr
|-
ATTRIBUTE
NameSpec
Expr
) =>
attribute-node(
, schema-component(
))
The next rule constructs an empty element.
|-
NameSpec
=>
of
|-

NameSpec
/> :
|-

NameSpec
/> =>
element-node(
, empty-sequence(),
empty-sequence(), empty-sequence(), schema-component(
))
The following
rule constructs an element from
its name and children sub-expressions.
The element constructor in
[XQuery 1.0 and XPath 2.0 Data Model]
requires
that all children be nodes, which means that any simple-typed value
in the element's sequence of child expressions
must be converted to a text node before applying the constructor.
The auxilliary function simple-to-text-node defined below performs
this conversion.
|-
NameSpec
=>
|-
Expr
=>
of
|-

NameSpec
> {
Expr
} NameSpec
> :
|-

NameSpec
> {
Expr
} NameSpec
=>
element-node(
, empty-sequence(),
empty-sequence(), simple-to-text-node(
), schema-component(
))
define function simple-to-text-node(xs:AnyTree* $s) returns xs:AnyTree* {
for $v in $s return
typeswitch ($v)
case xs:AnySimpleType return text-node(string-value($v))
default return $v
Ed. Note:
PF: Do we need to concatenate consecutive text-nodes ?
MF: The element constructor should do this.
The next rule constructs a sequence.
|-
Expr
=>
|-
Expr
=>
|-
Expr
Expr
=>
append(
We note here that in the
[XQuery 1.0 and XPath 2.0 Data Model]
, sequences
are always ``flat'', i.e., they do not contain other sequences.
The next three rules construct the union, difference, and
intersection
of two sequences.
The order of items in the resulting sequence is non-deterministic.
|-
Expr
=>
|-
Expr
=>
|-
Expr
union
Expr
=>
xfo:union(
|-
Expr
=>
|-
Expr
=>
|-
Expr
except
Expr
=>
xfo:difference(
|-
Expr
=>
|-
Expr
=>
|-
Expr
intersect
Expr
=>
xfo:intersect(
The next rule constructs the empty sequence.
|-

() => empty-sequence()
The next rule evaluates a conditional expression. If the
conditional's boolean expression
Expr
evaluates to true,
Expr
is evaluated and
its value is produced.
If the
conditional's boolean expression
evaluates to false,
Expr
is evaluated and
its value is produced.
|-
Expr
=> true
|-
Expr
=>
|-

if
Expr
then
Expr
else
Expr
=>
|-
Expr
=> false
|-
Expr
=>
|-
if
Expr
then
Expr
else
Expr
=>
The next rule evaluates a
let
expression:
it evaluates the body of the expression
Expr
in the environment
extended with the variable
Variable
bound to the value
|-
Expr
=>
, {
Variable
|->
} |-
Expr
=>
|-
let
Variable
:=
Expr
return
Expr
=>
The next rule evaluates a function application. It evaluates
all the function's arguments in the current environment, then extracts
the definition of the function's body from the function
environment.
It constructs a new environment that contains
the static and function environments of
and a new value environment that
maps
the function's formal arguments
Variable
· · ·
Variable
to the function's actual arguments,
and
then it evaluates the body of the function in this new environment.
|-
Expr
=>
···
|-
Expr
=>
(FE of
)(
QName
) = (
Expr
Variable
···
Variable
of
; {
Variable
|->
}, ·
· ·
Variable
|->
};
FE of
|-
Expr
=>
|-
QName
Expr
Expr
) =>
The next rule states that in any environment, the
error
expression evalutes to the ERROR
value.
|-
error
=> ERROR
5.4 Operators
The
[XQuery 1.0 and XPath 2.0 Data Model]
defines two equality functions,
xfo:node-equal and xfo:value-equal, which correspond to
XQuery's equality operators, '==' and '=', respectively.
These functions operate only on unit values, i.e.,
a singleton sequence containing a simple value or node.
|-
Expr
=>
|-
Expr
=>
|-
Expr
==
Expr
=>
xfo:node-equal(
|-
Expr
=>
|-
Expr
=>
|-
Expr
Expr
=>
xfo:value-equal(
The boolean operators
and
and
or
, and the boolean function
not
and defined in terms of
if-then-else
expressions.
E1 and E2 ==> if (E1) then (if (E2) then true else false) else false
E1 or E2 ==> if (E1) then true else (if (E2) then true else false)
not (E) ==> if (E) then false else true
We have not defined the semantics of all the arithmetic operators in
XQuery.
A joint task force on operators with members from the
[XSLT 99]
XML Schema, and XML Query working groups is chartered to define arithmetic
operators.
XQuery will adopt the decisions of that group
(See
Issue-0056:
Operators
on Simple Types
).
In the following two rules, we assume that the binary and unary
operators
are implemented by the
apply
function whose semantics are
defined by the operator task force and that
this function only operates on simple values.
|-
Expr
=>
|-
Expr
=>
|-
Expr
Op
arith
Expr
=>
apply(
Op
arith
|-
Expr
=>
= apply(
Op
|-
Op
Expr
=>
5.5 Built-in functions
There is a near one-to-one correspondence between
XQuery expressions for constructing and accessing
data model values
Figure 2
and the data model constructors and accessors.
The next three rules construct comment, processing instruction, and
reference nodes, respectively.
|-
Expr
=>
|-
comment
Expr
=>
comment-node(
|-
Expr
=>
|-
Expr
=>
|-
processing-instruction
Expr
Expr
=>
processing-instruction-node(
|-
Expr
=>
|-
ref
Expr
=>
reference-node(
The following rules define all of the accessor and other data-model functions.
In the following rule, the function name
denotes any
one of the following accessors:
nodes
|-
Expr
=>
|-
deref
Expr
=>
dereference(
|-
Expr
=>
|-
local-name
Expr
=>
local-name(
|-
Expr
=>
|-
namespace-uri
Expr
=>
namespace-uri(
|-
Expr
=>
|-
name
Expr
=>
name(
|-
Expr
=>
|-
parent
Expr
=>
parent(
|-
Expr
=>
|-
string-value
Expr
=>
string-value(
|-
Expr
=>
|-
typed-value
Expr
=>
typed-value(
The
sortby
expression may return any permutation of its input.
The easiest way to explain the dynamic semantics of
sortby
is to assume the existence of a function
stable-sort
that
takes a sequence of
pair
elements, each of which contains
a key value in its
fst
subelement
and the sort value in its
snd
subelement
The pairs are
sorted in ascending or descending order
based on the value in the
fst
subelement.
The purpose of is
stable-sort
is to explain the semantics of the
sortby
expression.
An implementation may choose
to implement the
sortby
expression as it chooses, as long as it guarantees
stability on sequences.
Given a
stable-sort
function, the semantics of
sortby
is defined in terms of a
for
expression, which constructs
the key, value pairs, and the
stable-sort
function.
E1 sortby E2 ascending ==>
let sorted-pairs :=
stable-sort(
for $dot in E1 return
E2$dot,
"ascending")
return sorted-pairs/q:snd/node()
E1 sortby E2 descending ==>
let sorted-pairs :=
stable-sort(
for $dot in E1 return
E2$dot,
"descending")
return sorted-pairs/q:snd/node()
5.6 Iteration expressions
The next two rules evaluate iteration expressions.
If the iteration expression evaluates to the empty sequence, then
the entire expression evalutes to the empty sequence.
|-
Expr
=>
empty(
|-

for
Variable
in
Expr
return
Expr
=> empty-sequence()
The next rule first evaluates the iteration expression
Expr
, which produces
the sequence
, ...,
For each unit value
in the sequence,
it evaluates the body of the iteration expression in the
environment
extended with the variable
Variable
bound to
which produces the value
All the
values are appended
into the result sequence.
|-
Expr
=>
, ···,
, {
Variable
|->
} |-
Expr
=>
···
, {
Variable
|->
} |-
Expr
=>
|-

for
Variable
in
Expr
return
Expr
=>
append(
···,
5.7 Typeswitch expressions
When evaluating a typeswitch expression, the variable
Variable
and the value
to match
against occurs on the left of the turnstile |-.
Each case rule of a typeswitch expression is always evaluated
against
this value. Alternative case rules are tried
from left to right.
The rule for the typeswitch expression evaluates its expression
and sets up the appropriate
environment for the case rules:
|-
Expr
=>
; (
Variable
) |-
CaseRules
=>
|-
typeswitch
Expr
as
Variable
CaseRules
=>
If the value
is in the domain of
the type expression
Type
the next rule
extends the environment by binding the variable
Variable
to
and evaluates the body of the case rule.
The
domain
of a type is the possibly
infinite set containing all values
that are instances of that type.
We can check whether a value
is in the
domain of a type by checking whether
's run-time type is
a subsumed by
Type
For an element or attribute, the
declaration
accessor in
[XQuery 1.0 and XPath 2.0 Data Model]
returns its run-time type.
For a simple value, the
type
accessor
returns its run-time type.
in Dom(
Type
, {
Variable
|->
} |-
Expr
=>
; (
Variable
) } |-
case
Type
return
Expr
CaseRules
=>
If the value
is not in the domain of
the type expression
Type
the next rule
evaluates the case rules following the current one.
The body of the given case rule is not evaluated if
is not in the domain of the given type.
not (
in Dom(
Type
))
; (
Variable
) |-
CaseRules
=>
; (
Variable
) |-
case
Type
return
Expr
CaseRules
=>
The next rule states that the else branch of a typeswitch expression
always evaluates to its given expression.
|-
Expr
=>
; (
Variable
) |-
default return
Expr
=>
5.8 Top-level declarations and query expressions
The value-inference rules for top-level declarations and query
expressions return a value.
All top-level declarations return
the empty-sequence value.
Context declarations
return the empty-sequence value.
|-
namespace
NCName
StringLiteral
=> ()
|-
default namespace
StringLiteral
=> ()
|-
type
NCName
=> ()
|-
define function
QName
Type
Variable
· · ·,
Type
Variable
returns
Type
Expr
} => ()
We use the function
dynamic-env
to compute the initial
environment for evaluating a query expression.
dynamic-env
type
) = (
static-env
type
); (); ())
dynamic-env
define function
QName
Type
Variable
···,
Type
Variable
returns
Type
Expr
} =
static-env
define function
QName
Type
Variable
···,
Type
Variable
returns
Type
Expr
}); (); (
QName
|=> (
Expr
Variable
, ···
Variable
)))
dynamic-env
namespace
NCName
StringLiteral
) =
static-env
namespace
NCName
StringLiteral
); (); ())
dynamic-env
default namespace
StringLiteral
) =
static-env
default namespace
StringLiteral
); (); ())
A function declaration extends the top-level environment
by
adding the mapping from the function's
QName
to
the expression that is the function's body,
and the function's formal arguments, i.e.,
a sequence of variables that are free in the function's body.
A top-level expression sequence has no effect on the environment
and returns a value that may be
returned to the programming environment in which the
XQuery expression is evaluated.
|-
Expr
=>
···
|-
Expr
=>
|-
Expr
···
Expr
=>
append(
, ···,
The expression sequence in a
QueryModule
is
evaluated in the dynamic environment computed by
dynamic-env
|-
dynamic-env
ContextDecl
),...,
dynamic-env
ContextDecl
),
dynamic-env
TypeDecl
),...,
dynamic-env
TypeDecl
),
dynamic-env
FunctionDecl
),...,
dynamic-env
FunctionDecl
|-
Expr
=>
···,
|-
Expr
=>
|-
ContextDecl
, ···,
ContextDecl
TypeDecl
, ···,
TypeDecl
FunctionDecl
, ···,
FunctionDecl
Expr
···,
Expr
=>
append(
···,
6 XQuery Mapping to Core
As explained in the introduction, the semantics of the full
XQuery language is obtained by mapping full XQuery expression (In the
full XQuery grammar, see
[XQuery 1.0: A Query Language for XML]
) into the core syntax
(In the Core Xquery grammar, see
3 XQuery Core Syntax
). In
4 Static Semantics : Type-Inference Rules
and
5 Dynamic Semantics : Value-Inference Rules
we
have given the complete static and dynamic semantics for the core. We
now explain how the full XQuery syntax is mapped into this core.
Please note: this mapping is still preliminary and contains
inconsistencies. See
Issue-0099:
Incomplete/inconsistent mapping from XQuery to core
In XQuery, a query is composed of a preamble (containing
schema, namespace and function declarations) and a body (containing a
single XQuery expression). First, we give a mapping for XQuery
expressions into Core XQuery expressions, then we give a mapping for
XQuery declarations into Core XQuery declarations. This mapping is
based on the XQuery grammar given in appendix B.
6.1 Notations
We will use the following notations.
E Expression
l Local Name (NCName)
n:l QName with namespace n and local name l
a Qualified name

$v variables
$dot Distinguished variable used to contain the current
node.
$roots Distinguished variable that contains a sequence of
document root nodes.

T Type

[[ E ]]_c ==> E' Given the context c, the XQuery expression E is mapped
to the Core Xquery expression E'.
When the context is clear, we will write: [[ E ]] ==> E'.
6.2 Mapping for XQuery expressions
We give a mapping for each class of XQuery expression. Each
of these classes corresponds to some specific productions in the full
XQuery Grammar.
6.2.1 Path expressions
XQuery uses a fragment of XPath, plus two additional
features: dereference and range predicates. XQuery and the Core XQuery
do not currently support all of the axis of XPath.
The mapping assumes that path steps are always given an
explicit input expression. I.e., XPath abreviations are resolved, for
instance, name is already in the form ./name, /person[name = "John"]
is already in the form /person[./name = "John"], etc.
6.2.1.1 Current Node
In XQuery, '.' denotes the current node. The current
node is a special node, whose value depends on the context of the
expression within which it is evaluated. Inside the XQuery core, we
will use a distinguished variable, called dot, to contain the value of
the current node. Variable dot will always be bound explicitly in the
core (see for instance, navigation and SORTBY expressions).
[[ . ]] ==> $dot
6.2.1.2 Root node
In XQuery, '/' denotes a fixed set of input document
roots, the mapping is:
[[ / ]] ==> $roots
Note that the value for variable $roots is defined in
the environment, before compilation and evaluation of the
query. Therefore, it is fixed for the duration of query compilation
and evaluation. There is no operation in the language that can modify
that value.
6.2.1.3 Simple Navigation
The XQuery Core does not contain path
expressions. Instead, it uses a combination of access to children,
iteration and typeswitch in order to capture navigation in path
expressions. The following mapping applies when 'a' is a
NameSet
[[ E/a ]] ==> for $v1 in [[ E ]] return
for $v2 in children($v1) return
typeswitch ($v2) as $v3
case ELEMENT a (AnyComplexType) return $v3
default return ()

[[ E/@a ]] ==> for $v1 in [[ E ]] return
for $v2 in attributes($v1) return
typeswitch ($v2) as $v3
case ATTRIBUTE a (AnyComplexType) return $v3
default return ()

[[ /a ]] ==> [[ $root/a ]]
Projecting the simple-typed value
of an element or attribute is equivalent to applying the typed-value
accessor in
[XQuery 1.0 and XPath 2.0 Data Model]
[[ E/DATA() ]] ==> for $v1 in [[ E ]] return
typed-value([[ E ]])
6.2.1.4 Recursive Navigation
Recursive navigation uses the built-in function
descendent-or-self that returns the current node as well as all its
descendents.
[[ E//a ]] ==> [[ descendent-or-self([[E]])/a ]]

[[ //a ]] ==> [[ descendent-or-self($root)/a ]]
6.2.1.5 Access to COMMENT, NODES, PIs, and TEXT
Again, access to specific nodes in path expressions is
mapped to iteration and type matching.
[[ E/COMMENT() ]] ==> for $v1 in [[ E ]] return
for $v2 in children($v1) return
typeswitch ($v2) as $v3
case Comment return $v3
default return ()

[[ E/PROCESSING-INSTRUCTION() ]] ==> for $v1 in [[ E ]] return
for $v2 in children($v1) return
typeswitch ($v2) as $v3
case PI return $v3
default return ()

[[ E/NODE() ]] ==> for $v1 in [[ E ]] return
children($v1)

[[ E/TEXT() ]] ==> string([[ E ]])
6.2.1.6 Dereference
This uses the support for dereference in the XQuery
core. This assumes an agreement on what is a reference and what is not
(e.g., that ID/IDREF are converted to ref() in the data model).
[[E => a]] ==> for $v1 in [[ E ]] return
for $v2 in deref($v1) return
typeswitch ($v2) as $v3
case ELEMENT a (AnyComplexType) return $v3
default return ()

[[E => @a]] ==> for $v1 in [[ E ]] return
for $v2 in deref($v1) return
typeswitch ($v2) as $v3
case ATTRIBUTE a (AnyComplexType) return $v3
default return ()
6.2.1.7 Predicates
Local XPath predicates iterate over the nodes in a
sequence, and selects only the nodes that verify the predicate.
There are three kinds of predicates. Predicates which
take a boolean expression as a parameters return only the nodes which
for which that expression returns true. Predicates which take an
integer as a parameter return the nodes whose index in the sequence is
equal to that integer. Finally, range predicates select nodes whose
index is between the bounds of the range expression.
[[ E1[i] ]] ==> [[ E1[i to i] ]]

[[ E1[i1 to i2] ]] ==> for $v in index([[ E1 ]]) return
if ([[ $v/fst/data() >= i1 ]] and [[ $v/fst/data() <= i2 ]])
then [[ $v/snd/deref() ]] else ()

[[ E1[E2] ]] ==> for $v in [[ E1 ]] return
let $dot := $v return
if [[ E2 ]] then $v else ()
6.2.1.8 Parent
Parent navigation is mapped to the corresponding parent built-in
function in the core.
[[ E/.. ]] ==> parent([[ E ]])
6.2.2 Element and attribute constructors
Element constructors in XQuery can support full XML
syntax. As a result the mapping give here is more involved and
requires collaboration with the XML parser. The content of elements
is always mapped to enclosed expressions with '{' '}' in the
core. The mapping then takes content of element constructors and
generate appropriate node creation statements using the data model
constructors.
In order to map element constructors, we will use the following
additional mapping notations.
Ci's are allowed characters or entity references
Ni' are elementary components within the element content
[[ ]]_elemcontent is a specific mapping rule for the content of elements
[[ ]]_elem is a specific mapping rule for elementary
components within the element content
The first rules assume that the parser can indicate
'breaking points' in the content of element constructors in order to
generate corresponding text nodes, subelements, etc
//text node creation
[[ C1C2C3... ]]_elem ==> text("C1C2C3...")

//{} are always produced from the embedding rule for the element
[[ { E } ]]_elem ==> [[ E ]]

// cdata node creation
[[ "<![CDATA[" C1C2C3... "]]>" ]]_elem ==> cdata("C1C2C3...")

// nested element are kept unchanged
[[ "<" X ">" ]] ==> "<" X ">"

[[ N1N2N3... ]]_elemcontent ==> [[N1]]_elem[[N2]]_elem[[N3]]_elem...
Then the next rules convert the attribute
specifications separately by embedding them within the content of the element
constructors.
[[ E ]] ==>
{[ ATTRIBUTE a1 [[E1]], ..., ATTRIBUTE an [[En]], [[E]]_elemcontent ]}

[[ E ]] ==>
{[ ATTRIBUTE a1 [[E1]], ..., ATTRIBUTE an [[En]], [[E]] ]}

[[ ]] ==>
{[ ATTRIBUTE a1 [[E1]], ..., ATTRIBUTE an [[En]], [[E]] ]}
Note that if the Ei's do not return an attribute value,
this will be detected by the Core XQuery type system at compile
time. Note also, that the expressions E or might return attributes, in
which case the element constructor will append them at the beginning
along with the explicitely declared attributes (see corresponding
dynamic semantics).
6.2.3 FLWR expressions
6.2.3.1 FLWR normalization
In the full XQuery grammar, Flower expressions are
defined using the following production:
FlwrExpr ::= (ForClause | LetClause)+ WhereClause? ReturnClause
This allows complex forms of FLWR expressions in the
full XQuery syntax, where LET and FOR clauses may have several
variables. On the other hand, the XQuery core only allows elementary
FOR and LET clauses independant from each other and terminated by a
RETURN.
The mapping from full XQuery to the Core XQuery
performs the corresponding transformation by separating multiple FOR
and LET statements and adding RETURN clauses whenever necessary.
Let C be a FlwrClause. The mapping from XQuery to the
core is defined using an auxiliary mapping function noted [[]]_clause
which processes FLWR clauses one at a time.
The first two rules are used to map each clause one at
a time.
[[ C return E ]]
==>
[[ C ]]_clause([[ E ]])