W3C

XQuery 1.0 and XPath 2.0 Formal Semantics

W3C Working Draft 16 August 2002

This version:
http://www.w3.org/TR/2002/WD-query-semantics-20020816/
Latest version:
http://www.w3.org/TR/query-semantics/
Previous versions:
http://www.w3.org/TR/2002/WD-query-semantics-20020326/
http://www.w3.org/TR/2001/WD-query-semantics-20010607/
http://www.w3.org/TR/2001/WD-query-algebra-20010215/
http://www.w3.org/TR/2000/WD-query-algebra-20001204/
Editors:
Denise Draper (XML Query WG), Nimble Technology <ddraper@nimble.com>
Peter Fankhauser (XML Query WG), Infonyte GmbH <fankhaus@infonyte.com>
Mary Fernández (XML Query WG), AT&T Labs - Research <mff@research.att.com>
Ashok Malhotra (XML Query and XSL WGs), Microsoft <ashokma@microsoft.com>
Kristoffer Rose (XSL WG), IBM Research <krisrose@us.ibm.com>
Michael Rys (XML Query WG), Microsoft <mrys@microsoft.com>
Jérôme Siméon (XML Query WG), Lucent Technologies <simeon@research.bell-labs.com>
Philip Wadler (XML Query WG), Avaya <wadler@avaya.com>

Abstract

This document defines the formal semantics of XQuery 1.0 [XQuery 1.0: A Query Language for XML] and XPath 2.0 [XML Path Language (XPath) 2.0].

Status of this Document

This is a public W3C Working Draft for review by W3C Members and other interested parties. This section describes the status of this document at the time of its publication. It is a draft document and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use W3C Working Drafts as reference material or to cite them as other than "work in progress." A list of current public W3C technical reports can be found at http://www.w3.org/TR/.

This document is a work in progress. It contains many open issues, and should not be considered to be fully stable. Vendors who wish to create preview implementations based on this document do so at their own risk. While this document reflects the general consensus of the working groups, there are still controversial areas that may be subject to change.

Among the most important changes from the previous version of this document are:

A complete list of issues is maintained in [C Issues]. The following are identified as high priority issues.

Public comments on this document and its open issues are welcome. Comments should be sent to the W3C XPath/XQuery mailing list, public-qt-comments@w3.org (archived at http://lists.w3.org/Archives/Public/public-qt-comments/).

XQuery 1.0, XPath 2.0, and their formal semantics has been defined jointly by the XML Query Working Group (part of the XML Activity) and the XSL Working Group (part of the Style Activity).

Patent disclosures relevant to this specification may be found on the XML Query Working Group's patent disclosure page at http://www.w3.org/2002/08/xmlquery-IPR-statements and the XSL Working Group's patent disclosure page at http://www.w3.org/Style/XSL/Disclosures.

Table of Contents

1 Introduction
2 Preliminaries
    2.1 Processing model
    2.2 Namespaces
    2.3 Data Model
        2.3.1 Data model overview
        2.3.2 Node identity
        2.3.3 Document order and sequence order
        2.3.4 Type annotations
    2.4 Schemas and types
        2.4.1 The elements of a (statically) typed language
        2.4.2 XML Schema and the XQuery type system
        2.4.3 Structural and named typing
        2.4.4 Subtyping
            2.4.4.1 Type substitutability
            2.4.4.2 Subtyping and XML Schema derivation
    2.5 Functions
        2.5.1 Functions and operators
        2.5.2 Functions and static typing
        2.5.3 The error function
        2.5.4 Data Model Accessors and XPath Axes
        2.5.5 Other Formal Semantics functions
    2.6 Notations
        2.6.1 Grammar productions
        2.6.2 Judgments
        2.6.3 Inference rules
        2.6.4 Environments
        2.6.5 Putting it together
    2.7 The Formal Semantics
        2.7.1 Normalization
        2.7.2 Static type inference
        2.7.3 Dynamic Evaluation
3 The XQuery Type System
    3.1 Values and Types
        3.1.1 Values
        3.1.2 Types
        3.1.3 Top level definitions
        3.1.4 Built-in type declarations
        3.1.5 Syntactic constraints on types
        3.1.6 Example
    3.2 Auxiliary judgments
        3.2.1 Derivation and substitution
            3.2.1.1 Derives
            3.2.1.2 Substitutes
        3.2.2 Extension
        3.2.3 Mixed content
        3.2.4 Adjusts
        3.2.5 Resolution
        3.2.6 Derives
        3.2.7 Lookup
        3.2.8 Interleaving
        3.2.9 Filtering
    3.3 Matching
        3.3.1 Nil-matches
        3.3.2 Matches
        3.3.3 Optimized matching
    3.4 Erase and Annotate
        3.4.1 Erasure
            3.4.1.1 Simply erases
            3.4.1.2 Erases
        3.4.2 Annotate
            3.4.2.1 Simply annotate
            3.4.2.2 Nil-annotate
            3.4.2.3 Annotate
    3.5 Subtyping
        3.5.1 Subtype
        3.5.2 Type equivalence
    3.6 Auxiliary typing judgments for for, unordered, and sortby expressions
        3.6.1 Prime types
        3.6.2 Computing Prime Types and Occurrence Indicators
    3.7 Auxiliary typing judgments for typeswitch expressions
        3.7.1 Computing common types and occurrence in typeswitch
        3.7.2 Computing Common Prime Types and Occurrence Indicators
    3.8 Major type issues
4 Basics
    4.1 Expression Context
        4.1.1 Static Context
        4.1.2 Evaluation Context
    4.2 Input Functions
    4.3 Expression Processing
    4.4 Types
        4.4.1 Type Checking
        4.4.2 SequenceType
        4.4.3 Type Conversions
            4.4.3.1 Atomization
            4.4.3.2 Effective Boolean Value
            4.4.3.3 Fallback Conversion
    4.5 Errors and Conformance
5 Expressions
    5.1 Primary Expressions
        5.1.1 Literals
        5.1.2 Variables
        5.1.3 Parenthesized Expressions
        5.1.4 Function Calls
        5.1.5 Comments
    5.2 Path Expressions
        5.2.1 Steps
            5.2.1.1 Axes
            5.2.1.2 Node Tests
        5.2.2 Predicates
        5.2.3 Unabbreviated Syntax
        5.2.4 Abbreviated Syntax
    5.3 Sequence Expressions
        5.3.1 Constructing Sequences
        5.3.2 Combining Sequences
    5.4 Arithmetic Expressions
    5.5 Comparison Expressions
        5.5.1 Value Comparisons
        5.5.2 General Comparisons
        5.5.3 Node Comparisons
        5.5.4 Order Comparisons
    5.6 Logical Expressions
    5.7 Constructors
        5.7.1 Element Constructors
        5.7.2 Computed Element and Attribute Constructors
            5.7.2.1 Computed Element Nodes
            5.7.2.2 Constructed Attribute Nodes
        5.7.3 Whitespace in Constructors
        5.7.4 Other Constructors and Comments
    5.8 [For/FLWR] Expressions
        5.8.1 FLWR expressions
        5.8.2 For expression
        5.8.3 Let Expression
    5.9 Order-Related Expressions
        5.9.1 Sorting Expressions
        5.9.2 Unordered Expressions
    5.10 Conditional Expressions
    5.11 Quantified Expressions
    5.12 Expressions on SequenceTypes
        5.12.1 Instance Of
        5.12.2 Typeswitch
        5.12.3 Cast and Treat
            5.12.3.1 Cast as
            5.12.3.2 Treat as
    5.13 Validate Expressions
6 The Query Prolog
    6.1 Namespace Declarations
    6.2 Schema Imports
    6.3 Xmlspace Declaration
    6.4 Default Collation
    6.5 Function Definitions
7 Additional Semantics of Functions
    7.1 Formal Semantics Functions
        7.1.1 The fs:characters-to-string function
        7.1.2 The fs:distinct-doc-order function
        7.1.3 The fs:item-sequence-to-node-sequence function
        7.1.4 The fs:item-sequence-to-string function
    7.2 Functions with specific typing rules
        7.2.1 The xf:error function
        7.2.2 The xf:distinct-nodes, and xf:distinct-values functions
        7.2.3 The op:union, op:intersect and op:except operators
        7.2.4 The op:to operator
        7.2.5 The xf:data function
8 Importing Schemas
    8.1 Introduction
        8.1.1 Features
        8.1.2 Organization
        8.1.3 Main mapping rules
        8.1.4 Special attributes
            8.1.4.1 use
            8.1.4.2 minOccurs and maxOccurs
            8.1.4.3 mixed
            8.1.4.4 nillable
            8.1.4.5 substitutionGroup
    8.2 Attribute Declarations
        8.2.1 Global attributes declarations
        8.2.2 Local attribute declarations
    8.3 Element Declarations
        8.3.1 Global element declarations
        8.3.2 Local element declarations
    8.4 Complex Type Definitions
        8.4.1 Global complex type
        8.4.2 Local complex type
        8.4.3 Complex type with simple content
        8.4.4 Complex type with complex content
    8.5 Attribute Uses
    8.6 Attribute Group Definitions
        8.6.1 Attribute group definitions
        8.6.2 Attribute group reference
    8.7 Model Group Definitions
    8.8 Model Groups
        8.8.1 All groups
        8.8.2 Choice groups
        8.8.3 Sequence groups
    8.9 Particles
        8.9.1 Element reference
        8.9.2 Group reference
    8.10 Wildcards
        8.10.1 Attribute wildcards
        8.10.2 Element wildcards
    8.11 Identity-constraint Definitions
    8.12 Notation Declarations
    8.13 Annotation
    8.14 Simple Type Definitions
        8.14.1 Global simple type definition
        8.14.2 Local simple type definition
        8.14.3 Simple type content
    8.15 Schemas as a whole
        8.15.1 Schema
        8.15.2 Include
        8.15.3 Redefine
        8.15.4 Import

Appendices

A Normalized core grammar
    A.1 Core lexical structure
        A.1.1 Syntactic Constructs
    A.2 Core BNF
B References
    B.1 Normative References
    B.2 Non-normative References
    B.3 Background References
C Issues
    C.1 Introduction
    C.2 Issues list
    C.3 Alphabetic list of issues
        C.3.1 Open Issues
        C.3.2 Resolved (or redundant) Issues
    C.4 Delegated Issues
        C.4.1 XPath 2.0
        C.4.2 XQuery
        C.4.3 Operators


1 Introduction

This document defines the formal semantics of XQuery 1.0 and XPath 2.0. The present document is part of a set of documents that together define the XQuery 1.0 and XPath 2.0 languages:

Ed. Note: [Kristoffer/XSL] The role of the formal semantics document could be clarified: does it supplement or subsume the language specification in case of conflict?

The scope and goals for the [XPath/XQuery] language are discussed in the charter of the W3C [XSL/XML Query] Working Group and in the [XPath/XQuery] requirements [XML Query 1.0 Requirements].

[XPath/XQuery] is a powerful language, capable of selecting and extracting complex patterns from XML documents , reformulating them into results in arbitrary ways, and computing expressions over the result. This document defines the semantics of [XPath/XQuery] by giving a precise formal meaning to each of the constructions of the [XPath/XQuery] specification in terms of the [XPath/XQuery] data model. This document assumes that the reader is already familiar with the [XPath/XQuery] language.

Two important design aspects of [XPath/XQuery] are that it is functional and that it is typed. These two aspects play an important role in the [XPath/XQuery] Formal Semantics.

[XPath/XQuery] is a functional language. It is built from expressions, rather than statements. Every construct in the language (except for the query prolog) is an expression and expressions can be composed arbitrarily. The result of one expression can be used as the input to any other expression, as long as the type of the result of the former expression is compatible with the input type of the latter expression with which it is composed. Another aspect of the functional approach is that variables are always passed by value and their value cannot be modified through side-effects.

[XPath/XQuery] is a typed language. Types can be imported from one or more XML Schemas describing the documents that will be processed, and the [XPath/XQuery] language can then perform operations based on these types (e.g., using a treat as operation). In addition, [XPath/XQuery] also supports a level of static type analysis. This means that the system can perform infer the type of a [expression/query], based on the type of its inputs. Static typing allows early error detection, and can be used as the basis for certain forms of optimization. The type system of [XPath/XQuery] is based on [XML Schema]. The [XPath/XQuery] type system models most of the features of [XML Schema Part 1], including global and local element and attribute declarations, complex and simple type definitions, named and anonymous types, derivation by restriction, extension, list and union, substitution groups, and wildcard types. It does not model uniqueness constraints and facet constraints on simple types. The main issues with respect to the [XPath/XQuery] type system are discussed in [3.8 Major type issues].

The [XPath/XQuery] formal semantics builds on long-standing traditions in the database and in the programming languages communities. In particular, the [XPath/XQuery] formal semantics has been inspired by works on SQL [SQL], OQL [ODMG], [BKD90], [CM93], and nested relational algebra (NRA) [BNTW95], [Col90], [LW97], [LMW96]. Other references include Quilt [Quilt], UnQL [BFS00], XDuce [HP2000], XML-QL [XMLQL99], XPath 1.0 [XML Path Language (XPath) : Version 1.0], XQL [XQL99], XSLT [XSLT 99], and YATL [YAT99]. Additional related work can be found in the bibliography [B References].

This document is organized as follows. [2 Preliminaries] introduces notations used to define the [XPath/XQuery] formal semantics. [3 The XQuery Type System] describes the [XPath/XQuery] type system, operations on the [XPath/XQuery] type system, and explains the relationship between the [XPath/XQuery] type system and XML Schema. [4 Basics] describes semantics for basic [XPath/XQuery] concepts, and [5 Expressions], describes the dynamic and static semantics of [XPath/XQuery] expressions. [6 The Query Prolog] describes the semantics of the [XPath/XQuery] prolog. [7 Additional Semantics of Functions] describes any additional semantics required for [XPath/XQuery] functions. Finally, [8 Importing Schemas], specifies how XML Schemas are imported into the [XPath/XQuery] type system.

2 Preliminaries

This section provides the background necessary to understand the [XPath/XQuery] Formal Semantics and introduces the notations that are used.

2.1 Processing model

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

The processing model consists of five phases; each phase consumes the result of the previous phase and generates output for the next phase. For each processing phase, we furthermore point to the relevant notations introduced later in the document.

  1. Parsing. The grammar for the [XPath/XQuery] syntax is defined in [XQuery 1.0: A Query Language for XML]. Parsing may generate syntax errors. If no error occurs, an internal representation of the parsed syntax tree corresponding to the query is created: this ensures that we can unambiguously specify the following phases by a case per syntax production.

  2. Context Processing. The semantics of [expression/query] depends on the input context. The input context needs to be generated before the [expression/query] can be processed. In XQuery, the input context is described in the Query Prolog (See [6 The Query Prolog]). In XPath, the input context is generated by the processing environment. The input context is split in a static and a dynamic part (denoted statEnv and dynEnv, respectively).

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

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

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

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

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

    If the [expression/query] is not type-safe, static type analysis can result in a static error. For instance, a comparison between an integer value and a string value might be detected as an error during the static type analysis. If static type analysis succeeds, it results in a syntax tree where each sub-expression is "decorated" with its static type, and in an output type for the result of the [expression/query].

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

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

  5. Dynamic Evaluation. This is the phase in which the result of the [expression/query] is computed. The semantics of evaluation is defined only for Core [expression/query] terms. Evaluation works by bottom-up application of evaluation rules over expressions, starting with evaluation of literals. This guarantees that every expression can be unambiguously reduced to a value, which is the final result of the [expression/query].

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

Ed. Note: Issue:[Kristoffer/XSL] The distinction between errors manifest by not being able to prove a judgment and special error values is not clear. Also the processing model does not allow for skipping static typing. See [Issue-0094:  Static type errors and warnings], [Issue-0171:  Raising errors], and [Issue-0169:  Conformance Levels].

The first four phases above are "analysis-time" (sometimes also called "compile-time") steps, which is to say that they can be performed on a [expression/query] before examining any input document. Indeed, analysis-time processing can be performed before such document even exists. Analysis-time processing can detect many errors early-on, e.g., syntax errors or type errors. If no error occurs, the result of analysis-time processing could be some compiled form of [expression/query], suitable for execution by a compiled-[expression/query] processor. The last phase is an "execution-time" (sometimes also called "run-time") step, which is to say that the query is evaluated on actual input document(s).

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

While implementations may be free to employ different processing models, the [XPath/XQuery] static semantics relies on the existence of a static type analysis phase that precedes any access to the input data. Statically typed implementations are required to find and report static type errors, as specified in this document. It is still an open issue (See [Issue-0098:  Implementation of and conformance levels for static type checking]) whether to make the static type analysis phase optional to allow implementations to return a result for a type-invalid [expression/query] in special cases where the [expression/query] happens to perform correctly on a particular instance of input data. (Note that this is not the same as merely permitting that the static type error is emitted at evaluation time as is done below.)

Notice that the separation of logical processing into phases is not meant to imply that implementations must separate analysis-time from evaluation-time processing: [expression/query] processors may choose to perform all phases simultaneously at evaluation-time and may even mix the phases in their internal implementations. The processing model defines only what the final result.

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

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

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

  3. Serialization phase. Once the [expression/query] is evaluated, processors might want to serialize the result of the [expression/query] as actual XML documents. Serialization of data model instances is still an open issue (See [Issue-0116:  Serialization]) and is not discussed further here.

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

For the other three phases (normalization, static type analysis and evaluation), instead or giving an algorithm in pseudo-code, the semantics is described formally by means of inference rules. Inference rules provide a notation to describe how the semantics of an expression derives from the semantics of its sub-expressions. Hence, they provide a concise and precise way for specifying bottom-up algorithms, as required by the normalization, static type analysis, and evaluation phases.

2.2 Namespaces

The Formal Semantics uses the following namespace prefixes.

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

Ed. Note: [Kristoffer/XSL] The fs: prefix URI should be defined here.

2.3 Data Model

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

This section presents an introduction to (statically) typed languages in general, and a conceptual overview of the [XPath/XQuery] type system in particular. The [XPath/XQuery] type system is discussed formally in [3 The XQuery Type System].

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.

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

2.4.4.1 Type substitutability

Subtyping plays a crucial role in the semantics of function application since all functions have an associated signature that declares the types of input parameters and the type of the result of the function.

Intuitively, one can call a function not only by passing an argument of the declared type, but also any argument whose type is a subtype of the declared type. This property is called type substitutability.

Ed. Note: [Kristoffer/XSL] Type substitutability should really be true for any subexpression, not just function arguments (it just happens that in functional languages, where type substitutability is usually defined, the situations are equivalent). Specifically type substitutability does not apply to any subexpression of [XPath/XQuery]: typeswitch violates it. In particular this means that while one may replace a function argument with one whose type is a subtype this does not guarantee that the resulting value is the same even if the value is the same (but cast to a subtype).

2.4.4.2 Subtyping and XML Schema derivation

Subtyping in [XPath/XQuery] is related to, but not identical to, "derivation by restriction" in XML Schema. A type derived by restriction is always a subtype of its base type, but the opposite is not true. For instance, consider the following types:

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

The first type is a subtype of the second, because any sequence that contains one or more doubles is also an example of a sequence containing a double followed by a sequence of zero or more integers or doubles. But the first type cannot be derived from the second type using derivation by restriction as defined in XML Schema.

2.5 Functions

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 Notations

In order to make the specification of the semantics both concise and precise, formal notations in the form of judgments and inference rules are used. This section, introduces the notations for judgments, inference rules and mapping rules, as well as the notion of an environment.

This section is intended for the reader who may not be familiar with these notations. The reader familiar with these notations can skip this section and go directly to [2.7 The Formal Semantics].

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.

[10 (XQuery)]   FLWRExpr   ::=   ((ForClause |  LetClause)+ WhereClause? "return")* QuantifiedExpr

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.

[13 (XPath)]   ForExpr   ::=   (ForClause "return")* QuantifiedExpr

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.

[8 (Core)]   ForExpr   ::=   (ForClause "return")* TypeswitchExpr

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.

[27 (Formal)]   Definition   ::=   (<"define" "element"> ElementName Substitution? Nillable? TypeSpecifier)
|  (<"define" "attribute"> AttributeName TypeSpecifier)
|  (<"define" "type"> TypeName TypeDerivation)

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

Painting is beautiful

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

Expr => Value

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

Notation

The judgment

Expr : Type

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. Expr1, Expr2), 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 'Expr1 => Expr1' but '$x+0 => 3' is not since the two expressions '$x+0' and '3' cannot be both instance of the pattern Expr1. On the contrary, '$x+0 => 3' is an instance of the judgment 'Expr1 => Expr2'.

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

premise1 ... premisen

conclusion

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:

$x => 0      3 => 3

$x + 3 => 3

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:


3 => 3

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:

Variable => Integer

Variable + 0 => Integer

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( symbol1 |-> object1 ; ... ; symboln |-> objectn ) ]" 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(symbol1 |-> object1)]) ... [mem(symboln |-> objectn)])".

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

dynEnv |- Expr => Value

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:

statEnv |- Expr1 : Type1      statEnv |- Expr2 : Type2

statEnv |- Expr1 , Expr2 : Type1, Type2

This rule is read as follows: if two expressions Expr1 and Expr2 have already been statically inferred to have types Type1 and Type2 (the two premises above the line), then it is the case that the expression below the line "Expr1 , Expr2" must have the type "Type1, Type2", which is the sequence of types Type1 and Type2.

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.

statEnv |- Expr1 : Type1      statEnv [ varType(QName : Type1) ] |- Expr2 : Type2

statEnv |- let $QName := Expr1 return Expr2 : Type2

This rule should be read as follows. First, the type Type1 for the "let" input expression Expr1 is computed. Second the "let" variable is added into the varType member of the static environment group statEnv, with type Type1. Finally, the type Type2 of Expr2 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 The Formal Semantics

Finally, this section introduces the top-level notations defining the processing model phases described above. These notations are used to define the normalization, static type analysis, and dynamic evaluation processing phases.

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:

 
[Object]Subscript
==
Mapped Object

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

statEnv |- [Object] Subscript == Mapped Object

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

 
[Expr]Expr
==
CoreExpr

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

statEnv |- Expr : Type

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:

statEnv |- Expr1 : xs:boolean      statEnv |- Expr2 : Type2      statEnv |- Expr3 : Type3

statEnv |- if Expr1 then Expr2 else Expr3 : ( Type2 | Type3 )

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: '(Type2|Type3)'.

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 Expr1, Expr2, and Expr3) 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

statEnv ; dynEnv |- Expr => Value

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 The XQuery Type System

Ed. Note: Status:This section has been extensively revised to improve the alignment between the [XPath/XQuery] type system and XML Schema. It now incorporates "named typing". Feedback on the new design is solicited.

The [XPath/XQuery] type system is used for the specification of both the dynamic and the static semantics of [XPath/XQuery]. It is used to describe the semantics of expressions on sequence types and in type conversion rules. It is also the basis for the static semantics of [XPath/XQuery].

This section defines formal values and types, four main operations on types. Three operations (match, erase, and annotate) are used for the dynamic semantics. The last operation (subtyping) is used for the static semantics.

3.1 Values and Types

This section introduces formal notations for describing XQuery types and values. Those notations are used extensively throughout this document to represent values and types in inference rules. We use formal notations for values and types because they are more compact, and are easier to manipulate within the inference rules. The formal notations for values and types introduced here are not exposed to the XQuery user.

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.

[1 (Formal)]   Value   ::=   Item
|  (Value "," Value)
|  ("(" ")")
[2 (Formal)]   SimpleValue   ::=   AtomicValue
|  (SimpleValue "," SimpleValue)
|  ("(" ")")
[3 (Formal)]   ElementValue   ::=   "element" ElementName TypeAnnotation "{" Value "}"
[4 (Formal)]   AttributeValue   ::=   "attribute" AttributeName TypeAnnotation "{" SimpleValue "}"
[5 (Formal)]   DocumentValue   ::=   "document" "{" Value "}"
[6 (Formal)]   TextValue   ::=   "text" "{" String "}"
[7 (Formal)]   NodeValue   ::=   ElementValue
|  AttributeValue
|  DocumentValue
|  TextValue
[8 (Formal)]   Item   ::=   NodeValue
|  AtomicValue
[9 (Formal)]   AtomicValue   ::=   AtomicTypeValue TypeAnnotation
[10 (Formal)]   AtomicTypeValue   ::=   String
|  Boolean
|  Decimal
|  Float
|  Double
|  Duration
|  DateTime
|  Time
|  Date
|  GYearMonth
|  GYear
|  GMonthDay
|  GDay
|  GMonth
|  HexBinary
|  Base64Binary
|  AnyURI
|  QName
|  NOTATION
[11 (Formal)]   TypeAnnotation   ::=   <"of" "type"> TypeName
[12 (Formal)]   ElementName   ::=   QName
[13 (Formal)]   AttributeName   ::=   QName
[14 (Formal)]   TypeName   ::=   QName

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

[15 (Formal)]   Type   ::=   ItemType
|  (Type Occurrence)
|  (Type "&" Type)
|  (Type "," Type)
|  (Type "|" Type)
|  ("(" ")")
|  "none"
[16 (Formal)]   Occurrence   ::=   "*" |  "+" |  "?"

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.

[17 (Formal)]   ItemType   ::=   ElementType
|  AttributeType
|  ("document" ("{" Type? "}")?)
|  "text"
|  "untyped"
|  AtomicTypeName
[18 (Formal)]   AtomicTypeName   ::=   QName

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.

[19 (Formal)]   ElementType   ::=   "element" ElementName? Nillable? TypeSpecifier?
[20 (Formal)]   AttributeType   ::=   "attribute" AttributeName? TypeSpecifier?
[21 (Formal)]   Nillable   ::=   "nillable"

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.

[22 (Formal)]   TypeSpecifier   ::=   TypeDerivation
|  TypeReference
[23 (Formal)]   TypeDerivation   ::=   Derivation? Mixed? "{" Type? "}"
[24 (Formal)]   TypeReference   ::=   <"of" "type"> TypeName
[25 (Formal)]   Derivation   ::=   ("restricts" TypeName)
|  ("extends" TypeName)
[26 (Formal)]   Mixed   ::=   "mixed"

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 t1 & t2 matches any sequence that is an interleaving of a sequence that matches t1 and a sequence that matches t2. 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.

[27 (Formal)]   Definition   ::=   (<"define" "element"> ElementName Substitution? Nillable? TypeSpecifier)
|  (<"define" "attribute"> AttributeName TypeSpecifier)
|  (<"define" "type"> TypeName TypeDerivation)
[28 (Formal)]   Substitution   ::=   <"substitutes" "for"> ElementName

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.

[29 (Formal)]   SimpleType   ::=   AtomicTypeName
|  (SimpleType Occurrence)
|  (SimpleType "|" SimpleType)
|  ("(" ")")
|  "none"

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.

[30 (Formal)]   AttributeAll   ::=   AttributeType
|  (AttributeType "?")
|  (AttributeAll "&" AttributeAll)
|  ("(" ")")
[31 (Formal)]   ElementAll   ::=   ElementType
|  (ElementType "?")
|  (ElementAll "&" ElementAll)
|  ("(" ")")
|  "none"
[32 (Formal)]   ElementNoAll   ::=   ElementType
|  "text"
|  (ElementType Occurrence)
|  (ElementAll "," ElementAll)
|  (ElementAll "|" ElementAll)
|  ("(" ")")
[130 (Formal)]   ElementContent   ::=   "ElementContent"
[33 (Formal)]   ElementBody   ::=   AttributeAll "ElementContent"

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

A number of auxiliary judgment that specify part of the semantics of Schema are defined. Those judgments are used in the rest of the section, but are not used directly used from other parts of the formal semantics.

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

Notation

The judgment

TypeName derives from TypeName

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

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.


statEnv |- TypeName derives from TypeName

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

statEnv.typeDefn(TypeName) => define type TypeName extends BaseTypeName Mixed? { Type? }

statEnv |- TypeName derives from BaseTypeName

statEnv.typeDefn(TypeName) => define type TypeName restricts BaseTypeName Mixed? { Type? }

statEnv |- TypeName derives from BaseTypeName

Derivation is transitive.

statEnv |- TypeName1 derives from TypeName2      statEnv |- TypeName2 derives from TypeName3

statEnv |- TypeName1 derives from TypeName3

3.2.1.2 Substitutes

Notation

The judgment

ElementName substitutes for ElementName

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

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

This judgment is specified by the following rules.

Every element name substitutes for itself.


statEnv |- ElementName substitutes for ElementName

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

statEnv.elemDecl(ElementName) => define element ElementName substitutes for BaseElementName Nillable? TypeSpecifier

statEnv |- ElementName substitutes for BaseElementName

Substitution is transitive.

statEnv |- ElementName1 substitutes for ElementName2      statEnv |- ElementName1 substitutes for ElementName3

statEnv |- ElementName1 substitutes for ElementName3

3.2.2 Extension

Notation

The judgment

Type1 extended by Type2 is Type

holds when the result of extending Type1 by Type2 is Type.

Semantics

This judgment is specified by the following rules.

statEnv |- Type1 = AttributeAll1 , ElementContent1      statEnv |- Type2 = AttributeAll2 , ElementContent2

statEnv |- Type1 extended by Type2 is (AttributeAll1 & AttributeAll2) , ElementContent1 , ElementContent2

3.2.3 Mixed content

Notation

The judgment

Type1 mixes to Type2

holds when the result of creating a mixed content from Type1 is Type2.

Semantics

This judgment is specified by the following rules.

statEnv |- Type = AttributeAll , ElementContent

statEnv |- Type mixes to AttributeAll , ( ElementContent & text* )

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

Mixed? Type1 adjusts to Type2

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.

statEnv |- Type mixes to Type'
statEnv |- Type' extended by BuiltInAttributes is Type''

statEnv |- mixed Type adjusts to Type''

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

statEnv |- Type extended by BuiltInAttributes is Type'

statEnv |- Type adjusts to Type'

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

3.2.5 Resolution

Notation

The judgment

TypeSpecifier resolves to TypeName { Type }

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.

statEnv |- Derivation? Mixed? { () } resolves to TypeName { Type }

statEnv |- Derivation? Mixed? { } resolves to TypeName { 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.

statEnv.typeDefn(TypeName) => define type TypeName TypeDerivation
statEnv |- TypeDerivation resolves to BaseTypeName { Type }

statEnv |- of type TypeName resolves to TypeName { 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.

statEnv |- Mixed? Type adjusts to AdjustedType

statEnv |- restricts TypeName Mixed? { Type } resolves to TypeName { AdjustedType }

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.

statEnv.typeDefn(TypeName) => define type TypeName Derivation? BaseMixed? { BaseType? }
statEnv |- BaseType? extended by Type is ExtendedType
statEnv |- Mixed? ExtendedType adjusts to AdjustedType

statEnv |- extends TypeName Mixed? { Type } resolves to TypeName { AdjustedType }

3.2.6 Derives

Notation

The judgment

TypeSpecifier derives from TypeSpecifier'

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.

statEnv |- TypeSpecifier resolves to TypeName { Type }      statEnv |- TypeName derives from TypeName'

statEnv |- TypeSpecifier derives from of type TypeName'

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

ElementName lookup ElementType yields Nillable? TypeSpecifier

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.

statEnv |- ElementName substitutes for ElementName'
statEnv.elemDecl(ElementName) => define element ElementName Substitution? Nillable? TypeSpecifier

statEnv |- ElementName lookup element ElementName' yields Nillable? TypeSpecifier

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.


statEnv |- ElementName lookup element ElementName Nillable? TypeSpecifier yields Nillable? TypeSpecifier

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


statEnv |- ElementName lookup element TypeSpecifier yields TypeSpecifier

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


statEnv |- ElementName lookup element yields of type xs:anyType

Notation

The judgment

AttributeName lookup AttributeType yields TypeSpecifier

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.

statEnv.attrDecl(AttributeName) => define attribute AttributeName TypeSpecifier

statEnv |- AttributeName lookup attribute AttributeName yields TypeSpecifier

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.


statEnv |- AttributeName lookup attribute AttributeName TypeSpecifier yields TypeSpecifier

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


statEnv |- AttributeName lookup attribute TypeSpecifier yields TypeSpecifier

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


statEnv |- AttributeName lookup attribute yields of type xs:anySimpleType

3.2.8 Interleaving

Notation

The judgment

Value1 interleave Value2 yields Value

holds if some interleaving of Value1 and Value2 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.


statEnv |- () interleave () yields ()

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

statEnv |- Value1 interleave Value2 yields Value

statEnv |- Item,Value1 interleave Value2 yields Item,Value

statEnv |- Value1 interleave Value2 yields Value

statEnv |- Value1 interleave Item,Value2 yields Item,Value

3.2.9 Filtering

Notation

The judgment

Value filter @QName => ()

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

Value filter @QName => SimpleValue

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

Value filter @QName => () or SimpleValue

holds if either of the previous two judgments hold.

Semantics

These judgments are defined using the auxiliary judgments

dynEnv |- Value on Axis => Value'

and

dynEnv |- Value on PrincipalNodeKind, NodeTest => Value'

which are defined in [5.2.1 Steps].

The filter judgments are defined as follows.

dynEnv |- Value on attribute:: => Value'
dynEnv |- Value' on "attribute", QName => ()

dynEnv |- Value filter @QName => ()

dynEnv |- Value on attribute:: => Value'
dynEnv |- Value' on "attribute",QName => Value''
Value'' = attribute QName { SimpleValue }

dynEnv |- Value filter @QName => SimpleValue

3.3 Matching

Introduction

The semantics of a type is given by the notion of matching, I.e., the set of all values which match that type. A tree in the [XQuery 1.0 and XPath 2.0 Data Model] matches a type in the [XPath/XQuery] type system, if and only if:

  • It verifies the structural constraints described by the type. For instance, the data model value:

      element bib:pubdate { 1954, 1966, 1974, 1986 }
    

    matches the following type:

      element { attribute country { xs:string }?, xs:integer* }
    

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

  • It verifies the name constraints described by the type. For instance, the data model value:

      element bib:pubdate of type xs:anyType { 1954, 1966, 1974, 1986 }
    

    does not match the following type:

      element of type PublicationInfo
      define type PublicationInfo { attribute country { xs:string }?, xs:integer* }
    

    because the element in the data model is annotated with the type name xs:anyType while the schema expects an element annotated with the type name PublicationInfo.

3.3.1 Nil-matches

Notation

The judgment

Value nil-matches Nillable? Type

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.

statEnv |- Value filter @xsi:nil => ()
statEnv |- Value matches Type

statEnv |- Value nil-matches Type

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

statEnv |- Value filter @xsi:nil => () or false
statEnv |- Value matches Type

statEnv |- Value nil-matches nillable 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.

statEnv |- Value filter @xsi:nil => true
statEnv |- Value matches AttributeAll

statEnv |- Value nil-matches nillable (AttributeAll, ElementContent)

3.3.2 Matches

Notation

The judgment

Value matches Type

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.


statEnv |- () matches ()

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

statEnv |- Value1 matches Type1
statEnv |- Value2 matches Type2

statEnv |- Value1,Value2 matches Type1,Type2

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

statEnv |- Value matches Type1

statEnv |- Value matches Type1|Type2

statEnv |- Value matches Type2

statEnv |- Value matches Type1|Type2

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

statEnv |- Value1 matches Type1
statEnv |- Value2 matches Type2
statEnv |- Value1 interleave Value2 yields Value

statEnv |- Value matches Type1 & Type2

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

statEnv |- Value matches (Type | ())

statEnv |- Value matches Type?

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


statEnv |- () matches Type*

statEnv |- Value1 matches Type      statEnv |- Value2 matches Type*

statEnv |- Value1, Value2 matches Type*

statEnv |- Value1 matches Type      statEnv |- Value2 matches Type*

statEnv |- Value1, Value2 matches 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, and the element value matches the enclosed type of the resolved type.

statEnv |- ElementName lookup ElementType yields Nillable? TypeSpecifier
statEnv |- TypeSpecifier resolves to TypeName' { Type }
statEnv |- TypeName derives from TypeName'
statEnv |- Value nil-matches Nillable? Type

statEnv |- element ElementName of type TypeName { Value } matches ElementType

The rule for attributes is similar.

statEnv |- AttributeName lookup AttributeType yields TypeSpecifier
statEnv |- TypeSpecifier resolves to TypeName' { Type }
statEnv |- TypeName derives from TypeName'
statEnv |- Value nil-matches Nillable? Type

statEnv |- attribute AttributeName of type TypeName { Value } matches AttributeType

A document node matches the corresponding document type.

statEnv |- Value matches Type

statEnv |- document { Value } matches document { Type }

A text node matches text.


statEnv |- text { String } 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.

statEnv |- AtomicType derives from AtomicType'

statEnv |- AtomicValue of type AtomicType matches AtomicType'

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


statEnv |- AtomicValue of type xs:anySimpleType matches untyped

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.

statEnv |- ElementName lookup ElementType yields Nillable? TypeSpecifier
statEnv |- TypeSpecifier resolves to TypeName' { Type }
statEnv |- TypeName derives from TypeName'
statEnv |- Value nil-matches Nillable? Type

statEnv |- element ElementName of type TypeName { Value } matches ElementType

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

statEnv |- ElementName lookup ElementType yields Nillable? of type TypeName'
statEnv |- TypeName derives from TypeName'
statEnv |- Value filter @xsi:nil => () or false

statEnv |- element ElementName of type TypeName { Value } matches ElementType

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 Erase and Annotate

Erase and annotate define the core of XML Schema validation. They are used to define (partially) the semantics of the validate operation in [XPath/XQuery].

3.4.1 Erasure

3.4.1.1 Simply erases

Notation

To define erasure, an auxiliary judgment is needed. The judgment

SimpleValue simply erases to String

holds when SimpleValue erases to the string String.

Semantics

This judgment is specified by the following rules.

The empty sequence erases to the empty string.

The concatenation of two non-empty sequences of values erases to the concatenation of their erasures with a separating space.

statEnv |- SimpleValue1 simply erases to String1 SimpleValue1 != ()
statEnv |- SimpleValue2 simply erases to String2 SimpleValue2 != ()

statEnv |- SimpleValue1,SimpleValue2 simply erases to xf:concat(String1," ",String2)

An atomic value erases to its string representation.


statEnv |- AtomicValue of type AtomicType simply erases to dm:string-value(AtomicValue)

3.4.1.2 Erases

Notation

The judgment

Value erases to Value'

holds when the erasure of Value is Value'.

Semantics

This judgment is specified by the following rules.

The empty sequence erases to itself.


statEnv |- () erases to ()

The erasure of the concatenation of two values is the concatenation of their erasure, so long as neither of the two original values is simple.

statEnv |- Value1 erases to Value1'      statEnv |- Value1 not a simple value
statEnv |- Value2 erases to Value2'      statEnv |- Value2 not a simple value

statEnv |- Value1,Value2 erases to Value1',Value2'

The erasure of an element is an element that has the same name and the type xs:anyType and the erasure of the original content.

statEnv |- Value erases to Value'

statEnv |- element ElementName of type TypeName { Value } erases to element ElementName of type xs:anyType { Value' }

The erasure of an attribute is an attribute that has the same name and the type xs:anySimpleType and the simple erasure of the original content labeled with xs:anySimpleType.

statEnv |- Value simply erases to String

statEnv |- attribute AttributeName of type TypeName { Value } erases to attribute AttributeName of type xs:anySimpleType { String of type xs:anySimpleType }

The erasure of a document is a document with the erasure of the original content.

statEnv |- Value erases to Value'

statEnv |- document { Value } erases to document { Value' }

The erasure of a text node is itself.


statEnv |- text { String } erases to text { String }

The erasure of a simple value is the corresponding text node.

statEnv |- SimpleValue simply erases to String

statEnv |- SimpleValue erases to text { String }

3.4.2 Annotate

3.4.2.1 Simply annotate

Notation

The judgment

simply annotate as SimpleType ( SimpleValue ) => SimpleValue'

holds if the result of casting the SimpleValue to SimpleType is SimpleValue'.

Ed. Note: Issue: The simply annotate judgment is used to describe the behavior of validation of simple values. This operation is essentially similar to casting from string to an atomic value. It is not clear if this actually aligns to the behavior of casting as specified by the [XQuery 1.0 and XPath 2.0 Functions and Operators]. See [Issue-0156:  Casting and validation].

Semantics

This judgment is specified by the following rules.

Simply annotating a simple value to a union type yields the result of simply annotating the simple value to either the first or second type in the union. Note that simply annotating to the second type is attempted only if simply annotating to the first type fails.

statEnv |- simply annotate as SimpleType1 (SimpleValue) => SimpleValue'

statEnv |- simply annotate as SimpleType1|SimpleType2 (SimpleValue) => SimpleValue'

statEnv |- (simply annotate as SimpleType1 (SimpleValue) => SimpleValue') fails
statEnv |- simply annotate as SimpleType2 (SimpleValue) => SimpleValue'

statEnv |- simply annotate as SimpleType1|SimpleType2 (SimpleValue) => SimpleValue'

The simple annotation rules for ?, +, *, and none are similar.


statEnv |- simply annotate as SimpleType1? ( () ) => ()

statEnv |- simply annotate as SimpleType (SimpleValue) => SimpleValue'

statEnv |- simply annotate as SimpleType? (SimpleValue) => SimpleValue'


statEnv |- simply annotate as SimpleType* ( () ) => ()

statEnv |- simply annotate as SimpleType (SimpleValue1) => SimpleValue1'      statEnv |- simply annotate as SimpleType* (SimpleValue2) => SimpleValue2'

statEnv |- simply annotate as SimpleType* (SimpleValue1,SimpleValue2) => SimpleValue1',SimpleValue2'

statEnv |- simply annotate as SimpleType (SimpleValue1) => SimpleValue1'      statEnv |- simply annotate as SimpleType* (SimpleValue2) => SimpleValue2'

statEnv |- simply annotate as SimpleType+ (SimpleValue1,SimpleValue2) => SimpleValue1',SimpleValue2'

Simply annotating an atomic value to xs:string yields its string representation.


statEnv |- simply annotate as xs:string (AtomicValue) => dm:string-value(AtomicValue)

Simply annotating an atomic value to xs:decimal yields the decimal that results from parsing its string representation.

Similar rules are assumed for the rest of the 19 XML Schema primitive types.

3.4.2.2 Nil-annotate

Notation

The judgment

nil-annotate as Nillable? Type ( Value ) => Value'

holds if it is possible to annotate value Value as if it had the nillable type Type and Value' is the corresponding annotated value.

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 it must be possible to annotate value Value as if it had the type Type.

statEnv |- Value filter @xsi:nil => ()
statEnv |- annotate as Type ( Value ) => Value'

statEnv |- nil-annotate as Type ( Value ) => Value'

If the type is nillable, and the xsi:nil attribute does not appear or is false, then it must be possible to annotate value Value as if it had the type Type.

statEnv |- Value filter @xsi:nil => () or false
statEnv |- annotate as Type ( Value ) => Value'

statEnv |- nil-annotate as nillable Type ( Value ) => Value'

If the type is nillable, and the xsi:nil attribute is true, then it must be possible to annotate value Value as if it had a type where the attributes in the type are kept and the element content of the type is ignored.

statEnv |- Value filter @xsi:nil => true
statEnv |- annotate as AttributeAll ( Value ) => Value'

statEnv |- nil-annotate as nillable (AttributeAll, ElementContent) ( Value ) => Value'

3.4.2.3 Annotate

Notation

The judgment

annotate as Type ( Value ) => Value'

holds if it is possible to annotate value Value as if it had type Type and Value' is the corresponding annotated value.

Note

Assume an XML Infoset instance X is validated against an XML Schema S, yielding PSVI instance X'. Then if X corresponds to Value and S corresponds to Type and X' corresponds to Value', the following should hold: annotate as Type ( Value ) => Value'.

Semantics

This judgment is specified by the following rules.

Annotating the empty sequence as the empty type yields the empty sequence.


statEnv |- annotate as () (()) => ()

Annotating a concatenation of values as a concatenation of types yields the concatenation of the annotated values.

statEnv |- annotate as Type1 (Value1) => Value1'
statEnv |- annotate as Type2 (Value2) => Value2'

statEnv |- annotate as Type1,Type2 (Value1,Value2) => Value1',Value2'

Annotating a value as a choice type yields the result of annotating the value as either the first or second type in the choice.

statEnv |- annotate as Type1 (Value) => Value'

statEnv |- annotate as Type1|Type2 (Value) => Value'

statEnv |- annotate as Type2 (Value) => Value'

statEnv |- annotate as Type1|Type2 (Value) => Value'

Annotating a value as an all group uses interleaving to decompose the original value and recompose the annotated value.

Ed. Note: Jerome and Phil: Note that this may reorder the original sequence. Perhaps we should disallow such reordering. Specifying that formally is not as easy as we would like.

statEnv |- annotate as Type1 ( Value1 ) => Value1'
statEnv |- annotate as Type2 ( Value2 ) => Value2'
statEnv |- Value1 interleave Value2 yields Value
statEnv |- Value1' interleave Value2' yields Value'

statEnv |- annotate as Type1 & Type2 ( Value ) => Value'

The annotation rules for ?, +, *, none are similar.

statEnv |- annotate as (Type | ())(Value) => Value'

statEnv |- annotate as Type? (Value) => Value'

statEnv |- annotate as Type (Value1) => Value1'      statEnv |- annotate as Type* (Value2) => Value2'

statEnv |- annotate as Type+ (Value1,Value2) => (Value1',Value2')


statEnv |- annotate as Type* ( () ) => ()

statEnv |- annotate as Type (Value1) => Value1'      statEnv |- annotate as Type* (Value2) => Value2'

statEnv |- annotate as Type* (Value1,Value2) => (Value1',Value2')

To annotate an element with no xsi:type attribute, first look up the the element type, next resolve the resulting type specifier, then annotate the value against the resolved type, and finally return a new element with the name of the original element, the resolved type name, and the annotated value.

statEnv |- Value filter @xsi:type => ()
statEnv |- ElementName lookup ElementType yields Nillable? TypeSpecifier
statEnv |- TypeSpecifier resolves to TypeName { Type }
statEnv |- nil-annotate as Type Nillable? (Value) => Value'

statEnv |- annotate as ElementType ( element ElementName of type xs:anyType { Value } ) => element ElementName of type TypeName { Value' }

To annotate an element with an xsi:type attribute, define a type specifier corresponding to the xsi:type. Look up the element type, yielding a type specifier, and check that the xsi:type specifier derives from this type specifier. Resolve the xsi:type specifier, then annotate the value against the resolved type, and finally return a new element with the name of the original element, the resolved type name, and the annotated value.

statEnv |- Value filter @xsi:type => TypeName
statEnv |- XsiTypeSpecifier = of type TypeName
statEnv |- ElementName lookup ElementType yields Nillable? TypeSpecifier
statEnv |- XsiTypeSpecifier derives from TypeSpecifier
statEnv |- XsiTypeSpecifier resolves to TypeName { Type }
statEnv |- nil-annotate as Type Nillable? (Value) => Value'

statEnv |- annotate as ElementType ( element ElementName of type xs:anyType { Value } ) => element ElementName of type TypeName { Value' }

Ed. Note: Issue: the treatment of xsi:type in the [XQuery 1.0: A Query Language for XML] document and in the formal semantics document still differ. See [Issue-0142:  Treatment of xsi:type in validation].

The rule for attributes is similar to the first rule for elements.

statEnv |- AttributeName lookup AttributeType yields TypeSpecifier
statEnv |- TypeSpecifier resolves to TypeName { Type }
statEnv |- nil-annotate as Type Nillable? (Value) => Value'

statEnv |- annotate as AttributeType ( attribute AttributeName of type xs:anySimpleType { Value } ) => attribute AttributeName of type TypeName { Value' }

Annotating a document node yields a document with the annotation of its contents.

statEnv |- annotate as Type (Value) => Value'

statEnv |- annotate as document { Type } ( document { Value } ) => document { Value' }

Annotating a text node as text yields itself.


statEnv |- annotate as text (text { String }) => text { String }

Annotating a text nodes as a simple type is identical to casting.

statEnv |- simply annotate as SimpleType ( String as xs:anySimpleType ) => SimpleValue'

statEnv |- annotate as SimpleType ( text { String } ) => SimpleValue'

Annotating a simple value as a simple type is identical to casting.

statEnv |- simply annotate as SimpleType ( SimpleValue ) => SimpleValue'

statEnv |- annotate as SimpleType ( SimpleValue ) => SimpleValue'

3.5 Subtyping

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.

3.5.1 Subtype

Notation

The judgment

Type <: Type'

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:

statEnv |- Type <: Type     

and it is transitive: if,

statEnv |- Type1 <: Type2     

and,

statEnv |- Type2 <: Type3     

then,

statEnv |- Type1 <: Type3

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

Type1 = Type2

holds if the Type1 is equivalent to the Type2.

Semantics

By definition, Type1 = Type2 if and only if, Type1<:Type2 and Type2<: Type1.

3.6 Auxiliary typing judgments for "for", "unordered", and "sortby" expressions

This section defines the notion of Prime Type, and operations on prime types. Prime types play an important role in defining the static semantics of [XPath/XQuery], and are used notably in the semantics of "for", "unordered", and "sortby" expressions.

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.

[34 (Formal)]   PrimeType   ::=   ItemType
|  (PrimeType "|" PrimeType)

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.

Type · 0  =  ()
Type · 1  =  Type
Type · ?  =  Type?
Type · +  =  Type+
Type · *  =  Type*

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.

prime(ItemType)  =  ItemType
prime(())  =  none
prime(none)  =  none
prime(Type1 , Type2)  =  prime(Type1) | prime(Type2)
prime(Type1 & Type2)  =  prime(Type1) | prime(Type2)
prime(Type1 | Type2)  =  prime(Type1) | prime(Type2)
prime(Type?)  =  prime(Type)
prime(Type*)  =  prime(Type)
prime(Type+)  =  prime(Type)

Semantics

The quantifier function is defined by induction as follows.

quantifier(ItemType)  =  1
quantifier(())  =  0
quantifier(none)  =  0
quantifier(Type1 , Type2)  =  quantifier(Type1) , quantifier(Type2)
quantifier(Type1 & Type2)  =  quantifier(Type1) , quantifier(Type2)
quantifier(Type1 | Type2)  =  quantifier(Type1) | quantifier(Type2)
quantifier(Type?)  =  quantifier(Type) · ?
quantifier(Type*)  =  quantifier(Type) · *
quantifier(Type+)  =  quantifier(Type) · +

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

 ,  0  1  ?  +  * 
 0  0  1  ?  +  * 
 1  1  +  +  +  + 
 ?  ?  +  *  +  * 
 +  +  +  +  +  + 
 *  *  +  *  +  * 
    
 |  0  1  ?  +  * 
 0  0  ?  ?  *  * 
 1  ?  1  ?  +  * 
 ?  ?  ?  ?  *  * 
 +  *  +  *  +  * 
 *  *  *  *  *  * 
    
 ·  0  1  ?  +  * 
 0  0  0  0  0  0 
 1  0  1  ?  +  * 
 ?  0  ?  ?  *  * 
 +  0  +  *  +  * 
 *  0  *  *  *  * 

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 Auxiliary typing judgments for "typeswitch" expressions

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(PrimeType1, PrimeType2) computes the type for all the items common between the prime types PrimeType1 and PrimeType2, and combines them into a new prime type.

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

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.

statEnv |- common-prime( ItemType1, ItemType1' ) = ItemType(1,1)
statEnv |- common-prime( ItemType1, ItemType2' ) = ItemType(1,2)
···
statEnv |- common-prime( ItemTypen, ItemTyper' ) = ItemType(n,r)

statEnv |- common-prime( ( ItemType1 | ··· | ItemTypen ), ( ItemType1' | ··· | ItemTyper' ) ) = ItemType(1,1) | ··· | ItemType(n,r)

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.

statEnv |- ItemType1 <: ItemType2

statEnv |- common-prime(ItemType1, ItemType2) = ItemType1

statEnv |- ItemType2 <: ItemType1

statEnv |- common-prime(ItemType1, ItemType2) = ItemType2

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:

statEnv |- common-prime(ItemType1, ItemType2) => none

Semantics

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

 common-occurrence  0  1  ?  +  * 
 0  0  0  0  0  0 
 1  0  1  1  1  1 
 ?  0  1  ?  1  ? 
 +  0  1  1  +  + 
 *  0  1  ?  +  * 

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

3.8 Major type issues

Ed. Note: Alignment between [XPath/XQuery], the [XQuery 1.0 and XPath 2.0 Data Model], and the [XPath/XQuery] formal semantics. There are some known discrepancies between the type models in the Data Model document, the [XPath/XQuery] document and this document. Currently the [XPath/XQuery] grammar does not contain comments, processing-instructions or schema-components. Currently this document does not deal with PI and comment nodes, which are present in the Data Model. See issues [Issue-0068:  Document Collections], [Issue-0105:  Types for nodes in the data model.].

Ed. Note: Complexity of type operations. There are concerns about the complexity of type inference, notably about type subsumption used during type inference, and validation used during evaluation of some of the type operations (e.g., typeswitch). Additionally, there are many language features for which it is possible to define special type inference rules that would give tighter bounds. The question is, which features, which rules, and how do they interact with the complexity of type inference and subtype computation. See [Issue-0080:  Typing of parent], [Issue-0083:  Expressive power and complexity of typeswitch expression], [Issue-0091:  Attribute expression].

4 Basics

The organization of this section parallels the organization of Section 2 of the [XPath/XQuery] document.

4.1 Expression Context

Introduction

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

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:

statEnv.namespace

The namespace environment maps namespace prefixes (NCNames) onto namespace URIs (URIs).

The namespace environment captures in-scope namespaces in the [XPath/XQuery] static context.

statEnv.default_namespace

The default namespace environment maps "element", and "function" to a namespace URI (a URI), as determined by the appropriate namespace declaration.

The default namespace environment captures the default namespace for element and type names and Default namespace for function names in the [XPath/XQuery] static context.

statEnv.typeDefn

The type definition environment maps type names (TypeNames) onto their global type definitions (Definitions).

The type definition environment captures in-scope schema definitions in the [XPath/XQuery] static context.

statEnv.elemDecl

The element declaration environment maps element names (ElementNames) onto their global element declarations (Definitions).

The element declaration environment does not have a counterpart in the [XPath/XQuery] static context. See [Issue-0159:  Element and attribute declarations in the static context].

statEnv.attrDecl

The attribute declaration environment maps attribute names (AttributeNames) onto their global attribute declarations (Definitions).

The attribute declaration environment does not have a counterpart in the [XPath/XQuery] static context. See [Issue-0159:  Element and attribute declarations in the static context].

statEnv.varType

The variable static type environment maps variable names (Variables) to their static types (Types).

The variable static type environment captures in-scope variables in the [XPath/XQuery] static context.

statEnv.funcType

The function declaration environment stores the static type signatures of functions. Because [XPath/XQuery] allows multiple functions with the same name differing only in the number of arguments, this environment maps function name/arity (QName, integer) pairs to function type signatures define function QName (Type1, ..., Typen) return Type, where the first is the return type and the rest are the types of the parameters, in order.

The function declaration environment captures in-scope functions in the [XPath/XQuery] static context.

statEnv.base_uri

The base uri environment contains a unique namespace URI (a URI).

The base uri environment captures the base URI in the [XPath/XQuery] static context.

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 NCName1:NCName2, and if statEnv.namespace(NCName1) = URI, then the expression yields qname(URI,NCName2). If the namespace prefix NCName1 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.

statEnv [ namespace(NCName |-> URI) ] |- Expr*

statEnv |- namespace NCName = URI Expr*

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:

statEnv [ namespace = (NewEnvironment) ]

4.1.2 Evaluation Context

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

The following environments are dynamic:

dynEnv.funcDefn

The dynamic function environment maps a function name to a function definition. The function definition consists of an expression, which is the function's body, and a list of variables, which are the function's formal parameters. As with statEnv.funcType, dynEnv.funcDefn requires a function name and a parameter count: it maps a (QName, integer) pair to a value list of the form (Expr , Variable1, ..., Variablen).

dynEnv.varValue

The dynamic value environment maps a variable name (QName) onto the variable's current value (Value).

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:

Built-in Variable  Represents:
$fs:dotcontext item
$fs:positioncontext position
$fs:lastcontext size
$fs:implicitTimezoneimplicit timezone

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.2 Input Functions

[XPath/XQuery] has three functions that provide access to input data: input, collection, and document. The dynamic semantics of these three input functions are described in more detail in [XQuery 1.0 and XPath 2.0 Functions and Operators]. The static typing for these function is still an open issue (See [Issue-0137:  Typing of input functions]).

4.3 Expression Processing

This section gives background material about the [XPath/XQuery] data model. More information on the [XPath/XQuery] data model can be found in [2.3 Data Model].

4.4 Types

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.

[64 (XQuery)]   SequenceType   ::=   (ItemType OccurrenceIndicator) |  "empty"
[65 (XQuery)]   ItemType   ::=   (("element" |  "attribute") ElemOrAttrType?)
|  "node"
|  "processing-instruction"
|  "comment"
|  "text"
|  "document"
|  "item"
|  AtomicType
|  "untyped"
|  <"atomic" "value">
[66 (XQuery)]   ElemOrAttrType   ::=   (QName (SchemaType |  SchemaContext?)) |  SchemaType
[67 (XQuery)]   SchemaType   ::=   <"of" "type"> QName
[60 (XQuery)]   SchemaContext   ::=   "in" SchemaGlobalContext ("/" SchemaContextStep)*
[61 (XQuery)]   SchemaGlobalContext   ::=   QName |  ("type" QName)
[62 (XQuery)]   SchemaContextStep   ::=   QName
[68 (XQuery)]   AtomicType   ::=   QName
[69 (XQuery)]   OccurrenceIndicator   ::=   ("*" |  "+" |  "?")?

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

Core Grammar

The core grammar productions for sequence types are:

[46 (Core)]   SequenceType   ::=   (ItemType OccurrenceIndicator) |  "empty"
[47 (Core)]   ItemType   ::=   (("element" |  "attribute") ElemOrAttrType?)
|  "node"
|  "processing-instruction"
|  "comment"
|  "text"
|  "document"
|  "item"
|  AtomicType
|  "untyped"
|  <"atomic" "value">
[48 (Core)]   ElemOrAttrType   ::=   (QName (SchemaType |  SchemaContext?)) |  SchemaType
[49 (Core)]   SchemaType   ::=   <"of" "type"> QName
[42 (Core)]   SchemaContext   ::=   "in" SchemaGlobalContext ("/" SchemaContextStep)*
[43 (Core)]   SchemaGlobalContext   ::=   QName |  ("type" QName)
[44 (Core)]   SchemaContextStep   ::=   QName
[50 (Core)]   AtomicType   ::=   QName
[51 (Core)]   OccurrenceIndicator   ::=   ("*" |  "+" |  "?")?

Ed. Note: Note that normalization on SequenceTypes does not occur during the normalization phase but whenever a dynamic or static rule requires it. The reason for this deviation from the processing model is that the result of SequenceType normalization is not part of the [XPath/XQuery] syntax (See issue [Issue-0089:  Syntax for types in XQuery]). SequenceType normalization is the only occurrence of such a deviation in the formal semantics.

Notation

To define the semantics of SequenceTypes, the following auxiliary mapping rule is used.

 
[SequenceType]sequencetype
==
Type

specifies that SequenceType is mapped to Type, in the XQuery type system.

Normalization

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

 
[ItemType OccurrenceIndicator]sequencetype
==
[ItemType]sequencetype OccurrenceIndicator

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

 
[empty]sequencetype
==
[()]sequencetype

The SequenceType component with type SchemaType is mapped directly into the [XPath/XQuery] type system.

 
[element SchemaType]sequencetype
==
element SchemaType
 
[attribute SchemaType]sequencetype
==
attribute SchemaType

The mapping still does not handle SequenceTypes using SchemaContext (See [Issue-0138:  Semantics of Schema Context]). The two following rules map references to a global element or attribute, without taking the schema context into account.

 
[element QName]sequencetype
==
element QName
 
[attribute QName]sequencetype
==
attribute QName

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

 
[text]sequencetype
==
text
 
[document]sequencetype
==
document
 
[untyped]sequencetype
==
untyped
 
[AtomicType]sequencetype
==
AtomicType

Processing instruction and comment types are ignored. See [Issue-0105:  Types for nodes in the data model.].

 
[comment]sequencetype
==
 
[processing-instruction]sequencetype
==

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

 
[node]sequencetype
==
(element | attribute | text | document)
 
[item]sequencetype
==
(element | attribute | text | document | xs:string | xs:decimal | ... )
 
[atomic value]sequencetype
==
(xs:string | xs:decimal | ... )

Ed. Note: Jerome: The Formal Semantics makes use of fs:numeric which is not in XML Schema. This is necessary for the specification of some of XPath type conversion rules. See [Issue-0127:  Datatype limitations].

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

4.4.3 Type Conversions

Introduction

Some expressions do not require their operands to exactly match the expected type. For example, function parameters and returns expect a value of a particular type, but automatically perform certain type conversions, such as extraction of atomic values from nodes, promotion of numeric values, and implicit casting of untyped values. The conversion rules for function parameters and returns are discussed in [5.1.4 Function Calls]. Other operators that provide special conversion rules include arithmetic operators, which are discussed in [5.4 Arithmetic Expressions], and value comparisons, which are discussed in [5.5.1 Value Comparisons].

Some special conversion rules: atomization, effective boolean value, and fallback conversions, are used in several places in the language.

4.4.3.1 Atomization

Notation

There are two variants of the normalization function []Atomize.

The first variant, []Atomize is not parameterized by the required type of the expression.

The second variant, []Atomize(Type), is parameterized by the required type.

Both functions convert an expression into an expression that returns an optional atomic value and is used in the normalization of expressions whose required type is an optional atomic value.

Normalization

A node is converted to an optional atomic value by extracting its typed content.

 
[Expr]Atomize
==
typeswitch (Expr)
case atomic value? $v return $v
case node $v return
   (typeswitch (xf:data($v))
     case atomic value? $w return $w
     default $w return xf:error()
default $v return xf:error()

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

 
[Expr]Atomize(Type)
==
typeswitch (Expr)
case untyped $v return cast as Type ($v)
case atomic value? $v return $v
case node $v return
   (typeswitch (xf:data($v))
     case untyped $w return cast as Type ($w)
     case atomic value? $w return $w
     default $w return [$w]Type_Exception(Type))
default $v return [$v]Type_Exception(Type)

Ed. Note: Issue:Don Chamberlin indicates that this rule should do type promotion. See [Issue-0161:  Type promotion in Atomization].

Notation

The following normalization rule implements type exceptions: []Type_Exception(Type).

Normalization

There are two definitions for each of these functions.

The definition here implements the strict type exception policy. The strict policy always raises an error:

 
[Expr]Type_Exception(Type)
==
xf:error()

The flexible type exception policy is defined in [4.4.3.3 Fallback Conversion].

4.4.3.2 Effective Boolean Value

Notation

The function []Effective_Boolean_Value takes an expression and normalizes it into an effective boolean value.

Normalization

The effective boolean value is obtained through the following normalization rule. Note that the default clause returns true is at least one item in the sequence is a node, otherwise, it raises a type exception.

 
[Expr]Effective_Boolean_Value
==
typeswitch (Expr)
case empty $v return xf:false()
case xs:boolean $v return $v
default $v return if (length([$v/self::node()]Expr) ge 1) then xf:true() else [$v]Type_Exception(xs:boolean)
4.4.3.3 Fallback Conversion

Normalization

The following rules define the "fallback conversions" that support the "flexible" type-exception policy. These rules depend on the required type for the expression that is being normalized.

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

 
[Expr]Type_Exception(xs:boolean)
==
typeswitch (Expr)
case empty $v return xf:false()
default $v return
   if (xf:count([$v/self::node()]Expr) >= 1) then xf:true()
   else xf:boolean(op:item-at($v, 1))

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

In the next rule, the required type is "node". The conditional expression in the "default return" clause below guarantees that, if the first item is a node, then it returns the node, otherwise it returns an error.

 
[Expr]Type_Exception(node)
==
typeswitch (Expr)
   case empty $v return xf:error()
   default $v return
     (typeswitch (op:item-at($v, 1))
       case node $w return $w
       default $w return xf:error())

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

4.5 Errors and Conformance

This section describes error handling and conformance levels.

Ed. Note: Issue: Error handling is not formally specified. See [Issue-0094:  Static type errors and warnings]

Ed. Note: Issue: Conformance levels are not formally specified. See [Issue-0169:  Conformance Levels]

5 Expressions

This section gives the semantics of all the [XPath/XQuery] expressions. The organization of this section parallels the organization of Section 3 of the [XPath/XQuery] document.

[5 (XQuery)]   Expr   ::=   SortExpr
[10 (XPath)]   Expr   ::=   OrExpr

For each expression, a short description and the relevant grammar productions are given. The semantics of an expression includes the normalization, static analysis, and dynamic evaluation phases. Recall that normalization rules translate [XPath/XQuery] syntax into core [XPath/XQuery] syntax. In the sections that contain normalization rules, the Core grammar productions into which the expression is normalized are also provided. After normalization, sections on static type inference and dynamic evaluation define the static type and dynamic value for the core expression.

Core Grammar

The core grammar production for expressions is:

[5 (Core)]   Expr   ::=   SortExpr

5.1 Primary Expressions

Primary expressions are the basic primitives of the language.They include literals, variables, function calls, and the use of parentheses to control precedence of operators.

[39 (XQuery)]   PrimaryExpr   ::=   Literal |  FunctionCall |  ("$" VarName) |  ParenthesizedExpr
[227 (XQuery)]   VarName   ::=   QName

Core Grammar

The core grammar productions for primary expressions are:

[24 (Core)]   PrimaryExpr   ::=   Literal |  FunctionCall |  ("$" VarName) |  ParenthesizedExpr
[169 (Core)]   VarName   ::=   QName

5.1.1 Literals

Introduction

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

[56 (XQuery)]   Literal   ::=   NumericLiteral |  StringLiteral
[55 (XQuery)]   NumericLiteral   ::=   IntegerLiteral |  DecimalLiteral |  DoubleLiteral
[193 (XQuery)]   IntegerLiteral   ::=   Digits
[194 (XQuery)]   DecimalLiteral   ::=   ("." Digits) |  (Digits "." [0-9]*)
[195 (XQuery)]   DoubleLiteral   ::=   (("." Digits) |  (Digits ("." [0-9]*)?)) ([e] | [E]) ([+] | [-])? Digits
[214 (XQuery)]   StringLiteral   ::=   (["] ((" ") |  [^"])* ["]) |  (['] ((' ') |  [^'])* ['])

Normalization

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

Core Grammar

The core grammar productions for literals are:

[38 (Core)]   Literal   ::=   NumericLiteral |  StringLiteral
[37 (Core)]   NumericLiteral   ::=   IntegerLiteral |  DecimalLiteral |  DoubleLiteral
[138 (Core)]   IntegerLiteral   ::=   Digits
[139 (Core)]   DecimalLiteral   ::=   ("." Digits) |  (Digits "." [0-9]*)
[140 (Core)]   DoubleLiteral   ::=   (("." Digits) |  (Digits ("." [0-9]*)?)) ([e] | [E]) ([+] | [-])? Digits
[158 (Core)]   StringLiteral   ::=   (["] ((" ") |  [^"])* ["]) |  (['] ((' ') |  [^'])* ['])

Static Type Analysis

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


statEnv |- IntegerLiteral : xs:integer

Dynamic Evaluation

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


dynEnv |- IntegerLiteral => dm:atomic-value(IntegerLiteral, xs:integer)

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

Static Type Analysis


statEnv |- DecimalLiteral : xs:decimal

Dynamic Evaluation


dynEnv |- DecimalLiteral => dm:atomic-value(DecimalLiteral, xs:decimal)

Static Type Analysis


statEnv |- DoubleLiteral : xs:double

Dynamic Evaluation


dynEnv |- DoubleLiteral => dm:atomic-value(DoubleLiteral, xs:double)

Static Type Analysis


statEnv |- StringLiteral : xs:string

Dynamic Evaluation


dynEnv |- StringLiteral => dm:atomic-value(StringLiteral, xs:string)

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

5.1.2 Variables

Introduction

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

Normalization

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

Static Type Analysis

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

statEnv.varType(Variable) = Type

statEnv |- Variable : Type

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

Dynamic Evaluation

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

dynEnv.varValue(Variable) = Value

dynEnv |- Variable => Value

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

5.1.3 Parenthesized Expressions

[57 (XQuery)]   ParenthesizedExpr   ::=   "(" ExprSequence? ")"

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

Core Grammar

The core grammar production for parenthesized expressions is:

[39 (Core)]   ParenthesizedExpr   ::=   "(" ExprSequence? ")"

5.1.4 Function Calls

Introduction

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

[58 (XQuery)]   FunctionCall   ::=   <QName "("> (Expr ("," Expr)*)? ")"

Because [XPath/XQuery] perform implicit operations when doing function calls, a normalization step is required.

Notation

Normalization of function calls uses an auxiliary mapping rule, []FormalArgument, used to map the formal arguments of a function call.

There are three variants of this mapping rule. If the required type of the formal argument is an optional atomic type, the following rule is applied: (Type is the required atomic type.)

 
[Expr]FormalArgument
==
[Expr]Atomize(Type)

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

 
[Expr]FormalArgument
==
for $x in (Expr) return
typeswitch ($x)
   case node $v return data($v)
   default $v return $v

Ed. Note: Jerome: it is not clear whether the above rule is correct. At least type promotion seems to be implied by the corresponding description in the [XPath/XQuery] document. See .

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

 
[Expr]FormalArgument
==
[Expr]Expr

Normalization

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

 
[ QName (Expr1, ..., Exprn) ]Expr
==
[[QName] ( [[Expr1 ]Expr]FormalArgument, ..., [[ Exprn ]Expr]FormalArgument)]FormalArgument

Note that this normalization rule depends on the static environment containing function signatures and is the only place where we exploit the implicit presence of statEnv.

Core Grammar

The core grammar production for function calls is:

[40 (Core)]   FunctionCall   ::=   <QName "("> (Expr ("," Expr)*)? ")"

Static Type Analysis

Based on the function's name and number of arguments (and in the case of built-in functions based also on the type of its arguments), the function signature is retrieved from the static environment. If the function is not present in the environment, an error is raised. The type of each actual argument to the function must be a subtype of the corresponding formal argument to the function, i.e., it is not necessary that the actual and formal types be the same.

Ed. Note: Issue: Michael Rys points out there is a dependency between normalization (which requires the function signature) and the fact that built-in functions may be overloaded for various types. See [Issue-0140:  Dependency in normalization and function resolution]

statEnv |- QName => qname
statEnv.funcType(qname, n) = define function qname(Type1, ..., Typen) returns Type
statEnv |- Expr1 : Type1'     Type1' <: Type1
...
statEnv |- Exprn : Typen'     Typen' <: Typen

statEnv |- QName (Expr1, ..., Exprn) : Type

Dynamic Evaluation

Based on the function's name and the number of arguments (and in the case of built-in functions based also based on the type of its arguments), the function body is retrieved from the dynamic environment. If the function is not present in the environment, an error is raised. The rule first evaluates each function argument, then extends dynEnv.varValue by binding each formal variable to its corresponding value, and then evaluates the body of the function in the new environment. The resulting value is the value of the function call.

dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
dynEnv |- QName => qname
statEnv.funcType(qname, n) = define function qname(Type1, ..., Typen) returns Type
statEnv |- Value1 matches Type1 ..., Valuen matches Typen
dynEnv.funcDefn(qname, n) = (Expr, Variable1, ... , Variablen)
dynEnv [ varValue = (Variable1 |-> Value1;...; Variablen |-> Valuen) ] |- Expr => Value
statEnv |- Value matches Type

dynEnv |- QName ( Expr1, ..., Exprn ) => Value

Note that the function body is evaluated in the default environment. Note also that input values and output values are matched against the types declared for the function. If static analysis was performed, all these checks are guaranteed to be true and may be omitted.

Ed. Note: This only describes the semantics of user defined functions. The semantics of built-in functions is still an open issue. See [Issue-0122:  Overloaded functions] and [Issue-0162:  How to describe the semantics of built-in functions].

5.1.5 Comments

[94 (XQuery)]   ExprComment   ::=   "{--" [^}]* "--}"

Comments are lexical constructs only, and have no meaning within the query and therefore have no Formal Semantics.

5.2 Path Expressions

Introduction

Path expressions are used to locate nodes within a tree. There are two kinds of path expressions, absolute path expressions and relative path expressions. An absolute path expression is a rooted relative path expression. A relative path expression is composed of a sequence of steps.

[23 (XQuery)]   PathExpr   ::=   ("/" RelativePathExpr?) |  ("//" RelativePathExpr) |  RelativePathExpr
[24 (XQuery)]   RelativePathExpr   ::=   StepExpr (("/" |  "//") StepExpr)*

Core Grammar

The core grammars productions for path expressions are:

[13 (Core)]   PathExpr   ::=   RelativePathExpr
[14 (Core)]   RelativePathExpr   ::=   StepExpr

Notation

To define the semantics of relative path expressions, the auxiliary mapping rule is used: [RelativePathExpr]Path.

Normalization

Absolute path expressions are path expressions starting with the / symbol, indicating that the expression must be applied on the root node in the current context. Remember that the root node in the current context is the topmost ancestor of the context node. The following two rules are used to normalize absolute path expressions to relative ones, and rely on the use of the xf:root() function, which computes the document node from the context node.

 
["/"]Expr
==
xf:root( $fs:dot )
 
["/" RelativePathExpr]Expr
==
fs:distinct-doc-order( [xf:root( $fs:dot ) "/" RelativePathExpr]Path )

Ed. Note: Some of the semantics of the root expression '/' are still undefined. For instance, what should the semantics of '/' be in case of a document fragment (e.g., created using XQuery element constructor). See [Issue-0123:  Semantics of /].

Ed. Note: [Kristoffer/XSL] Also the context node and document order are not defined when it is a context item).

In general, a path expression always returns a sequence in document order. The complete normalization of a Path expression is obtained by applying the Path normalization and then sorting the result in document order and removing duplicates.

 
[RelativePathExpr]Expr
==
fs:distinct-doc-order( [RelativePathExpr]Path )

Ed. Note: Jerome: the restriction that XPath expressions operate on nodes here seems too strict and is still an open issue. See [Issue-0125:  Operations on node only in XPath].

A composite relative path expression (using /) is normalized into a for expression by concatenating the sequences obtained by mapping each node of the left-hand side in document order to the sequence it generates on the right-hand side; the encapsulating call of the fs:distinct-doc-order function then ensures that the result is in document order without duplicates. The evaluation context is carefully set up (using two bindings of the $fs:last semantic variable).

 
[StepExpr "/" RelativePathExpr ]Path
==
let $fs:sequence := fs:distinct-doc-order( [StepExpr]Path ) return
  let $fs:last := xf:count($fs:sequence) return
    for $fs:dot in $fs:sequence return
      let $fs:position := op:index-of($fs:sequence, $fs:dot) return
          [RelativePathExpr]Path

Ed. Note: [Kristoffer/XSL] We have defined normalization over a right recursive variant of the syntax production -- this should perhaps be explained more elaborately.

5.2.1 Steps

Introduction

[25 (XQuery)]   StepExpr   ::=   (ForwardStep |  ReverseStep |  PrimaryExpr) Predicates
[50 (XQuery)]   ForwardStep   ::=   (ForwardAxis NodeTest) |  AbbreviatedForwardStep
[51 (XQuery)]   ReverseStep   ::=   (ReverseAxis NodeTest) |  AbbreviatedReverseStep
[54 (XQuery)]   Predicates   ::=   ("[" Expr "]")*

Core Grammar

The core grammars productions for XPath steps are:

[15 (Core)]   StepExpr   ::=   ForwardStep |  ReverseStep |  PrimaryExpr
[35 (Core)]   ForwardStep   ::=   ForwardAxis NodeTest
[36 (Core)]   ReverseStep   ::=   ReverseAxis NodeTest

Notation

Step expressions can be followed by predicates. Normalization of predicates uses the following auxiliary mapping rule: []Predicates.

Normalization

Normalization of predicates need to distinguish between forward and reverse axes.

As explained in the [XPath/XQuery] document, applying a step in XPath changes the focus (or context). The change of focus is made explicit by the normalization rule below, which binds the variable $fs:dot to the node currently being processed, and the variable $fs:position to the position (i.e., the position within the input sequence) of that node. Notice that the expression does not reorder the sequences obtained by evaluating the subexpressions: if they are RelativePathExprs then the contained path normalization will insert fs:distinct-doc-order appropriately.

 
[ForwardStep Predicates "[" Expr "]"]Path
==
let $fs:sequence := [ForwardStep Predicates]Path return
  let $fs:last := xf:count($fs:sequence) return
    for $fs:position in op:to(1, $fs:last) return
        let $fs:dot := op:item-at($fs:sequence, $fs:position) return
           if [Expr]Predicates then $fs:dot else ()
 
[ReverseStep Predicates "[" Expr "]"]Path
==
let $fs:sequence := [ReverseStep Predicates]Path return
  let $fs:last := xf:count($fs:sequence) return
    for $fs:position in op:to($fs:last,1) return
      let $fs:dot := op:item-at($fs:sequence, $fs:position) return
         if [Expr]Predicates then $fs:dot else ()

The []Predicates function is specified in [5.2.2 Predicates].

Ed. Note: Issue:These rules use the function xf:index-of to bind the position of a node in a sequence. This works since path expressions only work on nodes. See [Issue-0125:  Operations on node only in XPath]. Still, it might be preferable to be able to bind both the current node and its position through a single processing of the collection within the for expression. The FS editors have made several syntax proposals for such an operation. For instance: for $v at $i in E1 return E2. See [Issue-0124:  Binding position in FLWR expressions].

Ed. Note: Issue:The semantics of Predicates applied on primary expression is not specified. See [Issue-0163:  Normalization of XPath predicates]

5.2.1.1 Axes

Introduction

[40 (XQuery)]   ForwardAxis   ::=   <"child" "::">
|  <"descendant" "::">
|  <"attribute" "::">
|  <"self" "::">
|  <"descendant-or-self" "::">
[41 (XQuery)]   ReverseAxis   ::=   <"parent" "::">
[36 (XPath)]   ForwardAxis   ::=   <"child" "::">
|  <"descendant" "::">
|  <"attribute" "::">
|  <"self" "::">
|  <"descendant-or-self" "::">
|  <"following-sibling" "::">
|  <"following" "::">
|  <"namespace" "::">
[37 (XPath)]   ReverseAxis   ::=   <"parent" "::">
|  <"ancestor" "::">
|  <"preceding-sibling" "::">
|  <"preceding" "::">
|  <"ancestor-or-self" "::">

Core Grammar

The core grammars productions for XPath axis are:

[25 (Core)]   ForwardAxis   ::=   <"child" "::">
|  <"descendant" "::">
|  <"attribute" "::">
|  <"self" "::">
|  <"descendant-or-self" "::">
|  <"following-sibling" "::">
|  <"following" "::">
|  <"namespace" "::">
[26 (Core)]   ReverseAxis   ::=   <"parent" "::">
|  <"ancestor" "::">
|  <"preceding-sibling" "::">
|  <"preceding" "::">
|  <"ancestor-or-self" "::">

Notation

Some auxiliary grammar productions and judgments are introduced to structure the semantic rules for axes and node tests. The first is used to capture the principal node kind associated with each axis:

[51 (Formal)]   PrincipalNodeKind   ::=   "element" |  "attribute" |  "namespace"
[49 (Formal)]   Axis   ::=   ForwardAxis |  ReverseAxis

Notation

The principal node kind for each axis is specified using the following judgment.

Axis principal PrincipalNodeKind

Notation

The following auxiliary grammar production defines Filters, which denote either an axis, or a principal node kind in the context of a principal node kind. An Axis merely combines the forward and reverse axes to allow judgments that range over both.

[49 (Formal)]   Axis   ::=   ForwardAxis |  ReverseAxis
[50 (Formal)]   Filter   ::=   Axis |  (PrincipalNodeKind NodeTest)

Notation

The semantics of filters is defined with three auxiliary judgments. The first judgment defines the effect of a filter on a value, and is used in the dynamic semantics. This judgment should be read as follows: in the current context (i.e., with respect to the dynamic environment dynEnv.varValue), applying the Filter on Value1 yields Value2:

dynEnv |- Filter on Value1 => Value2

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

statEnv |- Filter on Type1 : Type2

The last judgment allows an additional type environment, localTypeEnv. This "local" type environment maps variables to types (in the same way as statEnv.varType), and is used when computing the static type of the descendant axis.

statEnv ; localTypeEnv |- Filter on Type1 : Type2

These judgments will be defined separately for axes and node tests below.

Ed. Note: Explain the judgments in detail, maybe similarly to in section 3.2.

Static Type Analysis

The static semantics of an Axis NodeTest pair is obtained by retrieving the type of the context node, and applying the two filters (the Axis, and then the NodeTest with a PrincipalNodeKind) on the result.

statEnv.varType($fs:dot) = Type1
statEnv |- Axis on Type1 : Type2
Axis principal PrincipalNodeKind
statEnv |- PrincipalNodeKind, NodeTest on Type2 : Type3

statEnv |- Axis NodeTest : Type3

Here are the common set of inference rules defining the static semantics of filters. Essentially, these rules are used to process complex types through a filter, breaking the types down to the type of a node or of a value. The semantics of a filter applied to a node or value type is then specific to each Axis and NodeTest.


statEnv |- Filter on () : ()


statEnv |- Filter on none : none

statEnv |- Filter on Type1 : Type3
statEnv |- Filter on Type2 : Type4

statEnv |- Filter on Type1,Type2 : Type3,Type4

statEnv |- Filter on Type1 : Type3
statEnv |- Filter on Type2 : Type4

statEnv |- Filter on Type1|Type2 : Type3|Type4

statEnv |- Filter on Type1 : Type3
statEnv |- Filter on Type2 : Type4

statEnv |- Filter on Type1&Type2 : Type3&Type4

The cases for specific axis and node test filters are given in the axis and node test sections below.

Dynamic Evaluation

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

dynEnv.varValue($fs:dot) = Value1
dynEnv |- Axis on Value1 => Value2
Axis principal PrincipalNodeKind
dynEnv |- PrincipalNodeKind, NodeTest on Value2 => Value3

dynEnv |- Axis NodeTest => Value3

Here are the common set of inference rules defining the dynamic semantics of filters. These rules apply filters to a sequence, by breaking the sequence down to a node or value.


dynEnv |- Filter on () => ()

dynEnv |- Filter on Value1 => Value3
dynEnv |- Filter on Value2 => Value4

dynEnv |- Filter on Value1,Value2 => Value3,Value4

Ed. Note: Jerome: These rules fetaure a notational abuse! Value1,Value2 indicates the concatenation of Value1 and Value2, and is used for both constructing a new sequence and deconstructing it. When doing the construction, it is equivalent to applying the op:concatenate operator. The Formal Semantics specification should use more consistent notation for data model constructions and deconstruction. See also [Issue-0118:  Data model syntax and literal values].

The semantics of a filter applied to a specific axis or nodetest is given in the appropriate section below.

Normalization

The semantics of the following(-sibling) and preceding(-sibling) axes are expressed by mapping them to core expressions, all other axes are part of core [XPath/XQuery] and therefore are left unchanged through normalization.

 
[following-sibling:: NodeTest]Path
==
typeswitch ($fs:dot)
  case attribute $v return ()
  default $v return
    (for $fs:new in (for $fs:dot in (for $fs:dot in $fs:dot return parent::node() ) return child::NodeTest) return
      if dm:node-before($fs:dot,$fs:new) then $fs:new else ())

Ed. Note: Should all mappings be unfolded all the way to the core language like the above one?

 
[following:: NodeTest]Path
==
[ancestor-or-self::node()/following-sibling::node()/descendant-or-self::NodeTest]Path

Otherwise, the forward axis is part of the core [XPath/XQuery] and handled by the Axis/NodeTest semantics below:

 
[child:: NodeTest]Path
==
child:: NodeTest
 
[attribute:: NodeTest]Path
==
attribute:: NodeTest
 
[self:: NodeTest]Path
==
self:: NodeTest
 
[descendant:: NodeTest]Path
==
descendant:: NodeTest
 
[descendant-or-self:: NodeTest]Path
==
descendant-or-self:: NodeTest
 
[namespace:: NodeTest]Path
==
namespace:: NodeTest

Reverse axes:

 
[preceding-sibling:: NodeTest]Path
==
for $fs:new in (for $fs:dot in (for $fs:dot in $fs:dot return parent::node()) return child::NodeTest) return
  if dm:node-before($fs:new,$fs:dot) then $fs:new else ()
 
[preceding:: NodeTest]Path
==
[ancestor-or-self::node()/preceding-sibling::node()/descendant-or-self::NodeTest]Path

Otherwise, the reverse axis is part of the core [XPath/XQuery] and is handled by the Axis/NodeTest semantics below.

 
[parent:: NodeTest]Path
==
parent:: NodeTest
 
[ancestor:: NodeTest]Path
==
ancestor:: NodeTest
 
[ancestor-or-self:: NodeTest]Path
==
ancestor-or-self:: NodeTest

Finally, the principal node kind of each axis is enumerated by the following rules (given here because they are used both by the static and dynamic semantic rules).


attribute:: principal attribute


namespace:: principal namespace

Axis != attribute::     Axis != namespace::

Axis principal element

Static Type Analysis

The following rules define the static semantics of the filter judgment when applied to an Axis.

The type for the self axis is the same type as the type of the context node.


statEnv |- self:: on NodeType : NodeType

In case of elements, the type of the child axis is obtained by extracting the children types out of the content model describing the type of the context node.


statEnv |- child:: on element qname { AttrType, ChildType } : ChildType

Ed. Note: [Kristoffer/XSL] Need to add filters for all cases.

The type of the attribute axis is obtained by extracting the attribute types out of the content model describing the type of the context node.


statEnv |- attribute:: on element qname { AttrType, ChildType } : AttrType

Ed. Note: [Kristoffer/XSL] Need to add filters for all cases.

The type for the parent axis is either an element, a document (for document elements), or empty.


statEnv |- parent:: on element : (element|document)?

Ed. Note: Better typing for the parent axis is still an open issue. See [Issue-0080:  Typing of parent].

The type for the namespace axis is always empty.


statEnv |- namespace:: on NodeType : ()

Ed. Note: Jerome: The type of namespace nodes is still an open issue. See [Issue-0105:  Types for nodes in the data model.].

The types for the descendant, and descendant-or-self, ancestor, and ancestor-or-self axis are implemented through recursive application of the children and parent filters. The corresponding inference rules use the auxiliary filter judgment with a local type environment. This local type environment is used to keep track of the visited elements in order to deal with recursive types.

statEnv ; { } |- descendant:: on Type : Type'

statEnv |- descendant:: on Type : Type'

The following two rules are used to deal with global elements. Global elements need careful treatment here in order to deal with possible recursion. Notably, if the global element has been seen before, then the rule terminates and returns the union of all types already visited in the local environment.

localTypeEnv(qname) = Type
localTypeEnv = { Type1, Type2, ... }

statEnv |- descendant:: on element qname : (Type1|Type2|...)*

localTypeEnv(qname) is an error
statEnv.elemDecl(qname) = define element qname TypeSpecifier
TypeSpecifier resolves to TypeName { Type }
statEnv ; localTypeEnv[qname : Type] |- descendant:: on Type : Type'

statEnv localTypeEnv |- descendant:: on element qname Type'

Ed. Note: Peter: I need yet to figure out, whether this works, there still appear a few glitches. See [Issue-0132:  Typing for descendant].

In all other cases, the following rule applies

statEnv |- child:: on NodeType : Type1
statEnv |- descendant:: on Type1 : Type2

statEnv |- descendant:: on NodeType : Type1,Type2

statEnv |- self:: on NodeType : Type1
statEnv |- descendant:: on Type1 : Type2

statEnv |- descendant-or-self:: on NodeType : Type1,Type2

The type for the ancestor axis is the element*,document? type indicating that it includes elements and possibly a document element.


statEnv |- ancestor:: on NodeType : element*

statEnv |- self:: on NodeType : Type1
statEnv |- ancestor:: on Type1 : Type2

statEnv |- ancestor-or-self:: on NodeType : Type1, Type2

In all the other cases, the filter application results in an empty type.

statEnv |- AxisName:: on NodeType : () otherwise.

Ed. Note: KHR: "otherwise" rules should be avoided and specify the cases exhaustively.

Dynamic Evaluation

The inference rules below indicate for each axis whether a particular node should be considered further or whether the node should be left out. Therefore, each rule either returns the input node, or returns the empty sequence. The overall result is obtained by putting together all of the remaining nodes, following the generic semantics for filters.

The self axis just returns the context node.


dynEnv |- self:: on NodeValue => NodeValue

The child, parent, attribute and namespace axis are implemented through their corresponding accessors in the [XQuery 1.0 and XPath 2.0 Data Model].


dynEnv |- child:: on NodeValue => dm:children(NodeValue)


dynEnv |- attribute:: on NodeValue => dm:attributes(NodeValue)


dynEnv |- parent:: on NodeValue => dm:parent(NodeValue)

The descendant, descendant-or-self, ancestor, and ancestor-or-self axis are implemented through recursive application of the children and parent filters.

dynEnv |- child:: on NodeValue => Value1
dynEnv |- descendant:: on Value1 => Value2

dynEnv |- descendant:: on NodeValue => fs:distinct-doc-order(op:concatenate(Value1, Value2))

dynEnv |- self:: on NodeValue => Value1
dynEnv |- descendant:: on Value1 => Value2

dynEnv |- descendant-or-self:: on NodeValue => op:concatenate(Value1, Value2)

dynEnv |- parent:: on NodeValue => Value1
dynEnv |- ancestor:: on Value1 => Value2

dynEnv |- ancestor:: on NodeValue => op:concatenate(Value1, Value2)

dynEnv |- self:: on NodeValue => Value1
dynEnv |- ancestor:: on Value1 => Value2

dynEnv |- ancestor-or-self:: on NodeValue => op:concatenate(Value1, Value2)

In all the other cases, the filter application results in an empty sequence.

dynEnv |- AxisName:: on NodeValue => () otherwise.

Ed. Note: Peter: Generally steps may operate on nodes and values alike; the axis rules only can operate on nodes (NodeValue). Is it a dynamic error to apply an axis rule on a value? See [Issue-0125:  Operations on node only in XPath].

5.2.1.2 Node Tests

Introduction

A node test is a condition applied on the nodes selected by an axis step. Possible node tests are described by the following grammar productions.

[42 (XQuery)]   NodeTest   ::=   KindTest |  NameTest
[43 (XQuery)]   NameTest   ::=   QName |  Wildcard
[44 (XQuery)]   Wildcard   ::=   "*" |  <NCName ":" "*"> |  <"*" ":" NCName>
[45 (XQuery)]   KindTest   ::=   ProcessingInstructionTest
|  CommentTest
|  TextTest
|  AnyKindTest
[46 (XQuery)]   ProcessingInstructionTest   ::=   <"processing-instruction" "("> StringLiteral? ")"
[47 (XQuery)]   CommentTest   ::=   <"comment" "("> ")"
[48 (XQuery)]   TextTest   ::=   <"text" "("> ")"
[49 (XQuery)]   AnyKindTest   ::=   <"node" "("> ")"

Core Grammar

The core grammars productions for XPath node tests are:

[27 (Core)]   NodeTest   ::=   KindTest |  NameTest
[28 (Core)]   NameTest   ::=   QName |  Wildcard
[29 (Core)]   Wildcard   ::=   "*" |  <NCName ":" "*"> |  <"*" ":" NCName>
[30 (Core)]   KindTest   ::=   ProcessingInstructionTest
|  CommentTest
|  TextTest
|  AnyKindTest
[31 (Core)]   ProcessingInstructionTest   ::=   <"processing-instruction" "("> StringLiteral? ")"
[32 (Core)]   CommentTest   ::=   <"comment" "("> ")"
[33 (Core)]   TextTest   ::=   <"text" "("> ")"
[34 (Core)]   AnyKindTest   ::=   <"node" "("> ")"

Static Type Analysis

The following typing rules apply to filters that are node tests in the context of a principal node kind.

Node tests on elements and attributes always accomplish the most specific type possible. For example, if $v is bound to an element with a computed name, the type of $v is element { Type }. The static type computed for the expression $v/self::foo is element foo {Type}, which makes use of the nametest foo to arrive at a more specific type. Also note that each case of name matching restricts the principal node kind to the appropriate one.

Ed. Note: [Kristoffer/XSL] Perhaps use statEnv |- expand(QName) = qname(URI, ncname) instead of qname = prefix:local? Also The ElemOrAttrType doesn't allow wildcard in the ElementName or AttributeName, so either the rules can be removed or the definition should be updated.

QName2 = Prefix2:LocalPart2
xf:get-namespace-uri( QName1) = statEnv.varType(Prefix2)
xf:get-local-name( QName1 ) = LocalPart2

statEnv |- element, QName2 on element QName1 {Type} : element QName1 {Type}

QName2 = Prefix2:LocalPart2
LocalPart1 = LocalPart2

statEnv |- element, QName2 on element *:LocalPart1 {Type} : element QName2 {Type}

QName2 = Prefix2:LocalPart2
statEnv.namespace(Prefix1) = statEnv.namespace(Prefix2)

statEnv |- element, QName2 on element Prefix1:* {Type} : element Prefix1:LocalPart2{Type}


statEnv |- element, QName2 on element {Type} : element QName2 {Type}

xf:get-local-name( QName1 ) = LocalPart2

statEnv |- element, *:LocalPart2 on element QName1 {Type} : element QName1 {Type}

LocalPart1 = LocalPart2

statEnv |- element, *:LocalPart2 on element *:LocalPart1 {Type} : element *:LocalPart2 {Type}


statEnv |- element, *:LocalPart2 on element Prefix1:* {Type} : element Prefix1:LocalPart2{Type}


statEnv |- element, *:LocalPart2 on element { Type } : element *:LocalPart2 {Type}

xf:get-namespace-uri( QName1) = statEnv.namespace(Prefix2)

statEnv |- element, Prefix2:* on element QName1 {Type} : element QName1 {Type}


statEnv |- element, Prefix2:* on element *:LocalPart1 {Type} : element Prefix2:LocalPart1 {Type}

statEnv.namespace(Prefix1) = statEnv.namespace(Prefix2)

statEnv |- element, Prefix2:* onelement Prefix1:* {Type} : element Prefix1:* {Type}


statEnv |- element, Prefix2:* on element {Type} : element Prefix2:* {Type}


statEnv |- element, * on element prefix:local {Type} : element prefix:local {Type}

Very similar typing rules apply to attributes:

QName2 = Prefix2:LocalPart2
xf:get-namespace-uri( QName1) = statEnv.namespace(Prefix2)
xf:get-local-name( QName1 ) = LocalPart2

statEnv |- attribute, QName2 on attribute QName1 {Type} : attribute QName1 {Type}

QName2 = Prefix2:LocalPart2
LocalPart1 = LocalPart2

statEnv |- attribute, QName2 on attribute *:LocalPart1 {Type} : attribute QName2 {Type}

QName2 = Prefix2:LocalPart2
statEnv.namespace(Prefix1) = statEnv.namespace(Prefix2)

statEnv |- attribute, QName2 on attribute Prefix1:* {Type} : attribute Prefix1:LocalPart2{Type}


statEnv |- attribute, QName2 on attribute {Type} : attribute QName2 {Type}

xf:get-local-name( QName1 ) = LocalPart2

statEnv |- attribute, *:LocalPart2 on attribute QName1 {Type} : attribute QName1 {Type}

LocalPart1 = LocalPart2

statEnv |- attribute, *:LocalPart2 on attribute *:LocalPart1 {Type} : attribute *:LocalPart2 {Type}


statEnv |- attribute, *:LocalPart2 on attribute Prefix1:* {Type} : attribute Prefix1:LocalPart2{Type}


statEnv |- attribute, *:LocalPart2 on attribute {Type} : attribute *:LocalPart2 {Type}

xf:get-namespace-uri( QName1) = statEnv.namespace(Prefix2)

statEnv |- attribute, Prefix2:* on attribute QName1 {Type} : attribute QName1 {Type}


statEnv |- attribute, Prefix2:* on attribute *:LocalPart1 {Type} : attribute Prefix2:LocalPart1 {Type}

statEnv.namespace(Prefix1) = statEnv.namespace(Prefix2)

statEnv |- attribute, Prefix2:* on attribute Prefix1:* {Type} : attribute Prefix1:* {Type}


statEnv |- attribute, Prefix2:* on attribute {Type} : attribute Prefix2:* {Type}


statEnv |- attribute, * on attribute prefix:local {Type} : attribute prefix:local {Type}

Comments, processing instructions, and text:


statEnv |- PrincipalNodeKind, processing-instruction() on processing-instruction : processing-instruction


statEnv |- PrincipalNodeKind, processing-instruction(String) on processing-instruction : processing-instruction


statEnv |- PrincipalNodeKind, comment() on comment : comment


statEnv |- PrincipalNodeKind, text() on text : text


statEnv |- PrincipalNodeKind, node() on NodeType : NodeType

If none of the above rules apply, then the node test returns the empty sequence and the following dynamic rule is applied:

statEnv |- PrincipalNodeKind, node() on NodeType : ()

Ed. Note: Peter: Except for self::, all axes guarantee that the NodeType is not the generic type node. However, when the type node is encountered, it has to be interpreted as element | attribute | text | comment | processing-instruction for these typing rules to work.

Dynamic Evaluation

The dynamic semantics indicates for each node test whether a node is retained.

dm:node-kind( NodeValue ) = PrincipalNodeKind
dm:name( NodeValue ) = QName1
QName2 = Prefix2:LocalPart2
xf:get-namespace-uri ( QName1 ) = statEnv.namespace(Prefix2)
xf:get-local-name ( QName1 ) = LocalPart2

dynEnv |- PrincipalNodeKind, QName2 on NodeValue => NodeValue

dm:node-kind( NodeValue ) = PrincipalNodeKind
dm:name ( NodeValue ) = qname

dynEnv |- PrincipalNodeKind, * on NodeValue => NodeValue

dm:node-kind( NodeValue ) = PrincipalNodeKind
dm:name ( NodeValue ) = qname
xf:get-namespace-uri ( qname ) = statEnv.namespace(prefix)

dynEnv |- PrincipalNodeKind, prefix:* on NodeValue => NodeValue

dm:node-kind( NodeValue ) = PrincipalNodeKind
dm:name ( NodeValue ) = qname
xf:get-local-name ( qname ) = local

dynEnv |- PrincipalNodeKind, *:local on NodeValue => NodeValue

dm:node-kind ( NodeValue ) = "processing-instruction"

dynEnv |- PrincipalNodeKind, processing-instruction() on NodeValue => NodeValue

dm:node-kind ( NodeValue ) = "processing-instruction"
dm:name ( NodeValue ) = qname
xf:get-local-name ( qname ) = String

dynEnv |- PrincipalNodeKind, processing-instruction( String ) on NodeValue => NodeValue

Ed. Note: Note the use of the xf:get-local-name function to extract the local name out of the name of the node.

dm:node-kind ( NodeValue ) = "comment"

dynEnv |- PrincipalNodeKind, comment() on NodeValue => NodeValue

dm:node-kind ( NodeValue ) = "text"

dynEnv |- PrincipalNodeKind, text() on NodeValue => NodeValue

The node() node test is true for all nodes. Therefore, the following rule does not have any precondition (remember that an empty upper part in the rule indicates that the rule is always true).


dynEnv |- PrincipalNodeKind, node() on NodeValue => NodeValue

If none of the above rules applies then the node test returns the empty sequence, and the following dynamic rule is applied:

dynEnv |- PrincipalNodeKind, node() on NodeValue => ()

5.2.2 Predicates

Introduction

Predicates are composed of zero or more expressions enclosed in square brackets.

[54 (XQuery)]   Predicates   ::=   ("[" Expr "]")*

Normalization

Predicates in path expressions are normalized with a special mapping rule:

 
[Expr]Predicates
==
typeswitch (Expr)
  case empty $v return xf:false()
  case numeric $v return op:numeric-equal(xf:round($v), $fs:position)
  case xs:boolean $v return $v
  default $v return
    if (xf:length([$v/self::node()]Path)>=1)
    then xf:true()
    else xf:error()

5.2.3 Unabbreviated Syntax

Ed. Note: XQuery Section 2.3.4 has no semantic content -- it just contains examples! (This suggests that perhaps the section structure is a little weird.)

5.2.4 Abbreviated Syntax

[52 (XQuery)]   AbbreviatedForwardStep   ::=   "." |  ("@" NameTest) |  NodeTest
[53 (XQuery)]   AbbreviatedReverseStep   ::=   ".."

Normalization

Here are normalization rules for the abbreviated syntax.

 
[ // RelativePathExpr ]Path
==
/ descendant-or-self::node() / [RelativePathExpr]Path
 
[ Expr // RelativePathExpr ]Path
==
[Expr]Expr / descendant-or-self::node() / [RelativePathExpr]Path
 
[ . ]Path
==
$fs:dot
 
[ .. ]Path
==
parent::node()
 
[ @ NameTest ]Path
==
attribute :: NameTest
 
[ NodeTest ]Path
==
child :: NodeTest

5.3 Sequence Expressions

Introduction

[XPath/XQuery] supports operators to construct and combine sequences. A sequence is an ordered collection of zero or more items. An item is either an atomic value or a node.

5.3.1 Constructing Sequences

[4 (XQuery)]   ExprSequence   ::=   Expr ("," Expr)*
[16 (XQuery)]   RangeExpr   ::=   AdditiveExpr ( "to"  AdditiveExpr )*

Normalization

The sequence expression is normalized into a sequence of core expressions:

 
["(" ExprSequence ")"]Expr
==
"(" [ ExprSequence ]Expr ")"
 
[Expr1 , ... , Exprn]Expr
==
[Expr1]Expr, ..., [Exprn]Expr

Ed. Note: Mike Kay remarks that it would be cleaner to have binary rules and recursion to define the semantics rather than the ... notation.

Core Grammar

The core grammar rule for sequence expressions is:

[4 (Core)]   ExprSequence   ::=   Expr ("," Expr)*

Static Type Analysis

The static semantics of the sequence expression follows. The type of the sequence expression is the sequence over the types of the individual expressions.

statEnv |- Expr1 : Type1      ...     statEnv |- Exprn : Typen

statEnv |- Expr1 , ... , Exprn : Type1, ..., Typen

Dynamic Evaluation

The dynamic semantics of the sequence expression follows. Each expression in the sequence is evaluated and the resulting values are concatenated into one sequence.

dynEnv |- Expr1 => Value1     dynEnv |- Expr2 => Value2     ...     dynEnv |- Exprn => Valuen

dynEnv |- Expr1, ..., Exprn => op:concatenate(Value1, op:concatenate(Value2, op:concatenate(... , Valuen) ) )

Normalization

The normalization of the infix "to" operator maps it into an application of op:to.

 
[Expr1 "op:to" Expr2]Expr
==
[op:to (Expr1, Expr2)]Expr

Static Type Analysis

The static semantics of the op:to function is defined in [7 Additional Semantics of Functions].

Dynamic Evaluation

The dynamic semantics rules for function calls given in [5.1.4 Function Calls] are applied to the function call op:to above.

Ed. Note: Should the "to" operator be defined formally? See [Issue-0133:  Should to also be described in the formal semantics?].

5.3.2 Combining Sequences

[XPath/XQuery] provides several operators for combining sequences.

[19 (XQuery)]   UnionExpr   ::=   IntersectExceptExpr ( ("union" |  "|")  IntersectExceptExpr )*
[20 (XQuery)]   IntersectExceptExpr   ::=   UnaryExpr ( ("intersect" |  "except")  UnaryExpr )*

Notation

First, a union, intersect, or except expression is normalized into a corresponding core expression. The mapping function []SequenceOp is defined by the following tables:

SequenceOp[SequenceOp]SequenceOp
"union"op:union
"|"op:union
"intersect"op:intersect
"except"op:except

Normalization

 
[Expr1 SequenceOp Expr2]Expr
==
[SequenceOp]SequenceOp ( [Expr1]Expr, [Expr2]Expr )

Static Type Analysis

The static semantics of the functions that operate on sequences are defined in [7 Additional Semantics of Functions].

Dynamic Evaluation

The dynamic semantics rules for function calls given in [5.1.4 Function Calls] are applied to the calls to functions on sequences above.

5.4 Arithmetic Expressions

[XPath/XQuery] provides arithmetic operators for addition, subtraction, multiplication, division, and modulus, in their usual binary and unary forms.

[17 (XQuery)]   AdditiveExpr   ::=   MultiplicativeExpr ( ("+" |  "-")  MultiplicativeExpr )*
[18 (XQuery)]   MultiplicativeExpr   ::=   UnionExpr ( ("*" |  "div" |  "idiv" |  "mod")  UnionExpr )*
[21 (XQuery)]   UnaryExpr   ::=   ("-" |  "+")* ValueExpr
[22 (XQuery)]   ValueExpr   ::=   ValidateExpr |  CastExpr |  Constructor |  PathExpr
[24 (XPath)]   ValueExpr   ::=   ValidateExpr |  CastExpr |  PathExpr

Core Grammar

All of those expressions are normalized to the following core grammar production:

[12 (Core)]   ValueExpr   ::=   ValidateExpr |  CastExpr |  Constructor |  PathExpr

Notation

Ed. Note: MFF: The operator table in this section was produced by Don Chamberlin. This table should be in one place, probably the Formal Semantics

Ed. Note: [Kristoffer/XSL] The present rules mix static and dynamic dispatch of which primitive function is used. We are investigating how to repair that as well as make the definitions work with both static and dynamic typing. See [Issue-0122:  Overloaded functions].

The tables in this section list the combinations of datatypes for which the various operators of [XPath/XQuery] are defined. For each valid combination of datatypes, the table indicates the name of the function that implements the operator and the datatype of the result. Definitions of the functions can be found in [XQuery 1.0 and XPath 2.0 Functions and Operators].

In the following tables, the term fs:numeric refers to the types xs:integer, xs:decimal, xs:float, and xs:double. When the result type of an operator is listed as numeric, it means "same as the highest type of any input operand, in promotion order." For example, when invoked with operands of type xs:integer and xs:float, the binary + operator returns a result of type xs:float.

In the following tables, the term Gregorian refers to the types xs:gYearMonth, xs:gYear, xs:gMonthDay, xs:gDay, and xs:gMonth. For binary operators that accept two Gregorian-type operands, both operands must have the same type (for example, if one operand is of type xs:gDay, the other operand must be of type xs:gDay.)

The functions []BinaryOp and []UnaryOp are defined by the following two tables. The function []BinaryOp takes the left-hand expression (A) and its type, the operator, the right-hand expression (b) and its type and returns a new expression, which applies the type-appropriate operator to the two expressions. The function []UnaryOp takes an operator and an expression and returns a new expression, which applies the appropriate operator to the expression.

OperatorType(A)Type(B)[A; Type(A); Operator; B; Type(B)]BinaryOpResult type
A + Bnumericnumericop:numeric-add(A, B)numeric
A + Bxs:datexs:yearMonthDurationop:add-yearMonthDuration-to-date(A, B)xs:date
A + Bxs:yearMonthDurationxs:dateop:add-yearMonthDuration-to-date(B, A)xs:date
A + Bxs:datexs:dayTimeDurationop:add-dayTimeDuration-to-date(A, B)xs:date
A + Bxs:dayTimeDurationxs:dateop:add-dayTimeDuration-to-date(B, A)xs:date
A + Bxs:timexs:dayTimeDurationop:add-dayTimeDuration-to-time(A, B)xs:time
A + Bxs:dayTimeDurationxs:timeop:add-dayTimeDuration-to-time(B, A)xs:time
A + Bxs:datetimexs:yearMonthDurationop:add-yearMonthDuration-to-dateTime(A, B)xs:dateTime
A + Bxs:yearMonthDurationxs:datetimeop:add-yearMonthDuration-to-dateTime(B, A)xs:dateTime
A + Bxs:datetimexs:dayTimeDurationop:add-dayTimeDuration-to-dateTime(A, B)xs:dateTime
A + Bxs:dayTimeDurationxs:datetimeop:add-dayTimeDuration-to-dateTime(B, A)xs:dateTime
A + Bxs:yearMonthDurationxs:yearMonthDurationop:add-yearMonthDurations(A, B)xs:yearMonthDuration
A + Bxs:dayTimeDurationxs:dayTimeDurationop:add-dayTimeDurations(A, B)xs:dayTimeDuration
A - Bnumericnumericop:numeric-subtract(A, B)numeric
A - Bxs:datexs:datexf:subtract-dates(A, B)xs:dayTimeDuration
A - Bxs:datexs:yearMonthDurationop:subtract-yearMonthDuration-from-date(A, B)xs:date
A - Bxs:datexs:dayTimeDurationop:subtract-dayTimeDuration-from-date(A, B)xs:date
A - Bxs:timexs:timexf:subtract-times(A, B)xs:dayTimeDuration
A - Bxs:timexs:dayTimeDurationop:subtract-dayTimeDuration-from-time(A, B)xs:time
A - Bxs:dateTimexs:dateTimexf:get-yearMonthDuration-from-dateTimes(A, B)xs:yearMonthDuration
A - Bxs:dateTimexs:dateTimexf:get-dayTimeDuration-from-dateTimes(A, B)xs:dayTimeDuration
A - Bxs:datetimexs:yearMonthDurationop:subtract-yearMonthDuration-from-dateTime(A, B)xs:dateTime
A - Bxs:datetimexs:dayTimeDurationop:subtract-dayTimeDuration-from-dateTime(A, B)xs:dateTime
A - Bxs:yearMonthDurationxs:yearMonthDurationop:subtract-yearMonthDurations(A, B)xs:yearMonthDuration
A - Bxs:dayTimeDurationxs:dayTimeDurationop:subtract-dayTimeDurations(A, B)xs:dayTimeDuration
A * Bnumericnumericop:numeric-multiply(A, B)numeric
A * Bxs:yearMonthDurationxs:decimalop:multiply-yearMonthDuration(A, B)xs:yearMonthDuration
A * Bxs:decimalxs:yearMonthDurationop:multiply-yearMonthDuration(B, A)xs:yearMonthDuration
A * Bxs:dayTimeDurationxs:decimalop:multiply-dayTimeDuration(A, B)xs:dayTimeDuration
A * Bxs:decimalxs:dayTimeDurationop:multiply-dayTimeDuration(B, A)xs:dayTimeDuration
A div Bnumericnumericop:numeric-divide(A, B)numeric
A div Bxs:yearMonthDurationxs:decimalop:divide-yearMonthDuration(A, B)xs:yearMonthDuration
A div Bxs:dayTimeDurationxs:decimalop:divide-dayTimeDuration(A, B)xs:dayTimeDuration
A mod Bnumericnumericop:numeric-mod(A, B)numeric
A eq Bnumericnumericop:numeric-equal(A, B)xs:boolean
A eq Bxs:booleanxs:booleanop:boolean-equal(A, B)xs:boolean
A eq Bxs:stringxs:stringop:numeric-equal(xf:compare(A, B), 1)xs:boolean
A eq Bxs:datexs:dateop:date-equal(A, B)xs:boolean?
A eq Bxs:timexs:timeop:time-equal(A, B)xs:boolean?
A eq Bxs:dateTimexs:dateTimeop:datetime-equal(A, B)xs:boolean?
A eq Bxs:yearMonthDurationxs:yearMonthDurationop:yearMonthDuration-equal(A, B)xs:boolean
A eq Bxs:dayTimeDurationxs:dayTimeDurationop:dayTimeDuration-equal(A, B)xs:boolean
A eq BGregorianGregorianop:Gregorian-equal(A, B)xs:boolean
A eq Bxs:hexBinaryxs:hexBinaryop:hex-binary-equal(A, B)xs:boolean
A eq Bxs:base64Binaryxs:base64Binaryop:base64-binary-equal(A, B)xs:boolean
A eq Bxs:anyURIxs:anyURIop:anyURI-equal(A, B)xs:boolean
A eq Bxs:QNamexs:QNameop:QName-equal(A, B)xs:boolean
A eq Bxs:NOTATIONxs:NOTATIONop:NOTATION-equal(A, B)xs:boolean
A ne Bnumericnumericxf:not(op:numeric-equal(A, B))xs:boolean
A ne Bxs:booleanxs:booleanxf:not(op:boolean-equal(A, B))xs:boolean
A ne Bxs:stringxs:stringxf:not(op:numeric-equal(xf:compare(A, B), 1))xs:boolean
A ne Bxs:datexs:datexf:not(op:date-equal(A,B))xs:boolean?
A ne Bxs:timexs:timexf:not(op:time-equal(A,B))xs:boolean?
A ne Bxs:dateTimexs:dateTimexf:not(op:datetime-equal(A, B))xs:boolean?
A ne Bxs:yearMonthDurationxs:yearMonthDurationxf:not(op:yearMonthDuration-equal(A, B))xs:boolean
A ne Bxs:dayTimeDurationxs:dayTimeDurationxf:not(op:dayTimeDuration-equal(A, B)xs:boolean
A ne BGregorianGregorianxf:not(op:Gregorian-equal(A, B))xs:boolean
A ne Bxs:hexBinaryxs:hexBinaryxf:not(op:hex-binary-equal(A, B))xs:boolean
A ne Bxs:base64Binaryxs:base64Binaryxf:not(op:base64-binary-equal(A, B))xs:boolean
A ne Bxs:anyURIxs:anyURIxf:not(op:anyURI-equal(A, B))xs:boolean
A ne Bxs:QNamexs:QNamexf:not(op:QName-equal(A, B))xs:boolean
A ne Bxs:NOTATIONxs:NOTATIONxs:not(op:NOTATION-equal(A, B))xs:boolean
A gt Bnumericnumericop:numeric-greater-than(A, B)xs:boolean
A gt Bxs:booleanxs:booleanop:boolean-greater-than(A, B)xs:boolean
A gt Bxs:stringxs:stringop:numeric-greater-than(xf:compare(A, B), 0)xs:boolean
A gt Bxs:datexs:dateop:date-greater-than(A, B)xs:boolean?
A gt Bxs:timexs:timeop:time-greater-than(A, B)xs:boolean?
A gt Bxs:dateTimexs:dateTimeop:datetime-greater-than(A, B)xs:boolean?
A gt Bxs:yearMonthDurationxs:yearMonthDurationop:yearMonthDuration-greater-than(A, B)xs:boolean
A gt Bxs:dayTimeDurationxs:dayTimeDurationop:dayTimeDuration-greater-than(A, B)xs:boolean
A lt Bnumericnumericop:numeric-less-than(A, B)xs:boolean
A lt Bxs:booleanxs:booleanop:boolean-less-than(A, B)xs:boolean
A lt Bxs:stringxs:stringop:numeric-less-than(xf:compare(A, B), 0)xs:boolean
A lt Bxs:datexs:dateop:date-less-than(A, B)xs:boolean?
A lt Bxs:timexs:timeop:time-less-than(A, B)xs:boolean?
A lt Bxs:dateTimexs:dateTimeop:datetime-less-than(A, B)xs:boolean?
A lt Bxs:yearMonthDurationxs:yearMonthDurationop:yearMonthDuration-less-than(A, B)xs:boolean
A lt Bxs:dayTimeDurationxs:dayTimeDurationop:dayTimeDuration-less-than(A, B)xs:boolean
A ge Bnumericnumericop:numeric-less-than(B, A)xs:boolean
A ge Bxs:stringxs:stringop:numeric-greater-than(xf:compare(A, B), -1)xs:boolean
A ge Bxs:datexs:dateop:date-less-than(B, A)xs:boolean?
A ge Bxs:timexs:timeop:time-less-than(B, A)xs:boolean?
A ge Bxs:dateTimexs:dateTimeop:datetime-less-than(B, A)xs:boolean?
A ge Bxs:yearMonthDurationxs:yearMonthDurationop:yearMonthDuration-less-than(B, A)xs:boolean
A ge Bxs:dayTimeDurationxs:dayTimeDurationop:dayTimeDuration-less-than(B, A)xs:boolean
A le Bnumericnumericop:numeric-greater-than(B, A)xs:boolean
A le Bxs:stringxs:stringop:numeric-less-than(xf:compare(A, B), 1)xs:boolean
A le Bxs:datexs:dateop:date-greater-than(B, A)xs:boolean?
A le Bxs:timexs:timeop:ime-greater-than(B, A)xs:boolean?
A le Bxs:dateTimexs:dateTimeop:datetime-greater-than(B, A)xs:boolean?
A le Bxs:yearMonthDurationxs:yearMonthDurationop:yearMonthDuration-greater-than(B, A)xs:boolean
A le Bxs:dayTimeDurationxs:dayTimeDurationop:dayTimeDuration-greater-than(B, A)xs:boolean
A is Bnodenodeop:node-equal(A, B)xs:boolean
A isnot Bnodenodexf:not(op:node-equal(A, B))xs:boolean
A << Bnodenodeop:node-before(A, B)xs:boolean
A >> Bnodenodeop:node-after(A, B)xs:boolean
A precedes Bnodenodeop:node-precedes(A, B)xs:boolean
A follows Bnodenodeop:node-follows(A, B)xs:boolean
A union Bnode*node*op:union(A, B)node*
A | Bnode*node*op:union(A, B)node*
A intersect Bnode*node*op:intersect(A, B)node*
A except Bnode*node*op:except(A, B)node*
A to Bxs:decimalxs:decimalop:to(A, B)xs:integer+
A , Bitem*item*op:concatenate(A, B)item*

An analogous table exists for unary operators.

OperatorOperand type [Operator; Expr]UnaryOpResult type
+ Anumericop:numeric-unary-plus(A)numeric
- Anumericop:numeric-unary-minus(A)numeric

Normalization

The normalization rules for the arithmetic operators "+" and "-" are similar, but not identical, because as the table above illustrates, "-" is not commutative.

The following normalization rule for "+" first applies []Atomize to each argument expression, binding the results of these expressions to two new variables, $e1 and $e2. It then applies a typeswitch on the left-hand operand $e1, and for each left-hand operand type, it applies a second typeswitch on the right-hand operand $e2. The function [Operator]BinaryOp takes the operator, the left-hand type, and the right-hand type and returns the appropriate function, which is applied to the argument values.

 
[Expr1 "+" Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     $z1 := [ $coree1 ]Atomize
     $e1 := typeswitch ($z1)
         case untyped $v1 return cast ($v1) as xs:double
         default $v1 return $v1,
     $z2 := [ $coree2 ]Atomize
     $e2 := typeswitch ($z2)
         case untyped $v2 return cast ($v2) as xs:double
         default $v2 return $v2
return
typeswitch ($e1)
case empty $v1 return ()
case fs:numeric $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case fs:numeric $v2 return [ $v1; numeric; "+"; $v2; numeric ]BinaryOp
     default $v2 return xf:error())
case xs:date $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:yearMonthDuration $v2 return [ $v1; xs:date; "+"; $v2; xs:yearMonthDuration ]BinaryOp
     case xs:dayTimeDuration $v2 return [ $v1; xs:date; "+"; $v2; xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case xs:time $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [ $v1; xs:time; "+"; $v2; xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case xs:dateTime $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:yearMonthDuration $v2 return [ $v1; xs:dateTime; "+"; $v2; xs:yearMonthDuration ]BinaryOp
     case xs:dayTimeDuration $v2 return [$v1; xs:dateTime; "+"; $v2; xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case xs:yearMonthDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:date $v2 return [ $v1; xs:yearMonthDuration; "+"; $v2; xs:date ]BinaryOp
     case xs:dateTime $v2 return [ $v1; xs:yearMonthDuration; "+"; $v2; xs:dateTime ]BinaryOp
     case xs:yearMonthDuration $v2 return [ $v1; xs:yearMonthDuration; "+"; $v2; xs:yearMonthDuration ]BinaryOp
     default $v2 return xf:error())
case xs:dayTimeDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:date $v2 return [$v1; xs:dayTimeDuration; "+"; $v2; xs:date ]BinaryOp
     case xs:dateTime $v2 return [ $v1; xs:dayTimeDuration; "+"; $v2; xs:dateTime ]BinaryOp
     case xs:dayTimeDuration $v2 return [ $v1; xs:dayTimeDuration; "+"; $v2; xs:dayTimeDuration ]BinaryOp
     case xs:time $v2 return [ $v1; xs:dayTimeDuration; "+"; $v2; xs:time ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

Ed. Note: MFF (01-May-2002) Not sure what to do about numeric promotion rules. Should they be expressed explicity in normalization rules?

Ed. Note: MFF: The Datatype production does not permit choices of item types -- this is annoying. See [Issue-0127:  Datatype limitations].

Ed. Note: Peter: the static semantics of operators is as strict as the one for functions, and is still under discussion. See [Issue-0129:  Static typing of union].

The following normalization rule for "-" is analogous to that for "+".

 
[Expr1 "-" Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     let $z1 := [ $coree1 ]Atomize return
     $e1 := typeswitch ($z1)
         case untyped $v1 return cast ($v1) as xs:double
         default $v1 return $v1,
     let $z2 := [ $coree2 ]Atomize return
     $e2 := typeswitch ($z2)
         case untyped $v2 return cast ($v2) as xs:double
         default $v2 return $v2
return
typeswitch ($e1)
     case empty $v1 return ()
     case fs:numeric $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case fs:numeric $v2 return [ $v1; numeric; "-"; $v2; numeric ]BinaryOp
     default $v2 return xf:error())
case xs:date $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [ $v1; xs:date; "-"; $v2; xs:dayTimeDuration ]BinaryOp
     case xs:yearMonthDuration $v2 return [ $v1; xs:date; "-"; $v2; xs:yearMonthDuration ]BinaryOp
     default $v2 return xf:error())
case xs:time $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [$v1; xs:time; "-"; $v2; xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case xs:dateTime $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [$v1; xs:dateTime; "-"; $v2; xs:dayTimeDuration ]BinaryOp
     case xs:yearMonthDuration $v2 return [$v1; xs:dateTime; "-"; $v2; xs:yearMonthDuration ]BinaryOp
     default $v2 return xf:error())
case xs:yearMonthDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:yearMonthDuration $v2 return [ $v1; xs:yearMonthDuration; "-"; $v2; xs:yearMonthDuration ]BinaryOp
     default $v2 return xf:error())
case xs:dayTimeDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [ $v1; xs:dayTimeDuration; "-"; $v2; xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

The multiplicative operators "*" and "div" are defined on numeric and xs:yearMonthDuration, xs:dayTimeDuration. The multiplicative operator "mod" is only defined on numeric, so its normalization rule is simple.

 
[Expr1 "*" Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     $z1 := [ $coree1 ]Atomize
     $e1 := typeswitch ($z1)
         case untyped $v1 return cast ($v1) as xs:double
         default $v1 return $v1,
     $z2 := [ $coree2 ]Atomize
     $e2 := typeswitch ($z2)
         case untyped $v2 return cast ($v2) as xs:double
         default $v2 return $v2
return
typeswitch ($e1)
case empty $v1 return ()
case xs:decimal $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:yearMonthDuration $v2 return [ $v1; xs:decimal; "*"; $v2; xs:yearMonthDuration ]BinaryOp
     case xs:dayTimeDuration $v2 return [ $v1; xs:decimal; "*"; $v2; xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case fs:numeric $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case fs:numeric $v2 return [ $v1; numeric; "*"; $v2; numeric ]BinaryOp
     default $v2 return xf:error())
case xs:dayTimeDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:decimal $v2 return [ $v1; xs:dayTimeDuration; "*"; $v2; xs:decimal ]BinaryOp
     default $v2 return xf:error())
case xs:yearMonthDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:decimal $v2 return [ $v1; xs:yearMonthDuration; "*"; $v2; xs:decimal ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()
 
[Expr1 "div" Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     $z1 := [ $coree1 ]Atomize
     $e1 := typeswitch ($z1)
         case untyped $v1 return cast ($v1) as xs:double
         default $v1 return $v1,
     $z2 := [ $coree2 ]Atomize
     $e2 := typeswitch ($z2)
         case untyped $v2 return cast ($v2) as xs:double
         default $v2 return $v2
return
typeswitch ($e1)
case empty $v1 return ()
case fs:numeric $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case fs:numeric $v2 return [ $v1; numeric; "div"; $v2; numeric ]BinaryOp
     default $v2 return xf:error())
case xs:dayTimeDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:decimal $v2 return [ $v1; xs:dayTimeDuration; "div"; $v2; xs:decimal ]BinaryOp
     default $v2 return xf:error())
case xs:yearMonthDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:decimal $v2 return [ $v1; xs:yearMonthDuration; "div"; $v2; xs:decimal ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()
 
[Expr1 mod Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     $z1 := [ $coree1 ]Atomize
     $e1 := typeswitch ($z1)
         case untyped $v1 return cast ($v1) as xs:double
         default $v1 return $v1,
     $z2 := [ $coree2 ]Atomize
     $e2 := typeswitch ($z2)
         case untyped $v2 return cast ($v2) as xs:double
         default $v2 return $v2
return
typeswitch ($e1)
case empty $v1 return ()
case fs:numeric $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case fs:numeric $v2 return [ $v1; numeric; mod $v2; numeric ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

For convenience, UnaryOp denotes the unary operators "+" and "-". The normalization rule for unary operators is straightforward:

 
[UnaryOp Expr]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $z1 := [ $coree1 ]Atomize
     $e1 := typeswitch ($z1)
         case untyped $v1 return cast ($v1) as xs:double
         default $v1 return $v1,
return [ UnaryOp; $e1 ]UnaryOp

Core Grammar

There are no core grammar rules for arithmetic expressions as they are normalized to function calls.

Static Type Analysis

In the [XQuery 1.0 and XPath 2.0 Functions and Operators], type promotion rules are given for all the arithmetic operators, denoted by op:operation, and the result types of these operations. The following static semantics rules specify the result types for all arithmetic operators when applied to specific numeric types.

statEnv |- Expr1 : Type1      Type1 <: xs:decimal      statEnv |- Expr2 : Type2      Type2 <: xs:decimal

statEnv |- op:operation(Expr1, Expr2) : xs:decimal

statEnv |- Expr1 : Type1      Type1 <: xs:float      statEnv |- Expr2 : Type2      Type2 <: xs:float

statEnv |- op:operation(Expr1, Expr2) : xs:float

statEnv |- Expr1 : Type1      Type1 <: xs:double      statEnv |- Expr2 : Type2      Type2 <: xs:double

statEnv |- op:operation(Expr1, Expr2) : xs:double

statEnv |- Expr1 : Type1      Type1 <: xs:integer      statEnv |- Expr2 : Type2      Type2 <: xs:integer

statEnv |- op:operation(Expr1, Expr2) : xs:integer

Ed. Note: MFF: Can the rules above be factored?

Analogous static type rules are given for the unary arithmetic operators.

statEnv |- Expr1 : Type1      Type1 <: xs:decimal

statEnv |- op:operation(Expr1) : xs:decimal

statEnv |- Expr1 : Type1      Type1 <: xs:float

statEnv |- op:operation(Expr1) : xs:float

statEnv |- Expr1 : Type1      Type1 <: xs:double

statEnv |- op:operation(Expr1) : xs:double

statEnv |- Expr1 : Type1      Type1 <: xs:integer

statEnv |- op:operation(Expr1) : xs:integer

Dynamic Evaluation

The normalization rules map all arithmetic operators into core expressions, whose dynamic semantics is defined in other sections. Therefore, there are no dynamic semantics rules for arithmetic operators. The dynamic semantics rules for function calls given in [5.1.4 Function Calls] apply to all the function calls: op:numeric-add, etc.

5.5 Comparison Expressions

Introduction

Comparison expressions allow two values to be compared. [XPath/XQuery] provides four kinds of comparison expressions, called value comparisons, general comparisons, node comparisons, and order comparisons.

[15 (XQuery)]   ComparisonExpr   ::=   RangeExpr ( (ValueComp
|  GeneralComp
|  NodeComp
|  OrderComp)  RangeExpr )?
[33 (XQuery)]   ValueComp   ::=   "eq" |  "ne" |  "lt" |  "le" |  "gt" |  "ge"
[32 (XQuery)]   GeneralComp   ::=   "=" |  "!=" |  "<" |  "<=" |  ">" |  ">="
[34 (XQuery)]   NodeComp   ::=   "is" |  "isnot"
[35 (XQuery)]   OrderComp   ::=   "<<" |  ">>"

Ed. Note: [Kristoffer/XSL] The present rules mix static and dynamic dispatch of which primitive function is used. We are investigating how to repair that as well as make the definitions work with both static and dynamic typing. See [Issue-0122:  Overloaded functions].

5.5.1 Value Comparisons

Normalization

The value comparison equality operators "eq" and "ne" are defined on a large set of types.

 
[Expr1 ValueEqOp Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     $e1 := [ $coree1 ]Atomize ,
     $e2 := [ $coree2 ]Atomize
return
typeswitch ($e1)
case empty $v1 return ()
case numeric $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case numeric $v2 return [ $v1; numeric; ValueEqOp; $v2; numeric ]BinaryOp
     case untyped $v2 return
         [ $v1; numeric; ValueEqOp; (cast ($v2) as xs:double); numeric ]BinaryOp
     default $v2 return xf:error())
case xs:boolean $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:boolean $v2 return [ $v1; xs:boolean; ValueEqOp; $v2; xs:boolean ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:boolean; ValueEqOp; (cast ($v2) as xs:boolean); xs:boolean ]BinaryOp
     default $v2 return xf:error())
case xs:string $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:string $v2 return [ $v1; xs:string; ValueEqOp; $v2; xs:string ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:string; ValueEqOp; (cast ($v2) as xs:string); xs:string ]BinaryOp
     default $v2 return xf:error())
case xs:date $v1 return
     (typeswitch ($e2) as $v2
     case empty $v2 return ()
     case xs:date $v2 return [ $v1; xs:date; ValueEqOp; $v2; xs:date ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:date; ValueEqOp; (cast ($v2) as xs:date); xs:date ]BinaryOp
     default $v2 return xf:error())
case xs:time $v1 return
     (typeswitch ($e2) as $v2
     case empty $v2 return ()
     case xs:time $v2 return [ $v1; xs:time; ValueEqOp; $v2; xs:time ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:time; ValueEqOp; (cast ($v2) as xs:time); xs:time ]BinaryOp
     default $v2 return xf:error())
case xs:dateTime $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dateTime $v2 return [ $v1; xs:dateTime; ValueEqOp; $v2; xs:dateTime ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:dateTime; ValueEqOp; (cast ($v2) as xs:dateTime); xs:dateTime ]BinaryOp
     default $v2 return xf:error())
case xs:dayTimeDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [ $v1; xs:dayTimeDuration; ValueEqOp; $v2; xs:dayTimeDuration ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:dayTimeDuration; ValueEqOp; (cast ($v2) as xs:dayTimeDuration); xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case xs:yearMonthDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:yearMonthDuration $v2 return [ $v1; xs:yearMonthDuration; ValueEqOp; $v2; xs:yearMonthDuration ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:yearMonthDuration; ValueEqOp; (cast ($v2) as xs:yearMonthDuration); xs:yearMonthDuration ]BinaryOp
     default $v2 return xf:error())
case Gregorian $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case Gregorian $v2 return [ $v1; Gregorian; ValueEqOp; $v2; Gregorian ]BinaryOp
     case untyped $v2 return
         [ $v1; Gregorian; ValueEqOp; (cast ($v2) as Gregorian); Gregorian ]BinaryOp
     default $v2 return xf:error())
case xs:hexBinary $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:hexBinary $v2 return [ $v1; xs:hexBinary; ValueEqOp; $v2; xs:hexBinary ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:hexBinary; ValueEqOp; (cast ($v2) as xs:hexBinary); xs:hexBinary ]BinaryOp
     default $v2 return xf:error())
case xs:base64Binary $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:base64Binary $v2 return [ $v1; xs:base64Binary; ValueEqOp; $x2; xs:base64Binary ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:base64Binary; ValueEqOp; (cast ($v2) as xs:base64Binary); xs:base64Binary ]BinaryOp
     default $v2 return xf:error())
case xs:anyURI $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:anyURI $v2 return [ $v1; xs:anyURI; ValueEqOp; $v2; xs:anyURI ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:anyURI; ValueEqOp; (cast ($v2) as xs:anyURI); xs:anyURI ]BinaryOp
     default $v2 return xf:error())
case xs:QName $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:QName $v2 return [ $v1; xs:QName; ValueEqOp; $v2; xs:QName ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:QName; ValueEqOp; (cast ($v2) as xs:QName) ; xs:QName ]BinaryOp
     default $v2 return xf:error())
case xs:NOTATION $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:NOTATION $v2 return [ $v1; xs:NOTATION; ValueEqOp; $v2; xs:NOTATION ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:NOTATION; ValueEqOp; (cast ($v2) as xs:NOTATION); xs:NOTATION ]BinaryOp
     default $v2 return xf:error())
case untyped $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case numeric $v2 return
         [ (cast ($v1) as xs:double); xs:double; ValueEqOp; $v2; xs:double; numeric]BinaryOp
     case xs:string $v2 return
         [ (cast ($v1) as xs:string); xs:string; ValueEqOp; $v2; xs:string]BinaryOp
     case xs:date $v2 return
         [ (cast ($v1) as xs:date); xs:date; ValueEqOp; $v2; xs:date]BinaryOp
     case xs:time $v2 return
         [ (cast ($v1) as xs:time); xs:time; ValueEqOp; $v2; xs:time]BinaryOp
     case xs:dateTime $v2 return
         [ (cast ($v1) as xs:dateTime); xs:dateTime; ValueEqOp; $v2; xs:dateTime]BinaryOp
     case xs:dayTimeDuration $v2 return
         [ (cast ($v1) as xs:dayTimeDuration); xs:dayTimeDuration; ValueEqOp; $v2; xs:dayTimeDuration]BinaryOp,
     case xs:yearMonthDuration $v2 return
         [ (cast ($v1) as xs:yearMonthDuration); xs:yearMonthDuration; ValueEqOp; $v2; xs:yearMonthDuration]BinaryOp,
     case xs:hexBinary $v2 return
         [ (cast ($v1) as xs:hexBinary); xs:hexBinary; ValueEqOp; $v2; xs:hexBinary ]BinaryOp
     case xs:base64Binary $v2 return
         [ (cast ($v1) as xs:base64Binary); xs:base64Binary; ValueEqOp; $v2; xs:base64Binary ]BinaryOp
     case xs:anyURI $v2 return
         [ (cast ($v1) as xs:anyURI); xs:anyURI; ValueEqOp; $v2; xs:anyURI ]BinaryOp
     case xs:QName $v2 return
         [ (cast ($v1) as xs:QName); xs:QName; ValueEqOp; $v2; xs:QName ]BinaryOp
     case xs:NOTATION $v2 return
         [ (cast ($v1) as xs:NOTATION); xs:NOTATION; ValueEqOp; $v2; xs:NOTATION ]BinaryOp
     case untyped $v2 return
         [ (cast ($v1) as xs:string); xs:string; ValueEqOp; (cast ($v2) as xs:string); xs:string ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

Ed. Note: MFF: The definition of equality operators could be factored by introducing another normalization function, which would be applied to the bodies of the cases. Is it clearer (albeit longer) to just enumerate all the cases? For now, they are enumerated.

Normalization

The value comparison in-equality operators "lt", "le", "gt", and "ge" are defined on a smaller set of types than are the equality operators "eq" and "ne". For convenience, ValueInEqOp denotes the operators "lt", "le", "gt", or "ge".

 
[Expr1 ValueInEqOp Expr2]Expr
==
let $coree1 := ([ Expr1 ]Expr),
     $coree2 := ([ Expr2 ]Expr),
     $e1 := [ $coree1 ]Atomize ,
     $e2 := [ $coree2 ]Atomize
return
typeswitch ($e1)
case empty $v1 return ()
case numeric $v2 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case numeric $v2 return [ $v1; numeric; ValueInEqOp; $v2; numeric ]BinaryOp
     case untyped $v2 return
         [ $v1; numeric; ValueInEqOp; (cast ($v2) as xs:double); numeric ]BinaryOp
     default $v2 return xf:error())
case xs:boolean $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:boolean $v2 return [ $v1; numeric; ValueInEqOp; $v2; numeric ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:boolean; ValueInEqOp; (cast ($v2) as xs:boolean); xs:boolean ]BinaryOp
     default $v2 return xf:error())
case xs:string $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:string $v2 return [ $v1; xs:string; ValueInEqOp; $v2; xs:string ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:string; ValueInEqOp; (cast ($v2) as xs:string); xs:string ]BinaryOp
     default $v2 return xf:error())
case xs:date $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:date $v2 return [ $v1; xs:date; ValueInEqOp; $v2; xs:date ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:date; ValueInEqOp; (cast ($v2) as xs:date); xs:date ]BinaryOp
     default $v2 return xf:error())
case xs:time $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:time $v2 return [ $v1; xs:time; ValueInEqOp; $v2; xs:time ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:time; ValueInEqOp; (cast ($v2) as xs:time); xs:time ]BinaryOp
     default $v2 return xf:error())
case xs:dateTime $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dateTime $v2 return [ $v1; xs:dateTime; ValueInEqOp; $v2; xs:dateTime ]BinaryOp
     case untyped return
         [ $v1; xs:dateTime; ValueInEqOp; (cast ($v2) as xs:dateTime); xs:dateTime ]BinaryOp
     default $v2 return xf:error())
case xs:dayTimeDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:dayTimeDuration $v2 return [ $v1; xs:dayTimeDuration; ValueInEqOp; $v2; xs:dayTimeDuration ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:dayTimeDuration; ValueInEqOp; (cast ($v2) as xs:dayTimeDuration); xs:dayTimeDuration ]BinaryOp
     default $v2 return xf:error())
case xs:yearMonthDuration $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case xs:yearMonthDuration $v2 return [ $v1; xs:yearMonthDuration; ValueInEqOp; $v2; xs:yearMonthDuration ]BinaryOp
     case untyped $v2 return
         [ $v1; xs:yearMonthDuration; ValueInEqOp; (cast ($v2) as xs:yearMonthDuration); xs:yearMonthDuration ]BinaryOp
     default $v2 return xf:error())
case untyped $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case numeric $v2 return
         [ (cast ($v1) as xs:double); xs:double; ValueInEqOp; $v2; numeric]BinaryOp
     case xs:string $v2 return
         [(cast ($v1) as xs:string); xs:string; ValueInEqOp; $v2; xs:string]BinaryOp
     case xs:date $v2 return
         [ (cast ($v1) as xs:date); xs:date; ValueInEqOp; $v2; xs:date]BinaryOp(cast ($v1) as xs:date, $v2)
     case xs:time $v2 return
         [ (cast ($v1) as xs:time); xs:time; ValueInEqOp; $v2; xs:time]BinaryOp
     case xs:dateTime $v2 return
         [ (cast ($v1) as xs:dateTime); xs:dateTime; ValueInEqOp; $v2; xs:dateTime]BinaryOp
     case xs:dayTimeDuration $v2 return
         [ (cast ($v1) as xs:dayTimeDuration); xs:dayTimeDuration; ValueInEqOp; $v2; xs:dayTimeDuration]BinaryOp
     case xs:yearMonthDuration $v2 return
         [ (cast ($v1) as xs:yearMonthDuration); xs:yearMonthDuration; ValueInEqOp; $v2; xs:yearMonthDuration]BinaryOp
     case untyped $v2 return
         [ (cast ($v1) as xs:string); xs:string; ValueInEqOp; (cast ($v2) as xs:string); xs:string ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

Core Grammar

There are no core grammar rules for value comparisons as they are normalized to function calls.

Static Type Analysis

There are no static type rules for the value comparison operators. They all have return type xs:boolean, as specified in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Evaluation

The normalization rules map all value comparison operators into core expressions, whose dynamic semantics is defined in other sections. Therefore, there are no dynamic semantics rules for value comparison operators. The dynamic semantics rules for function calls given in [5.1.4 Function Calls] apply to all the function calls: op:numeric-less-than, etc.

5.5.2 General Comparisons

Introduction

General comparisons are defined by adding existential semantics to value comparisons. The operands of a general comparison may be sequences of any length. The result of a general comparison is always true or false.

Notation

For convenience, GeneralOp denotes the operators "=", "!=", "<", "<=", ">", or ">=".

The function []ValueOp is defined by the following table:

GeneralOp[GeneralOp]ValueOp
=eq
!=ne
<lt
<=le
>gt
>=ge

Normalization

A general comparison expression is normalized by mapping it into an existentially quantified, value-comparison expression, which is normalized recursively.

 
[Expr1 GeneralOp Expr2]Expr
==
[some $v1 in Expr1 satisfies (some $v2 in Expr2 satisfies $v1 [GeneralOp]ValueOp $v2)]Expr

Core Grammar

There are no core grammar rules for general comparisons as they are normalized to existentially quantified core expressions.

Static Type Analysis

There are no static type rules for the general comparison operators. The existentially quantified "some" expression always returns xs:boolean. Its static typing semantics is given in [5.11 Quantified Expressions].

Dynamic Evaluation

The normalization rules map all general comparison operators into core expressions, whose dynamic semantics is defined in other sections. Therefore, there are no dynamic semantics rules for general comparison operators.

5.5.3 Node Comparisons

Notation

For convenience, NodeOp denotes the operators "is" and "isnot".

Normalization

The normalization rule for node comparison expressions checks that both operands are optional node values, otherwise it generates an error. If both operands are nodes, it applies the operator specified by the []BinaryOp function.

 
[Expr1 NodeOp Expr2]Expr
==
let $e1 := ([ Expr1 ]Expr),
     $e2 := ([ Expr2 ]Expr),
return
typeswitch ($e1)
case empty $v1 return
     (typeswitch ($e2)
     case node? $v2 return ()
     default $v2 return xf:error())
case node $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case node $v2 return [ $v1; node; NodeOp; $v2; node ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

Ed. Note: Don Chamberlin points out that the above rule is nearly identical to the one in the previous section. Merging the two rules should be considered.

Core Grammar

There are no core grammar rules for node comparisons as they are normalized to function calls.

Static Type Analysis

There are no static type rules for the node comparison operators.

Dynamic Evaluation

The normalization rules map the node comparison operators into core expressions, whose dynamic semantics is defined in other sections. Therefore, there are no dynamic semantics rules for node comparison operators.

5.5.4 Order Comparisons

Notation

For convenience, OrderOp denotes the operators "follow", "precedes", "<<", and ">>".

Normalization

The normalization rule for order comparison expressions checks that both operands are optional node values, otherwise it generates an error. If both operands are nodes, it applies the operator specified by the []BinaryOp function.

 
[Expr1 OrderOp Expr2]Expr
==
let $e1 := ([ Expr1 ]Expr),
     $e2 := ([ Expr2 ]Expr),
return
typeswitch ($e1)
case empty $v1 return
     (typeswitch ($e2)
     case node? $v2 return ()
     default $v2 return xf:error())
case node $v1 return
     (typeswitch ($e2)
     case empty $v2 return ()
     case node $v2 return [$v1; node; OrderOp; $v2; node ]BinaryOp
     default $v2 return xf:error())
default $v1 return xf:error()

Core Grammar

There are no core grammar rules for order comparisons as they are normalized to function calls.

Static Type Analysis

There are no static type rules for the order comparison operators.

Dynamic Evaluation

The normalization rules map the order comparison operators into core expressions, whose dynamic semantics is defined in other sections. Therefore, there are no dynamic semantics rules for order comparison operators.

5.6 Logical Expressions

Introduction

A logical expression is either an and-expression or an or-expression. The value of a logical expression is always one of the boolean values: true or false.

[7 (XQuery)]   OrExpr   ::=   AndExpr ( "or"  AndExpr )*
[8 (XQuery)]   AndExpr   ::=   UnorderedExpr ( "and"  UnorderedExpr )*
[12 (XPath)]   AndExpr   ::=   ForExpr ( "and"  ForExpr )*

Ed. Note: [Kristoffer/XSL] The present rules mix static and dynamic dispatch of which primitive function is used. We are investigating how to repair that as well as make the definitions work with both static and dynamic typing. See [Issue-0122:  Overloaded functions].

Normalization

The normalization rules for "and" and "or" first get the effective boolean value of each argument, then apply the appropriate operand.

 
[Expr1 and Expr2]Expr
==
let $e1 := [ Expr1 ]Effective_Boolean_Value return
     let $e2 := [ Expr2 ]Effective_Boolean_Value return
         if ($e1) then $e2
         else if (xf:not($e1)) then xf:false()
         else xf:error()

Ed. Note: Note that non-determinism in the semantics of logical expressions is not modeled here. See [Issue-0136:  Non-determinism in the semantics].

 
[Expr1 or Expr2]Expr
==
let $e1 := [ Expr1 ]Effective_Boolean_Value, return
     let $e2 := [ Expr2 ]Effective_Boolean_Value, return
         if ($e1) then xf:true()
         else if (xf:not($e1)) then $e2
         else $e2

Core Grammar

There are no core grammar rules for logical expressions which normalized to other kinds of [XPath/XQuery] expressions.

Static Type Analysis

There are no static type rules for the logical comparison operators. They both have return type xs:boolean, as specified in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Evaluation

The normalization rules map the logical comparison operators into core expressions, whose dynamic semantics is defined in other sections. Therefore, there are no dynamic semantics rules for logical comparison operators.

5.7 Constructors

[XPath/XQuery] supports two forms of constructors: a "literal" form that follows the XML syntax, and element and attribute constructors that can be used to construct stand-alone elements and attributes, possibly with a computed name.

[31 (XQuery)]   Constructor   ::=   ElementConstructor
|  XmlComment
|  XmlProcessingInstruction
|  CdataSection
|  ComputedDocumentConstructor
|  ComputedElementConstructor
|  ComputedAttributeConstructor
[70 (XQuery)]   ElementConstructor   ::=   ( |  "<") QName AttributeList ("/>" |  (">" ElementContent* "</" QName S? ">"))
[77 (XQuery)]   ElementContent   ::=   Char
|  "{{"
|  "}}"
|  ElementConstructor
|  EnclosedExpr
|  CdataSection
|  CharRef
|  PredefinedEntityRef
|  XmlComment
|  XmlProcessingInstruction
[78 (XQuery)]   AttributeList   ::=   (S (QName S? "=" S? AttributeValue)?)*
[79 (XQuery)]   AttributeValue   ::=   (["] (EscapeQuot |  AttributeValueContent)* ["])
|  (['] (EscapeApos |  AttributeValueContent)* ['])
[80 (XQuery)]   AttributeValueContent   ::=   Char
|  CharRef
|  "{{"
|  "}}"
|  EnclosedExpr
|  PredefinedEntityRef
[81 (XQuery)]   EnclosedExpr   ::=   ( |  "{") ExprSequence "}"

Core Grammar

The core grammar productions for constructors are:

[20 (Core)]   Constructor   ::=   XmlComment
|  XmlProcessingInstruction
|  ComputedDocumentConstructor
|  ComputedElementConstructor
|  ComputedAttributeConstructor
[57 (Core)]   EnclosedExpr   ::=   ( |  "{") ExprSequence "}"

5.7.1 Element Constructors

Introduction

[77 (XQuery)]   ElementContent   ::=   Char
|  "{{"
|  "}}"
|  ElementConstructor
|  EnclosedExpr
|  CdataSection
|  CharRef
|  PredefinedEntityRef
|  XmlComment
|  XmlProcessingInstruction

The static and dynamic semantics of the literal forms of element constructors is obtained after normalization to computed element constructors.

Notation

The auxiliary mapping rules []ElementContent and []AttributeContent are used for the normalization of element and attribute content respectively.

Normalization

Literal characters, escaped curly braces, character references, and predefined entity references in element content are treated specially. This normalization rule assumes:

  1. that the significant whitespace characters in element constructors have been preserved, as described in [5.7.3 Whitespace in Constructors];

  2. that character references have been resolved to individual characters and predefined entity references have been resolved to sequences of characters, and

  3. that the rule is applied to the longest contiguous sequence of characters.

The following normalization rules take the longest consecutive sequence of individual characters that arise from literal characters, escaped curly braces, character references, and predefined entity references and normalizes the character sequence as a text node.

 
[Char*]ElementContent
==
dm:text-node(fs:characters_to_string(Char*))

We start with the rules for normalizing a literal XML element's content. We normalize each individual value and construct a sequence of the normalized values. Consecutive sequences of characters are normalized as a unit, applying the rule above.

 
[ ElementContent0 ..., ElementContentn ]ElementContent
==
([ ElementContent0 ]ElementContent , ..., [ ElementContentn]ElementContent)

We normalize an enclosed expression in element content by normalizing each individual expression in its expression sequence and then construct a sequence of the normalized values:

 
[ { Expr0, ..., Exprn } ]ElementContent
==
([ Expr0 ]Expr , ..., [ Exprn]Expr, dm:text-node(""))

We need to distinguish between multiple enclosed expressions, because the rule for converting sequences of atomic values into strings are applied to sequences within distinct enclosed expressions. To distinguish between multiple enclosed expressions, we add an empty text node to the end of the constructed sequence above -- this empty text node is eliminated in the dynamic evaluation rule when consecutive text nodes are coalesced into a single text node. The text node guarantees that a whitespace character will not be inserted between atomic values computed by distinct enclosed expressions.

Processing instructions and comments in element content are normalized by applying the standard normalization rules.

 
[XmlProcessingInstruction]ElementContent
==
[XmlProcessingInstruction]Expr
 
[XmlComment]ElementContent
==
[XmlComment]Expr

The following rules normalize the two forms of literal XML element constructors by normalizing their name, attribute list, and element content and translates the normalized values into the corresponding computed element constructor.

[70 (XQuery)]   ElementConstructor   ::=   ( |  "<") QName AttributeList ("/>" |  (">" ElementContent* "</" QName S? ">"))
 
[ < QName AttributeList > ElementContent* </ QName S? > ]Expr
==
element [QName]{ [ AttributeList ]AttributeContent , [ ElementContent* ]ElementContent }
 
[ < QName AttributeList /> ]Expr
==
element [QName]{ [ AttributeList ]AttributeContent }

Like literal XML element constructors, literal XML attribute constructors are normalized to computed attribute constructors.

[78 (XQuery)]   AttributeList   ::=   (S (QName S? "=" S? AttributeValue)?)*
[79 (XQuery)]   AttributeValue   ::=   (["] (EscapeQuot |  AttributeValueContent)* ["])
|  (['] (EscapeApos |  AttributeValueContent)* ['])
[80 (XQuery)]   AttributeValueContent   ::=   Char
|  CharRef
|  "{{"
|  "}}"
|  EnclosedExpr
|  PredefinedEntityRef

Literal characters, escaped curly braces, character references, and predefined entity references in attribute content are treated as in element content. In addition, the normalization rule for characters in attributes assumes:

  1. that an escaped single or double quote is converted to an individual single or double quote.

The following normalization rules take the longest consecutive sequence of individual characters that arise from literal characters, escaped curly braces, character references, predefined entity references, and escaped single and double quotes and normalizes the character sequence as a string.

 
[Char*]AttributeContent
==
fs:characters_to_string(Char*)

We normalize an enclosed expression in attribute content by normalizing each individual expression in its expression sequence and then construct a sequence of the normalized values:

 
[ { Expr0, ..., Exprn } ]AttributeContent
==
([ Expr0 ]Expr , ..., [ Exprn]Expr, dm:text-node(""))

As in literal XML elements, we need to distinguish between multiple enclosed expressions in attribute content, because the rule for converting sequences of atomic values into strings are applied to sequences within distinct enclosed expressions. As in element content, to distinguish between multiple enclosed expressions in attribute content, we add an empty text node to the end of the constructed sequence above -- this empty text node is eliminated in the dynamic evaluation rule.

We normalize an AttributeValue (a literal attribute's value) by normalizing each individual value in its content and then construct a sequence of the normalized values. Consecutive sequences of characters are normalized as a unit, applying the rules above.

 
[ AttributeValueContent0 ..., AttributeValueContentn ]AttributeContent
==
([ AttributeValueContent0 ]AttributeContent , ..., [ AttributeValueContentn]AttributeContent)

An AttributeList is normalized by the following rule, which maps each of the individual attribute-value expressions in the attribute list and constructs a sequence of the normalized values.

 
[
QName0 S? = S? (AttributeValue0 | EnclosedExpr0) ...
QNamen S? = S? (AttributeValuen | EnclosedExprn) ...
]
==
(attribute [QName0] { [ (AttributeValue0 | EnclosedExpr0) ]AttributeContent},
...,
attribute [QNamen] { [ (AttributeValuen | EnclosedExprn) ]AttributeContent})

Core Grammar

There are no core grammar rules for literal XML element or attribute constructors as they are normalized to computed constructors.

Static Type Analysis

There are no additional static type rules for literal XML element or attribute constructors.

Dynamic Evaluation

There are no additional dynamic evaluation rules for literal XML element or attribute constructors.

5.7.2 Computed Element and Attribute Constructors

[72 (XQuery)]   ComputedElementConstructor   ::=   (<"element" QName "{"> |  (<"element" "{"> Expr "}" "{")) ExprSequence? "}"
[73 (XQuery)]   ComputedAttributeConstructor   ::=   (<"attribute" QName "{"> |  (<"attribute" "{"> Expr "}" "{")) ExprSequence? "}"
[71 (XQuery)]   ComputedDocumentConstructor   ::=   <"document" "{"> ExprSequence "}"
5.7.2.1 Computed Element Nodes

An element constructor may contain an arbitrary sequence of items, e.g., atomic values, attributes, and child elements. Here's an element constructor that contains an integer, an element, a string, and an attribute:

element address { 123, element street {"Roosevelt Ave."},
"Flushing, NY", attribute zip { "11368" } }

Normalization

Computed element constructors are normalized by mapping their name and expression sequence. The normalization rule partitions attribute nodes from other nodes and atomic values in the element content.

 
[element QName { ExprSequence }]Expr
==
let $e := [ExprSequence]Expr return
let $attributes := for $fs:new in $e return
     typeswitch $fs:new
     case attribute $a return $a
     default return ()
let $everythingelse := for $fs:new in $e return
     typeswitch $fs:new
     case attribute $a return ()
     default $v return $v
return
   element [QName] { $attributes, $everythingelse }

When the name of an element is computed, the normalization rule also checks that the value of the element's name is a xs:QName.

 
[element { Expr } { ExprSequence }]Expr
==
let xs:QName $name := [Expr]Expr return
let $e := [ExprSequence]Expr return
let $attributes := for $fs:new in $e return
     typeswitch $fs:new
     case attribute $a return $a
     default return ()
let $everythingelse := for $fs:new in $e return
     typeswitch $fs:new
     case attribute $a return ()
     default $v return $v
return
   element { $name } { $attributes, $everythingelse }
5.7.2.2 Constructed Attribute Nodes

Normalization

Computed attribute expressions are normalized by mapping their sub-expressions.

 
[attribute QName { ExprSequence }]Expr
==
attribute QName { [ExprSequence]Expr }
 
[attribute { Expr } { ExprSequence }]Expr
==
let xs:QName $name := [Expr]Expr return
attribute { $name } { [ExprSequence]Expr }

Core Grammar

The core grammar rules for computed constructors are:

[53 (Core)]   ComputedElementConstructor   ::=   (<"element" QName "{"> |  (<"element" "{"> Expr "}" "{")) ExprSequence? "}"
[54 (Core)]   ComputedAttributeConstructor   ::=   (<"attribute" QName "{"> |  (<"attribute" "{"> Expr "}" "{")) ExprSequence? "}"
[52 (Core)]   ComputedDocumentConstructor   ::=   <"document" "{"> ExprSequence "}"

Static Type Analysis

The normalization rules leave us with only the operator form of the element or attribute constructor to handle. The element (attribute) operator still has two forms: one in which a QName is supplied as the element (attribute) name, and the other in which a computed expression is supplied. In the latter case, the name cannot be known until runtime, and the element (attribute) is given a wildcard type.

Note that the static type for constructed elements and attributes is very poor as the static type of their content is lost during construction. A possible solution is to implicitly validate when the element is constructed. See [Issue-0169:  Conformance Levels] for suggestions.

statEnv |- expand(QName) = qname

statEnv |- element QName { ExprSequence } : element qname { xs:anyType }

statEnv |- Expr : xs:QName

statEnv |- element { Expr } { ExprSequence } : element { xs:anyType }

statEnv |- Expr : xs:QName

statEnv |- attribute { Expr } { ExprSequence } : attribute { xs:anySimpleType }

statEnv |- expand(QName) = qname

statEnv |- attribute QName { ExprSequence } : attribute qname { xs:anySimpleType }

Ed. Note: DD: the above is a necessary consequence of our current evaluation model. One variation that I can think of is that the static rules could try looking up the element name in element environment. If the element name is found, then the associated, named type is used (and the contents are required to match). If the named element type is not found, then the constructed type is used, as before. Thus, in this scenario, validation would be done whenever an element with a "global" name was created. See also comments on the impact of (non-)validation on element construction, in the next section.

Dynamic Evaluation

The following rules construct an element from its name and content. The earlier normalization rule guarantees that all attributes precede other element content, which is a sequence of node and atomic values. Section [3.7.4 Data Model Representation] in [XQuery 1.0: A Query Language for XML] specifies the rules for converting a sequence of atomic values into a text node prior to element construction. As formal specification of these conversion rules is not instructive, the function [7.1.3 The fs:item-sequence-to-node-sequence function] implements this conversion.

dynEnv |- QName => qname
dynEnv |- ExprSequence => ( AttributeValues, Items )

dynEnv |- element QName { ExprSequence } =>
       dm:element-node(qname,
dm:empty-sequence(),
AttributeValues,
fs:item-sequence-to-node-sequence(Items)
xs:anyType)

dynEnv |- Expr => qname
dynEnv |- ExprSequence => ( AttributeValues, Items )

dynEnv |- element { Expr } { ExprSequence } =>
       dm:element-node(qname,
dm:empty-sequence(),
AttributeValues,
fs:item-sequence-to-node-sequence(Items)
xs:anyType)

Note that the element constructor dm:element-node makes copies of any nodes in its arguments; therefore the result of element construction is a completely "new" element.

The following rules construct an attribute from its name and values and are similar to those for elements. Section [3.7.2 Data Model Representation] in [XQuery 1.0: A Query Language for XML] specifies the rules for converting a sequence of atomic values into a string prior to attribute construction. Each node is replaced by its string value. For each adjacent sequence of one or more atomic values returned by an enclosed expression, a string is constructed, containing the canonical lexical representation of all the atomic values, with a single blank character inserted between adjacent values. As formal specification of these conversion rules is not instructive, the function [7.1.4 The fs:item-sequence-to-string function] implements this conversion.

dynEnv |- QName => qname
dynEnv |- ExprSequence => AtomicValues

dynEnv |- attribute QName { ExprSequence } =>
       dm:attribute-node(qname,
fs:item-sequence-to-string(AtomicValues),
xs:anySimpleType)

dynEnv |- Expr => qname
dynEnv |- ExprSequence => AtomicValues

dynEnv |- attribute { Expr } { ExprSequence } =>
       dm:attribute-node(qname,
fs:item-sequence-to-string(AtomicValues),
xs:anySimpleType)

Ed. Note: DD: There are several issues with element construction:

  • Namespaces and more precise type annotations in the constructor are not supported. This is due to the bottom-up nature of element construction: in general, one does not know either the namespaces in scope or the validation-associated schema type until this element has been "seated" in some containing element (and so on recursively). See [Issue-0165:  Namespaces in element constructors].

    There is a possible solution to this chicken-and-egg problem, however: because the element constructor makes copies of its children, it could be the responsibility of the element constructor to "fill in" the values for namespaces-in-scope and schema-component on each newly-copied child (recursively), based on information provided for the node. In this scenario, these fields would remain "blank" until some appropriate activity caused a schema component to become associated with a node, etc.

    One implication of such a scheme would be that the "value" of elements could change as they are copied into a new containing element. For example, defaulted attributes could be added. Possibly the interpretation of data values would change as well, e.g. a data value supplied as a string could be re-interpreted as a number.

  • Any special treatment of xmlns, etc. that would be needed to associate namespaces with elements is not modeled.

  • Even if/when schema components are available, it is not clear when or how defaulted attributes and/or elements are created.

5.7.3 Whitespace in Constructors

Section [3.7.3 Whitespace in Constructors] in [XQuery 1.0: A Query Language for XML] describes how whitespace in element and attribute constructors is processed depending on the value of the xmlspace declaration in the query prolog. The formal semantics assumes that the rules for handling whitespace are applied prior to normalization rules, for example, during parsing of a query. Therefore, there are no formal rules for handling whitespace.

5.7.4 Other Constructors and Comments

[74 (XQuery)]   CdataSection   ::=   "<![CDATA[" Char* "]]>"
[75 (XQuery)]   XmlProcessingInstruction   ::=   "<?" PITarget Char* "?>"
[76 (XQuery)]   XmlComment   ::=   "<!--" Char* "-->"

Core Grammar

The core grammar productions for other constructors and comments are:

[55 (Core)]   XmlProcessingInstruction   ::=   "<?" PITarget Char* "?>"
[56 (Core)]   XmlComment   ::=   "<!--" Char* "-->"

Normalization

A literal XML character data (CDATA) section is normalized into a text node constructor by applying the rule for converting characters to a text node in element content.

 
[<![CDATA[" Char* "]]>]Expr
==
[Char*]ElementContent

A literal XML processing instruction is normalized into a processing instructor constructor; its character content is converted to a string as in attribute content.

 
[<? NCName Char* ?>"]Expr
==
dm:processing-instruction-node(NCName [Char*]AttributeContent)

A literal XML comment is normalized into a comment constructor; its character content is converted to a string as in attribute content.

 
[<!-- Char* -->]Expr
==
dm:comment-node([Char*]AttributeContent)

Static Type Analysis

There are no additional static type rules for CDATA, processing instructions or comments.

Dynamic Evaluation

There are no additional dynamic evaluation rules for CDATA, processing instructions or comments.

5.8 [For/FLWR] Expressions

Introduction

[XPath/XQuery] provides [For/FLWR] expressions for iteration, for binding variables to intermediate results, and filtering bound variables according to a predicate.

A FLWRExpr in XQuery 1.0 consists of a sequence of ForClauses and LetClauses, followed by an optional WhereClause, followed by an expression to be "return"ed, as described by the following grammar productions. Each variable binding is preceded by an optional type assertion which specify the type expected for the variable.

[10 (XQuery)]   FLWRExpr   ::=   ((ForClause |  LetClause)+ WhereClause? "return")* QuantifiedExpr
[26 (XQuery)]   ForClause   ::=   "for" TypeDeclaration? "$" VarName "in" Expr ("," TypeDeclaration? "$" VarName "in" Expr)*
[27 (XQuery)]   LetClause   ::=   "let" TypeDeclaration? "$" VarName ":=" Expr ("," TypeDeclaration? "$" VarName ":=" Expr)*
[28 (XQuery)]   WhereClause   ::=   "where" Expr
[63 (XQuery)]   TypeDeclaration   ::=   SequenceType
[13 (XPath)]   ForExpr   ::=   (ForClause "return")* QuantifiedExpr

5.8.1 FLWR expressions

Notation

Individual [For/FLWR] clauses are normalized by means of the auxiliary normalization rules:

[FLWRClause]FLWR(Expr)

Where FLWRClause can be any either a ForClause, a LetClause, or a WhereClause:

[56 (Formal)]   FLWRClause   ::=   ForClause |  LetClause |  WhereClause

Note that, as is, this auxiliary rule normalizes a fragment of the [For/FLWR] expression, while taking the remainder of the expression (in Expr) as an additional parameter.

Normalization

Full [For/FLWR] expressions are normalized to nested core expressions using two sets of normalization rules. Note that some of the rules also accept ungrammatical FLWRExprs such as "where Expr1 return Expr2". This does not matter, as normalization is always applied on parsed [XPath/XQuery] expressions, and ungrammatical FLWRExprs would be rejected by the parser beforehand.

The first set of rules is applied on a full [For/FLWR] expression, splitting it at the clause level, then applying further normalization on each separate clause.

 
[ (ForClause | LetClause | WhereClause) FLWRExpr ]Expr
==
[(ForClause | LetClause | WhereClause)]FLWR([FLWRExpr])
 
[ (ForClause | LetClause | WhereClause) return Expr ]Expr
==
[(ForClause | LetClause | WhereClause)]FLWR([Expr])

Then each [For/FLWR] clause is normalized separately. A ForClause may bind more than one variable, whereas a for expression in the [XPath/XQuery] core binds and iterates over only one variable. Therefore, a ForClause is normalized to nested for expressions:

 
[ for TypeDeclaration1? Variable1 in Expr1,..., TypeDeclarationn? Variablen in Exprn ] FLWR(Expr)
==
for TypeDeclaration1? Variable1 in [Expr1]Expr return
  ···
     for TypeDeclarationn? Variablen in [ Exprn ]Expr return Expr

Each individual for clause, is then normalized to always have a type assertion.

Note that the additional Expr parameter of the auxiliary normalization rule is used as the final return expression.

Likewise, a LetClause clause is normalized to nested let expressions:

 
[ let TypeDeclaration1? Variable1 := Expr1, ···, TypeDeclarationn? Variablen := Exprn]FLWR(Expr)
==
let TypeDeclaration1? Variable1 := [Expr1 ]Expr return
  ···
    let TypeDeclarationn? Variablen := [Exprn]Expr return Expr

A WhereClause is normalized to an IfExpr, with the else-branch returning the empty list:

 
[ where Expr1]FLWR(Expr)
==
if ( [Expr1]Expr ) then Expr else ()

Example

The following simple example illustrates, how a FLWRExpr is normalized. The for expression in the example below is used to iterate over two collections, binding variables $i and $j to items in these collections. It uses a let clause to binds the local variable $k to the sum of both numbers, and a where clause to select only those numbers that have a sum equal to or greater than the integer 5.

  for xs:integer $i in (1, 2),
      $j in (3, 4)
  let $k := $i + $j
  where $k >= 5
  return
    <tuple>
       <i> { $i } </i>
       <j> { $j } </j>
    </tuple>

By the first set of rules, this is normalized to (except for the operators and element constructor which are not treated here):

  for xs:integer $i in (1, 2) return
    for $j in (3, 4) return
      let $k := $i + $j return
        if ($k >= 5) then 
          <tuple>
            <i> { $i } </i>
            <j> { $j } </j>
          </tuple>
        else
          ()

For each binding of $i to an item in the sequence (1 , 2) the inner for expression iterates over the sequence (3 , 4) to produce tuples ordered by the ordering of the outer sequence and then by the ordering of the inner sequence. This core expression eventually results in the following document fragment:

  (<tuple>
      <i>1</i>
      <j>4</j>
   </tuple>,
   <tuple>
      <i>2</i>
      <j>3</j>
   </tuple>,
   <tuple>
      <i>2</i>
      <j>4</j>
   </tuple>)

with the static type:

  element tuple {
    element i { xs:integer },
    element j { xs:integer }
  }*

5.8.2 For expression

Core Grammar

After normalization, single for expressions are described by the following core grammar production.

[8 (Core)]   ForExpr   ::=   (ForClause "return")* TypeswitchExpr
[16 (Core)]   ForClause   ::=   "for" TypeDeclaration? "$" VarName "in" Expr
[45 (Core)]   TypeDeclaration   ::=   SequenceType

Static Type Analysis

A single for expression is typed as follows: First Type1 of the iteration expression Expr1 is inferred. Then the prime type of Type1 - prime(Type1) - is determined. This is a choice over all item types in Type1 (see also [3.6 Auxiliary typing judgments for for, unordered, and sortby expressions]). With the variable component of the static environment statEnv extended with Variable1 of type prime(Type1), the type Type2 of Expr2 is inferred. Because the for expression iterates over the result of Expr1, the final type of the iteration is Type2 multiplied with the possible number of items in Type1 (one, ?, *, or +). This number is determined by the auxiliary type-function quantifier(Type1).

statEnv |- Expr1 : Type1
statEnv [ varType(Variable1 : prime(Type1)) ] |- Expr2 : Type2

statEnv |- for Variable1 in Expr1 return Expr2 : Type2 · quantifier(Type1)

In the case a type assertion is present, the static semantics also checks that the type of the input expression is a subtype of the asserted type. This semantics is specified as the following typing rule.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
Type1 <: Type0
statEnv [ varType(Variable1 : prime(Type1)) ] |- Expr2 : Type2

statEnv |- for SequenceType Variable1 in Expr1 return Expr2 : Type2 · quantifier(Type1)

Example

For example, if $example is bound to the sequence (<one/> , <two/> , <three/>) of type element one {}, element two {}, element three {}, then the query

  for $s in $example
  return <out> {$s} </out>

is typed as follows:

  (1) prime(element one {}, element two {}, element three {}) =
      element one {} | element two {} | element three {}
  (2) quantifier(element one {}, element two {}, element three {}) = +
  (3) $s : element one {} | element two {} | element three {}
  (4) <out> {$s} </out> : 
      element out {element one {} | element two {} | element three {}}
  (5) result-type :
      element out {element one {} | element two {} | element three {}}+

This result-type is not the most specific type possible. It does not take into account the order of elements in the input type, and it ignores the individual and overall number of elements in the input type. The most specific type possible is: element out {element one {}}, element out {element two {}}, element out {element three {}}. However, inferring such a specific type for arbitrary input types and arbitrary return clauses requires significantly more complex type inference rules. In addition, if put into the context of an element, the specific type violates the "unique particle attribution" restriction of XML schema, which requires that an element must have a unique content model within a particular context.

Dynamic Evaluation

The evaluation of a for expression distinguishes two cases: If the iteration expression Expr1 evaluates to the empty sequence, then the entire expression evaluates to the empty sequence:

dynEnv |- Expr1 => Value      empty(Value)

dynEnv |- for TypeDeclaration? Variable1 in Expr1 return Expr2 => dm:empty-sequence()

Otherwise, the iteration expression Expr1, is evaluated to produce the sequence Item1, ..., Itemn. For each item Itemi in this sequence, the body of the for expression Expr2 is evaluated in the environment dynEnv extended with Variable1 bound to Itemi. This produces values Valuei, ..., Valuen which are concatenated to produce the result sequence.

dynEnv |- Expr1 => Item1 ,..., Itemn
dynEnv [ varValue(Variable1 |-> Item1) ] |- Expr2 => Value1
···
dynEnv [ varValue(Variable1 |-> Itemn) ] |- Expr2 => Valuen

dynEnv |- for Variable1 in Expr1 return Expr2 => op:concatenate(Value1 ,..., Valuen)

In the case a type assertion is present, the dynamic semantics also checks that the input value matches the asserted type. This semantics is specified as the following dynamic rule.

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
Item1 matches Type0
dynEnv [ varValue(Variable1 |-> Item1) ] |- Expr2 => Value1
···
Itemn matches Type0
dynEnv [ varValue(Variable1 |-> Itemn) ] |- Expr2 => Valuen

dynEnv |- for SequenceType Variable1 in Expr1 return Expr2 => op:concatenate(Value1 ,..., Valuen)

Ed. Note: The dynamic semantics of for could be better defined without the use of ··· and using recursion. See [Issue-0134:  Should we define for with head and tail?].

Example

Note that if the expression in the return clause results in a sequence, sequences are never nested in the [XPath/XQuery] data model. For instance, in the following for expression:

  
  for $i in (1,2)
    return (<i> {$i} </i>, <negi> {-$i} </negi>)

each iteration in the for results in a sequence of two elements, which are then concatenated and flattened in the resulting sequence (using the op:concatenate function):

  
  (<i>1</i>,
   <negi>-1</negi>,
   <i>2</i>,
   <negi>-2</negi>)

5.8.3 Let Expression

Core Grammar

After normalization, single let expressions are described by the following core grammar production.

[9 (Core)]   LetExpr   ::=   (LetClause "return")* TypeswitchExpr
[17 (Core)]   LetClause   ::=   "let" TypeDeclaration? "$" VarName ":=" Expr

Static Type Analysis

A let expression extends the type environment statEnv with Variable1 of type Type1 inferred from Expr1, and infers the type of Expr2 in the extended environment to produce the result type Type2.

statEnv |- Expr1 : Type1      statEnv [ varType(Variable1 : Type1) ] |- Expr2 : Type2

statEnv |- let Variable1 := Expr1 return Expr2 : Type2

In the case a type assertion is present, the static semantics also checks that the type of the input expression is a subtype of the asserted type. This semantics is specified as the following typing rule.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
Type1 <: Type0
statEnv [ varType(Variable1 : Type1) ] |- Expr2 : Type2

statEnv |- let Variable1 := Expr1 return Expr2 : Type2

Dynamic Evaluation

A let expression extends the dynamic environment dynEnv with Variable bound to Value1 returned by Expr1, and evaluates Expr2 in the extended environment to produce Value2.

dynEnv |- Expr1 => Value1
dynEnv [ varValue(Variable1 |-> Value1) ] |- Expr2 => Value2

dynEnv |- let Variable1 := Expr1 return Expr2 => Value2

In the case a type assertion is present, the dynamic semantics also checks that the input value matches the asserted type. This semantics is specified as the following dynamic rule.

dynEnv |- Expr1 => Value1
Type0 = [ SequenceType ]sequencetype
Value1 matches Type0
dynEnv [ varValue(Variable1 |-> Value1) ] |- Expr2 => Value2

dynEnv |- let SequenceType Variable1 := Expr1 return Expr2 => Value2

Example

Note the use of the environment discipline to define the scope of each variable. For instance, in the following nested let expression:

  let $k := 5 return
    let $k := $k + 1 return
      $k+1

the outermost let expression binds variable $k to the integer 5 in the environment, then the expression $k+1 is computed, yielding value 6, to which the second variable $k is bound. The expression then results in the final integer 7.

5.9 Order-Related Expressions

5.9.1 Sorting Expressions

[6 (XQuery)]   SortExpr   ::=   OrExpr ( "stable"? <"sort" "by" "("> SortSpecList ")" )
[36 (XQuery)]   SortSpecList   ::=   Expr SortModifier ("," SortSpecList)?
[37 (XQuery)]   SortModifier   ::=   ("ascending" |  "descending")? (<"empty" "greatest"> |  <"empty" "least">)?

Core Grammar

The core grammar productions for sortby are:

[6 (Core)]   SortExpr   ::=   UnorderedExpr ( "stable"? <"sort" "by" "("> SortSpecList ")" )
[21 (Core)]   SortSpecList   ::=   Expr SortModifier ("," SortSpecList)?
[22 (Core)]   SortModifier   ::=   ("ascending" |  "descending") (<"empty" "greatest"> |  <"empty" "least">)

Ed. Note: Status: The semantics of sortby is not currently specified. Revision is pending agreement about the semantics of sorting.See [Issue-0109:  Semantics of sortby].

5.9.2 Unordered Expressions

[9 (XQuery)]   UnorderedExpr   ::=   "unordered"FLWRExpr

Introduction

The unordered keyword may be used as a prefix to any expression to indicate that its order is not significant.

Core Grammar

The core grammar production for unordered expressions is:

[7 (Core)]   UnorderedExpr   ::=   "unordered"ForExpr

Notation

The dynamic semantics for unordered use an auxiliary judgments which disregards order between the items in a sequence.

The following judgment

dynEnv |- Value1 permutes to Value2

holds if the sequence of items in Value2 is a permutation of the sequence of items in Value1.

Static Type Analysis

The static semantics for unordered uses the auxiliary type functions prime(Type) and quantifier(Type); which are defined in [3.6 Auxiliary typing judgments for for, unordered, and sortby expressions]. The type of each argument is determined, and then prime(.) and quantifier(.) are applied to the sequence type (Type1, Type2).

statEnv |- Expr1 : Type1

statEnv |- unordered Expr1 : prime(Type1) · quantifier(Type1)

Dynamic Evaluation

The dynamic semantics for unordered is specified using the auxiliary judgments permutes to as follows.

dynEnv |- Expr1 => Value1
dynEnv |- Value1 permutes to Value2

statEnv |- unordered Expr1 => Value2)

It is important to remark that the permutes to judgments is non deterministics. There are many sequences which can be a permutation of a given sequence. Any of those permutations would satisfy the above semantics.

5.10 Conditional Expressions

Introduction

A conditional expression supports conditional evaluation of one of two expressions.

[13 (XQuery)]   IfExpr   ::=   (<"if" "("> Expr ")" "then" Expr "else")* InstanceofExpr

Normalization

 
[if (Expr1) then Expr2 else Expr3]Expr
==
let $fs:new := [ Expr1 ]Effective_Boolean_Value return
  if ($fs:new) then [Expr2]Expr else [Expr3]Expr

where $fs:new is a newly created variable that does not appear in the rest of the query.

Core Grammar

The core grammar rule for the conditional expression is:

[11 (Core)]   IfExpr   ::=   (<"if" "("> Expr ")" "then" Expr "else")* ValueExpr

Static Type Analysis

statEnv |- Expr1 : xs:boolean      statEnv |- Expr2 : Type2      statEnv |- Expr3 : Type3

statEnv |- if (Expr1) then Expr2 else Expr3 : (Type2 | Type3)

Dynamic Evaluation

If the conditional's boolean expression Expr1 evaluates to true, Expr2 is evaluated and its value is produced. If the conditional's boolean expression evaluates to false, Expr3 is evaluated and its value is produced. Note that the existence of two separate evaluation rules ensures that only one branch of the conditional is evaluated.

Ed. Note: DD: actually, I would like that last sentence to be true, but I don't think it is: there is nothing that I know of in the semantics of evaluation rules that says that the clauses must be evaluated left-to-right, so currently nothing stops an implementation from evaluating the body expressions first. Even if this is a functional language generally, I am sure there will be non-functional side-effects in implementation-dependent extensions to the language, and I think there must be a way to formally state that bodies of conditionals do not get executed if their test fails.

dynEnv |- Expr1 => true      dynEnv |- Expr2 => Value2

dynEnv |- if Expr1 then Expr2 else Expr3 => Value2

dynEnv |- Expr1 => false      dynEnv |- Expr3 => Value3

dynEnv |- if Expr1 thenExpr2 elseExpr3 => Value3

5.11 Quantified Expressions

Introduction

[XPath/XQuery] defines two quantification expressions:

[11 (XQuery)]   QuantifiedExpr   ::=   (("some" |  "every") TypeDeclaration? "$" VarName "in" Expr ("," TypeDeclaration? "$" VarName "in" Expr)* "satisfies")* TypeswitchExpr
[14 (XPath)]   QuantifiedExpr   ::=   ((<"some" "$"> |  <"every" "$">) VarName "in" Expr ("," "$" VarName "in" Expr)* "satisfies")* IfExpr

Normalization

The quantification expressions are entirely normalized into other core expressions using the following normalization rules.

First, multiple variable quantifiers are normalized to single variable quantifiers.

 
[some Variable1 in Expr1, ..., Variablen in Exprn satisfies Expr]Expr
==
[
some Variable1 in Expr1 satisfies
   some Variable2 in Expr2 satistfies
         ...
     some Variablen in Exprn satistfies
     Expr
]Expr
 
[every Variable1 in Expr1, ..., Variablen in Exprn satisfies Expr]Expr
==
[
every Variable1 in Expr1 satisfies
   every Variable2 in Expr2 satistfies
         ...
     every Variablen in Exprn satistfies
     Expr
]Expr
 
[some Variable in Expr1 satisfies Expr2]Expr
==
xf:not( xf:empty(
   for Variable in [Expr1]Expr return
     if ( [ Expr2 ]Effective_Boolean_Value ) then 1
     else ()
   ))
 
[every Variable in Expr1 satisfies Expr2]Expr
==
xf:empty(
   for Variable in [Expr1]Expr return
     if ( xf:not( [ Expr2 ]Effective_Boolean_Value) ) then 1
     else ()
   )

Ed. Note: Note that the non-determinism in the semantics of quantified expressions is not modeled here. See [Issue-0136:  Non-determinism in the semantics].

Core Grammar

There are no core grammar rules for quantified expressions as they are normalized to other core expressions.

Static Type Analysis

There are no additional static type rules for the quantified expressions.

Dynamic Evaluation

There are no additional dynamic evaluation rules for the quantified expressions.

5.12 Expressions on SequenceTypes

Introduction

Expressions on SequenceTypes are expressions whose semantics depends on the type of some of the sub-expressions to which they are applied. The syntax of SequenceType expressions is described in [4.4.2 SequenceType].

5.12.1 Instance Of

[14 (XQuery)]   InstanceofExpr   ::=   ComparisonExpr ( <"instance" "of"> SequenceType )

Introduction

The SequenceType expression "Expr instance of SequenceType" is true if and only if the result of evaluating expression Expr is an instance of the type referred to by SequenceType.

Normalization

An "instance of" expression is normalized into a "typeswitch" expression. Note that the following normalization rule uses a variable $fs:new, which is a newly created variable which must not conflict with any variables already in scope. This variable is necessary to comply with the syntax of typeswitch expressions in the core [XPath/XQuery], but is never used.

 
[Expr instance of SequenceType]Expr
==
typeswitch ([ Expr ]Expr)
  case SequenceType $fs:new return xf:true()
  default $fs:new return xf:false()

Ed. Note: MFF: The "instance of" expression allows an optional "only" modifier. The use case for such a modifier is based on named typing, while the [XPath/XQuery] semantics is currently based on structural typing. It is not clear what the semantics of the "only" modifier under structural typing should be and how it can be supported. See [Issue-0111:  Semantics of instance of ... only].

5.12.2 Typeswitch

[12 (XQuery)]   TypeswitchExpr   ::=   (<"typeswitch" "("> Expr ")" CaseClause+ "default" ("$" VarName)? "return")* IfExpr
[38 (XQuery)]   CaseClause   ::=   "case" SequenceType ("$" VarName)? "return" Expr

Introduction

The typeswitch expression of XQuery allows users to perform different operations according to the type of an input expression.

Each branch of a typeswitch expression may have an optional "Variable" statement, used to bind a variable to the result of the input expression. This variable is optional in [XPath/XQuery] but mandatory in the [XPath/XQuery] core. One of the reasons for having this variable is that it can have a more specific type for the corresponding branch.

Normalization

Normalization of typeswitch expressions is applied to make sure an appropriate "Variable" is present in each branch.

The following general normalization rule merely adds a newly created variable which does not appear in the rest of the query. Note that $fs:new is a newly generated variable that must not conflict with any variables already in scope but is not used in any of the sub-expressions.

 
[
typeswitch ( Expr0 )
  case SequenceType1 return Expr1
    ···
  case SequenceTypen return Exprn
  default return Exprn+1
]Expr
==
typeswitch ( [ Expr0 ]Expr )
  case SequenceType1 $fs:new1 return [ Expr1 ]Expr
    ···
  case SequenceTypen $fs:newn return [ Exprn ]Expr
  default $fs:newn+1 return [ Exprn+1 ]Expr

Core Grammar

The core grammar productions for typeswitch are:

[10 (Core)]   TypeswitchExpr   ::=   (<"typeswitch" "("> Expr ")" CaseClause+ "default" "$" VarName "return")* IfExpr
[23 (Core)]   CaseClause   ::=   "case" SequenceType "$" VarName "return" Expr

Notation

The following auxiliary grammar production is used to identify branches of the typeswitch.

[57 (Formal)]   CaseRules   ::=   ("case" SequenceType "$" VarName "return" Expr CaseRules) |  ("default" "return" "$" VarName Expr)

Notation

The following judgment

dynEnv |- Value1 against CaseRules => Value2

is used in the dynamic semantics of typeswitch. It indicate that under the environment dynEnv, and with the input value of the typeswitch being "Value1", the given case rules yields the value Value2.

Notation

The following judgment

statEnv |- Type knowing (Type1 | ... | Typen) against CaseRules : Type2

is used in the static semantics of typeswitch. It indicates that under the type environment statEnv, with the input type of the typeswitch being "Type", and with the previously visited types Type1 | ... | Typen, the given case rules (e.g., "CaseRules") has type Type2. This typing judgment keep track of all previously visited types in the typeswitch. This additional information is used later on in typing the default clause.

Static Type Analysis

The typeswitch expression possesses one of the more complex sets of static typing rules. The rules account for the fact that if the static type of the conditional expression is known, then it is possible to determine statically that some of the case clauses do not apply, and thus do not contribute to the static type of a typeswitch expression.

Like the dynamic typeswitch rule, the static typeswitch rule relies upon auxiliary rules to determine the type of each of the case clauses and of the default clause. These auxiliary rules are provided after the main rule. Note that the type of the input expression is always treated as a sequence of prime types, using the "prime" and "quantifier" operations on types. This is necessary because the further typing rules compute the common prime types for each case clause of the type switch.

Ed. Note: Jerome: the use of the common prime types replaces the previous use of type intersection. Common prime types simplifies significantly the complexity in implementing typeswitch, but is less precise in certain cases.

statEnv |- Expr0 : Type0
CaseType0 = prime(Type0) · quantifier(Type0)
CaseType1 = [ SequenceType1 ]sequencetype
    ···
CaseTypen = [ SequenceTypen ]sequencetype
statEnv |- CaseType0 knowing () against case SequenceType1 Variable1 return Expr1 : Type1
    ···
statEnv |- CaseType0 knowing (CaseType1 | ... | CaseTypen-1) against case SequenceTypen Variablen return Exprn : Typen
statEnv |- CaseType0 knowing (CaseType1 | ... | CaseTypen) against default Variablen+1 return Exprn+1 : Typen+1

statEnv |-  
(typeswitch (Expr0)
  case SequenceType1 Variable1 return Expr1
    ···
  case SequenceTypen Variablen return Exprn
  default Variablen+1 return Exprn+1)
 : Type1 | ... | Typen+1

The rules that determine the static type of each case clause in the typeswitch are given next. In each rule, one needs to compute the "common prime types" between the input type and the case clause SequenceType.

The first rule is applied if the "common prime types" is none. In that case, it is known for sure the corresponding case clause is not evaluated and that the corresponding result type is none. Thanks to this rule, it is often possible to infer a precise type for the overall typeswitch by eliminating some of the cases.

CaseType = [ SequenceType ]sequencetype
common-prime(prime(CaseType0), prime(CaseType)) = none

statEnv |- CaseType0 knowing (CaseType1 | ... | CaseTyper)) against case SequenceType Variable return Expr : none

The second rule is applied if the "common prime types" is anything other than none. In that case, the input variable is added into the type environment and type inference is applied on the expression on the right-hand side of the case clause. Note that the type of the input variable is set to the "common prime types", and not to the input type.

CaseType = [ SequenceType ]sequencetype
Type0 = common-prime(prime(CaseType0), prime(CaseType))
Occurrence0 = common-occurrence(quantifier(CaseType0), quantifier(CaseType))
not(Type0 = none)
statEnv [ varType(Variable : (Type0 · Occurrence0)) ] |- Expr : Type1

statEnv |- CaseType0 knowing (CaseType1 | ... | CaseTyper)) against case SequenceType Variable return Expr : Type1

Note that these two rules do not take the visited datatypes into account. The "default" clause differs from the other clauses in that it does not specify a SequenceType. The typing rule for the "default" clause uses the visited type instead. Intuitively, the type corresponding to the "default" clause is any type but the ones in the other cases clauses.

Therefore, if the type of the input expression is a subtype of the choice of all visited types, then it is known for sure that the case clause is not evaluated and that the type of the default clause is none.

CaseType0 <: (CaseType1 | ... | CaseTypen)

statEnv |- CaseType0 knowing (CaseType1 | ... | CaseTyper)) against default Variable return Expr : none

Otherwise, the input variable is added into the type environment, and type inference is applied to the expression on the right-hand side of the default clause. Note that the type of the input variable is set to the input type of the expression.

not(CaseType0 <: (CaseType1 | ... | CaseTypen))
statEnv [ varType(Variable : CaseType0) ] |- Expr : Type1

statEnv |- CaseType0 knowing (CaseType1 | ... | CaseTyper)) against default Variable return Expr : Type1

Ed. Note: Jerome: There is an asymmetry here. It would be nicer to be able to have the type be more precise, like for the other case clauses. The technical problem is the need for some form of negation. I think one could define a "non-common-primes" function that would do the trick, but I leave that open for now until further review of the new typeswitch section is made. See [Issue-0112:  Typing for the typeswitch default clause].

Example

The typing rules for typeswitch provides reasonably precise type information in a number of useful cases. For example consider the following simple schema and query.

    <xs:element name="book">
       <xs:complexType>
          <xs:element name="title" type="xs:string"/>
          <xs:element name="author>
             <xs:complexType>
                <xs:element name="name" type="xs:string"/>
                <xs:element name="affiliation" type="xs:string"/>
             </xs:complexType>
          </xs:element>
       </xs:complexType>
    </xs:element>
    
    <xs:element name="bib">
       <xs:complexType>
          <xs:element ref="book" minOccurs="0" maxOccurs="unbounded"/>
       </xs:complexType>
    </xs:element>
    
    ...
    
    for $x in $bib/book/*
    return
       typeswitch $x
       case element author $a return $a/name
       case element editor $e return $e
       case element title $t return <wrote>{data($t)}</wrote>
       default return ()

The static rules for typeswitch can determine (1) that, with the given input schema, the second case matching against element editor never applies, and (2) that the data() function in the third case matching against element title, will not raise an error, because $e is guaranteed to contain data rather than more nodes. The resulting type corresponds to the following schema fragment.

    <xs:choice minOccurs="0" maxOccurs="unbounded">
       <xs:element name="name" type="xs:string"/>
       <xs:element name="wrote" type="xs:string"/>
    </xs:choice>

The type rules for typeswitch do not, however, account for the interdependence between successive case clauses. Thus if two case clauses had overlapping SequenceTypes, the static rules would behave as if both case clauses "fired", rather than just the first one.

Ed. Note: Jerome: It seems that the simpler version of typeswitch proposed here would actually allow us to take previous case clauses into account. This is something worth exploring as it would improve the static analysis in a way that might be helpful to users. See [Issue-0112:  Typing for the typeswitch default clause].

Ed. Note: Issue: There seem to be cases where the current semantics of typeswitch breaks type substitutability. See [Issue-0174:  Semantics of 'element foo of type T'].

Dynamic Evaluation

The evaluation of a typeswitch proceeds as follows. First, the input expression is evaluated, yielding an input value. Then the first case clause whose SequenceType type matches that value is selected and its corresponding expression is evaluated.

Note that the dynamic environmentdynEnv is only extended with this binding by the first auxiliary rule, which applies, if the input value matches the corresponding sequence type, or by the third auxiliary rule for the default case.

dynEnv |- Expr => Value0
dynEnv |- Value0 against CaseRules => Value1

dynEnv |- typeswitch (Expr) CaseRules => Value1

If the value matches the sequence type, the first auxiliary rule applies: It extends the environment by binding the variable Variable to Value0 and evaluates the body of the case rule.

CaseType = [ SequenceType ]sequencetype
Value0 matches CaseType
dynEnv [ varValue(Variable |-> Value0) ] |- Expr => Value1

dynEnv |- Value0 against case SequenceType Variable return Expr CaseRules => Value1

If the value does not match the sequence type, the second auxiliary rule evaluates on the remaining case rules, and the current case rule is not evaluated.

CaseType = [ SequenceType ]sequencetype      not (Value0 matches CaseType)      dynEnv |- Value0 against CaseRules => Value1

dynEnv |- Value0 against case SequenceType Variable return Expr CaseRules => Value1

Finally, the last rule states that the "default" branch of a typeswitch expression always evaluates to its given expression.

dynEnv [ varValue(Variable |-> Value0) ] Expr => Value1

dynEnv |- Value0 against default Variable return Expr => Value1

5.12.3 Cast and Treat

[30 (XQuery)]   CastExpr   ::=   (<"cast" "as"> |  <"treat" "as">) SequenceType ParenthesizedExpr
[30 (XPath)]   CastExpr   ::=   (<"cast" "as"> |  <"treat" "as">) SequenceType ParenthesizedExpr

Core Grammar

The core grammar production for cast as is:

[19 (Core)]   CastExpr   ::=   <"cast" "as"> SequenceType ParenthesizedExpr

Cast expressions are expressions that check or change the type of an expression against a given type.

5.12.3.1 Cast as

Introduction

The expression "cast as SequenceType ( Expr )" can be used to explicitly convert the result of an expression from one type to another. It changes both the type and value of the result of an expression, and can only be applied on an atomic value.

The semantics of cast expressions follows the specification given in Section [14. Casting Functions] of the [XQuery 1.0 and XPath 2.0 Functions and Operators] document. The casting table in Section [14. Casting Functions] of the [XQuery 1.0 and XPath 2.0 Functions and Operators] document indicates whether a cast is allowed or not. In case it is allowed, a specific cast function is applied, based on the input and output XML Schema simple types. The semantics of the cast function follows casting rules which are described in the the remainder of Section [14. Casting Functions] of the [XQuery 1.0 and XPath 2.0 Functions and Operators] document and is not specified further here.

Ed. Note: Jerome: The [XQuery 1.0 and XPath 2.0 Functions and Operators] document does not provide any function for casting, just a table and casting rules. It would be preferable to either have an explicit function to normalize to, or to put the semantics of casts in the Formal Semantics. This relates to Issue 17 in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document.

Normalization

Cast operations perform atomization. This is captured during normalization, as specified by the following rule.

 
[cast as SequenceType (Expr)]Expr
==
let $v := [ Expr ]Atomize return
  cast as SequenceType ($v)

Notation

The following auxiliary judgments are used to represent access to the casting table and to the semantics of casting, as described in Section [14. Casting Functions] of the [XQuery 1.0 and XPath 2.0 Functions and Operators] document.

The judgment:

Type1 cast allowed Type2 => { Y, M, N }

holds if casting from type Type1 to Type2 is always possible (Y), may be possible (M), or is not allowed (N).

The notation:

cast as Type2 ( Value1 ) => Value2

indicates that applying the casting rules for Type2 on Value1 yields the value Value2.

Static Type Analysis

If the cast table indicates the cast is not allowed (N), the system raises a static type error. Otherwise, the following static typing rules give the static semantics of "cast as" expression. Two cases are distinguished: if the static type of the expression Type1 can be the empty sequence, then the static output type of the cast is the given type Type2 made optional. Otherwise the static output type is the given type Type2

statEnv |- Expr : Type1
quantifier(Type1) = ? or quantifier(Type1) = *
Type2 = [ SequenceType2 ]sequencetype
Type1 cast allowed Type2 => Y or Type1 cast allowed Type2 => M

statEnv |- cast as SequenceType2 (Expr) : Type2 ?

statEnv |- Expr : Type1
quantifier(Type1) != ?     quantifier(Type1) != *
Type2 = [ SequenceType2 ]sequencetype
Type1 cast allowed Type2 => Y or Type1 cast allowed Type2 => M

statEnv |- cast as SequenceType2 (Expr) : Type2

Dynamic Evaluation

If the cast is allowed (Y or M), the following evaluation rule applies the casting rules on the result of the input expression. The rule uses the data model function dm:type in order to obtain the dynamic type of the input value, SequenceType normalization to obtain the output type, and the above auxiliary judgments to check whether the cast is allowed and to apply the casting rules.

dynEnv |- Expr1 => Value1
Type2 = [ SequenceType2 ]sequencetype
cast as Type2 ( Value1 ) => Value2

dynEnv |- cast as SequenceType2 ( Expr1 ) => Value2

Note that in the case that the casting table indicates "M", the casting operation is allowed but might fail at run-time if the input value is inappropriate (e.g. attempting to cast the string "VRAI" into xs:boolean). In that case, the dynamic evaluation returns an error value.

If the casting table returns "N", the cast is not allowed and the dynamic semantics always returns an error value.

dynEnv |- Expr1 => Value1
dm:type(Value1) = Type1
Type2 = [ SequenceType2 ]sequencetype
Type1 cast allowed Type2 => N

dynEnv |- cast as SequenceType2 ( Expr1 ) => xf:error()

5.12.3.2 Treat as

Introduction

The expression "treat as SequenceType ( Expr )", can be used to change the static type of the result of an expression without changing its value. Treat as raises a static type error, if the static type of expression and the specified type are incompatible. Treat as raises a run-time error, if the dynamic type of the expression is not an instance of the specified type.

Normalization

Treat as expressions are normalized to typeswitch expressions. Note that the following normalization rule uses a variable $fs:new, which is a newly created variable which must not conflict with any variables already in scope.

 
[treat as SequenceType ( Expr )]Expr
==
typeswitch ([ Expr ]Expr) as $fs:new
  case SequenceType return $fs:new
  default return xf:error()

5.13 Validate Expressions

[29 (XQuery)]   ValidateExpr   ::=   "validate" SchemaContext? "{" Expr "}"

Core Grammar

The core grammar production for validate is:

[18 (Core)]   ValidateExpr   ::=   "validate" SchemaContext? "{" Expr "}"

A validate expression validates its argument with respect to the in-scope schema definitions, using the schema validation process described in [XML Schema]. The argument to a validate expression may be any sequence of elements. Validation replaces element and attribute nodes with new nodes that have their own identity and contain type annotations and defaults created by the validation process. If a node that has a parent is validated, the parent of the original node will not be the parent of the validated node.

Static Type Analysis

Ed. Note: Issue: The current form of validate cannot be typed statically. See [Issue-0166:  Static typing for validate].

Dynamic Evaluation

An important effect of validation is that it removes existing type annotations and values (erasure), and it revalidates the corresponding data model instance, possibly adding new type annotations and values (annotation). Both erasure and annotation are described formally in [3.4 Erase and Annotate]. Indeed, the conjunction of erasure and annotation provides a formal model for a large part of actual schema validation. The semantics of the "validate" operation is (partially) specified as follows.

dynEnv.varValue |- Expr => Value1
Value1 erases to element ElementName { Value2 }
annotate as element ElementName (element ElementName { Value2 }) => Value3

dynEnv |- validate element ElementName { Expr } => Value3

Ed. Note: Issue: This semantics only applies when validating against a top-level element. See [Issue-0138:  Semantics of Schema Context]

6 The Query Prolog

Introduction

The Query Prolog is a series of declarations and definitions that affect query processing. The Query Prolog can be used to define namespaces, import type definitions from XML Schemas, and define functions. Namespace declarations and schema imports always precede function definitions, as specified by the following grammar productions.

[1 (XQuery)]   Query   ::=   QueryProlog QueryBody
[2 (XQuery)]   QueryProlog   ::=   (NamespaceDecl
|  XMLSpaceDecl
|  DefaultNamespaceDecl
|  DefaultCollationDecl
|  SchemaImport)* FunctionDefn*
[3 (XQuery)]   QueryBody   ::=   ExprSequence?

The order in which functions are defined is immaterial. Notably, user-defined functions may invoke other user-defined functions in any order.

Namespace Declarations and Schema Import are not part of the query proper but are used to modify the input context for the rest of the query processing. Namespace Declarations and Schema Import are processed before the normalization phase.

The semantics of Schema Import is described in terms of the XQuery type system. The process of converting an XML Schema into a sequence of type declarations is described in Section [8 Importing Schemas]. This section describes how the resulting sequence of type declarations is added into the static environment when the prolog is processed.

Notation

Prolog declarations are either namespace declarations or type declarations.

[58 (Formal)]   PrologDeclList   ::=   PrologDecl*
[59 (Formal)]   PrologDecl   ::=   NamespaceDecl
|  XMLSpaceDecl
|  DefaultNamespaceDecl
|  DefaultCollationDecl
|  SchemaImport

Notation

The following auxiliary judgments are used when processing the [XPath/XQuery] prolog.

The judgment:

PrologDeclList => statEnv

holds if the sequence of prolog declarations PrologDeclList yields the static environment statEnv.

The judgment:

statEnv1 |- PrologDecl => statEnv2

holds if under the static environment statEnv1, the single prolog declarations PrologDeclList yields the new static environment statEnv2.

Context Processing

Prolog declarations are processed in the order they are encountered, as described by the following inference rules. The first rule specifies that for an empty sequence of prolog declarations, the static environment is composed of a default context.

Ed. Note: Jerome: What do the default namespace and type environments contain? I believe at least the default namespace environment should contain the "xs", "xf" and "op" prefixes, as well as the default namespaces bound to the empty namespace. Should the default type environment contain wildcard types? See [Issue-0115:  What is in the default context?].


() => statEnvDefault

PrologDeclList => statEnv1
statEnv1 |- PrologDecl => statEnv2

PrologDecl PrologDeclList => statEnv2

6.1 Namespace Declarations

[84 (XQuery)]   NamespaceDecl   ::=   <"declare" "namespace"> NCNameForPrefix "=" URLLiteral
[86 (XQuery)]   DefaultNamespaceDecl   ::=   (<"default" "element"> |  <"default" "function">) "namespace" "=" URLLiteral

Context Processing

A namespace declaration adds a new (prefix,uri) binding in the namespace component of the static environment.

statEnv1 = statEnv [ namespace(NCName |-> StringLiteral) ]

statEnv |- namespace NCName = StringLiteral => statEnv1

A default element namespace declaration changes the default element namespace prefix binding in the namespace component of the static environment.

statEnv1 = statEnv [ namespace(fsdefaultelem |-> StringLiteral) ]

statEnv |- default element namespace = StringLiteral => statEnv1

A default function namespace declaration changes the default function namespace prefix binding in the namespace component of the static environment.

statEnv1 = statEnv [ namespace(fsdefaultfunc |-> StringLiteral) ]

statEnv |- default function namespace = StringLiteral => statEnv1

Note that for namespaces, later declarations can override earlier declarations of the same prefix.

6.2 Schema Imports

[89 (XQuery)]   SchemaImport   ::=   <"import" "schema"> (StringLiteral |  SubNamespaceDecl |  DefaultNamespaceDecl) <"at" StringLiteral>?
[85 (XQuery)]   SubNamespaceDecl   ::=   "namespace" NCNameForPrefix "=" URLLiteral

Notation

The following auxiliary judgments are used when processing schema imports.

The judgment:

statEnv1 |- Definition* => statEnv2

holds if under the static environment statEnv1, the sequence of type definitions Definition* yields the new static environment statEnv2.

The judgment:

statEnv1 |- Definition => statEnv2

holds if under the static environment statEnv1, the single definition Definition yields the new static environment statEnv2.

Context Processing

Schema imports are first imported into the query type system and yield a sequence of type definitions. Then each type definitions is added to the static environment.

Definition* = [Schema]Schema
statEnv |- Definition* => statEnv1

statEnv |- import schema Schema => statEnv1

An empty sequence of definitions yields the original environment.


statEnv |- () => statEnv

Each definition is added into the static environment.

statEnv |- Definition* => statEnv1
statEnv1 |- Definition1 => statEnv2

Definition1 Definition* => statEnv2

Type, element and attribute declarations are added respectively to the type, element and attribute declarations components of the static environment.

statEnv1 = statEnv [ typeDefn(TypeName |-> define type TypeName TypeDerivation ) ]

statEnv |- define type TypeName TypeDerivation => statEnv1

statEnv1 = statEnv [ elemDecl(ElementName |-> define element ElementName Substitution? Nillable? TypeSpecifier) ]

statEnv |- define element ElementName Substitution? Nillable? TypeSpecifier => statEnv1

statEnv1 = statEnv [ attrDecl(AttributeName |-> define attribute AttributeName TypeSpecifier) ]

statEnv |- define attribute AttributeName TypeSpecifier => statEnv1

Note that for namespaces, later declarations can override earlier declarations of the same prefix. In the case of global elements, attributes and types, multiple declarations correspond to an error.

6.3 Xmlspace Declaration

[82 (XQuery)]   XMLSpaceDecl   ::=   <"declare" "xmlspace"> "=" ("preserve" |  "strip")

The impact of xmlspace declaration is not formally specified in this document.

6.4 Default Collation

[83 (XQuery)]   DefaultCollationDecl   ::=   <"default" "collation" "="> URLLiteral

The impact of default collation is not formally specified in this document. See [Issue-0160:  Collations in the static environment].

6.5 Function Definitions

Introduction

User defined functions specify the name of the function, the names and types of the parameters, and the type of the result. The function body defines how the result of the function is computed from its parameters.

[87 (XQuery)]   FunctionDefn   ::=   <"define" "function"> FuncName "(" ParamList? (")" |  (<")" "returns"> SequenceType)) EnclosedExpr
[88 (XQuery)]   ParamList   ::=   Param ("," Param)*
[59 (XQuery)]   Param   ::=   SequenceType? "$" VarName

Notation

The following auxiliary mapping rule is used for the normalization of parameters in function definitions: []Param.

Normalization

The only form of normalization required for user defined functions is adding the type for its parameters or for the return clause if it is not provided.

 
[ define function QName ( ParamList? ) returns SequenceType EnclosedExpr ]Expr
==
define function [QName] ( [ParamList?]Param ) returns SequenceType [EnclosedExpr]Expr

If the return type of the function is not provided, it is given the item* sequence type.

 
[define function QName ( ParamList? ) EnclosedExpr ]Expr
==
define function [QName] ( [ParamList?]Param ) returns item* [EnclosedExpr]Expr

Parameters without a declared typed are given the item* sequence type.

 
[Variable]Param
==
item* Variable
 
[SequenceType Variable]Param
==
SequenceType Variable

Context Processing

First, all the function signatures are added into the static environment, and all the function bodies are added into the dynamic environment. This process happens before static type analysis occurs.

FunctionDefnList => statEnv, dynEnv
statEnv' = statEnv [ funcType(QName |-> ( SequenceType1 , ··· SequenceTypen , SequenceTyper)) ]
dynEnv' = dynEnv [ funcDefn(QName |-> ( Expr , Variable1 , ··· Variablen)) ]

FunctionDefnList define function QName ( SequenceType1 Variable1, ··· SequenceTypen Variablen )
returns SequenceTyper
{ Expr } => statEnv', dynEnv'

Static Type Analysis

The static typing rules for function definitions checks whether the type of the enclosed expression is consistent with the type of the input parameters, and the type of the return clause.

statEnv [ varType( Variable1 : SequenceType1 ;...; Variablen : SequenceTypen ) ] |- Expr : Type
Type <: SequenceTyper

statEnv |- define function QName ( SequenceType1 Variable1 , ··· SequenceTypen Variablen )
returns SequenceTyper
{ Expr }

What this typing rule is checking is: if the input parameters are of the given type, then is it true that the result of the function is of the return type. If the type checking fails, the system raises an error. Otherwise, it does not have any other effect, as function signatures are already inside the static environment.

Dynamic Evaluation

There is no need to describe a dynamic semantics at this point, as functions are only evaluated when called. The actual semantics of function calls is described in [5.1.4 Function Calls].

7 Additional Semantics of Functions

Ed. Note: Status: This section is still incomplete. This section will be completed as soon as Sections 4 and 5 are consolidated. See [Issue-0135:  Semantics of special functions].

As was explained in section [2.5 Functions], a number of functions play a role in defining the formal semantics of [XPath/XQuery]. Some other functions from the [XQuery 1.0 and XPath 2.0 Functions and Operators] document need special static typing rules. This section gives the semantics of all "special" functions, used in the formal semantics.

7.1 Formal Semantics Functions

Introduction

This section gives the definition and semantics of functions which are used in the formal semantics but are not part of the [XQuery 1.0 and XPath 2.0 Functions and Operators] document.

7.1.1 The fs:characters-to-string function

The fs:characters-to-string function takes a sequence of character values and synthecizes a string.

7.1.2 The fs:distinct-doc-order function

The fs:distinct-doc-order function sorts by document order and removes duplicates. It is defined as the composition of the [XQuery 1.0 and XPath 2.0 Functions and Operators] functions xf:distinct-nodes and sorting by document order.

The dynamic semantics of fs:distinct-doc-order cannot be specified as a simple sortby expression. See [Issue-0168:  Sorting by document order].

7.1.3 The fs:item-sequence-to-node-sequence function

The fs:item-sequence-to-node-sequence function converts a sequence of item values to nodes by applying the rules in Section [3.7.2 Data Model Representation] in .

7.1.4 The fs:item-sequence-to-string function

The fs:item-sequence-to-node-sequence function converts a sequence of item values to a string by applying the rules in Section [3.7.2 Data Model Representation] in .

In particular, each node is replaced by its string value. For each adjacent sequence of one or more atomic values returned by an enclosed expression, a string is constructed, containing the canonical lexical representation of all the atomic values, with a single blank character inserted between adjacent values.

7.2 Functions with specific typing rules

7.2.1 The xf:error function

Static Type Analysis

The xf:error function always returns the none type.


statEnv |- xf:error() : none

7.2.2 The xf:distinct-nodes, and xf:distinct-values functions

Static Type Analysis

The xf:distinct-nodes function takes a sequence of nodes as input and returns a sequence of prime types.

statEnv |- Expr : Type
statEnv |- Type <: node*

statEnv |- xf:distinct-nodes(Expr) : prime(Type) · quantifier(Type)

The xf:distinct-values function takes a sequence of atomic values as input and returns a sequence of prime types.

statEnv |- Expr : Type
statEnv |- Type <: atomic value*

statEnv |- xf:distinct-values(Expr) : prime(Type) · quantifier(Type)

7.2.3 The op:union, op:intersect and op:except operators

Static Type Analysis

The static semantics for op:union uses the auxiliary type functions prime(Type) and quantifier(Type); which are defined in [3.6 Auxiliary typing judgments for for, unordered, and sortby expressions]. The type of each argument is determined, and then prime(.) and quantifier(.) are applied to the sequence type (Type1, Type2).

statEnv |- Expr1 : Type1      statEnv |- Expr2 : Type2

statEnv |- op:union(Expr1, Expr2) : prime(Type1 , Type2) · quantifier(Type1 , Type2)

The static semantics of op:intersect is analogous to that for op:union, but uses the common-prime and common-occurrence operations. Because an intersection may always be empty, the result type needs to be made optional.

statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
statEnv |- PrimeType3 = common-prime(prime(Type1), prime(Type2))
statEnv |- Occurrence3 = common-occurrence(quantifier(Type1), quantifier(Type2))

statEnv |- op:intersect(Expr1, Expr2) : PrimeType3 · Occurrence3 ?

The static semantics of op:except follows. The type of the second argument is ignored as it does not contribute to the result type. Like with op:intersect the result of op:except may be the empty list.

statEnv |- Expr1 : Type1

statEnv |- op:except(Expr1, Expr2) : prime(Type1) · quantifier(Type1) · ?

7.2.4 The op:to operator

The static semantics of the op:to function states that it always returns an integer sequence:

statEnv |- Expr1 : xs:integer      statEnv |- Expr2 : xs:integer

statEnv |- op:to(Expr1, Expr2) : xs:integer*

Ed. Note: MFF: the binary operator "to" is not defined on empty sequences. The [XQuery 1.0 and XPath 2.0 Functions and Operators] document says operands are decimals, while the XQuery document says they are integers. What happens when Expr1 > Expr2? See [Issue-0119:  Semantics of op:to].

7.2.5 The xf:data function

Introduction

The xf:data function is used to access the value content of an element or attribute. This function corresponds to the dm:typed-value accessor in the [XPath/XQuery] data model.

Ed. Note: Some aspects of the semantics of the xf:data() function are still an open issue. For instance, what should be the result of xf:data() over a text node. See [Issue-0107:  Semantics of data()].

Notation

Infering the type for the xf:data function is done by applying the xf:data function as a Filter, using the same approach as for the XPath steps.

The following notation, adapted from the Filter judgment in [5.2.1 Steps], is used.

dynEnv.varValue ; Type1 |- xf:data : Type2

Static Type Analysis

Static type analysis for the xf:data function checks that the function is applied on an element or a