XQuery 1.0 Formal Semantics

2.2.1 Data model components

The components manipulated in XQuery, such as simple-typed values and nodes (attributes, elements, etc.), are defined in the [XQuery 1.0 and XPath 2.0 Data Model] document. In this section we present only a short review of these components. We refer the reader to the [XQuery 1.0 and XPath 2.0 Data Model] document for more details.

There are five kinds of components in the [XQuery 1.0 and XPath 2.0 Data Model]: Error, SimpleValue, Node, Sequence, and SchemaComponent.

• A single error value.

• A SimpleValue: a value from any of the value spaces of XML Schema simple types, as defined in [XML Schema Part 2].

• A Node; which is one of the following kinds: DocumentNode, ElementNode, AttributeNode, NamespaceNode, CommentNode, PINode and TextNode. XML documents and their content are represented in the data model as trees composed of nodes and values. [XQuery 1.0 and XPath 2.0 Data Model] defines a mapping from the PSVI (Post Schema Validation Information Set) to such trees.

• A Sequence: which is an ordered collection of nodes, an ordered collection of simple-typed values, or an ordered collection of items (i.e., any mixture of nodes and simple-typed values). An important characteristic of sequences is that they cannot be nested. That is, all sequences are "flat", and cannot be composed of other sequences. Moreover, there is no distinction between a single item and a singleton sequence containing that item. That is, a single item and a singleton sequence containing that item are equivalent. It is still open whether sequences of entire documents are permitted [Issue-0068:  Document Collections].

• A SchemaComponent: the type of a node. The content and use of this schema component is still an open issue.

[XQuery 1.0 and XPath 2.0 Data Model] defines constructors, functions to construct each of these kinds of data model component, as well as accessors, functions to access their contents. For instance, the xf:children function can be used to retrieve the children nodes of an element node.

2.2.2 Node identity

In the [XQuery 1.0 and XPath 2.0 Data Model], nodes have an identity. Node identity follows from the unique location of any node within exactly one XML document (or document fragment, in the case of XML being constructed within the query itself). It is possible for two expressions to return not only the same value, but also the exact same node. On the other hand, two expressions could have results with the same document structure, but different identities. XQuery supports comparison of two nodes using either "node equality" (equality by identity) or "value equality" (equality by equal values), for instance using one of the two operators == or =.

Simple-typed values do not have an associated identity and are therefore always compared by value equality.

The difference between node equality and value equality is illustrated on the following example:

let $a1 := <book><author>Suciu</author></book>,
    $a2 := <author>Suciu</author>,
    $a3 := $a1/author
return
    ($a1/author == $a3), {-- true, they refer to the same node --}
    ($a1/author = $a2),  {-- true, they have the same value --}
    ($a1/author == $a2)  {-- false, they are not the same node --}

All XQuery's operators preserve node identity with the exception of explicit copy operations and node (element, attribute, etc.) constructors. An element constructor always creates a deep copy of its attributes and children nodes. Other operators, such as sequence construction or path expressions, do not result in copies of the corresponding nodes. So, for example, ($a3, $a2) creates a new sequence of nodes, the first of which has the same identity as $a1/author.

2.2.3 Document order and sequence order

There are two kinds of order in XQuery: sequence order and document order.

Sequence order. Sequences of items in the XQuery data model are ordered. Sequence order refers to the order of these items within a given sequence.

Document order. Document order refers to the total order among all nodes within a given document. It is defined as the order of appearance of the nodes when performing a pre-order, depth-first traversal of a tree. For elements, this corresponds to the order of appearance of their opening tags in the corresponding XML serialization. Document order is equivalent to the definition used in [XML Path Language (XPath) : Version 1.0].

Depending on the context, it may be possible to talk about two different notions of order for the same (set of) nodes. For example:

let $e := <list>
              <item id="1"/>
              <item id="2"/>
          </list>,
    $s := ($e/item[@id='2'], $e/item[@id='1'])
...

The item "1" is before item "2" in document order, but the same two nodes are in the opposite order in the sequence $s.

In the case of nodes among several documents, the order between the document is implementation defined but must be stable. I.e., it must not change for the duration of query evaluation. Support for document order among elements in distinct documents or document fragments is discussed in [Issue-0003:  Document Order].

2.2.4 Errors

Some queries result in an error. Errors that are detected at compile-time, like parse errors or type errors, are reported to the user by the system. Dynamic errors must return the Error value defined by the [XQuery 1.0 and XPath 2.0 Data Model].

Whenever necessary, we use the notation dm:error() to refer to the error value in the [XQuery 1.0 and XPath 2.0 Data Model]. General handling of errors in XQuery is still an open issue (See [Issue-0094:  Static type errors and warnings] and Issue-98 in [XQuery 1.0: A Query Language for XML]).

2.3.1 The elements of a (static) type system

A type system relates values, types, and expressions. A (static) type system requires several constituent parts:

• A universe of possible types. Every type system starts with a set of primitive types and most (including XQuery's) have type constructors that allow the construction of complex types.

  In XQuery, the primitive types are the built-in simple datatypes types of [XML Schema Part 2]. There are also type constructors for sequences and node types such as attributes and elements. These correspond to the concepts of group, attribute and element in [XML Schema Part 1] (or more precisely, in the formalization of XML Schema in [XML Schema : Formal Description]).

• A notation for types. A syntax is necessary to define and manipulate types. In order to write the type related semantics of XQuery, this document uses its own notation, which is used notably in type inference and dynamic semantics rules.

• A notion of instances, and domain of a type. Formally, a type is defined to be the (usually infinite) set of instance values that belong to that type. Thus the type xs:integer consists of the set of all integer values, and the type element address { xs:string } consists of all elements named "address" whose contents are a single string value.

• A notion of subtyping. Subtyping is a relationship between type, i.e., it relates types to each other.

  Subtyping plays a crucial role in a type system. Most notably, it is used to determine the legality of arguments to functions.

• Rules that relate expressions to types. The heart of static type inference is associating a static type with each expression in a query. In a strongly-typed language like XQuery, the static type is a guarantee that, no matter what the input to the query is, the result of evaluating the expression is a value that belongs to its static type.

• Rules that relate values to types. During query evaluation, expressions are evaluated to yield values. The dynamic component of a typing system determines the actual types of data values as they are computed.

2.3.2 Subtyping

One type is a subtype of another if every value belonging to the first type also belongs to the other. Here is a simple example of subtyping:

( xs:double )*
( xs:integer | xs:double )*

The first type is a subtype of the second, because any sequence that contains only doubles is also an example of a sequence containing either integers or doubles.

We write Type₁ <: Type₂ to indicate that type Type₁ is a subtype Type₂. Note that we use the subtype notation <: when defining the XQuery semantics, but it is not part of the XQuery syntax.

( xs:integer | xs:double )*
( xs:double | xs:integer )*

( xs:double )+
xs:double, ( xs:integer | xs:double )*

2.3.3 Static types and dynamic types

One consequence of having a static type system is that for the same expression, a type is first computed during the static phase, then a type for the actual value which is the result of that expression is computed during the dynamic phase. We use the terms static type and dynamic type respectively for each of these computed types for a given expression. It is important to note that for the same expression the dynamic type is often more precise than the static one, since the real value is not known statically. Indeed, the static type can be considered as an approximation of the dynamic one based on the available static information. Consider, for example, an XPath expression

      
$x/(foo | bar)
    

In this expression the static type might be

      
( element foo | element bar )*
    

If during execution, $x happens to contain exactly two foo elements, the dynamic type of (the result of evaluating) $x is a sequence of two foo elements.

      
( element foo, element foo ).
    

Of course, the basic guarantee of static type inference is that the dynamic type is always a subtype of the static type. Note that dynamic types are specific: they never contain choices, all groups, or quantifiers.

Ed. Note: MFF: This next paragraph should be changed to describe type annotations.

The XQuery data model also defines SchemaComponents associated with Nodes. SchemaComponents relate to the type associated with a Node through schema validation. This may be different from either the static or the dynamic type of the node. The relationship between static types, dynamic types and schema components in the data model is still an open issue. See [Issue-0018:  Align algebra types with schema].

2.4.1 Functions and operators

The [XQuery 1.0 and XPath 2.0 Functions and Operators] document provides a number of useful basic functions over the components of the XQuery data model (simple-typed values, nodes, sequences, etc). We use a number of these functions in the course of describing the XQuery semantics. Here is the list of functions from the [XQuery 1.0 and XPath 2.0 Functions and Operators] document that are used in the XQuery formal semantics:

• op:intersect
• op:union
• op:except
• op:concatenate
• op:boolean-and
• op:boolean-or
• op:union-value
• op:except-value
• op:to
• op:numeric-equal
• op:numeric-add
• op:get-end-datetime
• op:numeric-subtract
• op:get-duration
• op:get-start-datetime
• op:numeric-multiply
• op:numeric-divide
• op:numeric-mod
• op:boolean-equal
• op:datetime-equal
• op:duration-equal
• op:hex-binary-equal
• op:base64-binary-equal
• op:numeric-greater-than
• op:datetime-greater-than
• op:duration-greater-than
• op:numeric-less-than
• op:datetime-less-than
• op:duration-less-than
• op:node-equal
• op:node-before
• op:node-after
• op:numeric-unary-plus
• op:numeric-unary-minus
• op:operation
• xf:false
• xf:true
• xf:length
• xf:boolean
• xf:item-at
• xf:get-namespace-uri
• xf:get-local-name
• xf:round
• xf:compare
• xf:not
• xf:not3
• xf:empty-sequence
• xf:root
• xf:index-of

2.4.2 Functions and static typing

Many functions in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document are generic: they perform operations on arbitrary components of the data model, e.g., any kind of node, or any sequence of items. For instance, the xf:distinct-nodes function removes duplicates in any sequence of nodes. As a result, the signature given in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document is also generic. For instance, the signature of the xf:distinct-nodes function is:

define function xf:distinct-nodes(node*) returns node*

If applied as is, this signature would result in poor static type information. In general, it would be preferable if some of these function signatures could take the type of input parameters into account. For instance, if the function xf:distinct-nodes is applied on a parameter of type element a*, element b, one can easily deduce that the resulting sequence is a collection of either a or b elements.

In order to provide better static typing, we specify typing rules for some of the functions in [XQuery 1.0 and XPath 2.0 Functions and Operators]. These additional typing rules are given in [6 Additional Semantics of Functions]. Here is the list of functions that are given specific typing rules.

• dm:error
• op:union
• op:intersect
• op:expect
• op:to

Ed. Note: This list reflects the content of Sections 6, but should be expanded. See [Issue-0135:  Semantics of special functions].

2.4.3 Data Model Accessors and XPath Axes

The XQuery Data Model provides operations to construct or access component of the Data Model. Some of these operations are used in the course of defining the formal semantics. We use the namespace prefix dm: those functions to distinguish them for other functions from the [XQuery 1.0 and XPath 2.0 Functions and Operators] document.

Here is a list of data model constructors or accessors used for formal semantics specification.

• dm:error
• dm:atomic-value
• dm:children
• dm:attributes
• dm:parent
• dm:name
• dm:node-kind
• dm:dereference
• dm:empty-sequence
• dm:namespaces
• dm:type
• dm:typed-value
• dm:attribute-simple-node
• dm:element-simple-node
• dm:text-node

XPath axes are used to describe tree navigation in instances of the XQuery data model. The semantics of axis navigation is described in terms of data model functions. Some of the XPath axes are directly supported through existing data model accessors. Some axes (e.g., ancestor) are defined as a simple recursive application of a data model accessor and others (e.g., following) require more complex computation on top of existing data model accessors. The correspondence between XPath axis and data model accessors is specified in section [4.3.1 Axis Steps]

2.4.4 Other formal semantics functions

In a few cases, the formal semantics makes use of some functions that are not currently in the [XQuery 1.0 and XPath 2.0 Functions and Operators] or in the [XQuery 1.0 and XPath 2.0 Data Model] documents. We use the namespace prefix fs: for those functions, to distinguish them from functions in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document and from Data Model accessors.

Here is a list of additional functions used for formal semantics specification.

• fs:document
• fs:distinct-doc-order
• fs:data
• fs:unique-item-at

2.5.1 Judgments and patterns

Ed. Note: The following is a somewhat terse explanation of inference rules using formal semantic lingo informally. It needs some examples.

The basic building block of an inference rule is a judgment that expresses some property. A judgment is specified by a description that contains a combination of basic patterns, each identifying a sort of value that can be inserted, interspersed with symbols. Symbols must occur literally in judgments between values of a sort that corresponds to the used patterns.

A pattern is identified by one or more italic words. The names of patterns are significant: each pattern name corresponds to a sort of value that can be substituted legally for the pattern. For this reason, a pattern is sometimes called a metavariable that is instantiated to some value of the appropriate sort.

We employ the following conventions for pattern names:

1. patterns for syntactic sorts denoting lexical items begin with upper case and their names correspond to terminals or nonterminals in the XQuery grammar. For example, Expr is a pattern that can be instantiated with any XQuery Expr.

2. patterns for semantic sorts, to be defined, begin with lower case letters. For example, denotes a semantic value.

Furthermore, all patterns may appear with subscripts (e.g. Expr₁, Expr₂), which simply name different instances of the same pattern sort.

For example, '3 => 3' and '$x+0 => 3' are both instances of the judgment described by 'Expr => value'. It is no problem that we are overloading the symbol '3' to denote both the '3' in an expression and the value 3: this is unambiguous because of the strict use of sorts in the judgment descriptions.

Finally, we require that each distinct pattern is instantiated to a single expression or value so if the same pattern occurs twice in a judgment description then it should be instantiated with the same value. This means that '3 => 3' is an instance of the judgment described by 'Expr => Expr' but '$x+0 => 3' is not. (Both, however, are instances of the judgment described by 'Expr₁ => Expr₂'.)

2.5.2 Inference rules

Inference rules are used to express the logical relation between judgments and define how complex judgments can be concluded from simpler premise judgments. (As explained in [2.1 Processing model], this approach lends itself well to bottom-up algorithms.)

A logical inference rule is written as two collections of premise and conclusion judgments, written above and below a dividing line, respectively:

The interpretation of an inference rule is: if all the premise judgments above the line are true, then we know that each of the conclusion judgments below the line are also true.

Here is a simple example to illustrate (based on the example judgment from above described by 'Expr₁ => Expr₂'):

This rule expresses the property of the evaluation judgment 'Expr=>value': if an expression containing the variable reference '$x' yields the value zero, and the literal expression '3' yields the value '3', then we know that '$x + 3' yields the value '3'.

It is also possible for the expression above the line to have no judgments at all; this simply means that the expression below the line is true under all premises:

This judgment says that evaluating the expression '3' always yields the value three.

The rules above are expressed in terms of specific variables and values, but usually rules are more abstract. That is, the judgments they relate contain patterns that match sorts of things. For example, here is a rule that says for any variable, adding 0 yields the same value:

Formally, the rule states that if some variable in XQuery, to which Variable is instantiated, evaluates to some value, to which value is instantiated, then we can conclude that the query 'Variable + 0', with Variable substituted by the actual variable, evaluates to the same value.

We require that each unique patterns used in a particular inference rules is instantiated to the same value for the entire rule. This means that we can refer to "the value of Variable" instead of the more precise "what Variable is instantiated to in (this particular instantiation of) the inference rule".

Putting these together, here is an example of an inference rule that occurs later in this document:

This rule states that if the conditional expression of an if expression has type boolean, then the type of the entire expression is one of the two types of its then and else clauses. Note that this is represented as a choice type: '(Type₂|Type₃)'.

The rule also illustrates a convention of judgment expressions: Judgments usually consist of three parts: the assumptions, the problem, and the result, organized as "assumptions |- problem =>> result" The "|-" symbol is pronounced "turnstile" and is ubiquitous in the rules whereas the actual symbol used instead of "=>>" varies with the defined judgment -- in this particular example it is the ":" symbol. The idea is that with the assumption defined one can compute the result from the problem.

Ed. Note: Jonathan suggests to explain how to 'chain' inference rules. I.e., how several inference rules are applied recursively.

2.5.3 Normalization rules

Normalization is presented as logical rewrite rules, which specify those expressions that are rewritten into some other expression in the XQuery core. The static semantics is presented as type inference rules, which relate XQuery expressions to types and specify under what conditions an expression is well typed. The dynamic, or operational, semantics is presented as value inference rules, which specify the order in which an XQuery expression is evaluated and relate XQuery expressions to values.

Ed. Note: I'm leaving this unchanged, but I think we can and should change the definition of normalization so that it doesn't force the use of "no-op" rules; i.e. instead of forcing the recurrent execution of more mapping rules, allow them to be pattern matched just as the rest of the inference rules are.

Normalization applies a translation function to each expression in the XQuery syntax and returns an expression in the XQuery core syntax; The notation [ Expr ] denotes the result of translating the XQuery expression Expr into an expression in the XQuery core. All normalization rules have the following structure:

The [ Expr ] above the == sign denotes an expression in the XQuery language before translation and the coreExpr beneath the == sign denotes an equivalent expression in the XQuery core.

For convenience, the translation of an optional expression, e.g., Expr?, is denoted by ( [ Expr ] )?, meaning that the optional expression is translated, if it exists. Similarly, the translation of a repeated expression, e.g., Expr* is denoted by [ Expr ]*, meaning that each expression in the repetition is translated individually.

Many of the mapping rules from XQuery into the core convert expressions that have implicit arguments, types, or complex semantics into core expressions that have explicit arguments, types, and a more verbose, but explicit semantics.

2.5.4 Environments

Logical inference rules use environments to record information computed during static type inference or dynamic evaluation so that information can be used by other logical inference rules. For example, the type signature of a user-defined function in a query prolog can be recorded in an environment and used by subsequence rules. Similarly, the value assigned to a variable within a let statement can be captured in an environment and used for further evaluations.

In general an environment is a dictionary that maps a symbol (e.g., a function name or a variable name) to a value. If env is an environment then "env( symbol )" denotes the value that symbol is mapped to by env. Depending on the kind of environment, the "value" can be a type, a data value, etc. The notation is intentionally akin to function application as an environment can be seen as a "function" from the argument symbol to the value that symbol maps to.

In this specification we use environment groups that group related environments. If "envs" is an environment group with the member "mem", then that environment is denoted "envs.mem" and the value that it maps symbol to is denoted "envs.mem(symbol)".

In particular, updating is only defined on environment groups:

• "envs [ mem(symbol |-> value) ]" denotes the environment group which is just like envs except that the mem environment has been updated to map symbol to value.

• If the "value" is a type then we use the conventional variant notation "envs [ mem(symbol : value) ]".

• We allow the shorthand "envs [ mem( symbol₁ |-> value₁ ; ... ; symbol_n |-> value_n ) ]" for the nested " (...(envs[mem(symbol₁ |-> value₁)]) ... [mem(symbol_n |-> value_n)])".

Note that updating the environment overrides any previous binding that might exist for the same name. Updating the environment is used to properly capture the scope of variables, namespaces, etc. Also, note that there are no operations to remove entries from environments: the need never arises because the environment group from "before" the update remains accessible concurrently with the updated version.

Finally, an example that brings several of the notations above together. Here is a rule that extends the varType member of the static environment group statEnvs with a typing of a new variable:

2.5.5 Static type inference

The result of static type inference is to associate a static type with every expression in a query, such that any evaluation of that expression is guaranteed to yield a value that belongs to that type. This section outlines how this is done.

For each type of expression (as defined by the grammar production rules of XQuery), we define static type inference rules. Here is a simple example of such a rule:

This rule is read as follows: if two expressions Expr₁ and Expr₂ have already been statically inferred to have types Type₁ and Type₂ (that's the premises above the line), then it is the case that the expression below the line "Expr₁ , Expr₂" must have the type "Type₁, Type₂". Basically, it says that when two expressions are concatenated together, the result type is the concatenation of their types.

The "left half" of the expression below the line (the part before the ":") corresponds to some phrase in a query, for which we want to compute a type. If the query has been parsed into an internal parse tree, this usually corresponds to some node in that tree. The expression usually has patterns in it (Expr₁ and Expr₂) that need to be matched against the children of the node in the parse tree. The expressions above the line indicate things that we need to know or compute to use this rule; in this case, we need to know the types of the two sub-expressions of the "," operator. Once we know those types (by applying static inference rules recursively to the expressions on each side), then we can compute the type of this expression. This illustrates a general feature of the type system: the type of an expression depends only on the type of its sub-expressions. The overall static type inference algorithm is a recursive, following the parse structure of the query. At each point in the recursion, an appropriate matching inference rule is sought; if at any point there is no applicable rule, then static type inference has failed: the query is not type-safe.

As stated earlier, the types computed by static inference rules are sound, which means that they guarantee that any value computed by an expression must belong to the static type of the expression. Another characteristic of a static type system is completeness. A type system is complete if it computes the "tightest possible" static type for every expression. It is very rare for type systems to be complete, and XQuery is no exception: there are expressions for which the static type system of XQuery computes a type that is not the tightest type possible.

2.5.6 Evaluation rules

Dynamic semantics associates values with query expressions. As with static type inference, we use logical inference rules to determine the value of expressions given values of sub-expressions, and information contained in environments. XQuery's dynamic semantics is modeled on the dynamic semantics presented in [Milner].

The dynamic rules use judgments of the form: dynEnvs |- phrase => value, where phrase is a phrase in XQuery syntax, and value is a value.

The inference rules used for dynamic evaluation, like those for static type inference, follow a top-down recursive structure, computing the value of expressions from the values of their sub-expressions.

The dynamic type of data values is completely determined by the values themselves. Thus, there are no extra rules or machinery for computing dynamic types.

3.1.1 Wildcard types

XQuery defines the following built-in datatypes:

define type xs:AnySimpleType { xs:integer | xs:float | xs:string ... }
define type xs:AnyAttribute  { attribute * { type xs:AnySimpleType * }}
define type xs:AnyElement    { element *  { type xs:AnyType } }
define type xs:AnyNode       { type xs:AnyAttribute | type xs:AnyElement }
define type xs:AnyItem       { type xs:AnySimpleType | type xs:AnyNode }
define type xs:AnyType       { type xs:AnyItem* }

The concepts of xs:AnySimpleType and xs:AnyType have the same interpretation as anySimpleType and anyType of XML Schema, respectively, though this version of xs:AnyType contains types (such as comments and processing instructions) that do not occur in XML Schema.

3.2.1 Domain of a NameTest

The semantics of a given NameTest is defined by the set of names that matches a that NameTest.

Notation

We denote access to the domain of a NameTest with the following auxiliary judgment. The notation:

indicates that the QName QName is in the domain defined by the NameTest NameTest₂.

We specify the relationship QName₁ in_wild NameTest₂ by decomposing both sides in to QNames or WildCards, and then defining the relationship between each component of the name.

First, is always in the domain of QName is always a singleton compose of itself. Note that the following inference rule takes namespace resolution into account.

Now the rules for QName in_wild WildCard:

3.2.2 Semantics of the Domain of a Type

Notation

We denote the domain of a type using the following auxiliary judgment. The notation:

indicates that the value is the domain of type Type.

The XQuery type system is based on tree grammars. The semantics for the domain of a type is based on the set of a trees accepted by the corresponding tree grammar.

We do now give a full specification of the notion of language recognized by a tree grammar at this point, but refer the reader to the literature on tree grammars, for instance [Languages], or [TATA]

Ed. Note: Future versions of that document will include a more complete description of the notion of domain of a type.

Ed. Note: The use of pure tree grammars for defining the domain yields a structural definition of the domain of a type. This definition will have to be revised as soon as the named typing proposal is added.

3.3.1 NameTest Subtyping

Notation

We denote NameTest subtyping with the following auxiliary judgment. The notation:

indicates that NameTest NameTest₁ is a subtype of the NameTest NameTest₂.

We evaluate NameTest₁ <:_wild NameTest₂ by decomposing both sides in to QNames or WildCards, and then defining a subtyping relation between each component of the name.

First QName <:_wild QName is only true if they represent the same fully qualified name:

Now the rules for QName <:_wild WildCard:

And finally rules for WildCard₁ <:_wild WildCard₂. Note that the second rule also prevents NCName:* from being a subtype of anything unless it is a valid known prefix.

Ed. Note: DD: (1) I've taken liberties comparing, e.g. NCName = ncname, (2) this doesn't take into account any resolution of URIs.

3.3.2 Semantics of Subtyping

Notation

We denote subtyping with the following auxiliary judgment. The notation:

indicates that type Type₁ is a subtype of Type₂.

The definition of subtyping is based on the notion of domain, as defined in [3.2 Instances, and Domain of a Type]

By definition, Type₁ <: Type₂ if and only if all the instances in the domain of Type₁ are also in the domain of Type₂. That is, for every value value such that:

it is also the case that:

It is easy to see that the subtype relation <: is a partial order, i.e. it is reflexive: statEnvs |- Type <: Type

and it is transitive: if, statEnvs |- Type₁ <: Type₂      and, statEnvs |- Type₂ <: Type₃      then, statEnvs |- Type₁ <: Type₃

Note

The above definition although complete and precise, does not give a simple means to compute subtyping.

The XQuery type system is based on tree grammars. Computing subtyping between two types can be done by computing inclusion between their corresponding tree grammar.

We do now give a full algorithm to compute inclusion between tree grammar at this point, but refer the reader to the literature on tree grammars, for instance [Languages], or [TATA]

Ed. Note: Future versions of that document will include a more complete description of algorithms to compute subtyping.

Ed. Note: The use of pure tree grammars for defining the domain yields a structural definition of the notion of subtyping. This definition will have to be revised as soon as the named typing proposal is added.

3.3.3 Type equivalence

In a few cases, we use the fact that two types are equivalent, I.e., that they define exactly the same domain over data model instances.

By definition, we write Type₁ = Type₂ if and only if, Type₁<:Type₂ and Type₂<: Type₁.

3.4.1 Prime types and sequences of items with similar types

Some expressions operate on sequences of similar items. These include FLWR expressions, sorting, and duplicate elimination. For example, consider the following small document:

  <paper>
      <author>Buneman</author>
      <author>Davidson</author>
      <author>Fernandez</author>
      <author>Suciu</author>
      <title>Adding structure to unstructured data</title>
      <editor>Afrati</editor>
      <editor>Kolaitis</editor>
   </paper>
:  element paper {
      element author {xsd:string}+,
      element title {xsd:string},
      element editor {xsd:string}*
   }

The following query extracts a sequence of authors followed by editors and sorts them by content. This results in a sequence with authors and editors arbitrarily interleaved. The result type reflects this by repeating a choice of author and editor.

   (/paper/author , /paper/editor) sortby .
    => <editor>Afrati</editor>
       <author>Buneman</author>
       <author>Davidson</author>
       <author>Fernandez</author>
       <editor>Kolaitis</editor>
       <author>Suciu</author>
    :  (element author {xsd:string} | element editor {xsd:string})+
    

Such operation always operate on sequences over choices of items, that we call a Prime type.

Prime types can be described by the following grammar production.

This section explains the details about computing over prime types and sequences of prime types. For instance, we explain why the above type ends in a plus rather than a star.

3.4.2 Computing Prime Types

We use two auxiliary functions on types. Note that both functions are only used by XQuery's type inference rules; they are not part of the XQuery syntax.

The type function prime(Type) extracts all item types from the type expression Type and combines them by a choice.

The type function quantifier(Type) approximates the possible number of items in Type with the quantifiers supported by XQuery type expressions (?, +, *). To quantify interim results, we use the auxiliary quantifiers 1 for exactly one occurrence, 0 for exactly zero occurrences, i.e., the quantifier of the empty list, and - for infinitely many occurrences, i.e., the quantifier of the empty choice none, which is used to type errors.

The tables below specify the necessary arithmetics to compute the sum (q₁ , q₂), the choice (q₁ | q₂), and the product (q₁ · q₂) of two quantifiers q₁, q₂.

The auxiliary quantifiers for interim results are eliminated with the following type simplification rules.

prime(Type) · quantifier(Type) enjoys two desirable properties:

(1) for all types Type₁, Type₂: Type₁ <: Type₂ implies prime(Type₁) · quantifier(Type₁) <: prime(Type₂) · quantifier(Type₂).
For example, for the two syntactically different but semantically equivalent types Type₁ = (xsd:string & xsd:integer)* and Type₂ =((xsd:string,xsd:integer) | (xsd:integer,xsd:string))*, prime(Type₁) · quantifier(Type₁) = prime(Type₂) · quantifier(Type₂) = (xsd:string | xsd:integer)*.

(2) for all types Type: Type <: prime(Type) · quantifier(Type).
Note that for some type expressions prime(Type) · quantifier(Type) may be regarded as too general. For example, the result-type of sorting a sequence of type xsd:integer , xsd:string is (xsd:integer | xsd:string)+. A more specific result-type would be xsd:integer & xsd:string, which preserves the individual quantifiers for xsd:integer and xsd:string. However, computing such result-types for arbitrary type expressions loses type precision for choice types (e.g. (xsd:integer | xsd:string)+ becomes (xsd:integer* & xsd:string*)), and it requires more complicated typing rules.

Ed. Note: (Peter): I'm not sure whether we need to elaborate on this here, but at least Denise may wonder why we ditched disorder(). In addition, I'm aware that (2) is a corollary of Phil's famous factoring theorem, I'm not sure whether this also holds for (1), but haven't spend much thought on it. BTW. Impotence holds of course as well.

Using these two auxiliary functions, the result type of a SortExpr can be computed as follows. If Expr has type Type then Expr sortby SortSpecList has type prime(Type) · quantifier(Type). For the formal type inference rule see [4.10 Sorting Expressions]. Similar rules are applied to type the other operations that destroy sequence order - union, intersect, except, distinct-node, distinct-value, and unorder.

Ed. Note: (Peter): I deliberately do not introduce the formal inference rule here, because (a) the machinery for type inference probably hasn't been explained yet at this place in the document, and (b) the current static semantics of SortExpr is incomplete anyway. Maybe the example should use unorder() instead of sortby.

3.4.3 Common Prime Types

Ed. Note: Status: This section contains new material necessary for the simplified semantics of typeswitch.

When performing type checking for certain XQuery expressions, we also need to compute the common prime types between two types, and the common occurrence indicator between two types.

The type function common-primes(Type₁,Type₂) extracts all item types that are common from the prime types and and combines them into a new prime type.

Notation

In order to define the "common-primes" function, we use the following auxiliary judgment.

specifies that under the current static environment, the common prime of ItemType₁, ItemType₂ is type Type.

We define the common primes by looking at each combination of items in each prime type.

We then we define whether each item is kept or discarded using the auxiliary judgment. In the case the item is discarded, the result of common-primes is none. Remember that none is the unit for choice.

In the case of a simple type, or globally defined attribute or element, one keeps the corresponding item if both items in the functions are the same.

When matching an element (resp. attribute), if the left-hand side item type is a subtype of the right-hand side item type, then the function returns the left-hand side item type. This rule is particularly useful, when the right hand side is a wildcard type, as might be often the case in a typeswitch expression.

Otherwise, if the left-hand side item and the right-hand side item have compatible names, then the function returns the right-hand side item type.

Finally, in all the other cases, the common type is none. I.e., otherwise:

3.5.1 Schema

Schemas are imported by the 'schema' declaration in the preamble of a query. To import a schema, the document referred to by the given URI is opened and the schema declarations contained in the document are translated into the corresponding in-line type definitions.

To make the translation rules a bit easier to read, we use grammar rules to distinguish between the various parts of a <schema> element:

(Note: attributes that are ignored are emphasized)

An imported schema is associated with the namespace prefix that it defines:

Redefine is unsupported.

Annotations are unsupported.

3.5.2 QNames

3.5.3 Complex Type Definitions

The following productions describe the structure of a complex type definition in XML Schema.

We distinguish between global complex types (which are mapped to sort declarations) and local complex types (which are mapped to type definitions).

3.5.4 Groups

3.5.5 minOccurs and maxOccurs

The following structure describes minOccurs and maxOccurs attributes in XML Schema.

minOccurs and maxOccurs are mapped to the type system in the following way.

Right now, the proposed type system grammar does not capture other occurrences cases. Therefore, these are converted into a collection.

3.5.6 Elements

The following structure describes element declarations in XML Schema.

3.5.7 Attributes

The following structure describes attribute declarations in XML Schema.

3.5.8 Simple Content

For simple content, one just map their content in the type system. The mapping ignores most of the other information, notably facets.

The only part of the <restriction> content that is mapped is simpleType? and the attributes.

All facets are ignored:

We also ignore <extension> for now.

3.5.9 Attribute Group

3.5.10 Complex Content

3.5.11 Simple Types

Global simple types:

Anonymous local simple type:

Again, we ignore all facets and only translate simpleType?

4.1.1 Expression Context

Introduction

The expression context for a given expression consists of all the information that can affect the result of the expression. This information is organized into the static context and the evaluation context. This section specifies the environments that represent the context information used by XQuery expressions.

4.1.2 Type Conversions

Notation

For the basic-conversion rules, we define three normalization functions: []_{Optional_Atomic_Value} []_{Atomic_Value_Sequence}, and []_{Node_Sequence}. They are used in the definition of arithmetic, comparison, and function-call expressions.

Normalization

There are two variants of the normalization function []_{Optional_Atomic_Value}: the first variant is not parameterized by the required type of the expression and the second variant is parameterized by the required type. The function converts an expression into an expression that returns an optional atomic value and is used in the normalization of expressions whose required type is an optional atomic value. A node is converted to an optional atomic value by extracting its typed content.

In the parameterized variant, an atomic value with type fs:UnknownSimpleType is always cast to the required type:

Ed. Note: The type fs:UnknownSimpleType denotes untyped character data. The name of this type is an open XPath/XQuery issue (Issue-174).

The function []_{Atomic_Value_Sequence(Type)} is parameterized by the atomic type of the sequence. This rule is used in the normalization of expressions whose required type is a sequence of atomic values. The rule converts each value in the argument expression to an atomic value. An atomic value with type fs:UnknownSimpleType is always cast to the required type. A node is converted to a sequence of atomic values by extracted its typed content and, for each atomic value in that sequence, cast any value with type fs:UnknownSimpleType to the required type and return all other values unchanged.

The function []_{Node_Sequence} is used in the normalization of expressions whose required type is node sequence. They all map an XQuery core expression to an XQuery core expression.

Notation

Two more normalization functions implement type exceptions They are: []_{Type_Exception_Opt_Atomic(Type)} and []_{Type_Exception_Other}.

Normalization

These definitions implement the strict type exception policy. The strict policy always raises an error:

In the first rule, the required type is xs:boolean. The conditional expression in the "default return" clause below guarantees that in an arbitrary sequence of items, if at least one value is a node, then the boolean expression evaluates to true.

Ed. Note: MFF: The rule above requires that $v/self::node() on a simple value returns () rather than raise an error.

Ed. Note: The semantics of Boolean node tests over sequences is still an open issue. See [Issue-0131:  Boolean node test and sequences].

In the next rule, the required type is node type. The conditional expression in the "default return" clause below guarantees that in an arbitrary sequence of items, if the first item is a node, then the boolean expression evaluates to true.

Ed. Note: MFF: All the remaining rules in the fallback conversions table must be specified. See [Issue-0113:  Incomplete specification of type conversions]

4.2.1 Literals

Introduction

A literal is a direct syntactic representation of a atomic value. XQuery supports two kinds of literals: string literals and numeric literals.

Normalization

All literals are core expressions, therefore there are no normalization rules for literals.

Core Grammar

The core grammar rules for literals are:

Static Type Analysis

In the static semantics, the type of an integer literal is simply xs:integer:

Dynamic Evaluation

In the dynamic semantics, an integer literal is evaluated by constructing a atomic value in the data model, which consists of the literal value and its type:

The formal definitions of decimal, double, and string literals are analogous to those for integer.

Static Type Analysis

Dynamic Evaluation

Static Type Analysis

Dynamic Evaluation

Static Type Analysis

Dynamic Evaluation

Ed. Note: MFF: Phil has noted that the data model should support primitive literals in their lexical form, in which case no explicit dynamic semantic rule would be necessary. See [Issue-0118:  Data model syntax and literal values].

4.2.2 Variables

Introduction

A variable evaluates to the value to which the variable's QName is bound in the evaluation context.

Normalization

A variable is a core expression, therefore there is no normalization rule for a variable.

Core Grammar

The core grammar rules for variables are:

Static Type Analysis

In the static semantics, the type of a variable is simply its type in the static type environment statEnvs.varType:

In case the variable is not bound in the environment, the system raises an error.

Dynamic Evaluation

In the dynamic semantics, a variable is evaluated by "looking up" its value in dynEnvs.varValue:

In case the variable is not bound in the environment, the system raises an error.

4.2.3 Parenthesized Expressions

The formal definition of parenthesized expressions is in [4.4 Sequence Expressions].

4.2.4 Function Calls

Introduction

A function call consists of a QName followed by a parenthesized list of zero or more expressions.

Notation

We define a normalization function,[]_{Formal_Argument} for mapping the formal argument of a function call. There are three variants of this mapping rule. If the required type of the formal argument is an optional atomic value, the following rule is applied: (Type is the required atomic type.)

If the required type of the formal argument is a sequence of atomic values, the following rule is applied: (Type is the atomic type of the sequence.)

If the required type of the formal argument is neither an optional atomic value or a sequence of atomic values, the expression is simply mapped to its corresponding core expression:

Normalization

First, each argument in a function call is normalized to its corresponding core expression by applying []_{Formal_Argument}.

Note that this normalization rule depends on the static environment containing function signatures. This is working as the static context is built from the query prolog, before the normalization phase. [5 The Query Prolog] explains how the query prolog is processed.

Core Grammar

The core grammar rule for a function call is:

Static Type Analysis

In the static semantics for core function calls, 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 that the actual and formal types be equal.

Dynamic Evaluation

In the dynamic semantics for core function calls, we first evaluate each function argument. Then we extend dynEnvs.varValue by binding each formal variable to its corresponding actual value, and then evaluate the body of the function in the new environment. The resulting value is the value of the function call.

Note that the function body is evaluated in the default environment,

Ed. Note: This semantics only works for non-overloaded function. This is always the case for user defined functions, but not for [XQuery 1.0 and XPath 2.0 Functions and Operators] functions. See [Issue-0122:  Overloaded functions].

4.2.5 Comments

Comments are lexical constructs only, and have no meaning within the query and therefore have no formal semantics.

4.3.1 Axis Steps

Introduction

An axis step is either a combination of an axis accessor, a node test and a step qualifier, or an abbreviated step. We define here the semantics of Axis NodeTest pairs. The semantics of StepQualifiers is defined in [4.3.3 Step Qualifiers] and the semantics of abbreviated steps is defined in [4.3.5 Abbreviated Syntax].

Ed. Note: (Michael Kay): there is a bug here in the formal semantics which does not deal properly with principal node types. See [Issue-0108:  Principal node types in XPath].

Notation

During the normalization process, we have to distinguish between forward and reverse Axis. In order to do so, we need to slightly reorganize the XQuery grammar production to make that distinction. This reorganization does not actually change the syntax, but merely regroup together different productions. Here is the grammar that is the basis for the following normalization of steps.

We then use two auxiliary normalization rules denoted [...]_ForwardPath and [...]_ReversePath

Normalization

A forward axis is directly translated to core XQuery

A reverse axis is directly translated to core XQuery

Core Grammar

We have now normalized all Axis Steps into the following core grammar.

Next, we give the static and dynamic semantics for Axis Steps.

Notation

We use the term Filter to denote either an axis or a node test.

To define the semantics of axis and nodetest, we use the two following auxiliary judgments for filters. The first judgment is defining the effect of a filter (either an axis or a nodetest) on a value, and is used in the dynamic semantics. This judgment should be read as follows: in the current context (i.e., with respect to the dynamic environment dynEnvs.varValue), applying the filter Filter on value Value1 yields the value Value2

The second judgment is defining the effect of a filter (either an axis or a nodetest) on a type and is used in the static semantics. This judgment should be read as follows: in the current context, (i.e., with respect to the the static environment statEnvs.varType), applying the filter Filter on type Type1 yields the type Type2

In a few cases, when applying the type filter judgment recursively, we need to use an additional type environment that contains local type information. We use the following notation.

We write updates to the local type environment as "localTypeEnv[qname : Type]"

Static Type Analysis

The static semantics of an Axis NodeTest pair is obtained by retrieving the type of the context node, and applying the two filters (Axis, then NodeTest) on the result. The application of each filter is expressed through the static filter judgment as follows.

Dynamic Evaluation