XQuery 1.0 and XPath 2.0 Formal Semantics

2.3.1 Data model overview

This section gives an overview of the main data model features that are relevant to the Formal Semantics. The reader is referred to the [XQuery 1.0 and XPath 2.0 Data Model] document for more details.

• An atomic value is a value in the value space of one of the [XML Schema Part 2] atomic types (that is, a primitive simple type that is not derived by list or union).

• A node is one of the following kinds: document, element, attribute, namespace, comment, processing-instruction and text. The [XPath/XQuery] Formal Semantics does not currently discuss namespace, comment, and processing-instruction nodes (See [Issue-0105:  Types for nodes in the data model.]). Components of nodes can be typed values, string values, names, type annotations, or other nodes.

• XML documents and their contents are represented in the data model as trees composed of nodes and atomic values. [XQuery 1.0 and XPath 2.0 Data Model] defines a mapping from the PSVI (Post Schema Validation Information Set) to such trees.

• [XQuery 1.0 and XPath 2.0 Data Model] defines constructors, which are functions that construct nodes and atomic values, and accessors, which are functions that access a value's properties or components.

  For instance, the children function returns all the child nodes of an element node. The typed value of a node is a sequence of zero or more atomic values. The string value of a node is an instance of the type xs:string. The name of a node is an instance of the type xs:QName.

• An item is either an atomic value or a node.

• Every value in the data model is a sequence. A sequence is an ordered collection of zero or more items. Sequences are represented by items separated by commas, enclosed in parentheses.

  A sequence containing exactly one item is called a singleton sequence. An item is identical to a singleton sequence containing that item. Sequences are never nested--for example, combining the values 1, (2, 3), and () into a single sequence results in the sequence (1, 2, 3). A sequence containing zero items is called an empty sequence.

• The data model annotates element nodes, attribute nodes, and atomic values with type names. This type annotation is the type name given to the element, attribute, or value through the validation process.

The remainder of the section is devoted to several related features that merit special attention: node identity, order, and type annotations.

2.3.2 Node identity

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

Atomic values do not have an associated identity and are therefore always compared by value.

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

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

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

2.3.3 Document order and sequence order

There are two kinds of order in [XPath/XQuery]: sequence order and document order.

Sequence order. Sequences of items in the [XPath/XQuery] data model are ordered. Sequence order refers to the order of items within a given sequence.

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

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

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

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

The order between nodes from distinct documents is implementation defined but must be stable. That is, it must not change for the duration of query evaluation.

2.3.4 Type annotations

A type annotation indicates the type name for each element and attribute node, which results from the validation process or is assigned by default (depending on the way the data was built). In the case of anonymous types, the data model annotates element and attributes with xs:anyType and xs:anySimpleType respectively.

For instance, consider the document fragment

  <fact>The cat weighs <weight>12</weight> pounds.</fact>

and the associated schema

  <xs:element name="fact" type="FactType"/>

  <xs:complexType name="FactType" mixed="true">
    <xs:sequence>
      <xs:element name="weight" type="xs:integer">
    </xs:sequence>
  </xs:complexType>

Before validation, the two elements fact and weight in the document are annotated by xs:anyType.

After validation, the element fact is annotated with the type name FactType and the element weight is annotated with the type name xs:integer.

Type annotations are taken into account during [expression/query] evaluation and have an impact on the semantics of [XPath/XQuery].

For instance, consider the following function declaration

  define function convert_weight(element of type FactType $x)
    { ... }

This function only accepts as input an element annotated with the type FactType, or with one of the types derived from it. Therefore, the previous document fragment is only accepted by the function after it has been validated against the given schema.

[3 The XQuery Type System] gives a formal description of data model values with type annotations and explain how type annotations are taken into account when matching a value against a given type.

2.4.1 The elements of a (statically) typed language

A type system relates values, types, and expressions in the language.

The main constituent parts of a typed system are:

• A universe of possible types. Type are composed of other types, starting with primitive types, and can be built using type constructors.

  In [XPath/XQuery], the primitive types are the primitive atomic types of [XML Schema Part 2]. Type constructors are also based on schema, and can be used to build types for attributes and elements, sequence and choice groups, etc. The [XPath/XQuery] type system is defined in [3.1 Values and Types].

• A notation for specifying types.

  In [XPath/XQuery], types are imported from XML Schema, and can be used in expressions using the SequenceType syntax. In order to model and reason about types in [XPath/XQuery], this document introduces its own notation for types. This notation is defined in [3.1 Values and Types].

• A relationship between values and types. Formally, the semantics of a type is defined to be the (usually infinite) set of instance values which match that type.

  For example, the type xs:integer consists of the set of all integer values, and the type element address { xs:string } consists of all elements named "address" whose contents are a single string value, etc.

  Matching a [XPath/XQuery] value against a type is defined in [3.3 Matching].

• A notion of subtyping. Subtyping is a relationship between types that plays an important role in a statically typed language. Notably, it is used to determine whether function calls are legal or not.

  Subtyping in [XPath/XQuery] is defined in [3.5.1 Subtype].

For a statically typed language one also needs to define:

• Rules that relate expressions to types. Static type analysis infers a type for each expression in the language. The most important property for a static type system is that the type inferred statically must be such that for all valid inputs, evaluating the expression returns a result that matches the inferred type. If this property holds, then the static typing provides guarantees that certain kinds of errors can not occur at run-time.

  The static typing rules for [XPath/XQuery] are defined for all [XPath/XQuery] expressions in [5 Expressions], [6 The Query Prolog] and [7 Additional Semantics of Functions].

Finally, types can also be used during language evaluation if the language provides:

• Expressions on types. A language can support operations that take types into account, such as casting, type matching, etc.

  [XPath/XQuery] provide several such expressions: "typeswitch", "cast as", "treat as", and "validate as". [XPath/XQuery] also support a "validate" expression, which performs XML Schema validation. Validation is related to matching in that if validation succeeds, it returns a value which matches the type used for validation. Expressions on types are defined in [5.12 Expressions on SequenceTypes]. The validate expression is defined in [3.4 Erase and Annotate].

The remainder of the section is devoted to several related features that merit special attention: the relationship between the [XPath/XQuery] type system and XML Schema, structural and named typing, and subtyping.

2.4.2 XML Schema and the XQuery type system

The [XPath/XQuery] type system is based on [XML Schema]. An introduction to XML Schema can be found in [XML Schema Part 0].

The [XPath/XQuery] type system captures a large subset of XML Schema. This section gives a summary of which features are captured and in some cases deviations from XML Schema.

The following components and features of XML Schema are captured exactly in the [XPath/XQuery] type system:

• Element and attribute declarations;

• Simple and complex type definitions;

• Local attributes and elements;

• Named and anonymous types;

• the type name hierarchy;

• Sequence, choice and all groups;

• Wildcards;

• Derivation by extension, list and union;

• Substitution groups.

The following components or features of XML Schema are not represented in the [XPath/XQuery] type system.

• Simple type facets;

• Identity-constraint definitions;

• Notations and annotations.

The following components or features of XML Schema are represented partially or differently in the [XPath/XQuery] type system.

• The [XPath/XQuery] type system only captures an approximation of minOccurs and maxOccurs. Like DTDs, the [XPath/XQuery] type system only supports *, +, and ? which correspond to [minOccurs="0" maxOccurs="unbounded"], [minOccurs="1" maxOccurs="unbounded"], and [minOccurs="0" maxOccurs="1"] respectively.

• The [XPath/XQuery] type system generalizes the notion of derivation by restriction for the needs of static type analysis. Derivation by restriction in XML Schema relies on a syntactic relationship between content models. The [XPath/XQuery] type system uses a generalization of this relationship based on the notion of inclusion between types -- also called structural subtyping.

At compile time, the [XPath/XQuery] environment imports XML Schema declarations, and loads them as declarations in the [XPath/XQuery] type system. This loading process is specified by a mapping from XML Schema to the [XPath/XQuery] type system, given in [8 Importing Schemas].

2.4.3 Structural and named typing

XML Schema is a powerful schema language for XML. XML Schema can describe both structural constraints as well as type annotations that apply to XML documents. These aspects are referred to as structural typing and named typing respectively.

• Structural typing. An important notion underlying XML Schema is the concept of regular expressions, and their tree counterparts, regular tree grammars. An introduction to regular (tree) languages can be found in [Languages] or in [TATA].

  Tree grammars can be used to capture the structural constraints imposed by an XML Schema. Automata are the traditional way of implementing tree grammars and can be used to implement part of the XML Schema validation process.

  For instance, consider the following element declaration:

    <xs:element name="root">
      <xs:complexType>
        <xs:sequence maxOccurs="unbounded">
  	<xs:choice minOccurs="0" maxOccurs="unbounded">
  	  <xs:element ref="a"/>
  	  <xs:element ref="b" minOccurs="0"/>
  	</xs:choice>
  	<xs:element ref="c"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
  

  The structural constraints imposed by the definition of the content of element root can be described by the following regular expression (written here in DTD notation): ((a|b?)*,c)+. Such a constraint can be checked using a finite state automaton applied on the children of the element root in the instance document.

• Named typing. In addition, XML Schema provides the ability to associate names with type definitions and to declare relationships between type names.

  For instance, consider the following two element declarations:

    <xs:element name="person">
      <xs:complexType name="Person">
        <xs:sequence>
          <xs:element ref="ssn">
  	<xs:choice>
            <xs:sequence>
    	    <xs:element ref="major" minOccurs="0"/>
    	    <xs:element ref="minors" maxOccurs="unbounded"/>
            </xs:sequence>
            <xs:element ref="job_desc"/>
  	</xs:choice>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
  
    <xs:element name="student">
      <xs:complexType name="Student">
        <xs:complexContent>
          <xs:restriction base="Person">
            <xs:sequence>
              <xs:element ref="ssn">
              <xs:element ref="major" minOccurs="0"/>
              <xs:element ref="minors" maxOccurs="unbounded"/>
            </xs:sequence>
          </xs:restriction>
        </xs:complexType>
      </xs:complexContent>
    </xs:element>
  
  

  The type Studentof the element student is derived by restriction from the type Person. Such a declaration not only defines a new type, but also creates a relationship between the type names Person and Student which needs to be taken into account when doing validation and matching against a given type. For instance, the following function

    define function salary(element of type Person $x)
      { .... }
  

  accepts as parameters elements of type Person as well as elements with types derived by restriction from Person, but does not accept elements with the same content model as the element person but a type which does not derive from the type Person.

2.4.4 Subtyping

A type is a subtype of another type if every value matching the first type also matches the second type. Since matching takes both type structure and type names into account, so is subtyping.

Here is a simple example of subtyping on two regular expressions:

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

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

Type₁ <: Type₂ indicates that type Type₁ is a subtype of Type₂. Note that the notation <: is used when defining the [XPath/XQuery] semantics, but is not part of the [XPath/XQuery] syntax.

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

2.5.1 Functions and operators

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

• op:numeric-add
• op:numeric-subtract
• op:numeric-multiply
• op:numeric-divide
• op:numeric-mod
• op:numeric-unary-plus
• op:numeric-unary-minus
• op:numeric-equal
• op:numeric-less-than
• op:numeric-greater-than
• op:boolean-equal
• op:boolean-less-than
• op:boolean-greater-than
• op:yearMonthDuration-equal
• op:yearMonthDuration-less-than
• op:yearMonthDuration-greater-than
• op:dayTimeDuration-equal
• op:dayTimeDuration-less-than
• op:dayTimeDuration-greater-than
• op:dateTime-equal
• op:dateTime-less-than
• op:dateTime-greater-than
• op:add-yearMonthDurations
• op:subtract-yearMonthDurations
• op:multiply-yearMonthDuration
• op:divide-yearMonthDuration
• op:add-dayTimeDurations
• op:subtract-dayTimeDurations
• op:multiply-dayTimeDuration
• op:divide-dayTimeDuration
• op:add-yearMonthDuration-to-dateTime
• op:add-dayTimeDuration-to-dateTime
• op:subtract-yearMonthDuration-from-dateTime
• op:subtract-dayTimeDuration-from-dateTime
• op:add-yearMonthDuration-to-date
• op:add-dayTimeDuration-to-date
• op:subtract-yearMonthDuration-from-date
• op:subtract-dayTimeDuration-from-date
• op:add-dayTimeDuration-to-time
• op:subtract-dayTimeDuration-from-time
• op:QName-equal
• op:anyURI-equal
• op:hex-binary-equal
• op:base64-binary-equal
• op:NOTATION-equal
• op:node-equal
• op:node-before
• op:node-after
• op:node-precedes
• op:node-follows
• op:to
• op:concatenate
• op:item-at
• op:union
• op:intersect
• op:except
• op:operation
• xf:false
• xf:true
• xf:count
• xf:boolean
• xf:get-namespace-uri
• xf:get-local-name
• xf:round
• xf:compare
• xf:not
• xf:empty
• xf:root
• xf:error

2.5.2 Functions and static typing

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

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

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

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

• xf:error
• xf:distinct-nodes
• xf:distinct-values
• op:union
• op:intersect
• op:except
• op:to
• xf:data

Ed. Note: There might be other functions that need specific typing rules. See [Issue-0135:  Semantics of special functions].

2.5.3 The error function

Some queries result in an error. Errors that are detected at compile-time, like parse errors or type errors, are reported to the user by the system. Dynamic errors are raised using the xf:error() function. General handling of errors in the Formal Semantics is still an open issue (See [Issue-0094:  Static type errors and warnings], [Issue-0098:  Implementation of and conformance levels for static type checking], [Issue-0171:  Raising errors], and [Issue-0169:  Conformance Levels]).

2.5.4 Data Model Accessors and XPath Axes

The [XPath/XQuery] Data Model provides operations to construct or access components of the Data Model, some of which are used in the course of defining the [XPath/XQuery] semantics. The Formal Semantics uses the namespace prefix dm: for those functions to distinguish them from other functions in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document.

Here is a list of data model constructors or accessors used for Formal Semantics specification.

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

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

2.5.5 Other Formal Semantics functions

In a few cases, the Formal Semantics makes use of functions that are not currently in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document. The namespace prefix fs: is used for those functions, to distinguish them from functions in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document.

Here is a list of additional functions used for Formal Semantics specification.

• fs:characters-to-string
• fs:distinct-doc-order
• fs:item-sequence-to-node-sequence
• fs:item-sequence-to-string

2.6.1 Grammar productions

Grammar productions are used in this document 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 the document, and are annotated with "(Path)". 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 the [XPath/XQuery] type system. XQuery 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 which 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.6.2 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 painting Painting is beautiful.

Or more relevant, here are two example of judgments that are used extensively in the rest of this document.

Notation

The judgment

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

Notation

The judgment

holds when the expression Expr has type Type.

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 can be used to represent any [XPath/XQuery] expression, Value can be used to represent 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₂), which simply name 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₁. On the contrary, '$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.6.3 Inference rules

Whether a judgments holds or not is specified by means of inference rules. Inference rules express the logical relation between judgments and describe how complex judgments can be concluded from simpler premise judgments. (As explained in [2.1 Processing model], this approach lends itself well to bottom-up algorithms.)

A logical inference rule is written as 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".

2.6.4 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" statement 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 to. The notation is intentionally akin to function application as an environment can be seen as a "function" from the argument symbol to the "object" that the symbol is mapped to.

This specification 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 a new environment group which 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 conventional variant notation is used: "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 simple 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 variables, namespaces, etc. Also, note that there are no operations to remove entries from environments: the need never arises because the environment group from "before" the update remains accessible concurrently with the updated version.

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 ubiquitous in inference rules.

For instance, the judgment

should be read: 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 [4.1 Expression Context].

2.6.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₂ have already been statically inferred to have 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 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/return" expression. The binding of the new variable is captured by an update to the varType component of the original static environment.

This rule should be read as follows. First, the type Type₁ for the "let" input expression Expr₁ is computed. Second the "let" variable is added into the varType member 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.7.1 Normalization

Normalization is specified using mapping rules which describe how a [XPath/XQuery] expression is rewritten into another expression in the [XPath/XQuery] Core. Note that 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 done in the context of the static context the above is really a shorthand for

but we shall stay with the shorthand because statEnv will always be implied.)

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

Ed. Note: [Kristoffer/XSL] We should decide whether to use a shorthand notation as suggested or modify the mapping rules throughout.

Specifically 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
        return
          element pair { ($i,$j) }

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

2.7.2 Static type inference

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, assuming the static environment statEnv is given, 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 are given to describe, 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 of such a rule:

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 choice: '(Type₂|Type₃)'.

The "left half" of the expression below the line (the part before the :) corresponds to some phrase in a [expression/query], for which a type is computed. If the [expression/query] has been parsed into an internal parse tree, this usually corresponds to some node in that tree. The expression usually has patterns in it (here Expr₁, Expr₂, and Expr₃) that need to be matched against the children of the node in the parse tree. The expressions above the line indicate things that need to be computed to use this rule; in this case, the types of the two sub-expressions of the "," operator. 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 illustrates a general feature of the type system: the type of an expression depends only on the type of its sub-expressions. The overall static type inference algorithm is recursive, following the parse structure 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-safe.

2.7.3 Dynamic Evaluation

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, assuming the static environment statEnv and dynamic environment dynEnv are given, the expression Expr yields the value Value.

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. [XPath/XQuery]'s dynamic semantics is modeled on the dynamic semantics presented in [Milner].

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

3.1.1 Values

The following grammar introduces formal notations for values. This notation is used to formally represent values in the the [XQuery 1.0 and XPath 2.0 Data Model].

A value is a sequence of zero or more items. An item is either a node or an atomic value. A node is either an element, an attribute, a document node, or a text node. Text nodes always contain string values of type xs:anySimpleType. Elements, attributes, and atomic values have a type annotation, which is the QName of a type.

Elements may be annotated with any type, and attributes may be annotated with any simple type.

A atomic value encapsulates an XML Schema atomic type (which is its type annotation) and a corresponding value of that type. An XML Schema atomic type [XML Schema Part 2] may be primitive or derived, or xs:anySimpleType. The corresponding atomic type value may be a value in the value space of one of the 19 primitive XML Schema types.

Type annotations are always present. Untyped elements or attributes (e.g., from well-formed documents before validation has been performed) are annotated with xs:anyType and attributes and atomic values with no other type information are annotated with xs:anySimpleType.

A value is called a simple value if it consists of a sequence of zero or more atomic values.

Notation

In the above grammar, the atomic type names are used to represents the value space of the corresponding XML Schema atomic type. For instance, "String" indicates the value space of xs:string, and "Decimal" indicates the value space of xs:decimal.

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

Ed. Note: Issue: Although the XQuery data model describes an error value, this error value is not represented formally here. Formal treatment of errors is deferred to a future version of that document.

Ed. Note: Issue: The formal semantics does not represent comments and process-instructions (See [Issue-0143:  Support for PI, comment and namespace nodes]).

Ed. Note: Issue: This formal notation for values only represents either text nodes or values. (See [Issue-0144:  Representation of text nodes in formal values])

Example

Example (1):

  <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 xs:anySimpleType
      }
      text { "12" }
    },
    text { " pounds." }
  }

Example (2):

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

The formal model 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 xs:anySimpleType
    },
    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
  }

Note that the typing rules must permit attributes with name xsi:type and xsi:nil to appear on any element.

Example (3):

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

Example (4): Example 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 against this Schema, the element is represented as:

  element sizes of type xs:anySimpleType {
    1 of type xs:integer,
    2 of type xs:integer,
    3 of type xs:integer
  }

Example (5): Example 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
  }

3.1.2 Types

As they are in DTDs, types in [XPath/XQuery] are based on regular expressions. A type is 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 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 appears in the definition of [3.6.1 Prime types], and is the type for [2.5.3 The error function].

An item type is an element or attribute type, a document node type, a text node type, the untyped type (i.e., which is the type of untyped text values), or an atomic type.

An element or attribute type gives an optional name and an optional type specifier. A name with a type specifier is a local declaration. A type specifier alone is a local declaration that matches any name. A name alone refers to a global declaration. The word "element" or "attribute" alone refers to any element or any attribute.

A type specifier either references a global type, or specifies an anonymous type. An anonymous type is described by naming the base type it derives from and giving the type, optionally with a flag indicating a mixed content.

Example

Example (1).

  element

matches any element.

Example (2).

  element of type xs:integer 

matches any element of type xs:integer, such as:

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

Example (3).

  element restricts xs:anyType { xs:integer* }

matches any element of any type that contains a sequence of integers, such as:

  element numbers of type xs:integer {
    1 of type xs:integer,
    2 of type xs:integer,
    3 of type xs:integer
  }

Example (4).

  element sizes

refers to the global declaration for element "sizes".

Example (5).

  element trouble of type xs:anyType { ( xs:float | xs:string )* }

describes an element with a simple type derived by union. This type matches the following instance:

  validate as trouble { <trouble>this is not 1 string</trouble> }
=>
  element trouble of type xs:anyType {"this", "is", "not", 1, "string" }

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

  element bib { () }
  element bib { }

If the content model is omitted, then the element, (resp. attribute or type) name must be a proper QName, and refers to the global element (resp. attribute or type) with that name, which must be defined (by importation from a schema or through a type definition expression).

The type system includes three operators on types: ",", "|" and "&", corresponding respectively to sequence, choice and all groups in Schema.

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

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

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

The "|" operator builds a "choice" between two types. For example,

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

means either an element editor of type string, or a sequence of bib:author elements.

The "&" operator builds the "interleaved product" of two types. The type t₁ & t₂ matches any sequence that is an interleaving of a sequence that matches t₁ and a sequence that matches t₂. For example,

  (element a , element b) & xs:string   =
    element a, element b, xs:string
  | element a, xs:string, element b
  | xs:string, element a, element b

In each case, the order of element a and element b is unchanged, but the xs:string can be interleaved in any position.

The interleaved product is used to represent all groups in XML Schema. The xs:all construct in XML Schema may only consist of global or local element declarations with lower bound 0 or 1, and upper bound 1.

3.1.3 Top level definitions

At the top level, one can define elements, attributes, and types.

Global element and attribute declarations, like local element and attribute declarations, contain a type specifier. In addition, a global element declaration may declare the substitution group for the element and whether the element is nillable. A global type declaration specifies both the derivation and the declared type.

Ed. Note: Issue: The formal semantics provide support for substitution group. Support for substitution group is still an open issue in the [XPath/XQuery] document. (See [Issue-0144:  Representation of text nodes in formal values])

3.1.4 Built-in type declarations

The following type definitions capture the primitive types from Schema.

  define type xs:string restricts xs:anySimpleType { xs:string }
  define type xs:decimal restricts xs:anySimpleType { xs:decimal }
  ...

In the above definitions, each name (such as xs:string) appears twice. The first appearance is used for named typing (xs:string is derived by restriction from xs:anySimpleType), and the second for structural typing (the value space of xs:string is given by xs:string -- the apparent circularity here is broken in the rule for matching in [3.3 Matching], which defines matching against xs:string directly).

The following type definition captures the Ur simple type from Schema.

  define type xs:anySimpleType restricts xs:anyType {
    ( xs:string | xs:decimal | ... )*
  }

The name of the Ur simple type is xs:anySimpleType, and its structural definition is given by the union of all simple type.

Note that there is no separate "value space" for the type xs:anySimpleType, it's value space being the same as xs:string. The following example shows the distinction between a value of type string containing "Database" and an untyped value containing "Database": both are using string values as content with different type names.

"Databases" of type xs:string
"Databases" of type xs:anySimpleType
  }

The following type definition captures the Ur type from Schema.

  define type xs:anyType restricts xs:anyType {
    attribute*, 
      ( xs:anySimpleType |
        ( element* & text* ) )
  }

Schema defines four built-in attributes that can appear on any element in the document without being explicitly declared in the schema. Those four attributes need to be added inside content models when doing matching. The four built-in attributes of Schema are declared as follows.

  define attribute xsi:type of type xs:QName
  define attribute xsi:nil of type xs:boolean
  define attribute xsi:schemaLocation of type xs:anySimpleType {
    xs:anyURI*
  }
  define attribute xsi:noNamespaceSchemaLocation of type xs:anyURI

For convenience, a type that is an all group of the four built-in XML Schema attributes is defined.

  BuiltInAttributes =
      attribute xsi:type ?
    & attribute xsi:nil ?
    & attribute xsi:schemaLocation ?
    & attribute xsi:noNamespaceSchemaLocation ?

3.1.5 Syntactic constraints on types

The type system given in [3.1.2 Types] gives a simple but overly general definition of types. For instance, the above type grammar allows types to describe sequences of attributes and elements in any order. For example, the following type, describing a sequence of zero or more elements or attributes with name "year", is allowed.

  (element year of type string | attribute year of type string)*

There are two reasons for this approach. First, it makes the grammar for types simpler. Second, it allows to describe types for heterogeneous sequences, that can result from [XPath/XQuery] expressions but cannot be represented as an XML Schema. For example, the above type is inferred for the following query.

  for $b in //book return
    if ($b/publisher = "Springer") then
      element year { $b/year/text() }
    else
      attribute year { $b/year/text() }

When constructing elements, or attributes, some additional constraints on type need to be imposed, for which this grammar is too general. This section gives auxiliary grammar productions which impose additional constraints on the content of elements and attributes.

First, a grammar for simple types is defined. This grammar is a subset of the grammar for types. A simple type is composed from atomic types by optional, one or more, zero or more, choice, or empty choice.

An all group contains only attributes or only elements; attributes or elements in an all group may be optional but not repeated; attributes always precede other content of an element.

The type in an element type should always match the grammar for ElementBody given above. (Note that in case the element type is omitted altogether, e.g., like in element a { }, the type is implicitely matching the empty sequence.)

Those auxiliary productions is be used when matching the type content of elements or attributes within inference rules.

3.1.6 Example

Here is a schema describing purchase orders, taken from the XML Schema Primer, followed by its mapping into the [XPath/XQuery] type system. The complete mapping from XML Schema into the [XPath/XQuery] type system is given in [8 Importing Schemas].

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

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

  define element purchaseOrder of type ipo: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 ipo: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 {
      element productName of type xsd:string,
      element quantity restricts xsd:positiveInteger { xsd:positiveInteger },
      element USPrice of type xsd:decimal,
      element comment?,
      element shipDate of type xsd:date?
    }*
  }

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

3.2.1 Derivation and substitution

The following judgements capture the relationship between names, obtained from derivation and substitution groups in a given XML Schema.

3.2.2 Extension

Notation

The judgment

holds when the result of extending Type₁ by Type₂ is Type.

Semantics

This judgment is specified by the following rules.

3.2.3 Mixed content

Notation

The judgment

holds when the result of creating a mixed content from Type₁ is Type₂.

Semantics

This judgment is specified by the following rules.

3.2.4 Adjusts

An element may optionally include the four built-in attributes xsi:type, xsi:nil, xsi:schemaLocation, or xsi:noNamespaceSchemaLocation.

Notation

The judgment

holds when the second type is the same as the first, with the four built-in attributes added, and with text nodes added if the type is mixed.

Semantics

This judgment is specified by the following rules.

If the type is flagged as mixed, then mix the type and extend it by the built-in attributes.

Otherwise, just extend the type by the built-in attributes.

The definition of BuiltInAttributes appears in [3.1.4 Built-in type declarations].

3.2.5 Resolution

Notation

The judgment

holds when an element matches the type declaration if the element has a type annotation that derives from the type name, and a content that matches the type.

Semantics

This judgment is specified by the following rules.

If the type is omitted, it is resolved as the empty sequence type.

If the type specifier names a global type, then the type name is the name of that type, and the type is taken by resolving the type specifier of the global type.

In the above inference rule, note that BaseTypeName is the base type of the type referred to. So this is indeed the original type name, TypeName, which must be returned, and eventually used to annotated the corresponding element or attribute. However, the type specifier needs to be obtained through a second application of the judgment.

If the type specifier is a restriction, then the type name is the name of the base type, and the type is taken from the type specifier.

If the type specifier is an extension, then the type name is the name of the base type, and the type is the base type extended by the type in the type specifier.

3.2.6 Derives

Notation

The judgment

holds if the first type is derived from the second type. This corresponds to [Type Derivation OK] in [XML Schema Part 1].

Semantics

This judgment is specified by the following rules.

A type specifier validly derives from a type reference if the type specifier resolves to a type name that derives from the referenced type.

There is no rule if the type specifier not a type reference, because it is not possible for a local type to derive from another local type.

3.2.7 Lookup

Notation

The judgment

holds when matching an element with the given element name against the given element type requires that the element be nillable as indicated and matches the type specifier.

Semantics

This judgment is specified by the following rules.

If the element type is a reference to a global element, then lookup yields the type specifier in the element declaration for the given element name. The given element name must be in the substitution group of the global element.

If the given element name matches the element name in the element type, and the element type contains a type specifier, then lookup yields that type specifier.

If the element type has no element name but contains a type specifier, then lookup yields the type specifier.

If the element type has no element name and no type specifier, then lookup yields xs:anyType.

Notation

The judgment

holds when matching an attribute with the given attribute name against the given attribute type matches the type specifier.

Semantics

This judgment is specified by the following rules.

If the attribute type is a reference to a global attribute, then lookup yields the type specifier in the attribute declaration for the given attribute name.

If the given attribute name matches the attribute name in the attribute type, and the attribute type contains a type specifier, then lookup yields that type specifier.

If the attribute type has no attribute name but contains a type specifier, then lookup yields the type specifier.

If the attribute type has no attribute name and no type specifier, then lookup yields xs:anySimpleType.

3.2.8 Interleaving

Notation

The judgment

holds if some interleaving of Value₁ and Value₂ yields Value. Interleaving is non-deterministic; it is used for processing all groups.

Semantics

This judgment is specified by the following rules.

Interleaving two empty sequences yields the empty sequence.

Otherwise, pick an item from the head of one of the sequences, and recursively interleave the remainder.

3.2.9 Filtering

Notation

The judgment

holds if there are no occurrences of the attribute QName in Value. The judgment

holds if there is one occurrence of the attribute QName in Value, and the value of that attribute is SimpleValue. The judgment

holds if either of the previous two judgments hold.

Semantics

These judgments are defined using the auxiliary judgments

and

which are defined in [5.2.1 Steps].

The filter judgments are defined as follows.

3.3.1 Nil-matches

Notation

The judgment

holds when the given value matches the given nillable type.

Semantics

This judgment is specified by the following rules.

If the type is not nillable, then the xsi:nil attribute must not appear in the value, and the value must match the type.

If the type is nillable, and the xsi:nil attribute does not appear or is false, then the value must match the type.

If the type is nillable, and the xsi:nil attribute is true, then the value must match the attributes in the type. The element content of the type is ignored.

3.3.2 Matches

Notation

The judgment

holds when the given value matches the given type.

Semantics

This judgment is specified by the following rules.

The empty sequence matches the empty sequence type.

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

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

If two values match two types, then their interleaving matches the corresponding all group.

An optional type matches a value of that type or the empty sequence.

The following rules are used to match a value against a sequence of zero (or one) or more types.

An element matches an element type if the element type resolves to another element type, and the type annotation is derived from the type annotation of the resolved type, and the element value matches the enclosed type of the resolved type.

The rule for attributes is similar.

A document node matches the corresponding document type.

A text node matches text.

An atomic value matches an atomic type if its type annotation derives from the atomic type. The value itself is ignored -- this is checked as part of validation.

An atomic value matches "untyped" only if it is annotated with xs:anySimpleType.

Note

The above definition of matching, although complete and precise, does not give a simple means to compute the structural matching. Notably, some of the above rules can be non-deterministic (e.g., the rule for matching of choice or repetition).

The structural component of the [XPath/XQuery] type system can be modeled by tree grammars. Computing structural matching can be done by computing if a given tree grammar recognizes the given data model value.

This document does not provide a complete algorithm to recognize a given tree by a tree grammar. The interested reader can consult the relevant literature, for instance [Languages], or [TATA].

Ed. Note: A future version of this document should include a more complete description of algorithms to compute type matching.

3.3.3 Optimized matching

Recall the rule for matching an element against an element type.

This rule simplifies greatly in the case that the type specifier is a reference to a global type.

In this case, it is not necessary to do resolution or to check that the value matches the type, because this is guaranteed by the way in which elements are labeled with types. Note that the optimization applies only if xsi:nil is not true.

A similar optimization applies to attributes.

3.4.1 Erasure

3.4.2 Annotate

3.5.1 Subtype

Notation

The judgment

holds if the first type is a subtype of the second.

Semantics

This judgment is true if and only if, for every value Value, then Value matches Type implies Value matches Type'.

Note

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

and it is transitive: if,

and,

then,

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

The structural component of the [XPath/XQuery] type system can be modeled by tree grammars. Computing subtyping between two types can be done by computing if inclusion holds between their corresponding tree grammars.

This document does not provide a complete algorithm to compute inclusion between tree grammar. The interested reader can consult the relevant literature on tree grammars, for instance [Languages], or [TATA].

Ed. Note: A future version of this document should include a more complete description of algorithms to compute subtyping.

3.5.2 Type equivalence

In a few cases, equivalence between two types (i.e., that they define exactly the same domain over data model instances) is used.

Notation

The judgment

holds if the Type₁ is equivalent to the Type₂.

Semantics

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

3.6.1 Prime types

Some expressions must operate on sequences where all items have the same type -- this type possibly being a choice of item types. These include FLWR expressions, sortby, and distinct. For example, let's assume the document

  <paper>
      <author>Buneman</author>
      <author>Davidson</author>
      <author>Fernandez</author>
      <author>Suciu</author>
      <title>Adding structure to unstructured data</title>
      <editor>Afrati</editor>
      <editor>Kolaitis</editor>
   </paper>

is of type

   element paper {
      element author {xs:string}+,
      element title {xs:string},
      element editor {xs:string}*
   }

The following query extracts a sequence of authors followed by editors and sorts them by their content.

   (/paper/author,/paper/editor) sortby (.)

This results in a sequence of authors and editors.

      <editor>Afrati</editor>
      <author>Buneman</author>
      <author>Davidson</author>
      <author>Fernandez</author>
      <editor>Kolaitis</editor>
      <author>Suciu</author>

Based on the content model for the paper element, the type inferred for the expression (/paper/author,/paper/editor) is simply element author {xs:string}+, element editor{xs:string}*. This type indicates that there should be a sequence of one or more authors, followed by zero or more editors. Due to the sortby expression, the original order of elements within the type can then be changed in an arbitrary way. As a result, the regular expression which describes the type cannot preserve any information which relates to order. The type infered for the complete expression reflects the arbitrary order by repeating a choice of author and editor elements.

       (element author {xs:string} | element editor {xs:string})+

Intuitively, sorting expressions, as well as iteration with for expressions, always operate on sequences of items of the same type, this type possibly being a choice. A choice of items is called a Prime type, and can be described by the following grammar production.

When inferring the type of a for or a sortby expression, the system needs to compute such a prime type.

It also needs to compute the appropriate occurrence indicator for the sequence type. For instance, note that the type in the above example ends in a plus rather than a star, since there must be at least one author element in the sequence.

The rest of this section defines operations related to prime types and occurrence indicators, which are used during static type analysis.

3.6.2 Computing Prime Types and Occurrence Indicators

Notation

Two auxiliary functions on types are used.

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

The function quantifier(Type) approximates the possible number of items in Type with the occurrence indicators supported by the [XPath/XQuery] type system (?, +, *).

For interim results, the following auxiliary occurrence indicators are used: 1 for exactly one occurrence, and 0 for exactly zero occurrences, i.e., the occurrence indicator of the empty list.

Types and occurrence can be combined with the · operation, as follows.

Example

For instance, here are the result of applying prime and quantifier on a few simple types.

  prime(element a+)                         = element a
  prime(element a | ())                     = element a
  prime(element a?,element b?)              = element a | element b
  prime(element a | element b+, element c*) = element a | element b | element c

  quantifier(element a+)                         = +
  quantifier(element a | ())                     = ?
  quantifier(element a?,element b?)              = *
  quantifier(element a | element b+, element d*) = +

Note that the last occurrence indicator should be '+', since the regular expression is such that there must be at least one element in the sequence (this element being an 'a' element or a 'b' element).

Note

Note that both prime and quantifier functions are only used within type inference rules; they are not part of the [XPath/XQuery] syntax.

Semantics

The prime function is defined by induction as follows.

Semantics

The quantifier function is defined by induction as follows.

This definition uses the sum (Occurrence₁ , Occurrence₂), the choice (Occurrence₁ | Occurrence₂), and the product (Occurrence₁ · Occurrence₂) of two occurrence indicators Occurrence₁, Occurrence₂, which are defined by the following tables.

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

Note

Note that prime(Type) · quantifier(Type) is always a super type of the original type Type and therefore, can be used as an approximation for it. More formally, the following property always holds: Type <: prime(Type) · quantifier(Type). This property is important for the soundness of the static type analysis.

3.7.1 Computing common types and occurrence in typeswitch

Static type analysis for the "typeswitch" expression has to compute the choice of all the common items between two types, and the corresponding occurrence indicators.

For instance, consider the following typeswitch expression, applied on the result of the previous query.

   let $persons := (/paper/author,/paper/editor) sortby (.)
   return
     typeswitch $person
        case element author return <single-author> { $person } </single-author>
        case element author* return <authors-only> { $person } </authors-only>
        default return <authors-and-editors> { $person } </authors-and-editors>

Static type analysis needs to compute the type of the variable $person within each case clause. In the first case, the variable is of type element author. In the second case, the variable is of type element author+. The '+' occurrence indicator can be infered since the input type guarantees the input sequence has at least one author.

3.7.2 Computing Common Prime Types and Occurrence Indicators

Notation

The two following auxiliary functions on types are used.

The function common-prime(PrimeType₁, PrimeType₂) computes the type for all the items common between the prime types PrimeType₁ and PrimeType₂, and combines them into a new prime type.

The function common-occurrence(Occurrence₁, Occurrence₂) computes the occurrence indicator which approximates the possible number of items that can result from the constraints described by both Occurrence₁, and Occurrence₂.

Example

For instance, here are the result of applying common-prime and common-occurrence on a few simple prime types.

  common-prime((element a),(element a))                                      = element a
  common-prime((element a),(element b))                                      = none
  common-prime((element a | element b | element c), (element c | element a)) = element a | element c

  common-occurrence(+,+)   = +
  common-occurrence(*,+)   = +
  common-occurrence(?,+)   = 1

Note that the last occurrence indicator should be '1', since the first input occurrence indicator '?' specifies that there should be at most one item, while the second '+' specifies that there should be at least one.

Semantics

The common-prime function is defined by induction as follows.

The common-prime for two arbitrary prime types, is defined as the choice containing the results of the function common-prime applied between all possible pairs of items in each input prime types.

The common-prime function between any pair of item types return either a new item type or the empty choice (none); remember that none is the unit for choice.

If one of the item type is a subtype of the other, then the function returns the smaller item type.

Ed. Note: Issue: The above rule does not deal with cases where the two item types might have some intersection (i.e., there exist values which match both types), but subtyping does not hold between them. See [Issue-0155:  Common primes for incomparable types].

In all the other cases, common-prime returns none. I.e., otherwise:

Semantics

The common-occurrence function is defined by the following table.

Example

The above definition relies on subtyping which covers complex cases (involving derivation, substitution groups, etc.) appropriately. For instance, consider the following type declarations.

 define element person of type Person define type Person
  { element name of type xs:string }

  define element student substitutes for person of type Student
  define type Student extends Person {
    element promotion of type Promotion,
    element grade of type Grade
  }

  define type Promotion restricts xs:integer { xs:integer }
  define type Grade restricts xs:integer { xs:integer }

Here are some more complex examples of the application of the common-prime type function involving that schema.

  common-prime(Promotion, xs:integer)                           = Promotion
  common-prime(Promotion, Grade)                                = none
  common-prime(element of type Person, element of type Student) = element of type Student
  common-prime(element person, element student)                 = element student

4.1.1 Static Context

The [XPath/XQuery] static inference rules use the environment group statEnv containing the environments built during static type checking and used during both static type checking and dynamic evaluation.

The following environments are maintained in the static environment group:

Ed. Note: Issue: The static environment does not represent collations. See [Issue-0160:  Collations in the static environment]

Environments have an initial state when [expression/query] processing begins, containing, for example, the function signatures of all built-in functions.

A common use of the static environment is to expand QNames by looking up namespace prefixes in the statEnv.namespace environment.

The helper function expand is used to expand QNames by looking up the namespace prefix in statEnv.namespace. This function is defined as follows:

   statEnv |- expand(QName) = qname(URI, ncname)

or

   statEnv |- expand(QName) = qname(ncname)

the right hand side is a QName value (not a QName expression).

The helper expand function is defined as follows:

• If QName matches NCName₁:NCName₂, and if statEnv.namespace(NCName₁) = URI, then the expression yields qname(URI,NCName₂). If the namespace prefix NCName₁ is not found in statEnv.namespace, then the expression does not apply (that is, the inference rule will not match).

• If QName matches NCName, NCName is an element or type name, and statEnv.default_namespace("element") = URI, then the expression yields qname(URI,NCName), where URI is the default namespace in effect.

• If QName matches NCName, NCName is a function name, and statEnv.default_namespace("function") = URI, then the expression yields qname(URI,NCName), where URI is the default namespace in effect.

Ed. Note: The above rules could be given as proper inference rules defining the expand judgment.

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 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 the common idiom for passing new information in an environment using sub-expressions. In the case where the environment must be updated with a completely new component, the following notation is used:

4.1.2 Evaluation Context

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

The following environments are dynamic:

Ed. Note: DD: this still does not account for those functions that are genuinely overloaded, as some of the built-in functions are. Probably this will be handled by special rules for those functions in the main semantics section of the document. See [Issue-0122:  Overloaded functions]

Finally, dynamic environments have an initial state when [expression/query] processing begins, containing, for example, the function declarations of all built-in functions.

Ed. Note: Somewhere an exact definition of what is in the initial environments is needed. Notice that for XPath this is partially defined by the containing language. See [Issue-0115:  What is in the default context?].

The following Formal Semantics built-in variables represent the context item, context position , and context size properties of the evaluation 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.

Ed. Note: "fs" is actually a namespace prefix and should be replaced with a proper namespace URI unique to this spec. See [Issue-0100:  Namespace resolution].

Values of $fs:dot, $fs:position and $fs:last can be obtained by invoking the xf:context-item(), xf:position() and xf:last() functions, respectively. The context document, can be obtained by application of the xf:root() function.

The variable $fs:implicitTimezone is used to represent the implicit timezone, and is used by the timezone related functions in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Ed. Note: The Formal Semantics does not yet model the semantics of semantics of timezone related functions.

Ed. Note: The following dynamic contexts have no formal representation yet: current-date, current-time and current-dateTime. See [Issue-0114:  Dynamic context for current date and time]

4.4.1 Type Checking

This section gives background material about [XPath/XQuery] type checking. More information on the [XPath/XQuery] type system can be found in [2.4 Schemas and types] and [3 The XQuery Type System].

4.4.2 SequenceType

Introduction

SequenceTypes can be used in [XPath/XQuery] to refer to a type imported from a schema (see [6 The Query Prolog]). 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.