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 the 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 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 the number in [XML Path Language (XPath) 2.0], and are annotated with "(XPath)". For instance, the following production describes for expressions in XPath.

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

The Formal Semantics sometimes needs to manipulate "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 [XQuery 1.0 and XPath 2.0 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.

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 which is not exactly the name of a grammar production but is based on it. For instance, a BaseTypeName is a pattern which 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, respectively written 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'.

It is also possible for an inference rule to have no premises above the line to have no judgments at all; this simply 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. For example, 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, for instance 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 either access existing information from an environment, or update the environment.

If "env" is an environment, then "env(symbol)" denotes the "object" to which symbol is mapped. The notation is intentionally akin to function application as an environment can be seen as 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)".

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.

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

• 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)".

Note that updating the environment overrides any previous binding that might exist for the same name. Updating the environment is used to capture 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 environme group remains accessible along with the updated copy.

Environments are typically used as part of a judgment, to capture some of the context in which the judgment is computed. Indeed, 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.

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].

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 as follows: First, the type Type₁ for the "let" input expression Expr₁ is computed. Second the "let" variable is added into the varType component of the static environment group statEnv, with type Type₁. Finally, the type Type₂ of Expr₂ is computed in that new environment.

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

2.2.1 Formal 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 [XML 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 xs:anyType, untyped attributes are annotated with xs:anySimpleType, and untyped atomic values (i.e., text content or attribute content in well-formed documents) are annotated with xdt:untypedAtomic.

Element have 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 they have no content and an attribute xsi:nil set to "true".

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).

Ed. Note: Issue: The formal semantics does not represent namespace nodes (See Issue 486. (FS-Issue-0143)).

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 xs:anyType {
    text { "The cat weighs " },
    element weight of type xs:anyType {
      attribute units of type xs:anySimpleType {
        "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 xs:anyType {
    attribute xsi:type of type xs:anySimpleType {
      "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 xs:anyType {
    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 xs:anyType {
    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 element with a nillable

  <sizes xsi:nil="true"/>

Before validation, this element is represented as:

  element sizes of type xs:anyType {
    attribute xsi:nil of type xs:anySimpleType { "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:anySimpleType { "true" }
  }

An element with a union type

  <sizes>1 two 3 four</sizes>

Before validation, this element is represented as:

  element sizes of type xs:anyType {
    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 XML Schema. 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. Those 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 which corresponds to the standard DTD constructs +, *, and ?. Choices are represented using the standard DTD construct |. 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 as well as indentity constraints are not formally represented in the [XPath/XQuery] type system. Still, [XPath/XQuery] implementation supporting XML Schema import and validation must follow the XML Schema specification and take simple type facets and indentity constraints into account.

The complete 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.

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 any element or any attribute. In addition, an element type has an optional nillable flag which 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

Note that 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.3.1 SequenceType Matching].

Examples

A text node type

  text

matches any text node, such as:

  text { "Text is beautiful" }

A wildcard element

  element

matches any element.

A wildcard element of type string

  element of type xs:integer 

matches any element of type string, such as:

  element name of type xs:string { "John Doe" }

A nillable element of type string

  element size nillable of type xs:integer 

matches any element with name size of type xs:integer, such as:

  element size of type xs:integer {
    2 of type xs:integer
  }

or it matches any element with name size which has no content and the xsi:nil attribute set to true, such as:

  element size of type xs:integer {
    attribute xsi:nil of type xs:anySimpleType { "true" }
  }

A reference to a globally declared attribute

  attribute sizes

refers to the global declaration for the attribute sizes.

An element with an anonymous type

  element sizes of type [Anon1]

matches any element with name sizes and the anonymous type [Anon1], such as:

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

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.1 The fn:error function].

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 is used to represent all groups in XML Schema. All group 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 gobal 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.