XQuery 1.0 and XPath 2.0 Formal Semantics

2.1.1 Notations from grammar productions

Grammar productions are used to describe "objects" (values, types, [XPath/XQuery] expressions, etc.) manipulated by the Formal Semantics. The Formal Semantics makes use of several kinds of grammar productions.

XQuery grammar productions describe the XQuery language and expressions. XQuery productions are identified by a number, which corresponds to their number in the [XQuery 1.0: A Query Language for XML] document, and are annotated with "(XQuery)". For instance, the following production describes FLWR expressions in XQuery.

[For/FLWR] Expressions

For the purpose of this document, the differences between the XQuery 1.0 and the XPath 2.0 grammars are mostly irrelevant. By default, this document uses XQuery 1.0 grammar productions. Whenever the grammar for XPath 2.0 differs from the one for XQuery 1.0, the corresponding XPath 2.0 productions are also given. XPath productions are identified by a number, which corresponds to their number in [XML Path Language (XPath) 2.0], and are annotated with "(XPath)". For instance, the following production describes for expressions in XPath.

[For/FLWR] Expressions

XQuery Core grammar productions describe the XQuery Core. The Core grammar is given in [A Normalized core grammar]. Core productions are identified by a number, which corresponds to their number in [A Normalized core grammar], and are annotated by "(Core)". For instance, the following production describes the simpler form of the "FLWR" expression in the XQuery Core.

Core FLWOR Expressions

The Formal Semantics manipulates "objects" (values, types, expressions, etc.) for which there is no existing grammar production in the [XQuery 1.0: A Query Language for XML] document. In these cases, specific grammar productions are introduced. Notably, additional productions are used to describe values in the [Data Model], and to describe the [XPath/XQuery] type system. Formal Semantics productions are identified by a number, and are annotated by "(Formal)". For instance, the following production describes global type definitions in the [XPath/XQuery] type system.

Type Definitions

Note that grammar productions that are specific to the Formal Semantics (i.e., with the "(Formal)" annotation) are not part of [XPath/XQuery]. They are not accessible to the user and are only used in the course of defining the language's semantics.

2.1.2 Notations for judgments

The basic building block of the formal specification is called a judgment. A judgment expresses whether a property holds or not.

For example:

Notation

The judgment

holds if the object Painting is beautiful.

Notation

Here are three judgments that are used extensively in this document.

The judgment

holds if the expression Expr yields (or evaluates to) the value Value.

The judgment

holds when the expression Expr has type Type.

The judgment

holds when the expression Expr raises the error Error.

A judgment can contain symbols and patterns.

Symbols are purely syntactic and are used to write the judgment itself. In general, symbols in a judgment are chosen to reflect its meaning. For example, 'is beautiful', '=>' and ':' are symbols, the second and third of which should be read "yields", and "has type" respectively.

Patterns are written with italicized words. The name of a pattern is significant: each pattern name corresponds to an "object" (a value, a type, an expression, etc.) that can be substituted legally for the pattern. By convention, all patterns in the Formal Semantics correspond to grammar non-terminals, and are used to represent entities that can be constructed through application of the corresponding grammar production. For example, Expr represents any [XPath/XQuery] expression, and Value represents any value in the [XPath/XQuery] data model.

When applying the judgment, each pattern must be instantiated to an appropriate sort of "object" (value, type, expression, etc). For example, '3 => 3' and '$x+0 => 3' are both instances of the judgment 'Expr => Value'. Note that in the first judgment, '3' corresponds to both the expression '3' (on the left-hand side of the => symbol) and to the the value '3' (on the right-hand side of the => symbol).

Patterns may appear with subscripts (e.g. Expr₁, Expr₂) to distinguish different instances of the same sort of pattern. Each distinct pattern must be instantiated to a single "object" (value, type, expression, etc.). If the same pattern occurs twice in a judgment description then it should be instantiated with the same "object". For example, '3 => 3' is an instance of the judgment 'Expr₁ => Expr₁' but '$x+0 => 3' is not since the two expressions '$x+0' and '3' cannot be both instance of the pattern Expr₁. The judgment'$x+0 => 3' is an instance of the judgment 'Expr₁ => Expr₂'.

In a few cases, patterns may have a name that is not exactly the name of a grammar production but is based on it. For instance, a BaseTypeName is a pattern that stands for a type name, as would TypeName, or TypeName₂. This usage is limited, and only occurs to improve the readability of some of the inference rules.

2.1.3 Notations for inference rules

Inference rules are used to specify whether a judgment holds or not. Inference rules express the logical relation between judgments and describe how complex judgments can be concluded from simpler premise judgments.

A logical inference rule is written as a collection of premises and a conclusion, written respectively above and below a dividing line:

All premises and the conclusion are judgments. The interpretation of an inference rule is: if all the premise judgments above the line hold, then the conclusion judgment below the line must also hold.

Here is a simple example of inference rule, which uses the example judgment 'Expr => Value' from above:

This inference rule expresses the following property of the judgment 'Expr => Value': if the variable expression '$x' yields the value '0', and the literal expression '3' yields the value '3', then the expression '$x + 3' yields the value '3'.

An inference rule may have no premises above the line, which means that the expression below the line always holds:

This inference rule expresses the following property of the judgment 'Expr => Value': evaluating the literal expression '3' always yields the value '3'.

The two above rules are expressed in terms of specific variables and values, but usually rules are more abstract. That is, the judgments they relate contain patterns. Here is a rule that says that for any variable Variable that yields the integer value Integer, adding '0' yields the same integer value:

As in a judgment, each pattern in a particular inference rule must be instantiated to the same "object" within the entire rule. This means that one can talk about "the value of Variable" instead of the more precise "what Variable is instantiated to in (this particular instantiation of) the inference rule".

Note

In effect, inference rules are just a notation that describes a bottom-up algorithm. In the examples above, the rules describe an evaluation algorithm where the result of an expression depends on the result for its sub-expressions.

2.1.4 Notations for environments

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

An environment is a dictionary that maps a symbol (e.g., a function name or a variable name) to an "object" (e.g., a function body, a type, a value). One can access information in an environment or update the environment.

The two main environments used in the Formal Semantics are: a dynamic environment (dynEnv), which captures the [XPath/XQuery]'s dynamic context, and a static environment (statEnv), which captures the [XPath/XQuery]'s static context. Both are defined in [3.1 Expression Context].

If "env" is an environment, then "env(symbol)" denotes the "object" to which symbol is mapped. The notation is intentionally similar to function application, because an environment can be considered a function from the argument symbol to the "object" to which the symbol is mapped.

This document uses environment groups that group related environments. If "env" is an environment group with the member "mem", then that environment is denoted "env.mem" and the value that it maps symbol to is denoted "env.mem(symbol)". For example, dynEnv.varValue denotes the dynamic environment that maps variables to values and dynEnv.varValue(Variable) denotes the value of the variable Variable in the dynamic environment.

Updating is only defined on environment groups:

• "env + mem(symbol => object) " denotes the new environment group that is identical to env except that the mem environment has been updated to map symbol to object. The notation symbol => object indicates that symbol is mapped to object in the new environment.

• The following shorthand is also allowed: "env + mem( symbol₁ => object₁ ; ... ; symbol_n => object_n ) " in which each symbol is mapped to a corresponding object in the new environment.

  This notation is equivalent to nested updates, as in " (env + mem( symbol₁ => object₁) + ... ) + mem(symbol_n => object_n)".

• If the "object" is a type then the following notation relates a symbol to a type: "env + mem(symbol : object) ".

Updating the environment overrides any previous binding that might exist for the same name. Updating the environment captures the scope of a symbol (e.g., a variable, a namespace prefix, etc.) Also, note that there are no operations to remove entries from environments: this is never necessary because updating an the environment group effectively creates a new extended copy of the original environment group, and the original environment group remains accessible along with the updated copy.

Environments are used in a judgment to capture some of the context in which the judgment is computed, and most judgments are computed assuming that some environment is given. This assumption is denoted by prefixing the judgment with "env |-". The "|-" symbol is called a "turnstile" and is used in almost all inference rules.

For instance, the judgment

is read as: Assuming the dynamic environment dynEnv, the expression Expr yields the value Value.

2.1.5 Putting it together

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

This rule is read as follows: if two expressions Expr₁ and Expr₂ are known to have the static types types Type₁ and Type₂ (the two premises above the line), then it is the case that the expression below the line "Expr₁ , Expr₂" must have the static type "Type₁, Type₂", which is the sequence of types Type₁ and Type₂. The above inference rule does not modify the (static) environment.

The following rule defines the static semantics of a "let" expression. The binding of the new variable is captured by an update to the varType component of the original static environment.

This rule is read as follows: First, because the variable is a QName, it is first expanded into an expanded QName. Second, the type Type₁ for the "let" input expression Expr₁ is computed. Ten the "let" variable with expanded name, expanded-QName with type Type₁ is added into the varType component of the static environment group statEnv. Finally, the type Type₂ of Expr₂ is computed in that new environment.

2.2.1 Formal values

For reference, a summary of the data model is given below, followed by the formal notation for data model values. Although not specified in this document, all the normative constraints specified in [Data Model] apply to the formal notation for data model values.

A value is a sequence of zero or more items. An item is either an atomic value or a node.

An atomic value is a value in the value space of an atomic type and is labeled with the name of that atomic type. An XML Schema atomic type [Schema Part 2] may be primitive or derived, or xdt:untypedAtomic.

A node is either an element, an attribute, a document, a text, a comment, or a processing-instruction node. Elements have a type annotation and contain a value. Attributes have a type annotation and contain a simple value, which is a sequence of atomic values. Text nodes always contain one string value of type xdt:untypedAtomic, therefore the corresponding type annotation is omitted.

A type annotation can be either the QName of a declared type or an anonymous type. An anonymous type corresponds to an XML Schema type for which the schema writer did not provide a name. Anonymous type names are not visible to the user, but are generated during schema validation and used to annotate nodes in the data model. By convention, anonymous type names are written in the Formal Semantics as: [Anon0], [Anon1], etc.

Untyped elements (e.g., from well-formed documents) are annotated with xdt:untypedAny, untyped attributes are annotated with xdt:untypedAtomic, and untyped atomic values (i.e., text content or attribute content in well-formed documents) are annotated with xdt:untypedAtomic.

An element has an optional "nilled" marker. This marker can only be present if the element has been validated against an element type in the schema which is "nillable", and the element has no content and an attribute xsi:nil set to "true".

An element also has a sequence of namespace annotations, which are the set of active namespace declarations that are in-scope for the element. Each namespace annotation is a prefix, URI pair. Namespace annotations are not values, i.e., they are never the result of evaluating an expression, and they only occur as annotations on elements. In examples, we omit the namespace annotations when they are empty. For example, the following two values are equivalent:

  element weight of type xs:integer { text { "42" } } {}
  element weight of type xs:integer { text { "42" } } 

Values

Notation

In the above grammar, "String" indicates the value space of xs:string, "Decimal" indicates the value space of xs:decimal, etc.

Note that the same rule about constructing sequences apply to the values described by that grammar. Notably sequences cannot be nested. For example, the sequence (10, (1, 2), (), (3, 4)) is equivalent to the sequence (10, 1, 2, 3, 4).

2.2.2 Examples of values

A well-formed document

  <fact>The cat weighs <weight units="lbs">12</weight> pounds.</fact>

In the absence of a Schema, this document is represented as

  element fact of type xdt:untyped {
    text { "The cat weighs " },
    element weight of type xdt:untyped {
      attribute units of type xdt:untypedAtomic {
        "lbs" of type xdt:untypedAtomic
      }
      text { "12" }
    },
    text { " pounds." }
  }

A document before and after validation.

  <weight xsi:type="xs:integer">42</weight>

The formal model for values can represent values before and after validation. Before validation, this element is represented as:

  element weight of type xdt:untyped {
    attribute xsi:type of type xdt:untypedAtomic {
      "xs:integer" of type xdt:untypedAtomic
    },
    text { "42" }
  }

After validation, this element is represented as:

  element weight of type xs:integer {
    attribute xsi:type of type xs:QName {
      "xs:integer" of type xs:QName
    },
    42 of type xs:integer
  }

An element with a list type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 2 3" }
  }

Assume the following Schema.

  <xs:element name="sizes" type="sizesType"/>
  <xs:simpleType name="sizesType">
    <xs:list itemType="sizeType"/>
  </xs:simpleType>
  <xs:simpleType name="sizeType">
    <xs:restriction base="xs:integer"/>
  </xs:simpleType>

After validation against this Schema, the element is represented as:

  element sizes of type sizesType {
    1 of type sizeType,
    2 of type sizeType,
    3 of type sizeType
  }

An element with an anonymous type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 2 3" }
  }

Assume the following Schema.

  <xs:element name="sizes">
    <xs:simpleType>
      <xs:list itemType="xs:integer"/>
    </xs:simpleType>
  </xs:element>

After validation, this element is represented as:

  element sizes of type [Anon1] {
    1 of type xs:integer,
    2 of type xs:integer,
    3 of type xs:integer
  }

where [Anon1] stands for the internal anonymous name generated by the system for the sizes element.

An nillable element with xsi:type set to true

  <sizes xsi:nil="true"/>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    attribute xsi:nil of type xdt:untypedAtomic { "true" }
  }

Assume the following Schema.

  <xs:element name="sizes" type="sizesType" nillable="true"/>

After validation against this Schema, the element is represented as:

  element sizes nilled of type sizesType {
    attribute xsi:nil of type xs:boolean { "true" }
  }

An element with a union type

  <sizes>1 two 3 four</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untypedAtomic {
    text { "1 two 3 four" }
  }

Assume the following Schema:

  <xs:element name="sizes" type="sizesType"/>
  <xs:simpleType name="sizesType">
    <xs:list itemType="sizeType"/>
  </xs:simpleType>
  <xs:simpleType name="sizeType">
    <xs:union memberType="xs:integer xs:string"/>
  </xs:simpleType>

After validation against this Schema, the element is represented as:

  element sizes of type sizesType {
    1 of type xs:integer,
    "two" of type xs:string,
    3 of type xs:integer,
    "four" of type xs:string
  }

2.3.1 XML Schema and the [XPath/XQuery] Type System

The [XPath/XQuery] type system is based on [Schema Part 1] and [Schema Part 2]. [Schema Part 1] and [Schema Part 2] specify normatively the schema information available in [XPath/XQuery]. Formalizing the treatment of types in [XPath/XQuery], however, requires some adjustments.

Use of formal notations for types. The Formal Semantics uses formal notations for types instead of XML Schema syntax. These notations are used extensively to describe and manipulate types in the inference rules. The formal notations for types introduced here are not exposed to the [XPath/XQuery] user.

Representation of content models. For the purpose of static typing, the [XPath/XQuery] type system only describes minOccurs, maxOccurs combinations that correspond to the DTD operators +, *, and ?. Choices are represented using the DTD operator |. All groups are represented using the & notation.

Representation of anonymous types. To clarify the semantics, the [XPath/XQuery] type system makes all anonymous types explicit.

Representation of XML Schema simple type facets and identity constraints. For simplicity, XML Schema simple type facets and identity constraints are not formally represented in the [XPath/XQuery] type system. However, an [XPath/XQuery] implementation supporting XML Schema import and validation must must take simple type facets and identity constraints into account.

The mapping from XML Schema into the [XPath/XQuery] type system is given in [8 Importing Schemas]. The rest of this section is organized as follows. [2.3.2 Item types] describes types items, [2.3.3 Content models] describes content models, and [2.3.4 Top level definitions] describe top-level type declarations.

2.3.2 Item types

An item type is either an atomic type, an element type, an attribute type, a document node type, a text node type, a comment node type, or a processing instruction type.

Item Types

An element or attribute type has an optional name and an optional type reference. A name alone corresponds to a reference to a global element or attribute declaration. A name with a type reference corresponds to a local element or attribute declaration. The word "element" or "attribute" alone refers to the wildcard types for any element or any attribute. In addition, an element type has an optional nillable flag that indicates whether the element can be nilled or not.

A document type has an optional content type. If no content type is given, then it refers to the wildcard type describing any document.

Note

Generic node types (e.g., node()), are interpreted in the type system as union types (e.g., element | attribute | text | comment | processing-instruction) and therefore do not appear here. The semantics of sequence types is described in [3.4.4 SequenceType Matching].

Examples

The following is a text node type

  text

The following is a type for all elements

  element

The following is a type for all elements of type string

  element of type xs:integer 

The following is a type for a nillable element of type string

  element size nillable of type xs:integer 

The following is a reference to a global attribute declaration

  attribute sizes

The following is a type for elements with anonymous type [Anon1]

  element sizes of type [Anon1]

2.3.3 Content models

Following XML Schema, types in [XPath/XQuery] are composed from item types by optional, one or more, zero or more, all group, sequence, choice, empty sequence, or empty choice (written none).

The type empty matches the empty sequence. The type none matches no values. It is called the empty choice because it is the identity for choice, that is (Type | none) = Type)). The type none is the static type for [6.2.5 The fn:error function].

Types

The [XPath/XQuery] type system includes three binary operators on types: ",", "|" and "&", corresponding respectively to sequence, choice and all groups in Schema. The [XPath/XQuery] type system includes three unary operators on types: "*", "+", and "?", corresponding respectively to zero or more instances of the type, one or more instances of the type, or an optional instance of the type.

The "&" operator builds the "interleaved product" of two types. The type Type₁ & Type₂ matches any sequence that is an interleaving of a sequence that matches Type₁ and a sequence that matches Type₂. The interleaved product represents all groups in XML Schema. All groups in XML Schema are restricted to apply only on global or local element declarations with lower bound 0 or 1, and upper bound 1.

Examples

A sequence of elements

The "," operator builds the "sequence" of two types. For example,

  element title of type xs:string, element year of type xs:integer

is a sequence of an element title of type string followed by an element year of type integer.

The union of two element types

The "|" operator builds the "union" of two types. For example,

  element editor of type xs:string | element bib:author

means either an element editor of type string, or a reference to the global element bib:author.

An all group of two elements

The "&" operator builds the "interleaved product" of two types. For example,

  (element a & element b) =
    element a, element b
  | element b, element a

which specifies that the a and b elements can occur in any order.

An empty type

The following type matches the empty sequence.

  empty

A sequence of zero or more elements

The following type matches zero or more elements each of which can be a surgeon or a plumber.

  (element surgeon | element plumber)*

2.3.4 Top level definitions

Top level definitions correspond to global element declarations, global attribute declarations and type definitions in XML Schema.

Type Definitions

A type definition has a name (possibly anonymous) and a type derivation. In the case of a complex type, or a simple type derived by list or union, derivation indicates if the type is derived by extension or restriction from its base type, gives its content model, and an optional flag indicating if it has mixed content. In the case of an atomic type, it just indicates from which type it is derived. When the type derivation is omitted, the type derives by restriction from xs:anyType, as in:

  define type Bib { xs:integer } =
  define type Bib restricts xs:anyType { xs:integer }

Empty content can be indicated with the explicit empty sequence, or omitted, as in:

  define type Bib { } =
  define type Bib { empty }

Global element and attribute declarations always have a name and a reference to a (possibly anonymous) type. A global element declaration also may declare a substitution group for the element and whether the element is nillable.

Examples

A type declaration with complex content

  define type Address {
    element name of type xsd:string,
    element street of type xsd:string*
  }

A type declaration with complex content derived by extension

  define type USAddress extends Address {
    element zip name of type xsd:integer
  }

A type declaration with mixed content

  define type Section mixed {
    (element h1 of type xsd:string |
     element p of type xsd:string |
     element div of type Section)*
  }

A type declaration with simple content derived by restriction

  define type SKU restricts xsd:string { xsd:string }

An element declaration

  define element address of type Address

An element declaration with a substitution group

  define element usaddress substitutes for address of type USAddress

An element declaration which is nillable

  define element zip nillable of type xs:integer

2.3.5 Example of a complete Schema

Here is a schema describing purchase orders from [XML Schema Part 0].

  <xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
  
   <xsd:annotation>
    <xsd:documentation xml:lang="en">
     Purchase order schema for Example.com.
     Copyright 2000 Example.com. All rights reserved.
    </xsd:documentation>
   </xsd:annotation>
  
   <xsd:element name="purchaseOrder" type="PurchaseOrderType"/>
  
   <xsd:element name="comment" type="xsd:string"/>
  
   <xsd:complexType name="PurchaseOrderType">
    <xsd:sequence>
     <xsd:element name="shipTo" type="USAddress"/>
     <xsd:element name="billTo" type="USAddress"/>
     <xsd:element ref="comment" minOccurs="0"/>
     <xsd:element name="items"  type="Items"/>
    </xsd:sequence>
    <xsd:attribute name="orderDate" type="xsd:date"/>
   </xsd:complexType>
  
   <xsd:complexType name="USAddress">
    <xsd:sequence>
     <xsd:element name="name"   type="xsd:string"/>
     <xsd:element name="street" type="xsd:string"/>
     <xsd:element name="city"   type="xsd:string"/>
     <xsd:element name="state"  type="xsd:string"/>
     <xsd:element name="zip"    type="xsd:decimal"/>
    </xsd:sequence>
    <xsd:attribute name="country" type="xsd:NMTOKEN"
        fixed="US"/>
   </xsd:complexType>
  
   <xsd:complexType name="Items">
    <xsd:sequence>
     <xsd:element name="item" minOccurs="0" maxOccurs="unbounded">
      <xsd:complexType>
        <xsd:sequence>
         <xsd:element name="productName" type="xsd:string"/>
         <xsd:element name="quantity">
          <xsd:simpleType>
           <xsd:restriction base="xsd:positiveInteger">
            <xsd:maxExclusive value="100"/>
           </xsd:restriction>
          </xsd:simpleType>
         </xsd:element>
         <xsd:element name="USPrice"  type="xsd:decimal"/>
         <xsd:element ref="comment"   minOccurs="0"/>
         <xsd:element name="shipDate" type="xsd:date" minOccurs="0"/>
        </xsd:sequence>
        <xsd:attribute name="partNum" type="SKU" use="required"/>
      </xsd:complexType>
     </xsd:element>
    </xsd:sequence>
   </xsd:complexType>
  
   <!-- Stock Keeping Unit, a code for identifying products -->
   <xsd:simpleType name="SKU">
    <xsd:restriction base="xsd:string">
     <xsd:pattern value="\d{3}-[A-Z]{2}"/>
    </xsd:restriction>
   </xsd:simpleType>
  
  </xsd:schema>

Here is the mapping of the above schema into the [XPath/XQuery] type system.

  namespace xsd = "http://www.w3.org/2001/XMLSchema"

  define element purchaseOrder of type PurchaseOrderType
 
  define element comment of type xsd:string
  
  define type PurchaseOrderType {
    attribute orderDate of type xsd:date?,
    element shipTo of type USAddress,
    element billTo of type USAddress,
    element comment?,
    element items of type Items
  }

  define type USAddress {
    attribute country of type xsd:NMTOKEN?,
    element name of type xsd:string,
    element street of type xsd:string,
    element city of type xsd:string,
    element state of type xsd:string,
    element zip of type xsd:decimal
  }

  define type Items {
    attribute partNum of type SKU,
    element item of type [Anon1]*
  }

  define type [Anon1] {
    element productName of type xsd:string,
    element quantity of type [Anon2],
    element USPrice of type xsd:decimal,
    element comment?,
    element shipDate of type xsd:date?
  }

  define type [Anon2] restricts xsd:positiveInteger

  define type SKU restrict xsd:string

Note that the two anonymous types in the item element declarations are mapping to types with names [Anon1] and [Anon2].

The following additional definitions illustrate how more advanced XML Schema features (a complex type derived by extension, an anonymous simple type derived by restriction, and substitution groups) are represented in the [XPath/XQuery] type system.

  <complexType name="NYCAddress">
    <complexContent>
     <extension base="USAddress">
      <sequence>
       <element ref="apt"/>
      </sequence>
     </extension>
    </complexContent>
  </complexType>

  <element name="apt">
    <xsd:simpleType>
     <xsd:restriction base="xsd:positiveInteger">
      <xsd:maxExclusive value="10000"/>
     </xsd:restriction>
    </xsd:simpleType>
  </element>

  <element name="usaddress" substitutionGroup="address" type="USAddress"/>
  <element name="nycaddress" substitutionGroup="usaddress" type="NYCAddress"/>

The above definitions are mapped into the [XPath/XQuery] type system as follows:

  define type NYCAddress extends USAddress {
    element apt
  }

  define element apt of type [Anon3]

  define type [Anon3] restricts xsd:positiveInteger

  define element usaddress  substitutes for address of type USAddress
  define element nycaddress substitutes for usaddress of type NYCAddress

2.4.1 Processing model

The [XPath/XQuery] processing model is defined in Section 2.2 Processing Model^XQ, which contains the following figure depicting the processing model.

Figure 1: Processing Model Overview

This processing model is not intended to describe an actual implementation, although a naive implementation might be based upon it. It does not prescribe an implementation technique, but any implementation should produce the same results as obtained by following this processing model and applying the rest of the Formal Semantics specification.

Query processing consists of two phases: a static analysis phase and a dynamic evaluation phase. Static analysis is further divided into four sub-phases. Each phase consumes the result of the previous phase and generates output for the next phase. For each processing phase, we point to the relevant notations introduced later in the document.

The static analysis phase (sometimes also called "compilation"), can be performed on a [expression/query] before examining any input document. Indeed, static analysis can be performed before input documents even exist. Static analysis can detect many errors early, e.g., syntax errors or type errors. If no error occurs, the result of static analysis could be some compiled form of [expression/query], suitable for execution by a compiled-[expression/query] processor. Static analysis consists of the following sub-phases:

1. Parsing. (Step SQ1 in Figure 1). The grammar for the [XPath/XQuery] syntax is defined in [XQuery 1.0: A Query Language for XML]. Parsing may generate syntax errors. If no error occurs, an internal operation tree of the parsed query is created.

2. Static Context Processing. (Steps SQ2, SQ3, and SQ4 in Figure 1). The static semantics of [expression/query] depends on the static input context. The static input context needs to be generated before the [expression/query] can be analysed. In XQuery, static the input context may be defined by the processing environment and by declarations in the Query Prolog (See [5 Modules and Prologs]). In XPath, the static input context is defined by the processing environment. The static input context is denoted by statEnv.

3. Normalization. (Step SQ5 in Figure 1). To simplify the semantics specification, some normalization is performed on the [expression/query]. The [XPath/XQuery] language provides many powerful features that make [expression/query]s simpler to write and use, but are also redundant. For instance, a complex for expression might be rewritten as a composition of several simple for expressions. The language composed of these simpler [expression/query] is called the [XPath/XQuery] Core language and is described by a grammar which is a subset of the XQuery grammar. The grammar of the [XPath/XQuery] Core language is given in [A Normalized core grammar].

   During the normalization phase, each [XPath/XQuery] [expression/query] is mapped into its equivalent [expression/query] in the core. (Note that this has nothing to do with Unicode Normalization, which works on character strings.) Normalization works by bottom-up application of normalization rules over expressions, starting with normalization of literal expressions and variables.

   Specifically the normalization phase is defined in terms of the static part of the context (statEnv) and a [expression/query] (Expr) abstract syntax tree. Formal notations for the normalization phase are introduced in [2.4.2 Normalization judgment].

   After normalization, the full semantics is obtained by giving a semantics to the normalized Core [expression/query]. This is done during the last two phases.

4. Static type analysis. (Step SQ6 in Figure 1). Static type analysis is optional. If this phase is not supported, then normalization is followed directly by dynamic evaluation.

   Static type analysis checks whether each [expression/query] is type safe, and if so, determines its static type. Static type analysis is defined only for Core [expression/query]. Static type analysis works by bottom-up application of type inference rules over expressions, taking the type of literals and of input documents into account.

   If the [expression/query] is not type-safe, static type analysis yields a type error. For instance, a comparison between an integer value and a string value might be detected as an type error during the static type analysis. If static type analysis succeeds, it yields an abstract syntax tree where each sub-expression is "annotated" with its static type.

   More precisely, the static analysis phase is defined in terms of the static context (statEnv) and a core [expression/query] (CoreExpr). Formal notations for the static analysis phase are introduced in [2.4.3 Static typing judgment].

   Static typing does not imply that the content of XML documents must be rigidly fixed or even known in advance. The [XPath/XQuery] type system accommodates "flexible" types, such as elements that can contain any content. Schema-less documents are handled in [XPath/XQuery] by associating a standard type with the document, such that it may include any legal XML content.

The dynamic evaluation phase (sometimes also called "execution") evaluates a query on input document(s).

1. Dynamic Context Processing. (Steps DQ2 and DQ3 in Figure 1).The dynamic semantics of [expression/query] depends on the dynamic input context. The dynamic input context needs to be generated before the [expression/query] can be evaluated. The dynamic input context may be defined by the processing environment and by statements in the Query Prolog (See [5 Modules and Prologs]). In XPath, the dynamic input context is defined by the processing environment. The static input context is denoted by dynEnv.

2. Dynamic Evaluation. (Steps DQ4 and DQ5 in Figure 1). This phase computes the value of an [expression/query]. The semantics of evaluation is defined only for Core [expression/query] terms. Evaluation works by bottom-up application of evaluation rules over expressions, starting with evaluation of literals and variables. Evaluation may result in a value OR a dynamic error, which may be a non-type error or a type error. If static typing of an expression does not raise a type error, then dynamic evaluation of the same expression will not raise a type error, although dynamic evaluation may raise some non-type error.

   The dynamic evaluation phase is defined in terms of the static context (statEnv) and evaluation context (dynEnv), and a core [expression/query] (CoreExpr). Formal notations for the dynamic evaluation phase are introduced in [2.4.4 Dynamic evaluation judgment].

Static type analysis catches only certain classes of errors. For instance, it can detect a comparison operation applied between incompatible types (e.g., xs:int and xs:date). Some other classes of errors cannot be detected by the static analysis and are only detected at evaluation time. For instance, whether an arithmetic expression on 32 bits integers (xs:int) yields an out-of-bound value can only be detected at run-time by looking at the data.

While implementations are free to implement different processing models, the [XPath/XQuery] static semantics relies on the existence of a static type analysis phase that precedes any access to the input data. Statically typed implementations are required to find and report type errors during static analysis, as specified in this document. Dynamically typed implementations are required to find and report type errors during evaluation, but are permitted to report them during static analysis.

Notice that the separation of logical processing into phases is not meant to imply that implementations must separate the static analysis phase from the dynamic evaluation phase; processors may choose to perform all phases simultaneously at evaluation-time and may even mix the phases in their internal implementations. The processing model simply defines the final result.

The above processing phases are all internal to the [XPath/XQuery] processor. They do not deal with how the [XPath/XQuery] processor interacts with the outside world, notably how it accesses actual documents and types. A typical [expression/query] engine would support at least three other important processing phases:

1. Schema Import Processing. The [XPath/XQuery] type system is based on XML Schema. In order to perform dynamic or static typing, the [XPath/XQuery] processor needs to build type descriptions that correspond to the schema(s) of the input documents. This phase is achieved by mapping all schemas required by the [expression/query] into the [XPath/XQuery] type system. The XML Schema import phase is described in [8 Importing Schemas].

2. Data Model Generation. Expressions are evaluated on values in the [Data Model]. XML documents must be loaded into the [Data Model] before the evaluation phase. This is described in the [Data Model] and is not discussed further here.

3. Serialization. Once the [expression/query] is evaluated, processors might want to serialize the result of the [expression/query] as actual XML documents. Serialization of data model instances is described in [Data Model Serialization] and is not discussed further here.

The parsing phase is not specified formally; the formal semantics does not define a formal model for the syntax trees, but uses the [XPath/XQuery] concrete syntax directly. More details about parsing for XQuery 1.0 can be found in the [XQuery 1.0: A Query Language for XML] document and more details about parsing for XPath 2.0 can be found in the [XML Path Language (XPath) 2.0] document. No further discussion of parsing is included here.

2.4.2 Normalization judgment

Normalization is specified using mapping rules, which describe how a [XPath/XQuery] expression is rewritten into an expression in the [XPath/XQuery] Core. Mapping rules are also used in [8 Importing Schemas] to specify how XML Schemas are imported into the [XPath/XQuery] type system.

Notation

Mapping rules are written using a square bracket notation, as follows:

The original "object" is written above the == sign. The rewritten "object" is written beneath the == sign. The subscript is used to indicate what kind of "object" is mapped, and sometimes to pass some information between mapping rules.

Since normalization is always applied in the presence of a static context, the above rule is a shorthand for:

The static environment is used in certain normalization rules (e.g. for normalization of function calls). To keep the notation simpler, the static environment is not written in the normalization rules, but it is assumed to be available.

The normalization rule that is used to map "top-level" expressions in the [XPath/XQuery] syntax into expressions in the [XPath/XQuery] Core is:

which indicates that the expression Expr is normalized to the expression CoreExpr in the [XPath/XQuery] core (with the implied statEnv).

Example

For instance, the following [expression/query]

    for $i in (1, 2),
        $j in (3, 4)
    return
      element pair { ($i,$j) }

is normalized to the core expression

    for $i in (1, 2) return
      for $j in (3, 4) return
          element pair { ($i,$j) }

in which the "FWLR" expression is mapped into a composition of two simpler "for" expressions.

2.4.3 Static typing judgment

The static semantics is specified using type inference rules, which relate [XPath/XQuery] expressions to types and specify under what conditions an expression is well typed.

Notation

The judgment

holds when, in the static environment statEnv, the expression Expr has type Type.

Example

The result of static type inference is to associate a static type with every [expression/query], such that any evaluation of that [expression/query] is guaranteed to yield a value that belongs to that type.

For instance, the following expression.

   let $v := 3 return $v+5

has type xs:integer. This can be inferred as follows: the input literals '3' and '5' have type integer, so the variable $v also has type integer. Since the sum of two integers is an integer, the complete expression has type integer.

Note

The type of an expression is computed by inference. Static type inference rules define for each kind of expression how to compute the type of the expression given the types of its sub-expressions. Here is a simple example:

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 the resulting type is represented as a union: '(Type₂|Type₃)'.

The "left half" (the part before the :) of the expression below the line corresponds to some [expression/query], for which a type is computed. If the [expression/query] has been parsed into an internal abstract syntax tree, this usually corresponds to some node in that tree. The expression usually has patterns in it (here Expr₁, Expr₂, and Expr₃) that need to be matched against the children of the node in the abstract syntax tree. The expressions above the line indicate things that need to be computed to use this rule; in this case, the types of the condition expression and the two branches of the if-then-else expression. Once those types are computed (by further applying static inference rules recursively to the expressions on each side), then the type of the expression below the line can be computed. This example illustrates a general feature of the [XPath/XQuery] type system: the type of an expression depends only on the type of its sub-expressions. The overall static type inference algorithm is recursive, following the abstract syntax of the [expression/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 and the [expression/query] is not type correct.

2.4.4 Dynamic evaluation judgment

The dynamic, or operational, semantics is specified using value inference rules, which relate [XPath/XQuery] expressions to values, and in some cases specify the order in which an [XPath/XQuery] expression is evaluated.

Notation

The judgment

holds when, in the static environment statEnv and dynamic environment dynEnv, the expression Expr yields the value Value.

The judgment

holds when, in the static environment statEnv and dynamic environment dynEnv, the expression Expr raises the error Error.

The static environment is used in certain cases (e.g. for type matching) during evaluation. To keep the notation simpler, the static environment is not written in the dynamic inference rules, but it is assumed to be available.

Example

For instance, the following expression.

   let $v := 3 return $v+5

yields the integer value 8. This can be inferred as follows: the input literals '3' and '5' denote the values 3 and 5, respectively, so the variable $v has the value 3. Since the sum of 3 and 5 is 8, the complete expression has the value 8.

Note

As with static type inference, logical inference rules are used to determine the value of each expression, given the dynamic environment and the values of its sub-expressions.

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

2.5.1 Namespaces

The Formal Semantics uses the following namespace prefixes.

• fn: for functions and operators from the [Functions and Operators] document.

• xs: for XML Schema components and built-in types.

• xdt: for XML Schema components and built-in types.

All these prefixes are assumed to be bound to the appropriate URIs.

In addition, the Formal Semantics uses the following special prefixes for the means of specification.

• dm: for accessors of the [Data Model].

• op: for operators in [Functions and Operators].

• fs: for functions and types defined in the formal semantics.

These prefixes are always italicized to emphasize that the corresponding functions, variables, and types are abstract: they are not and cannot be made accessible in the host language. None of these special prefixes are given a URI.

2.5.2 Functions and operators

The [Functions and Operators] document defines built-in functions available in [XPath/XQuery]. A number of these functions are used to define the [XPath/XQuery] semantics; those functions are listed in [B.1 Functions and Operators used in the Formal Semantics].

Many functions in the [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 fn:distinct-nodes function removes duplicates in any sequence of nodes. As a result, the signature given in the [Functions and Operators] document is also generic. For instance, the signature of the fn:distinct-nodes function is:

  fn:distinct-nodes(node*) as node*

As defined, this signature provides little useful type information. For such functions, better type information can often be obtained by having the output type depend on the type of input parameters. For instance, if the function fn: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 for those functions, specific typing rules are given in [6 Additional Semantics of Functions].

3.1.1 Static Context

The environment group statEnv denotes the environments that are available during static analysis. Static analysis may extend parts of the static environment. The static environment is also available during dynamic evaluation.

If analysis of an expression relies on some component of the static context that has not been assigned a value, a static error is raised. This constraint is formalized in [3.5 Error Handling].

The following environments are part of the static environment group:

The XMLSpace policy in the [XPath/XQuery] static context is not represented in the Formal Semantics. All white-space processing the query text should be handled during parsing, and therefore is formalized in this document.

Environments have an initial state when [expression/query] processing begins, containing, for example, the function signatures of all built-in functions. The initial values for the static context are defined in Section C Context Components^XQ and Section C Context Components^XP and is denoted by statEnvDefault in the Formal Semantics.

Here is an example that shows how the static environment is modified in response to a namespace definition.

This rule reads as follows: "the phrase on the bottom (a namespace declaration in the query prolog followed by a sequence of expressions) is well-typed (accepted by the static type inference rules) within an environment statEnv if the sequence of expressions above the line is well-typed in the environment obtained from statEnv by adding the namespace declaration".

This is a common idiom for adding new information to an environment and passing that environment for use in sub-expressions. If the environment must be updated with a completely new component, the following notation is used:

The helper function fs:active_ns(statEnv) returns all the active in-scope namespaces in the given static environment.

For each attribute and element node in Value, such that the node has name expanded-QName in the namespace URI, the helper function fs:get_ns_from_items(statEnv, Value) returns the in-scope namespace that corresponds to URI. This is a reverse-lookup on statEnv.namespace by URI.

3.1.2 Dynamic Context

The environment group dynEnv denotes the group of environments built and used during dynamic evaluation.

If evaluation of an expression relies on some component of the dynamic context that has not been assigned a value, a dynamic error is raised. This constraint is formalized in [3.5 Error Handling].

The following environments are part of evaluation environment group:

The initial values for the dynamic context are defined in Section C Context Components^XQ and Section C Context Components^XP and is denoted by dynEnvDefault in the Formal Semantics.

The following Formal Semantics built-in variables represent the context item, context position, and context size properties of the dynamic context:

Variables with the "fs" namespace prefix are reserved for use in the definition of the Formal Semantics. It is a static error to define a variable in the "fs" namespace.

Values of $fs:dot and $fs:position and $fs:last can be obtained by invoking the fn:position and fn:last functions, respectively.

3.3.1 Document Order

Document order is defined in [Data Model].

3.3.2 Atomization

Atomization converts an item sequence into a sequence of atomic values and is implemented by the fn:data function. Atomization is applied in contexts where an arbitrary sequence of items is used where a sequence of atomic values is expected.

3.3.3 Effective Boolean Value

If a sequence of items is encountered where a boolean value is expected, the item sequence's effective boolean value is used. The fn:boolean function returns the effective boolean value of an item sequence.

3.3.4 Input Sources

[XPath/XQuery] has a set of functions that provide access to input data. These functions are of particular importance because they provide a way in which an expression can reference a document or a collection of documents. The dynamic semantics of these three input functions are described in more detail in [Functions and Operators].

3.4.1 Predefined Types

All the built-in types of XML Schema are recognized by [XPath/XQuery]. In addition, [XPath/XQuery] recognizes the predefined types Section 1.5.1 xdt:anyAtomicType^FO, Section 1.5.2 xdt:untypedAtomic^FO and Section 1.5.3 xdt:untypedAny^FO and the duration subtypes Section 9.2.1 xdt:yearMonthDuration^FO and Section 9.2.2 xdt:dayTimeDuration^FO. The representation of those types in the [XPath/XQuery] type system is given below.

[Definition: The following type definition of xs:anyType reflects the semantics of the Ur type from Schema in the [XPath/XQuery] type system.]

  define type xs:anyType restricts xs:anyType {
    attribute*,
    ( xdt:anyAtomicType* |
    ( element? & text? & comment? & processing-instruction? )* )
  }

[Definition: The following type definition of xs:anySimpleType reflects the semantics of the Ur simple type from Schema in the [XPath/XQuery] type system.]

  define type xs:anySimpleType restricts xs:anyType {
    ( xs:string
    | xs:boolean
    | xs:decimal
    | xs:float
    | xs:double
    | xs:duration
    | xs:dateTime
    | xs:time
    | xs:date
    | xs:gYearMonth
    | xs:gYear
    | xs:gMonthDay
    | xs:gDay
    | xs:gMonth
    | xs:hexBinary
    | xs:base64Binary
    | xs:anyURI
    | xs:QName
    | xs:NOTATION )*
  }

The name of the Ur simple type is xs:anySimpleType. It is derived by restriction from xs:anyType, its content a sequence of the union of all primitive atomic types.

[Definition: The following type definition of xdt:anyAtomicType reflects the semantics of xdt:anyAtomicType in the [XPath/XQuery] type system.]

  define type xdt:anyAtomicType restricts xs:anySimpleType {
    ( xs:string
    | xs:boolean
    | xs:decimal
    | xs:float
    | xs:double
    | xs:duration
    | xs:dateTime
    | xs:time
    | xs:date
    | xs:gYearMonth
    | xs:gYear
    | xs:gMonthDay
    | xs:gDay
    | xs:gMonth
    | xs:hexBinary
    | xs:base64Binary
    | xs:anyURI
    | xs:QName
    | xs:NOTATION 
    | xdt:untypedAtomic)
  }

[Definition: The following type definitions of the XML Schema primitive types reflects the semantics of the primitive types from Schema in the [XPath/XQuery] type system.]

  define type xs:string       restricts xdt:anyAtomicType
  define type xs:boolean      restricts xdt:anyAtomicType
  define type xs:decimal      restricts xdt:anyAtomicType
  define type xs:float        restricts xdt:anyAtomicType
  define type xs:double       restricts xdt:anyAtomicType
  define type xs:duration     restricts xdt:anyAtomicType
  define type xs:dateTime     restricts xdt:anyAtomicType
  define type xs:time         restricts xdt:anyAtomicType
  define type xs:date         restricts xdt:anyAtomicType
  define type xs:gYearMonth   restricts xdt:anyAtomicType
  define type xs:gYear        restricts xdt:anyAtomicType
  define type xs:gMonthDay    restricts xdt:anyAtomicType
  define type xs:gDay         restricts xdt:anyAtomicType
  define type xs:gMonth       restricts xdt:anyAtomicType
  define type xs:hexBinary    restricts xdt:anyAtomicType
  define type xs:base64Binary restricts xdt:anyAtomicType
  define type xs:anyURI       restricts xdt:anyAtomicType
  define type xs:QName        restricts xdt:anyAtomicType
  define type xs:NOTATION     restricts xdt:anyAtomicType

All of those primitive types derive from xdt:anyAtomicType. Note that the value space of each atomic type (such as xs:string) does not appear. The value space for each type is built-in and is as defined in [Schema Part 2].

[Definition: The type xdt:untypedAtomic is defined as follows.]

  define type xdt:untypedAtomic restricts xdt:anyAtomicType

Note that this rule does not indicate the value space of xdt:untypedAtomic. By definition, xdt:untypedAtomic has the same value space as xs:string.

The following example shows two atomic values. The first one is a value of type string containing "Database". The second one is an untyped value containing "Database". Both are using a string as content, but they have different type annotations.

  "Databases" of type xs:string
  "Databases" of type xdt:untypedAtomic

[Definition: The type xdt:untypedAny is defined as follows.]

  define type xdt:untypedAny restricts xs:anyType {
    attribute of type xdt:untypedAtomic*,
    ( element of type xdt:untypedAny? & text? & comment? & processing-instruction? )*
  }

[Definition: The following type definitions of the XML Schema derived types reflects the semantics of the XML Schema types derived derived by restriction from another atomic type.]

  define type xs:normalizedString   restricts xs:string
  define type xs:token              restricts xs:normalizedString
  define type xs:language           restricts xs:token
  define type xs:NMTOKEN            restricts xs:token
  define type xs:Name               restricts xs:token
  define type xs:NCName             restricts xs:Name
  define type xs:ID                 restricts xs:Name
  define type xs:IDREF              restricts xs:Name
  define type xs:ENTITY             restricts xs:Name
  define type xs:integer            restricts xs:decimal
  define type xs:nonPositiveInteger restricts xs:integer
  define type xs:negativeInteger    restricts xs:nonPositiveInteger
  define type xs:long               restricts xs:integer
  define type xs:int                restricts xs:long
  define type xs:short              restricts xs:int
  define type xs:byte               restricts xs:short
  define type xs:nonNegativeInteger restricts xs:integer
  define type xs:unsignedLong       restricts xs:nonNegativeInteger
  define type xs:unsignedInt        restricts xs:unsignedLong
  define type xs:unsignedShort      restricts xs:unsignedInt
  define type xs:unsignedByte       restricts xs:unsignedShort
  define type xs:positiveInteger    restricts xs:nonNegativeInteger

Three XML Schema built-in derived types are derived by list, as follows. Note that those derive directly from xs:anySimpleType, since they are derived by list, and that their value space is defined using a "one or more" occurrence indicator.

  define type xs:NMTOKENS restricts xs:anySimpleType { xs:NMTOKEN+ }
  define type xs:IDREFS   restricts xs:anySimpleType { xs:IDREF+ }
  define type xs:ENTITIES restricts xs:anySimpleType { xs:ENTITY+ }

For example, here is an element whose content is of type xs:IDREFS.

  element a of type xs:IDREFS {
    "id1" of type xs:IDREF,
    "id2" of type xs:IDREF,
    "id3" of type xs:IDREF
  }

Note that the type name xs:IDREFS derives from xs:anySimpleType, but not from xs:IDREF. As a consequence, calling the following three XQuery functions with the element a as a parameter succeeds for f1 and f2, but raises a type error for f3.

  define function f1($x as element(*,xs:anySimpleType)) { $x }
  define function f2($x as element(*,xs:IDREFS)) { $x }
  define function f3($x as element(*,xs:IDREF)) { $x }

[Definition: The totally ordered duration types, xdt:yearMonthDuration and xdt:dayTimeDuration , are derived by restriction from xs:duration.]

  define type xdt:yearMonthDuration restricts xs:duration
  define type xdt:dayTimeDuration   restricts xs:duration

3.4.2 Typed Value and String Value

The typed value of a node is computed by the fn:data function, and the string value of a node is computed by the fn:string function, defined in [Functions and Operators]. The normative definitions of typed value and string value are defined in [Data Model].

3.4.3 SequenceType Syntax

Introduction

SequenceTypes can be used in [XPath/XQuery] to refer to a type imported from a schema (see [5 Modules and Prologs]). SequenceTypes are used to declare the types of function parameters and in several kinds of [XPath/XQuery] expressions.

The syntax of SequenceTypes is described by the following grammar productions.

SequenceType

The semantics of SequenceTypes is defined by means of normalization rules from SequenceTypes to the [XPath/XQuery] type system (see [2.3 The [XPath/XQuery] Type System]).

Core Grammar

The Core grammar productions for sequence types are:

3.4.4 SequenceType Matching

Introduction

During processing of a query, it is sometimes necessary to determine whether a given value matches a type that was declared using the SequenceType syntax. This process is known as SequenceType matching, and is formally specified in [7.4 Judgments for type matching].

Sequence type matching is defined between a value and a type, rules to normalize a sequence type to the [XPath/XQuery] type system are necessary.

Notation

To define normalization of SequenceTypes to the [XPath/XQuery] type system, the following auxiliary mapping rule is used.

specifies that SequenceType is mapped to Type, in the [XPath/XQuery] type system.

Normalization

OccurenceIndicators are left unchanged when normalizing SequenceTypes into [XPath/XQuery] types. Each kind of SequenceType component is normalized separately into the [XPath/XQuery] type system.

The "empty" sequence type is mapped to the empty sequence type in the [XPath/XQuery] type system.

All of the KindTest SequenceType components are mapped directly into the [XPath/XQuery] type system.

The mapping still does not handle SequenceTypes using SchemaContext and nillable annotation (See Issue 481 (FS-Issue-0138)). The following rules map references to a global element or attribute, without taking the schema context or nillable into account.

Document nodes, text nodes, and atomic types are left unchanged.

The SequenceType components "node()" and "item()" correspond to wildcard types. node() indicates that any node is allowed and item() indicates that any node or atomic value is allowed. The following mapping rules make use of the corresponding wildcard types.

3.5.1 Kinds of Errors

Notation

The symbol Error denotes any error. We distinguish between a static error^XQ (denoted by statError), a type error^XQ (denoted by typeError), and a generic dynamic error^XQ (denoted by dynError), which represents all dynamic errors. A static error is raised during static analysis. A type error may be raised during static analysis or dynamic evaluation. A dynamic error is raised during dynamic evaluation. Non-type static errors are not formalized in this document.

3.5.2 Handling Dynamic Errors

In general, when an error is raised during evaluation of some expression Expr, the error is propogated to the expression Expr₁ in which Expr is evaluated. The expression Expr₁, in turn, propogates the error to the expression in which Expr₁ is evaluated, and so on, until the error is returned to the query environment.

Since most expressions propogate errors as described, we use one inference rule to specify this default behavior. The rule below states that if any sub-expression Expr_i of expression Expr raises an error dynError then Expr also raises dynError.

There are several expressions, such as [4.6 Logical Expressions] and [4.11 Quantified Expressions], that do not necessarily propogate an error raised by some sub-expression. For each such expression, we give specific error inference rules.

If analysis (evaluation) of an expression relies on some component of the static (dynamic) context that has not been assigned a value, a static (dynamic) error is raised. The following two rules handle all those cases when a component of an environment is accessed but not defined.

3.5.3 Errors and Optimization

In [XPath/XQuery], the detection and reporting of dynamic errors is implementation dependent. This permits different implementations to choose to evaluate or optimize an expression in different ways. When an implementation is able to evaluate an expression without evaluating some subexpression, the implementation is never required to evaluate that subexpression solely to determine whether it raises a dynamic error. For example, if a function parameter is never used in the body of the function, an implementation may choose whether to evaluate the expression bound to that parameter in a function call. Similarly, if the variable bound by a let expression is never used in the corresponding return expression, the implementation is not required to evaluate the expression to which the variable is bound.

For simplicity, the dynamic inference rules in Formal Semantics define an eager evaluation semantics for all expressions, i.e., all sub-expressions are evaluated regardless of whether their values are necessary to evaluate the containing expression. For example, every function parameter is evaluated before the body of the function is evaluated, and the expression bound to a let variable is always evaluated. The dynamic semantics rules in the Formal Semantics do not formalize the more flexible evaluation strategy above.

For example, in the following expression, the dynamic semantics rules of the Formal Semantics would raise a dynamic error because a path expression may not be applied to an atomic value. An implementation, however, may not raise an error, because the path expression is not necessary to evaluate the containing let expression.

  let $x := 1/foobar
  return 1

However, the static semantic rules, by definition, are conservative, and therefore a type is computed for every subexpression. In the example above, a static type error would be raised because a path expression may be applied to an atomic value.

3.6.1 Schema Import Feature

The semantics of XML Schema import is described in [8 Importing Schemas] and [5.6 Schema Import].

3.6.2 Static Typing Feature

The semantics of the static typing feature is specified by the static inference rules in the Formal Semantics.

3.6.3 Full Axis Feature

The semantics of all axes are specified in [4.2.1.1 Axes].

3.6.4 Module Feature

The semantics of main modules is specified in [5 Modules and Prologs]. The semantics of library modules and module import are not currently not specified.

3.6.5 Pragmas

Because pragmas are implementation defined, the Formal Semantics of extensions cannot be specified.

3.6.6 Must-Understand Extensions

Because extensions are implementation defined, the Formal Semantics of extensions cannot be specified.

3.6.7 Static Typing Extensions

For some expressions, the static typing rules defined in the Formal Semantics are not very precise (see, for instance, the type inference rules for the ancestor axes — parent, ancestor, and ancestor-or-self— and for the function fn:root function. Some implementations may wish to support more precise static typing rules.

A conforming implementation may provide a static typing extension^XQ, which is a type inference rule that infers a more precise static type than that inferred by the type inference rules in the Formal Semantics. Given an expression Expr, the type of Expr given by the extension must be a subtype of the type of Expr given by the Formal Semantics. This constraint is expressed formally by the following judgment:

4.1.1 Literals

Introduction

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

Literals

Core Grammar

The Core grammar productions for literals are:

Literals

Normalization

All literals are Core expressions, therefore no normalization rules are required for literals. Predefined entity references and character references in strings are resolved to characters as part of parsing and therefore they do not occur in the Core grammar.

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 an 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

Dynamic Errors

Literal expressions never raise a dynamic error.

4.1.2 Variable References

Introduction

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

Normalization

A variable is a Core expression, therefore no normalization rule is required for a variable.

Static Type Analysis

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

If the variable is not bound in the static environment, a static error is raised.

Dynamic Evaluation

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

Dynamic Errors

If the variable is not bound in the dynamic environment, a dynamic error is raised; the default rules in [3.5 Error Handling] cover this error.

4.1.3 Parenthesized Expressions

Core Grammar

The Core grammar production for parenthesized expressions is:

The empty-sequence expression () always has type empty. It is a static error for any expression other than () to have the empty type (see [4 Expressions].)

Static Type Analysis

Dynamic Evaluation

The empty-sequence expression evaluates to the empty sequence.

Dynamic Errors

The default rules for propogating errors, described in [3.5 Error Handling] apply to parenthesized expressions.

4.1.4 Context Item Expression

Introduction

A context item expression evaluates to the context item, which may be either a node or an atomic value.

Normalization

A context item expression is normalized to the built-in variable $fs:dot.

4.1.5 Function Calls

Introduction

A function call consists of a QName followed by a parenthesized list of zero or more expressions. In [XPath/XQuery], the actual argument to a function is called an argument and the formal argument of a function is called a parameter. We use the same terminology here.

Function Calls

Because [XPath/XQuery] implicitly converts the values of function arguments, a normalization step is required.

Notation

Normalization of function calls uses an auxiliary mapping []_{FunctionArgument(SequenceType)} used to insert conversions of function arguments that depend only on the expected SequenceType of the corresponding parameters. It is defined as follows:

where

• [Expr]_{AtomizeAtomic(SequenceType)} denotes

  fn:data(Expr)		If SequenceType <: xdt:anyAtomic* and Expr : Type and not(Type=empty)
  Expr		Otherwise

  which specifies that if the function expects atomic parameters, then fn:data is called to obtain them.

• [Expr]_{Extract(SequenceType)} denotes

  fn:subsequence(Expr,1,1)		If statEnv.xpath1.0_compatibility is true and SequenceType <: item?
  Expr		Otherwise

  which specifies that if the backwards compatibility mode is set, then the first node of the sequence passed as an argument is selected.

• [Expr]_{Convert(SequenceType)} denotes

  fs:convert-simple-operand( Expr,PrototypicalValue)	If SequenceType <: xs:anySimpleType
  Expr	Otherwise

  where PrototypicalValue has the following values for each possible SequenceType:

  Editorial note
  Todo: insert dummy prototypical values for each of the 44+4 types...

Note

The fs:convert-simple-operand function takes a PrototypicalValue, which is a value of the target type, to ensure that conversion to base types is possible even though types are not first class objects in [XPath/XQuery].

Core Grammar

The Core grammar production for function calls is:

Function Calls

Normalization

Each argument expression in a function call is normalized to its corresponding Core expression by applying []_{FunctionArgument(SequenceType)} for each argument with the expected SequenceType for the argument inserted.

Note that this normalization rule depends on the static environment containing function signatures and is the only normalization rule that depends on statEnv. Furthermore notice that the normalization is only well-defined when it is guaranteed that overloading is restricted to atomic types with the same quantifier. This is presently the case.

Static Type Analysis

To typecheck a Core function call we first check in Section [6 Additional Semantics of Functions] if there is a specialized typing rule for the function, and, if so, use it. Otherwise, the function signatures matching the function name and arity are retrieved from the static environment. The type of each argument to the function must be a subtype of a type that is promotable to the corresponding function parameter type of the function; if the expected type is a union of atomic types then this check is performed separately for each possibility.

The first rule bootstraps type checking of a function call: It expands the function's QName and then applies the function call rule for the expanded function call:

For a function call in which the static type of one of the expressions passed as argument is a union of atomic types, the function call is type checked once separately for each atomic type in that union. The static type of the entire function call expression is then the union of the types computed in each case, as follows:

Note

Notice that this semantics makes sense since the type declared for a function parameter, which uses the sequence types syntax, cannot itself be a union.

Finally, the following auxilliary rule type checks a function call in which none of the actual arguments has a type that is a union of atomic types. The rule looks up the function in the static environment and checks that some signature for the function satisfies the following constraint: the type of each actual argument is a subtype of some type that can be promoted to the type of the correponding function parameter. In this case, the function call is well typed and the result type is the return type specified in the function's signature.

The function body itself is not analyzed for each invocation: static typing of the function definition itself guarantees that the function body always returns a value of the declared return type.

Notice that the static typing rule checks the function signature in order to determine whether a function exists rather than just the function arity: this is consistent because it will reject function calls with the wrong arity in addition to function calls with the right arity but incompatible parameter types.

Dynamic Evaluation

Based on a function's name and parameter types, the function body is retrieved from the dynamic environment.

If the function is a user-defined function then it is evaluated as follows. First, the rule evaluates each actual function argument expression. Next, a match is searched for among the function's possible declaration signatures, retrieved from statEnv.funcType. If the function is not present in the environment, or there is no matching declaration signature, a type error is raised. Otherwise, the function body and formal variables are obtained from dynEnv.funcDefn for the matching declaration signature. The rule then extends dynEnv.varValue by binding each formal variable to its corresponding value (converted by the normalization as required for the expected type and backwards compatibility flag), and evaluates 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 (top-level) environment extended with just the parameter bindings. Note also that input values and output values are matched against the types declared for the function. If static analysis was performed, all these checks are guaranteed to be true and may be omitted.

If the function is a built-in or external function then the rule is somewhat simpler:

Calls to built-in or external functions use the following auxiliary judgment to evaluate the built-in or external function:

Dynamic Errors

If the evaluation of any actual argument raises an error, the function call can raise an error. This rule applies to both user-defined and built-in functions. Note that if more than one expression may raise an error, the function call may raise any one of the errors.

If, for all possible function signatures, the evaluation of some actual argument yields a value that cannot be promoted to the corresponding formal type of the parameter, the function call raises a type error. This rule applies to both user-defined and built-in functions.

If the evaluation of the function call to a user-defined function yields a value that cannot be promoted to the corresponding return type of the function, the function call raises a type error.

If the evaluation of the function call to a built-in or external function yields a value that cannot be promoted to the corresponding return type of the function, the built-in or external function call raises a type error.

Built-in function calls use the following auxiliary judgment to evaluate the built-in function call. If the built-in function raises an error, the function call raises an error.

4.1.6 [XPath/XQuery] Comments

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

4.2.1 Steps

Note that for this section uses some auxiliary judgments which are defined in [7.3 Judgments for step expressions and filtering].

Introduction

Steps

Core Grammar

The Core grammar productions for XPath steps are:

Steps

Note

Step expressions can be followed by predicates. Normalization of predicates uses the following auxiliary mapping rule: []_Predicates, which is specified in [4.2.2 Predicates]. Normalization for step expressions also uses the following auxiliary mapping rule: []_Axis, which is specified in [4.2.1.1 Axes].

Normalization

Normalization of predicates need to distinguish between forward steps, reverse steps, and primary expressions.

As explained in the [XPath/XQuery] document, applying a step in XPath changes the focus (or context). The change of focus is made explicit by the normalization rule below, which binds the variable $fs:dot to the node currently being processed, and the variable $fs:position to the position (i.e., the position within the input sequence) of that node.

There are two sets of normalization rules for Predicates. The first set of rules apply when the predicate is a numeric literal or the expression last(). The second set of rules apply to all predicate expressions other than numeric literals and the expression last(). In the first case, the normalization rules provides a more precise static type than if the general rules were applied.

When the predicate expression is a numeric literal or the fn:last function, the following normalization rules apply.

When predicates are applied on a reverse step, the position variable is bound in reverse document order.