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 and anonymous types

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

For example, consider the document fragment

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

and its 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.

In the case a schema type does not have an explicit name, it is called of anonymous types. In that case, the data model annotates the corresponding element or attributes with an implementation-defined type name. Those special anonymous type names, are not visible to the user.

For example, the above schema could be written as an anonymous type as follows.

and its associated schema

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

In that case, a type name is automatically generated by the system, this name is used to annotated the fact elements after schema validation.

Type annotations are have an impact on the semantics of [XPath/XQuery]. For example, consider the following function declaration

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

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.2 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.2 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.4 Judgments for type 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.4.3 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.8 Judgments for the validate expression].

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" type="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 name="student" type="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>
  

  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($x as element of type Person)
      { .... }
  

  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
• fn:false
• fn:true
• fn:count
• fn:boolean
• fn:get-namespace-uri
• fn:get-local-name
• fn:round
• fn:compare
• fn:not
• fn:empty
• fn:root
• fn: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 fn: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 fn:distinct-nodes function is:

  fn:distinct-nodes(node*) as 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 fn:distinct-nodes is applied on a parameter of type element a*, element b, one can easily deduce that the resulting sequence is a collection of either a or b elements.

In order to provide better static typing, 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.

• fn:error
• fn:distinct-nodes
• fn:distinct-values
• op:union
• op:intersect
• op:except
• op:to
• fn: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 fn: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

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

2.5.5 Other Formal Semantics functions

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 "(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 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.

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.

2.7.4 Formal Semantics internal links

Note that for convenience, the formal semantics features internal hyperlinks to be able to recall of the judgments and environments being used in inference rules. Clicking on a judgment or environment should point to the location where that judgment or environment has been defined.

3.2.1 Item types

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

An element or attribute type has an optional name and an optional type reference. A name alone corresponds to 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 have an optional nillable flag which indicates whether the element can be nilled or not.

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
  }

3.2.2 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 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 prime types in [3.6 Judgments for the typeswitch expression], and is the static type for [2.5.3 The error function].

The type system includes three binary operators on types: ",", "|" and "&", corresponding respectively to sequence, choice and all groups in Schema. The 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.

A choice between two elements

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

  ()

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

3.2.3 Top level definitions

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

A type definition has a name (possibly anonymous) and a type derivation. A type derivation indicates if the type is derived by extension or restriction from its based type, gives its content model, and an optional flag indicating if it has mixed content.

A type is derived either by extension or restriction from a base type. In case the type derivation is omitted, the type derives by restriction from xs:anyType, as in:

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

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

  define type Bib { } =
  define type Bib { () }

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

Examples

A type declaration with complex content

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

A type declaration with complex content derived by extension

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

A type declaration with mixed content

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

A type declaration with simple content derived by restriction

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

An element declaration

  define element address of type Address

An element declaration with a substitution group

  define element usaddress substitutes for address of type USAddress

An element declaration which is nillable

  define element zip nillable of type xs:integer

3.2.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 declares the relation between type names (xs:string is derived by restriction from xs:anySimpleType). The second declares the value space for the type (the value space of xs:string is described by xs:string, and corresponds to the value space as defined in the XML Schema specification).

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. It is derived by restriction from xs:anyType, its content is given by the union of all primitive atomic types.

Note that there is no separate "value space" for the type untyped. It has the same value space as xs:string, but its type annotation is xs:anySimpleType. 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 annotations.

"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* ) )
  }

The xs:anyType is defined by restriction from itself, and it can contain any number of attributes, and either a simple content or a complex content with any number of elements or text nodes.

3.2.5 Syntactic constraints on types

The type system given in [3.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 xs:string | attribute year of type xs: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.

When constructing elements, or attributes, some additional constraints on type must to be checked, 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.2.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 of type [Anon1]*
  }

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

  define type [Anon2] restricts xsd:positiveInteger { xsd:positiveInteger }

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

Note the way the two anonymous types inside the item element are handled by giving them anonymous names [Anon1] and [Anon2].

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

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

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

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

Those definitions are written in the type system as follows.

  define type NYCAddress extends USAddress {
    element appt
  }

  define element appt of type [Anon3]

  define type [Anon3] restricts xsd:positiveInteger

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

3.3.1 Derives

Notation

The judgment

holds when the first type name derives from the second type name.

Example

For example, assuming the extended XML Schema given in section [3.2.6 Example], then the following judgments hold.

  USAddress            derives from  xs:anyType
  NYCAddress           derives from  USAddress
  NYCAddress           derives from  xs:anyType
  xsd:positiveInteger  derives from  xsd:integer
  xsd:integer          derives from  xs:anySimpleType
  [Anon3]              derives from  xsd:positiveInteger
  [Anon3]              derives from  xsd:integer
  [Anon3]              derives from  xs:anySimpleType
  [Anon3]              derives from  xs:anyType

Note

Derivation is a partial order. It is reflexive and transitive by the definition below. It is asymmetric because no cycles are allowed in derivation by restriction or extension.

Semantics

This judgment is specified by the following rules.

Some rules have hypotheses that simply list a type, element, or attribute declaration.

Every type name derives from itself.

Every type name derives from the type it is declared to derive from by restriction or extension.

Derivation is transitive.

3.3.2 Substitutes

The substitutes judgment is used to know whether an element name is in the substitution group of another element name.

Notation

The judgment

holds when the first element name substitutes for the second element name.

Example

For example, assuming the extended XML Schema given in section [3.2.6 Example], then the following judgments hold.

  usaddress  substitutes element for  address
  nyaddress  substitutes element for  usaddress
  nyaddress  substitutes element for  address

Note

Substitution is a partial order. It is reflexive and transitive by the definition below. It is asymmetric because no cycles are allowed in substitution groups.

Semantics

The substitutes judgment for element names is specified by the following rules.

Every element name substitutes for itself.

Every element name substitutes for the element it is declared to substitute for.

Substitution is transitive.

3.4.1 Element and attribute lookup

Element and attribute types can be of various kinds: reference to a global element or attribute declaration, local element with or without a wildcard, an element can be nillable or not, etc. The lookup judgments are used to obtain the appropriate type annotations from any given attribute or element type.

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

Example

For example, assuming the extended XML Schema given in section [3.2.6 Example], then the following judgments hold.

  comment    lookup element comment                          yields of type xsd:string
  size       lookup element size nillable of type xs:integer yields nillable of type xsd:string
  appt       lookup element appt                             yields of type [Anon3]
  nycaddress lookup element address                          yields of type NYCAddress

Note that in the case the element name is in the substitution group, the lookup returns the type name of corresponding to the original element name (here the type NYCAddress for the element nycaddress, instead of Address for the element address).

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 reference 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 reference, then lookup yields that type reference.

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

If the element type has no element name and no type reference, 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 reference.

Example

For example, assuming the extended XML Schema given in section [3.2.6 Example], then the following judgments hold.

  orderDate  lookup  attribute orderDate of type xsd:date  yields  of type xsd:date?
  orderDate  lookup  attribute of type xsd:date            yields  of type xsd:date?

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 reference 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 reference, then lookup yields that type reference.

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

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

3.4.2 Matches

Notation

The judgment

holds when the given value matches the given type.

Example

For example, assuming the extended XML Schema given in section [3.2.6 Example], then the following judgments hold.

  element comment of type xsd:string { "This is not important" }
    matches
  element comment of type xsd:string

  (element appt of type [Anon3] { 2510 },
   element appt of type [Anon3] { 2511 })
    matches
  element appt+

  ()
    matches
  element usaddress?

  element usaddress of type USAddress {
    element name of type xsd:string { "The Archive" },
    element street of type xsd:string { "Christopher Street" },
    element city of type xsd:string { "New York" },
    element state of type xsd:string { "NY" },
    element zip of type xsd:decimal { 10210 }
  }
    matches
  element usaddress?

Semantics

We start by giving the inference rules for matching an element against an element type.

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. Note that there is no need to check structural constraints on the value since since those have been checked during XML Schema validation and the value is assumed to be consistent with its type annotation.

In the case the element has been nilled, the following alternative rule applies, which checks that the type is nillable and that there exists and xsi:nil attribute set to true in the element.

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 a string an is annotated with xs:anySimpleType.

A type can also be a sequence of items, in that case the matching rules also need to check whether the constraints described by the type as a regular expression hold. This 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.

Note

The above definition of type matching, although complete and precise, does not give a simple means to compute type 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 regular expressions. Regular expressions can be implemented by means of finite state automata. Computing type matching then is equivalent to check if a given sequence of items is recognized by its corresponding finite state automata. Finite state automata and their relationships to regular expressions have been extensively studied and documented in the literature. The interested reader can consult the relevant literature, for instance [Languages], or [TATA].

3.4.3 Subtype

Introduction

This section defines the semantics of subtyping in [XPath/XQuery]. Subtyping is used during the static type analysis, in typeswitch expressions, treat and assert expressions, and to check the correctness of function applications.

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, if Value matches Type₁ holds, then Value matches Type₂ also holds.

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,

Note

The above definition although complete and precise, does not give a simple means to compute subtyping. Notably the definition above refers to values which are not available at static type checking type.

The structural component of the [XPath/XQuery] type system can be modeled by regular expressions. Regular expressions can be implemented by means of finite state automata. Computing subtyping between two types can then be done by computing if inclusion holds between their corresponding finite states automata.

Finite state automata and how to compute operations on those automata, such as inclusion, emptiness or intersection have been extensively studied and documented in the literature. The interested reader can consult the relevant literature on tree grammars, for instance [Languages], or [TATA].

3.8.1 Builtin attributes

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 fs:anyURIlist
  define type fs:anyURIlist { 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.8.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.8.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.8.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.2.4 Built-in type declarations].

3.8.5 Type resolution

Notation

The judgment

holds when a type reference or a type derivation resolves to the given type name and type content.

Semantics

This judgment is specified by the following rules.

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

In case of a type reference, then the type name is the name of that type, and the type is taken by resolving the type declaration 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 needs to be obtained through a second application of the judgment.

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

If the type derivation 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 derivation.

3.8.6 Element and attribute lookup

Element and attribute lookup used in validation is identical to the one used for type matching and is defined in [3.4.1 Element and attribute lookup].

3.8.7 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.8.8 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.8.9 Structural matching

Introduction

We first extend the notion of type matching to handle both names and structures. The structural semantics of a type is given by the notion of structural matching.

A tree in the [XQuery 1.0 and XPath 2.0 Data Model] structurally matches a type in the [XPath/XQuery] type system, if and only if:

• It verifies the structural constraints described by the type.

• It verifies the name constraints described by the type.

Example

For example, the data model value

  element bib:pubdate of type [Anon3] { 1954, 1966, 1974, 1986 }

structurally matches the following type

  element of type [Anon3]
  define type [Anon3] { attribute country { xs:string }?, xs:integer* }

because the element name (bib:pubdate) matches the wildcard element in the type, the type annotation ([Anon3]) matches the type name, the attribute "country" is optional, and the content of that element is indeed a sequence of integers.

But the data model value

  element bib:pubdate of type [Anon3] { attribute pays { "France" }, 1954, 1966, 1974, 1986 }

does not structurally match the same type, since the element in the data model contains an attribute which is not described in the schema. This violates the structural requirement of the schema.

3.8.10 Erasure

3.8.11 Annotate