W3C

XQuery 1.0 and XPath 2.0 Formal Semantics

W3C Working Draft 22 August 2003

This version:
http://www.w3.org/TR/2003/WD-xquery-semantics-20030822/
Latest version:
http://www.w3.org/TR/xquery-semantics/
Previous versions:
http://www.w3.org/TR/2003/WD-xquery-semantics-20030502/ http://www.w3.org/TR/2002/WD-query-semantics-20021115/ http://www.w3.org/TR/2002/WD-query-semantics-20020816/ 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), Bell Labs, Lucent Technologies <simeon@research.bell-labs.com>
Philip Wadler (XML Query WG), Avaya <wadler@avaya.com>

Abstract

This document defines formally the 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 section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.

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

Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress. It contains a number of 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.

This version reflects the most recent semantics of [XPath/XQuery]. Among the most important changes from the previous version of this document are:

Public feedback is requested on the remaining open XPath issues: Issue 481 (Semantics of Schema Context), Issue 496 (Support for lax and strict wildcards), Issue 555 (Formal Semantics of Module Import), Issue 556 (Formal Semantics of Variable Definitions), Issue 557 (Formal semantics of Validation Declaration), and Issue 559 (New Sequence Type needs to be fully implemented in Formal Semantics).

This Working Draft references the Last Call Working Drafts of [XQuery 1.0 and XPath 2.0 Functions and Operators] and [XQuery 1.0 and XPath 2.0 Data Model]. Since these Last Call Working Drafts are not being re-published along with this Working Draft, it is possible that some differences may exist between this Working Draft and the Last Call Working Drafts. The public is encouraged to provide feedback on any differences that they find. The Working Groups are planning to publish a set of synchronized documents as early as possible.

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 and the XSL Working Group (both part of the XML 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 Introduction to the Formal Semantics
        2.1.1 Notations from grammar productions
        2.1.2 Notations for judgments
        2.1.3 Notations for inference rules
        2.1.4 Notations for environments
        2.1.5 Putting it together
    2.2 XML Values
        2.2.1 Formal values
        2.2.2 Examples of values
    2.3 The [XPath/XQuery] Type System
        2.3.1 XML Schema and the [XPath/XQuery] Type System
        2.3.2 Item types
        2.3.3 Content models
        2.3.4 Top level definitions
        2.3.5 Example of a complete Schema
    2.4 Processing model and main judgments
        2.4.1 Processing model
        2.4.2 Normalization judgment
        2.4.3 Static typing judgment
        2.4.4 Dynamic evaluation judgment
    2.5 Relationship with other documents
        2.5.1 Namespaces
        2.5.2 Functions and operators
3 Basics
    3.1 Expression Context
        3.1.1 Static Context
            3.1.1.1 Predefined Types
        3.1.2 Dynamic Context
    3.2 Processing Model
    3.3 Important Concepts
        3.3.1 Document Order
        3.3.2 Typed Value and String Value
        3.3.3 Input Sources
    3.4 Types
        3.4.1 SequenceType
            3.4.1.1 SequenceType Matching
        3.4.2 Type Conversions
            3.4.2.1 Atomization
            3.4.2.2 Effective Boolean Value
            3.4.2.3 XPath 1.0 Backward Compatibility
    3.5 Errors Handling
    3.6 Optional Features
        3.6.1 Basic XQuery
        3.6.2 Schema Import Feature
        3.6.3 Static Typing Feature
        3.6.4 Extensions
            3.6.4.1 Pragmas
            3.6.4.2 Must-Understand Extensions
            3.6.4.3 XQuery Flagger
4 Expressions
    4.1 Primary Expressions
        4.1.1 Literals
        4.1.2 Variables
        4.1.3 Parenthesized Expressions
        4.1.4 Context Item Expression
        4.1.5 Function Calls
        4.1.6 [XPath/XQuery] Comments
    4.2 Path Expressions
        4.2.1 Steps
            4.2.1.1 Axes
            4.2.1.2 Node Tests
        4.2.2 Predicates
        4.2.3 Unabbreviated Syntax
        4.2.4 Abbreviated Syntax
    4.3 Sequence Expressions
        4.3.1 Constructing Sequences
        4.3.2 Combining Sequences
    4.4 Arithmetic Expressions
    4.5 Comparison Expressions
        4.5.1 Value Comparisons
        4.5.2 General Comparisons
        4.5.3 Node Comparisons
        4.5.4 Order Comparisons
    4.6 Logical Expressions
    4.7 Constructors
        4.7.1 Direct Element Constructors
            4.7.1.1 Attributes
            4.7.1.2 Namespaces
            4.7.1.3 Content
            4.7.1.4 Whitespace in Element Content
            4.7.1.5 Type of a Constructed Element
        4.7.2 Other Direct Constructors
        4.7.3 Computed Constructors
            4.7.3.1 Computed Element Constructors
            4.7.3.2 Computed Attribute Constructors
            4.7.3.3 Document Node Constructors
            4.7.3.4 Text Nodes Constructors
            4.7.3.5 Computed Processing Instruction Constructors
            4.7.3.6 Computed Comment Constructors
            4.7.3.7 Computed Namespace Constructors
    4.8 [For/FLWR] Expressions
        4.8.1 FLWOR expressions
        4.8.2 For expression
        4.8.3 Let Expression
        4.8.4 Order By and Return Clauses
    4.9 Unordered Expressions
    4.10 Conditional Expressions
    4.11 Quantified Expressions
    4.12 Expressions on SequenceTypes
        4.12.1 Instance Of
        4.12.2 Typeswitch
        4.12.3 Cast
        4.12.4 Castable
        4.12.5 Constructor Functions
        4.12.6 Treat
    4.13 Validate Expressions
5 Modules and Prologs
    5.1 Version Declaration
    5.2 Namespace Declarations
    5.3 Default Namespace Declarations
    5.4 Schema Imports
    5.5 Module Imports
    5.6 Variable Definitions
    5.7 Validation Declaration
    5.8 Xmlspace Declaration
    5.9 Default Collation
    5.10 Function Definitions
6 Additional Semantics of Functions
    6.1 Formal Semantics Functions
        6.1.1 The fs:distinct-doc-order function
        6.1.2 The fs:item-sequence-to-node-sequence function
        6.1.3 The fs:item-sequence-to-untypedAtomic function
        6.1.4 The fs:convert-simple-operand function
        6.1.5 The fs:convert-operand function
        6.1.6 The arithmetic operator pseudo-functions: fs:minus, fs:plus, fs:times, fs:idiv, fs:div, and fs:mod
        6.1.7 The comparison pseudo-functions: fs:eq, fs:ne, fs:lt, fs:le, fs:gt, and fs:ge
    6.2 Standard functions with specific typing rules
        6.2.1 The fn:error function
        6.2.2 The fn:distinct-nodes and fn:distinct-values functions
        6.2.3 The fn:collection and fn:doc functions
        6.2.4 The op:union, op:intersect, and op:except operators
        6.2.5 The fn:data function
        6.2.6 The fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions
        6.2.7 The fn:subsequence, and fn:remove functions
        6.2.8 The fn:min fn:max, fn:avg, and fn:sum functions
7 Auxiliary Judgments
    7.1 Judgments for schema contexts
        7.1.1 Mode is
        7.1.2 Context is
    7.2 Judgments for accessing types
        7.2.1 Derives
        7.2.2 Substitutes
        7.2.3 Element and attribute type lookup
        7.2.4 Static element and attribute type lookup
        7.2.5 Extension
        7.2.6 Type adjustment
        7.2.7 Type expansion
    7.3 Judgments for step expressions and filtering
        7.3.1 Principal Node Kind
        7.3.2 Auxiliary judgments for axis
            7.3.2.1 Static semantics of axis
            7.3.2.2 Dynamic semantics of axis
        7.3.3 Auxiliary judgments for node tests
            7.3.3.1 Static typing of node tests
            7.3.3.2 Dynamic semantics of node tests
        7.3.4 Attribute filtering
    7.4 Judgments for type matching
        7.4.1 Matches
        7.4.2 Subtype
    7.5 Judgments for sequences of item types
    7.6 Judgments for type promotion
    7.7 Judgments for the validate expression
        7.7.1 Builtin attributes
        7.7.2 Mixed content
        7.7.3 Type resolution
        7.7.4 Interleaving
        7.7.5 Erasure
            7.7.5.1 Simply erases
            7.7.5.2 Erases
        7.7.6 Annotate
            7.7.6.1 Simply annotate
            7.7.6.2 Nil-annotate
            7.7.6.3 Annotate
        7.7.7 Validates as
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.1.5 Anonymous type names
    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 BNF
B Functions and Operators
    B.1 Functions and Operators used in the Formal Semantics
    B.2 Mapping of Overloaded Internal Functions
C References
    C.1 Normative References
    C.2 Non-normative References
    C.3 Background References
D XQuery 1.0 and XPath 2.0 Issues


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:

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

This document defines the semantics of [XPath/XQuery] by giving a precise formal meaning to each of the expressions 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. [XPath/XQuery] is built from expressions, rather than statements. Every construct in the language (except for the XQuery 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 that describe the input documents and the output document, and the [XPath/XQuery] language can then perform operations based on these types. In addition, [XPath/XQuery] supports static type analysis. This means a static analysis phase is defined on [XPath/XQuery] expressions that infers the output type of an expression, based on the type of its inputs. Static typing allows early detection of type errors, and can be used as the basis for certain forms of optimization. The [XPath/XQuery] type system captures 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.

This document is organized as follows. [2 Preliminaries] introduces the notations used to define the [XPath/XQuery] formal semantics. These include the formal notations for values in the [XPath/XQuery] data model and for types in XML Schema. The next three sections: [3 Basics], [4 Expressions], and [5 Modules and Prologs] have the same structure as the corresponding sections in the [XQuery 1.0: A Query Language for XML] and [XML Path Language (XPath) 2.0] documents. This allows the reader to quickly find the formal definition of a particular language construct. [3 Basics] defines the semantics for basic [XPath/XQuery] concepts, and [4 Expressions] defines the dynamic and static semantics of each [XPath/XQuery] expression. [5 Modules and Prologs] defines the semantics of the [XPath/XQuery] prolog. [6 Additional Semantics of Functions] defines the static semantics of several functions in [XQuery 1.0 and XPath 2.0 Functions and Operators] and gives the dynamic and static semantics of several supporting functions used in this document. The remaining sections, [7 Auxiliary Judgments] and [8 Importing Schemas], contain material that supports the formal semantics of [XPath/XQuery]. [7 Auxiliary Judgments] defines formal judgments that relate data model values to types, that relate types to types, and that support the formal definition of validation. These judgements are used in the definition of expressions in [4 Expressions]. Lastly, [8 Importing Schemas], specifies how XML Schema documents are imported into the [XPath/XQuery] type system and relates XML Schema types to 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 Introduction to the Formal Semantics

Why a Formal Semantics? The goal of the formal semantics is to complement the [XPath/XQuery] specification ([XQuery 1.0: A Query Language for XML] and [XML Path Language (XPath) 2.0]), by defining the meaning of [XPath/XQuery] expressions with mathematical rigor.

A rigorous formal semantics clarifies the intended meaning of the English specification, ensures that no corner cases are left out, and provides a reference for implementation.

Why use formal notations? Rigor is achieved by the use of formal notations to represent [XPath/XQuery] objects such as expressions, XML values, and XML Schema types, and by the systematic definition of the relationships between those objects to reflect the meaning of the language. In particular, the dynamic semantics relates [XPath/XQuery] expressions to the XML value to which they evaluate, and the static semantics relates [XPath/XQuery] expressions to the XML Schema type that is infered for that expression.

The Formal Semantics uses several kinds of formal notations to define the relationships between [XPath/XQuery] expressions, XML values, and XML Schema types. This section contains a small tutorial to introduce the notations for judgments, inference rules, and mapping rules as well as the notation for environments, which implement the dynamic and static contexts. The reader already familiar with these notations can skip this section and continue with [2.2 XML Values].

2.1.1 Notations from grammar productions

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

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

[For/FLWR] Expressions
[42 (XQuery)]   FLWORExpr   ::=   (ForClause | LetClause)+ WhereClause? OrderByClause? "return" ExprSingle

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

[For/FLWR] Expressions
[25 (XPath)]   ForExpr   ::=   SimpleForClause "return" ExprSingle

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.

For Expressions

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

Type Definitions
[43 (Formal)]   Definition   ::=   ("define" "element" ElementName Substitution? Nillable? TypeReference)
| ("define" "attribute" AttributeName TypeReference)
| ("define" "type" TypeName TypeDerivation)

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

2.1.2 Notations for judgments

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

For example:

Notation

The judgment

Painting is beautiful

holds if the object Painting is beautiful.

Notation

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

The judgment

Expr => Value

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

The judgment

Expr : Type

holds when the expression Expr has type Type.

The judgment

Expr raises Error

holds when the expression Expr raises the error Error.

A judgment can contain symbols and patterns.

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

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

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

Patterns may appear with subscripts (e.g. Expr1, Expr2) to distinguish different instances of the same sort of pattern. Each distinct pattern must be instantiated to a single "object" (value, type, expression, etc.). If the same pattern occurs twice in a judgment description then it should be instantiated with the same "object". For example, '3 => 3' is an instance of the judgment 'Expr1 => Expr1' but '$x+0 => 3' is not since the two expressions '$x+0' and '3' cannot be both instance of the pattern Expr1. The judgment'$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.1.3 Notations for inference rules

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

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

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

Note

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

2.1.4 Notations for environments

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

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

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

This document uses environment groups that group related environments. If "env" is an environment group with the member "mem", then that environment is denoted "env.mem" and the value that it maps symbol to is denoted "env.mem(symbol)".

Updating is only defined on environment groups:

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

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

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

    This notation is equivalent to nested updates, as in " (env + mem( 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 a symbol (e.g., a variable, a namespace prefix, etc.) Also, note that there are no operations to remove entries from environments: this is never necessary because updating an the environment group effectively creates a new extended copy of the original environment group, and the original environme group remains accessible along with the updated copy.

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

For instance, the judgment

dynEnv |- Expr => Value

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

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

2.1.5 Putting it together

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

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

statEnv |- Expr1 , Expr2 : Type1, Type2

This rule is read as follows: if two expressions Expr1 and Expr2 are known to have the static types 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 static 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" 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 is as follows: First, the type Type1 for the "let" input expression Expr1 is computed. Second the "let" variable is added into the varType component of the static environment group statEnv, with type Type1. Finally, the type Type2 of Expr2 is computed in that new environment.

Editorial note 
Jonathan suggests that we should explain 'chain' inference rules. I.e., how several inference rules are applied recursively.

2.2 XML Values

[XPath/XQuery] manipulates XML values as defined in the [XQuery 1.0 and XPath 2.0 Data Model]. XML values are composed of nodes, atomic values and sequences. This section introduces formal notations for describing [XPath/XQuery] values from [XQuery 1.0 and XPath 2.0 Data Model]. These notations are used to describe and manipulate values in inference rules, but are not exposed to the [XPath/XQuery] user.

2.2.1 Formal values

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

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

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

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

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

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

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

  element weight of type xs:integer { text { "42" } } {}
  element weight of type xs:integer { text { "42" } } 
Values
[14 (Formal)]   Value   ::=   Item
| (Value "," Value)
| ("(" ")")
[25 (Formal)]   Item   ::=   NodeValue
| AtomicValue
[26 (Formal)]   AtomicValue   ::=   AtomicValueContent TypeAnnotation
[7 (Formal)]   AtomicValueContent   ::=   String
| Boolean
| Decimal
| Float
| Double
| Duration
| DateTime
| Time
| Date
| GYearMonth
| GYear
| GMonthDay
| GDay
| GMonth
| HexBinary
| Base64Binary
| AnyURI
| QName
| NOTATION
[8 (Formal)]   TypeAnnotation   ::=   "of" "type" TypeName
[16 (Formal)]   ElementValue   ::=   "element" ElementName "nilled"? TypeAnnotation "{" Value "}" "{" NamespaceAnnotations "}"
[17 (Formal)]   AttributeValue   ::=   "attribute" AttributeName TypeAnnotation "{" SimpleValue "}"
[15 (Formal)]   SimpleValue   ::=   AtomicValue
| (SimpleValue "," SimpleValue)
| ("(" ")")
[18 (Formal)]   DocumentValue   ::=   "document" "{" Value "}"
[20 (Formal)]   CommentValue   ::=   "comment" "{" String "}"
[21 (Formal)]   ProcessingInstructionValue   ::=   "processing-instruction" QName "{" String "}"
[19 (Formal)]   TextValue   ::=   "text" "{" String "}"
[24 (Formal)]   NodeValue   ::=   ElementValue
| AttributeValue
| DocumentValue
| TextValue
| CommentValue
| ProcessingInstructionValue
[9 (Formal)]   ElementName   ::=   QName
[12 (Formal)]   AttributeName   ::=   QName
[27 (Formal)]   TypeName   ::=   QName | AnonymousTypeName
[13 (Formal)]   AnonymousTypeName   ::=   [Anon1] | [Anon2] | ...
[22 (Formal)]   NamespaceAnnotations   ::=   NamespaceAnnotation ... NamespaceAnnotation
[23 (Formal)]   NamespaceAnnotation   ::=   "namespace" NCName "{" AnyURI "}"

Notation

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

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

2.2.2 Examples of values

A well-formed document

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

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

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

A document before and after validation.

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

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

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

After validation, this element is represented as:

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

An element with a list type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xs:anyType {
    text { "1 2 3" }
  }

Assume the following Schema.

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

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

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

An element with an anonymous type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xs:anyType {
    text { "1 2 3" }
  }

Assume the following Schema.

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

After validation, this element is represented as:

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

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

An element with a nillable

  <sizes xsi:nil="true"/>

Before validation, this element is represented as:

  element sizes of type xs:anyType {
    attribute xsi:nil of type xs:anySimpleType { "true" }
  }

Assume the following Schema.

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

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

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

An element with a union type

  <sizes>1 two 3 four</sizes>

Before validation, this element is represented as:

  element sizes of type xs:anyType {
    text { "1 two 3 four" }
  }

Assume the following Schema:

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

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

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

2.3 The [XPath/XQuery] Type System

The [XPath/XQuery] type system is used in the specification of the dynamic and of the static semantics of [XPath/XQuery]. This section introduces formal notations for describing types.

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

The [XPath/XQuery] type system is based on XML Schema. Formalizing the treatment of types in [XPath/XQuery], however, requires some adjustments.

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

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

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

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

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

2.3.2 Item types

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

Item Types
[30 (Formal)]   ItemType   ::=   AtomicTypeName | NodeType
[32 (Formal)]   AtomicTypeName   ::=   QName
[31 (Formal)]   NodeType   ::=   ElementType
| AttributeType
| DocumentType
| "comment"
| "processing-instruction"
| "text"
[33 (Formal)]   ElementType   ::=   "element" ElementName? TypeSpecifier?
[34 (Formal)]   TypeSpecifier   ::=   Nillable? TypeReference
[35 (Formal)]   AttributeType   ::=   "attribute" AttributeName? TypeReference?
[36 (Formal)]   Nillable   ::=   "nillable"
[40 (Formal)]   TypeReference   ::=   "of" "type" TypeName
[51 (Formal)]   DocumentType   ::=   "document" ("{" Type? "}")?

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

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

Note

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

Examples

A text node type

  text

matches any text node, such as:

  text { "Text is beautiful" }

A wildcard element

  element

matches any element.

A wildcard element of type string

  element of type xs:integer 

matches any element of type string, such as:

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

A nillable element of type string

  element size nillable of type xs:integer 

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

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

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

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

A reference to a globally declared attribute

  attribute sizes

refers to the global declaration for the attribute sizes.

An element with an anonymous type

  element sizes of type [Anon1]

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

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

2.3.3 Content models

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

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

Types
[28 (Formal)]   Type   ::=   ItemType
| (Type Occurrence)
| (Type "&" Type)
| (Type "," Type)
| (Type "|" Type)
| "empty"
| "none"
[29 (Formal)]   Occurrence   ::=   "*" | "+" | "?"

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

The "&" operator builds the "interleaved product" of two types. The type Type1 & Type2 matches any sequence that is an interleaving of a sequence that matches Type1 and a sequence that matches Type2.

The interleaved product is used to represent all groups in XML Schema. All group in XML Schema are restricted to apply only on global or local element declarations with lower bound 0 or 1, and upper bound 1.

Examples

A sequence of elements

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

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

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

The union of two element types

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

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

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

An all group of two elements

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

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

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

An empty type

The following type matches the empty sequence.

  empty

A sequence of zero or more elements

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

  (element surgeon | element plumber)*

2.3.4 Top level definitions

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

Type Definitions
[43 (Formal)]   Definition   ::=   ("define" "element" ElementName Substitution? Nillable? TypeReference)
| ("define" "attribute" AttributeName TypeReference)
| ("define" "type" TypeName TypeDerivation)
[44 (Formal)]   Substitution   ::=   "substitutes" "for" ElementName
[37 (Formal)]   TypeDerivation   ::=   ComplexTypeDerivation | AtomicTypeDerivation
[38 (Formal)]   ComplexTypeDerivation   ::=   Derivation? Mixed? "{" Type? "}"
[39 (Formal)]   AtomicTypeDerivation   ::=   "restricts" AtomicTypeName
[41 (Formal)]   Derivation   ::=   ("restricts" TypeName)
| ("extends" TypeName)
[42 (Formal)]   Mixed   ::=   "mixed"

A type definition has a name (possibly anonymous) and a type derivation. In the case of a complex type, or a simple type derived by list or uniont, derivation indicates if the type is derived by extension or restriction from its based type, gives its content model, and an optional flag indicating if it has mixed content. In the case of an atomic type, it just indicate from which type it is derived from.

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

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

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

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

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

Examples

A type declaration with complex content

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

A type declaration with complex content derived by extension

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

A type declaration with mixed content

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

A type declaration with simple content derived by restriction

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

An element declaration

  define element address of type Address

An element declaration with a substitution group

  define element usaddress substitutes for address of type USAddress

An element declaration which is nillable

  define element zip nillable of type xs:integer

2.3.5 Example of a complete Schema

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

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

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

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

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

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

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

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

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

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

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

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

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

Those definitions are written in the [XPath/XQuery] type system as follows.

  define type NYCAddress extends USAddress {
    element apt
  }

  define element apt of type [Anon3]

  define type [Anon3] restricts xsd:positiveInteger

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

2.4 Processing model and main judgments

This section defines a processing model for [XPath/XQuery], then defines formal judgments for each key phase in that processing model (normalization, static type analysis and dynamic evaluation).

2.4.1 Processing model

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 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 abstract syntax tree of the parsed query is created.

  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 may be defined by the processing environment and by statements in the Query Prolog (See [5 Modules and Prologs]). In XPath, the input context is defined by the processing environment. The input context has a static and a dynamic part (denoted statEnv and dynEnv, respectively).

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

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

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

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

  4. Static type analysis. Static type analysis is optional. If this phase is not supported, then normalization is followed directly by dynamic evaluation.

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

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

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

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

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

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

The first four phases above are "analysis-time" (sometimes also called "compile-time") steps, meaning that they can be performed on a [expression/query] before examining any input document. Indeed, analysis-time processing can be performed before input documents even exist. 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, meaning 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 are free to implement different processing models, the [XPath/XQuery] static semantics relies on the existence of a static type analysis phase that precedes any access to the input data. Statically typed implementations are required to find and report type errors during static analysis, as specified in this document. Dynamically typed implementations are required to find and report type errors during evaluation, but are permitted to report them during static analysis.

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

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

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

  2. 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 described in [XQuery 1.0 and XPath 2.0 Data Model Serialization] and is not discussed further here.

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

2.4.2 Normalization judgment

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

Notation

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

 
[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

We use the shorthand because statEnv is always 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.

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

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.4.3 Static typing judgment

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

Notation

The judgment

statEnv |- Expr : Type

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

Example

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

For instance, the following expression.

   let $v := 3 return $v+5

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

Note

The type of an expression is computed by inference. Static type inference rules define for each kind of expression how to compute the type of the expression given the types of its sub-expressions. Here is a simple example of such a static typing 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 union: '(Type2|Type3)'.

The "left half" (the part before the :) of the expression below the line corresponds to some [expression/query], for which a type is computed. If the [expression/query] has been parsed into an internal abstract syntax tree, this usually corresponds to some node in that tree. The expression usually has patterns in it (here Expr1, Expr2, and Expr3) that need to be matched against the children of the node in the abstract syntax tree. The expressions above the line indicate things that need to be computed to use this rule; in this case, the types of the condition expression and the two branches of the if-then-else expression. Once those types are computed (by further applying static inference rules recursively to the expressions on each side), then the type of the expression below the line can be computed. This illustrates a general feature of the [XPath/XQuery] type system: the type of an expression depends only on the type of its sub-expressions. The overall static type inference algorithm is recursive, following the abstract syntax of the [expression/query]. At each point in the recursion, an appropriate matching inference rule is sought; if at any point there is no applicable rule, then static type inference has failed and the [expression/query] is not type-safe.

2.4.4 Dynamic evaluation judgment

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

Notation

The judgment

statEnv ; dynEnv |- Expr => Value

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

The judgment

statEnv ; dynEnv |- Expr raises Error

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

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

Example

For instance, the following expression.

   let $v := 3 return $v+5

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

Note

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

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

2.5 Relationship with other documents

2.5.1 Namespaces

Whenever appropriate, the Formal Semantics uses the following namespace prefixes.

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

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

Those prefixes are always shown in italics to emphasize that the corresponding functions, variables, and types are abstract: they are not and cannot be made accessible directly from the host language. None of those special prefixes are given a URI.

2.5.2 Functions and operators

The [XQuery 1.0 and XPath 2.0 Functions and Operators] document defines built-in functions available in [XPath/XQuery]. A number of these functions are used to define the [XPath/XQuery] semantics. 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 is given in [B.1 Functions and Operators used in the Formal Semantics].

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

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

Applied directly, this signature results in little type information. For such functions, better type information can often be obtained by having the output type depend on the type of input parameters. For instance, if the function fn:distinct-nodes is applied on a parameter of type element a*, element b, one can easily deduce that the resulting sequence is a collection of either a or b elements.

In order to provide better static typing for those functions, specific typing rules are given in [6 Additional Semantics of Functions].

3 Basics

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

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

3.1.1 Static Context

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

The following environments are part of the static environment group:

statEnv.xpath1.0_compatibility
The XPath 1.0 compatibility flag specifies whether the semantic rules for backward compatibility with XPath 1.0 are in effect.
statEnv.namespace
The namespace environment corresponds to in-scope namespaces in the [XPath/XQuery] static context.
The namespace environment maps a namespace prefix (NCName) onto a namespace kind and a namespace URI (URI). The namespace kind is either passive or active. The namespace kind determines whether a namespace node is created for an element during element construction.
statEnv.default_type_namespace
The default type namespace corresponds to the default namespace for element and type names in the [XPath/XQuery] static context.
The default type namespace contains a namespace URI (a URI) and is used for any unprefixed QName appearing in a position where an element or type name is expected.
statEnv.default_function_namespace
The default function namespace corresponds to the default namespace for function names in the [XPath/XQuery] static context.
The default function namespace contains a namespace URI (a URI) and is used for any unprefixed QName appearing as the function name in a function call.
statEnv.typeDefn
The type definition environment corresponds to the in-scope type definitions in the [XPath/XQuery] static context.
The type definition environment maps type names (TypeNames) onto their type definitions (Definitions). A type name may be globally declared or anonymous.
statEnv.elemDecl
The element declaration environment corresponds to the in-scope element definitions in the [XPath/XQuery] static context.
The element declaration environment maps element names (ElementNames) onto their global element declarations (Definitions).
statEnv.attrDecl
The attribute declaration environment corresponds to the in-scope attribute definitions in the [XPath/XQuery] static context.
The attribute declaration environment maps attribute names (AttributeNames) onto their global attribute declarations (Definitions).
statEnv.varType
The variable static-type environment corresponds to the in-scope variables in the [XPath/XQuery] static context.
The variable static type environment maps variable names (Variables) to their static types (Types).
statEnv.localElemDecl
The local element definition environment maps a local element name and the type in which the local element is declared (ElementNames, TypeNames) onto the local element's definition.
statEnv.localAttrDecl
The local attribute definition environment maps a local attribute name and the type in which the local attribute is declared (ElementNames, TypeNames) onto the local attribute's definition.
statEnv.funcType
The function declaration environment corresponds to the function signature part of the in-scope functions in the [XPath/XQuery] static context.
The function declaration environment stores the static type signatures of functions. Because [XPath/XQuery] allows multiple built-in functions with the same name differing only in the number and signature of the arguments, this environment maps a QName to the set of all function declaration signatures of the form "define function QName (Type1, ..., Typen) return Type" each corresponding to a declaration of the function. (For user-defined functions the set will contain exactly one such declaration.)
statEnv.collations
The collations environment corresponds to the in-scope collations in the [XPath/XQuery] static context.
The collations maps a unique namespace URI (a URI) to a pair of functions: the first function takes a set of strings and returns a sequence containing those strings in sorted order; and the second function takes two strings, returns true if they are considered equal, and false if not.
statEnv.defaultCollation
The default collation corresponds to the default collation in the [XPath/XQuery] static context.
The default collation is a pair of functions as described in statEnv.collations above.
statEnv.validationMode
The validation mode corresponds to the validation mode in the [XPath/XQuery] static context.
The validation mode is one of strict, lax, or skip. The default value is lax.
statEnv.validationContext
The valiation context corresponds to the validation context in the [XPath/XQuery] static context.
The validation context is either absent, meaning that the context is global, or it is a global or anonymous type name in the statEnv.typeDefn. Every valiation context that occurs in a query is a path that starts with a global element name in statEnv.elemDecl or a global type name in the statEnv.typeDefn and followed in an alternating order by local element names. An explicit context is represented in statEnv.validationContext by the global or anonymous type that contains the element denoted by the path.
statEnv.baseUri
The base uri corresponds to the base URI in the [XPath/XQuery] static context.
The base uri contains a unique namespace URI (a URI).
statEnv.collectionType
The collection type environment contains the static type for the input collections, and is used to provide the static type to the fn:collection function.
The collection type contains bindings from input URIs (a URI) to types (a Type).
statEnv.docType
The doc type environment contains the static type for the input documents, and is used to provide the static type to the fn:doc function.
The doc type contains bindings from input URIs (a URI) to types (a Type).

Environments have an initial state when [expression/query] processing begins, containing, for example, the function signatures of all built-in functions. The initial values for the static context are defined in [XQuery 1.0: An XML Query Language, section C Context Components] and [XML Path Language (XPath), section C Context Components].

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

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

   statEnv |- fs:expand(QName) = ExpandedQName(URI, ncname)

or

   statEnv |- fs:expand(QName) = ExpandedQName(ncname)

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

The helper fs:expand function is defined as follows:

  • If QName matches NCName1:NCName2, and if statEnv.namespace(NCName1) = (kind, URI), then the expression yields ExpandedQName(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_type_namespace = URI, then the expression yields ExpandedQName(URI,NCName), where URI is the default namespace in effect.

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

Editorial note 
The above rules could be given as proper inference rules defining the fs:expand judgment.

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

statEnv + namespace(NCName => (passive, URI)) |- Expr*

statEnv |- declare namespace NCName = URI Expr*

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

This is 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) ]

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

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

3.1.1.1 Predefined Types

All the built-in types of XML Schema are recognized by [XPath/XQuery]. In addition, [XPath/XQuery] recognizes the predefined types: xdt:anyAtomicType, xdt:untypedAtomic, xdt:yearMonthDuration, xdt:dayTimeDuration. The representation of those types in the [XPath/XQuery] type system is given below.

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

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

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

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

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

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

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

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

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

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

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

  define type xdt:untypedAtomic restricts xdt:anyAtomicType

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1.2 Dynamic Context

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

The following environments are part of evaluation environment group:

dynEnv.funcDefn
The dynamic function environment corresponds to the function definition part of the in-scope functions in the [XPath/XQuery] static context.
The dynamic function environment maps a function declaration name and parameter signature of the form "QName (Type1, ..., Typen)" to the remainder of the corresponding function definition, which is either the special constant #BUILT-IN, or the function's body, and the list of variables, which are the function's formal parameters, on the form "(Expr, Variable1, ,..., Variablen)".
The initial function environment maps the signatures of the internal functions defined in [B.2 Mapping of Overloaded Internal Functions] and the signatures of the functions defined in [XQuery 1.0 and XPath 2.0 Functions and Operators] to #BUILT-IN.
dynEnv.varValue
The dynamic value environment corresponds to the dynamic variables in the [XPath/XQuery] evaluation context.
The dynamic value environment maps a variable name (QName) onto the variable's current value (Value).
dynEnv.dateTime
The date-time corresponds to the current date and time in the [XPath/XQuery] evaluation context.
The date-time can be retrieved by the fn:current-date, fn:current-time, and fn:current-dateTime functions.
dynEnv.timezone
The timezone corresponds to the implicit timezone in the [XPath/XQuery] evaluation context and is used by the timezone related functions in [XQuery 1.0 and XPath 2.0 Functions and Operators].

The initial values for the dynamic context are defined in [XQuery 1.0: An XML Query Language, section C Context Components] and [XML Path Language (XPath), section C Context Components].

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

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

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

3.2 Processing Model

A simplified version of the processing model, used as the basis for formalization is given in [2.4 Processing model and main judgments].

3.3 Important Concepts

3.3.1 Document Order

Document order is defined in [XQuery 1.0 and XPath 2.0 Data Model].

3.3.2 Typed Value and String Value

Document order is defined in [XQuery 1.0 and XPath 2.0 Data Model] and [XQuery 1.0 and XPath 2.0 Functions and Operators].

3.3.3 Input Sources

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

3.4 Types

3.4.1 SequenceType

Introduction

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

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

SequenceType
[124 (XQuery)]   SequenceType   ::=   (ItemType OccurrenceIndicator?)
| ("empty" "(" ")")
[140 (XQuery)]   OccurrenceIndicator   ::=   "?" | "*" | "+"
[126 (XQuery)]   ItemType   ::=   AtomicType | KindTest | ("item" "(" ")")
[125 (XQuery)]   AtomicType   ::=   QName
[127 (XQuery)]   KindTest   ::=   DocumentTest
| ElementTest
| AttributeTest
| PITest
| CommentTest
| TextTest
| AnyKindTest
[130 (XQuery)]   PITest   ::=   "processing-instruction" "(" (NCName | StringLiteral)? ")"
[132 (XQuery)]   CommentTest   ::=   "comment" "(" ")"
[133 (XQuery)]   TextTest   ::=   "text" "(" ")"
[134 (XQuery)]   AnyKindTest   ::=   "node" "(" ")"
[131 (XQuery)]   DocumentTest   ::=   "document-node" "(" ElementTest? ")"
[128 (XQuery)]   ElementTest   ::=   "element" "(" ((SchemaContextPath LocalName)
| (NodeName ("," TypeName "nillable"?)?))? ")"
[129 (XQuery)]   AttributeTest   ::=   "attribute" "(" ((SchemaContextPath "@" LocalName)
| ("@" NodeName ("," TypeName)?))? ")"
[135 (XQuery)]   SchemaContextPath   ::=   SchemaGlobalContext "/" (SchemaContextStep "/")*
[14 (XQuery)]   SchemaGlobalContext   ::=   QName | SchemaGlobalTypeName
[15 (XQuery)]   SchemaContextStep   ::=   QName
[13 (XQuery)]   SchemaGlobalTypeName   ::=   "type" "(" QName ")"
[137 (XQuery)]   LocalName   ::=   QName
[138 (XQuery)]   NodeName   ::=   QName | "*"
[139 (XQuery)]   TypeName   ::=   QName | "*"

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

Core Grammar

The core grammar productions for sequence types are:

[85 (Core)]   SequenceType   ::=   (ItemType OccurrenceIndicator?)
| ("empty" "(" ")")
[101 (Core)]   OccurrenceIndicator   ::=   "?" | "*" | "+"
[87 (Core)]   ItemType   ::=   AtomicType | KindTest | ("item" "(" ")")
[86 (Core)]   AtomicType   ::=   QName
[88 (Core)]   KindTest   ::=   DocumentTest
| ElementTest
| AttributeTest
| PITest
| CommentTest
| TextTest
| AnyKindTest
[91 (Core)]   PITest   ::=   "processing-instruction" "(" (NCName | StringLiteral)? ")"
[93 (Core)]   CommentTest   ::=   "comment" "(" ")"
[94 (Core)]   TextTest   ::=   "text" "(" ")"
[95 (Core)]   AnyKindTest   ::=   "node" "(" ")"
[92 (Core)]   DocumentTest   ::=   "document-node" "(" ElementTest? ")"
[89 (Core)]   ElementTest   ::=   "element" "(" ((SchemaContextPath LocalName)
| (NodeName ("," TypeName "nillable"?)?))? ")"
[90 (Core)]   AttributeTest   ::=   "attribute" "(" ((SchemaContextPath "@" LocalName)
| ("@" NodeName ("," TypeName)?))? ")"
[96 (Core)]   SchemaContextPath   ::=   SchemaGlobalContext "/" (SchemaContextStep "/")*
[10 (Core)]   SchemaGlobalContext   ::=   QName | SchemaGlobalTypeName
[11 (Core)]   SchemaContextStep   ::=   QName
[9 (Core)]   SchemaGlobalTypeName   ::=   "type" "(" QName ")"
[98 (Core)]   LocalName   ::=   QName
[99 (Core)]   NodeName   ::=   QName | "*"
[100 (Core)]   TypeName   ::=   QName | "*"
Editorial 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 432 (FS-Issue-0089)). SequenceType normalization is the only occurrence of such a deviation in the formal semantics.
3.4.1.1 SequenceType Matching

Introduction

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

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

Notation

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

 
[SequenceType]sequencetype
==
Type

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

Normalization

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

 
[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
==
empty

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

 
[element()]sequencetype
==
element
 
[element(*)]sequencetype
==
element
 
[element(*,*)]sequencetype
==
element
 
[attribute()]sequencetype
==
attribute
 
[attribute(@*)]sequencetype
==
attribute
 
[attribute(@*,*)]sequencetype
==
attribute

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

 
[element(ElementName)]sequencetype
==
element ElementName
 
[attribute(@AttributeName)]sequencetype
==
attribute AttributeName
 
[element(ElementName,TypeName)]sequencetype
==
element ElementName of type TypeName
 
[attribute(@AttributeName,TypeName)]sequencetype
==
attribute AttributeName of type TypeName
 
[element(ElementName,TypeName nillable)]sequencetype
==
element ElementName nillable of type TypeName

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

 
[text()]sequencetype
==
text
 
[document-node()]sequencetype
==
document
 
[document-node(ElementTest)]sequencetype
==
document { [ElementTest]sequencetype }
 
[AtomicType]sequencetype
==
AtomicType
 
[comment()]sequencetype
==
comment
 
[processing-instruction()]sequencetype
==
processing-instruction
 
[processing-instruction(String)]sequencetype
==
processing-instruction

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

 
[node()]sequencetype
==
(element | attribute | text | document | comment | processing-instruction)
 
[item()]sequencetype
==
(element | attribute | text | document | comment | processing-instruction | xdt:anyAtomicType )
Editorial 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.

3.4.2 Type Conversions

Introduction

Some expressions do not require that their operands exactly match an 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 [4.1.5 Function Calls]. Other operators that provide special conversion rules include arithmetic operators ([4.4 Arithmetic Expressions]), value comparisons ([4.5.1 Value Comparisons]), and general comparisons ([4.5.2 General Comparisons]).

3.4.2.1 Atomization

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

3.4.2.2 Effective Boolean Value

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

3.4.2.3 XPath 1.0 Backward Compatibility

The semantics of some functions (see [6 Additional Semantics of Functions]) depends on whether the XPath 1.0 backward compatibility flag is true or false.

3.5 Errors Handling

Expressions can raise errors during static analysis or dynamic evaluation. The [XQuery 1.0 and XPath 2.0 Functions and Operators] [XQuery 1.0: A Query Language for XML], and [XML Path Language (XPath) 2.0] specify the conditions under which an expression or operator raises an error. The user may raise an error explicitly by calling the fn:error function, which takes an optional item as an argument.

Notation

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

Editorial note 
We use a generic dynamic error, because the definition of all errors raised by functions and operators in [XQuery 1.0 and XPath 2.0 Functions and Operators] is under discussion.

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

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

dynEnv |- Expri raises dynError      Expri is any subexpression of Expr

dynEnv |- Expr raises dynError

There are several expressions that do not propogate an error raised by some sub-expression. For each such expression, we give specific error inference rules.

3.6 Optional Features

Editorial note 
Issue: Optional features and conformance levels are not formally specified. See Issue 512 (FS-Issue-0169).

3.6.1 Basic XQuery

3.6.2 Schema Import Feature

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

3.6.3 Static Typing Feature

The semantics of the static typing feature is described using static inference rules in the formal semantics.

3.6.4 Extensions

The formal semantics of extensions is not specified.

3.6.4.1 Pragmas
[1 (XQuery)]   Pragma   ::=   "(::" "pragma" QName PragmaContents* "::)"
[5 (XQuery)]   PragmaContents   ::=   Char
3.6.4.2 Must-Understand Extensions
[6 (XQuery)]   ExtensionContents   ::=   Char
3.6.4.3 XQuery Flagger

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

[40 (XQuery)]   Expr   ::=   ExprSingle ("," ExprSingle)*
[41 (XQuery)]   ExprSingle   ::=   FLWORExpr
| QuantifiedExpr
| TypeswitchExpr
| IfExpr
| OrExpr
[15 (XPath)]   XPath   ::=   Expr?

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:

[31 (Core)]   Expr   ::=   ExprSingle ("," ExprSingle)*

Static Type Analysis

It is a static error for any expression other than the empty-sequence expression () to have the empty type. The rule below enforces the constraint that any expression other than () have a non-empty type. The static typing rule for () is in [4.1.3 Parenthesized Expressions].

statEnv |- Expr : Type      not(Expr = ())     not(Type = empty)

statEnv |- Expr : Type

4.1 Primary Expressions

Primary expressions are the basic primitives of the language.They include literals, variables, function calls, and the parenthesized expressions.

Primary Expressions
[75 (XQuery)]   PrimaryExpr   ::=   Literal | FunctionCall | ContextItemExpr | ("$" VarName) | ParenthesizedExpr | Constructor
[20 (XQuery)]   VarName   ::=   QName

Core Grammar

The core grammar productions for primary expressions are:

Primary Expressions
[47 (Core)]   PrimaryExpr   ::=   Literal | FunctionCall | ContextItemExpr | ("$" VarName) | ParenthesizedExpr | Constructor
[15 (Core)]   VarName   ::=   QName

4.1.1 Literals

Introduction

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

Literals
[93 (XQuery)]   Literal   ::=   NumericLiteral | StringLiteral
[94 (XQuery)]   NumericLiteral   ::=   IntegerLiteral | DecimalLiteral | DoubleLiteral
[7 (XQuery)]   IntegerLiteral   ::=   Digits
[8 (XQuery)]   DecimalLiteral   ::=   ("." Digits) | (Digits "." [0-9]*)
[9 (XQuery)]   DoubleLiteral   ::=   (("." Digits) | (Digits ("." [0-9]*)?)) ("e" | "E") ("+" | "-")? Digits
[10 (XQuery)]   StringLiteral   ::=   ('"' (PredefinedEntityRef | CharRef | ('"' '"') | [^"&])* '"') | ("'" (PredefinedEntityRef | CharRef | ("'" "'") | [^'&])* "'")
[22 (XQuery)]   PredefinedEntityRef   ::=   "&" ("lt" | "gt" | "amp" | "quot" | "apos") ";"
[24 (XQuery)]   CharRef   ::=   "&#" (Digits | ("x" HexDigits)) ";"

Normalization

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

Core Grammar

The core grammar productions for literals are:

Literals
[59 (Core)]   Literal   ::=   NumericLiteral | StringLiteral
[60 (Core)]   NumericLiteral   ::=   IntegerLiteral | DecimalLiteral | DoubleLiteral
[3 (Core)]   IntegerLiteral   ::=   Digits
[4 (Core)]   DecimalLiteral   ::=   ("." Digits) | (Digits "." [0-9]*)
[5 (Core)]   DoubleLiteral   ::=   (("." Digits) | (Digits ("." [0-9]*)?)) ("e" | "E") ("+" | "-")? Digits
[6 (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 => xs:integer (IntegerLiteral)

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 => xs:decimal(DecimalLiteral)

Static Type Analysis


statEnv |- DoubleLiteral : xs:double

Dynamic Evaluation


dynEnv |- DoubleLiteral => xs:double(DoubleLiteral)

Static Type Analysis


statEnv |- StringLiteral : xs:string

Dynamic Evaluation


dynEnv |- StringLiteral => xs:string(StringLiteral)

Dynamic Errors

Literal expressions never raise an error.

4.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 static environment, the system raises a static 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

Dynamic Errors

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

dynEnv.varValue(Variable) undefined

dynEnv.varValue |- Variable raises dynError

Editorial note 
MFF: Given sufficient consistency constraints on the static and dynamic environments, this error rule is not necessary, because every variable must be defined.

4.1.3 Parenthesized Expressions

[95 (XQuery)]   ParenthesizedExpr   ::=   "(" Expr? ")"

Core Grammar

The core grammar production for parenthesized expressions is:

[61 (Core)]   ParenthesizedExpr   ::=   "(" Expr? ")"

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

Static Type Analysis


statEnv |- ( ) : empty

statEnv |- Expr : Type

statEnv |- ( Expr ) : Type

Dynamic Evaluation

The empty-sequence expression evaluates to the empty sequence.


dynEnv |- () => ()

dynEnv |- Expr => Value

dynEnv |- ( Expr ) => Value

Dynamic Errors

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

4.1.4 Context Item Expression

[41]   ContextItemExpr   ::=   "."

Introduction

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

Normalization

A context item expression is normalized as the special purpose variable $fs:dot.

 
[.]Expr
==
$fs:dot

4.1.5 Function Calls

Introduction

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

Function Calls
[96 (XQuery)]   FunctionCall   ::=   QName "(" (ExprSingle ("," ExprSingle)*)? ")"

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

Notation

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

 
[Expr]FunctionArgument(SequenceType)
==
[[[Expr]AtomizeAtomic(SequenceType)]Extract(SequenceType)]Convert(SequenceType)

where

  • [Expr]AtomizeAtomic(SequenceType) denotes

    fn:data(Expr)  If SequenceType <: xs:anyAtomic*
    Expr  Otherwise

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

  • [Expr]Extract(SequenceType) denotes

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

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

  • [Expr]Convert(SequenceType) denotes

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

    where PrototypicalValue has the following values for each possible SequenceType:

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

Note

The fs:convert-simple-operand function uses a so-called PrototypicalValue, which is a value in the target type, to ensures that conversion to base types is possible eventhough types are not first class objects in [XPath/XQuery].

Normalization

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

 
[ QName (Expr1, ..., Exprn) ]Expr
==
QName ( [Expr1]FunctionArgument(SequenceType1), ..., [Exprn]FunctionArgument(SequenceTypen)) )

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. Furthermore notice that the normalization is only well-defined when it is guaranteed that overloading is restricted to atomic types with the same quantifier. This is presently the case.

Core Grammar

The core grammar production for function calls is:

Function Calls
[62 (Core)]   FunctionCall   ::=   QName "(" (ExprSingle ("," ExprSingle)*)? ")"

Static Type Analysis

Editorial note 
Proposal (Kris): The following rules attempt to solve the "atomic overload protection" problem by factoring typing over atomic unions. Also it is made explicit that specific typing rules for functions (in [6 Additional Semantics of Functions]) take precedence.

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

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

statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- Expr1 : Type1' ... Exprn : Typen'
statEnv |- ExpandedQName(Type1,...,Typen) : Type

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

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

Typei = (AtomicType1|...|AtomicTypem)
statEnv |- ExpandedQName(Type1,..., AtomicType1,..., Typen) : Type1'
...
statEnv |- ExpandedQName(Type1,..., AtomicTypem,..., Typen) : Typem'

statEnv |- ExpandedQName(Type1, ..., Typen) : (Type1'|...|Typem')

Note

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

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

not(Type1 = (AtomicType1,1|...|AtomicType1,m1)
...
not(Typen = (AtomicTypen,1|...|AtomicTypen,mn)
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function ExpandedQName(Type1'', ..., Typen'') as Type''
Type1 <: Type1'     ...     Typen <: Typen'
Type1' can be promoted to Type1''     ...     Typen' can be promoted to Typen''

statEnv |- ExpandedQName(Type1, ..., Typen) : Type''

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

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

Editorial note 
We could consider changing the language document to talk about type signatures instead of arities but I (Kris) do not personally believe that we it is important...and what IS important (for the dynamic function call rule below) is that the [XQuery 1.0 and XPath 2.0 Functions and Operators] specification does not overload functions with more than one definition per arity!

Dynamic Evaluation

Based on a function's name and argument types, the function body is retrieved from the dynamic environment. If the function is not present in the environment, a static error is raised.

If the function is a user-defined function then it is evaluated as follows. First, the rule evaluates each actual function argument expression. Next, a match is searched for among the function's possible declaration signatures, retrieved from the statEnv.funcType static environment component. If the function is not present in the environment, or there is no matching declaration signature, a type error is raised. Otherwise, the function body and formal variables are obtained from dynEnv.funcDefn for the matching declaration signature. The rule then extends dynEnv.varValue by binding each formal variable to its corresponding value (converted by the normalization as required for the expected type and backwards compatibility flag), and evaluates the body of the function in the new environment. The resulting value is the value of the function call.

statEnv |- fs:expand(QName) = ExpandedQName
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function ExpandedQName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(ExpandedQName(Type1, ..., Typen)) = (Expr, Variable1, ... , Variablen)
dynEnv [ varValue = ( Variable1 => Value1'; ...; Variablen => Valuen') ] |- Expr => Value
statEnv |- Value against Type promotes to Value'

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

Note that the function body is evaluated in the default (top-level) environment extended with just the parameter bindings. Note also that input values and output values are matched against the types declared for the function. If static analysis was performed, all these checks are guaranteed to be true and may be omitted.

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

statEnv |- fs:expand(QName) = ExpandedQName
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function ExpandedQName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(ExpandedQName(Type1, ..., Typen)) = #BUILT-IN
ExpandedQName(Value1', ..., Valuen') => Value
statEnv |- Value against Type promotes to Value'

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

Built-in function calls use the following auxiliary judgment to evaluate the built-in function:

"The built-in function F (from [XQuery 1.0 and XPath 2.0 Data Model], [XQuery 1.0 and XPath 2.0 Functions and Operators], or [6 Additional Semantics of Functions]) applied to the given parameter values yields the specified result value"

F(Value1, ..., Valuen) => Value

Editorial note 
Issue:Built-in function calls must be defined more precisely. See Issue 522 (FS-Issue-0179).

Dynamic Errors

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

statEnv |- QName => ExpandedQName
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function ExpandedQName(Type1, ..., Typen) as Type
dynEnv |- Expri raises Error      1 <= i <= n

dynEnv |- QName ( Expr1, ..., Exprn ) raises Error

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

statEnv |- QName => ExpandedQName
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDeclj = define function ExpandedQName(Type1, ..., Typen) as Type      for all 1 <= j <= m
dynEnv |- Expri => Valuei
statEnv |- not (Valuei against Typei promotes to Valuei')      1 <= i <= n

dynEnv |- QName ( Expr1, ..., Exprn ) raises typeError

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

statEnv |- QName => ExpandedQName
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDecli = define function ExpandedQName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(ExpandedQName(Type1, ..., Typen)) = (Expr, Variable1, ... , Variablen)
dynEnv [ varValue = ( Variable1 => Value1'; ...; Variablen => Valuen') ] |- Expr => Value
statEnv |- not (Value against Type promotes to Value')

dynEnv |- QName ( Expr1, ..., Exprn ) raises typeError

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

statEnv |- QName => ExpandedQName
statEnv.funcType(ExpandedQName) = { FuncDecl1, ..., FuncDeclm }
FuncDeclj = define function ExpandedQName(Type1, ..., Typen) as Type
dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
statEnv |- Value1 against Type1 promotes to Value1'
...
statEnv |- Valuen against Typen promotes to Valuen'
dynEnv.funcDefn(ExpandedQName(Type1, ..., Typen)) = #BUILT-IN
ExpandedQName(Value1', ..., Valuen') => Value
statEnv |- not (Value against Type promotes to Value')

dynEnv |- QName ( Expr1, ..., Exprn ) raises typeError

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

"The built-in function F (from data model, type constructor, or functions and operators) applied to the given parameter raises an error"

F(Value1, ..., Valuen) raises Error

Editorial note 
Issue:Built-in function calls must be defined more precisely. See Issue 522 (FS-Issue-0179).

4.1.6 [XPath/XQuery] Comments

[3 (XQuery)]   ExprComment   ::=   "(:" (ExprCommentContent | ExprComment)* ":)"
[4 (XQuery)]   ExprCommentContent   ::=   Char

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

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

Path Expressions
[69 (XQuery)]   PathExpr   ::=   ("/" RelativePathExpr?)
| ("//" RelativePathExpr)
| RelativePathExpr
[70 (XQuery)]   RelativePathExpr   ::=   StepExpr (("/" | "//") StepExpr)*

Core Grammar

PathExpr and RelativePathExpr are fully normalized. There for, there is no corresponding production in the core. The grammar of path expressions in the core starts with the StepExpr production.

Normalization

Absolute path expressions are path expressions starting with the / or / symbols, indicating that the expression must be applied on the root node in the current context. The root node in the current context is the greatest ancestor of the context node. The following two rules normalize absolute path expressions to relative ones. They use the fn:root function, which returns the greatest ancestor of its argument node. The let expressions guarantee that the value bound to the context variable $fs:dot is a node.

 
["/"]Expr
==
(fn:root(self::node()) treat as document-node())
 
["/" RelativePathExpr]Expr
==
[((fn:root(self::node())) treat as document-node()) "/" RelativePathExpr]Expr
 
["//" RelativePathExpr]Expr
==
[((fn:root(self::node())) treat as document-node) "/" descendant-or-self::node() "/" RelativePathExpr]Expr
 
[ StepExpr1 // StepExpr2 ]Expr
==
[StepExpr1 / descendant-or-self::node() / StepExpr2]Expr

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 call to the fs:distinct-doc-order function ensures that the result is in document order without duplicates. The evaluation context is defined by binding the $fs:dot, $fs:sequence, $fs:position and $fs:last variables.

Note that sorting by document order enforces the restriction that input and output sequences contains only nodes.

 
[StepExpr1 "/" StepExpr2]Expr
==
fs:distinct-doc-order (
  let $fs:sequence := [StepExpr1]Expr return
  let $fs:last := fn:count($fs:sequence) return
  for $fs:dot at $fs:position in $fs:sequence return
    [StepExpr2]Expr
)

4.2.1 Steps

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

Introduction

Steps
[71 (XQuery)]   StepExpr   ::=   AxisStep | FilterStep
[72 (XQuery)]   AxisStep   ::=   (ForwardStep | ReverseStep) Predicates
[73 (XQuery)]   FilterStep   ::=   PrimaryExpr Predicates
[84 (XQuery)]   ForwardStep   ::=   (ForwardAxis NodeTest) | AbbrevForwardStep
[85 (XQuery)]   ReverseStep   ::=   (ReverseAxis NodeTest) | AbbrevReverseStep

Core Grammar

The core grammar productions for XPath steps are:

Steps
[45 (Core)]   FilterStep   ::=   PrimaryExpr Predicates
[52 (Core)]   ForwardStep   ::=   ForwardAxis NodeTest
[53 (Core)]   ReverseStep   ::=   ReverseAxis NodeTest

Note

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

Normalization

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

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

There are two sets of normalization rules for Predicates. The first set of rules deals with the general case. The second set of rules deals with the case where the content of a predicate is a numeric literal. In that second case, the alternative normalization rules provides a more precise static type than if the general rules were applied.

In the case a predicates are applied on a forward step, the input sequence is first sorted in document order and duplicates are removed. The context is changed to bind the appropriate variable in document order.

Note that applying sorting by document order enforces the restriction that input and output sequences contains only nodes.

 
[ForwardStep Predicates "[" Expr "]"]Expr
==
let $fs:sequence := fs:distinct-doc-order( [ForwardStep Predicates]Expr ) return
let $fs:last := fn:count($fs:sequence) return
for $fs:dot at $fs:position in $fs:sequence return
   if [Expr]Predicates then $fs:dot else ()

In the case predicates are applied on a reverse step, the input sequence is first sorted in document order and duplicates are removed. The context is changed such that the position variable is bound in reverse document order.

Note that applying sorting by document order enforces the restriction that input and output sequences contains only nodes.

 
[ReverseStep Predicates "[" Expr "]"]Expr
==
let $fs:sequence := fs:distinct-doc-order( [ReverseStep Predicates]Expr ) return
let $fs:last := fn:count($fs:sequence) return
for $fs:dot at $fs:new in $fs:sequence return
let $fs:position := $fs:last - $fs:new + 1 return
  if [Expr]Predicates then $fs:dot else ()

In the case predicates are applied on a primary expression, the input sequence is processed in sequence order and the context is bound as in the case of forward axis. In that case, the sequence can contain both nodes and atomic values.

 
[PrimaryExpr Predicates "[" Expr "]"]Expr
==
let $fs:sequence := [PrimaryExpr Predicates]Expr return
let $fs:last := fn:count($fs:sequence) return
for $fs:dot at $fs:position in $fs:sequence return
   if [Expr]Predicates then $fs:dot else ()

In the case the predicate applies to a numeric literal, the following normalization rules apply.

 
[ForwardStep Predicates "[" Numeric "]"]Expr
==
let $fs:sequence := fs:distinct-doc-order( [ForwardStep Predicates]Expr ) return
let $fs:last := fn:count($fs:sequence) return
let $fs:position := Numeric return
if (($fs:position > 0) and ($fs:position <= $fs:last))
   then fn:item-at($fs:sequence,$fs:position)
   else ()

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

 
[ReverseStep Predicates "[" Expr "]"]Expr
==
let $fs:sequence := fs:distinct-doc-order( [ForwardStep Predicates]Expr ) return
let $fs:last := fn:count($fs:sequence) return
let $fs:position := $fs:last - Numeric + 1 return
if (($fs:position > 0) and ($fs:position <= $fs:last))
   then fn:item-at($fs:sequence,$fs:position)
   else ()

In the case predicates are applied on a primary expression, the input sequence is processed in sequence order and the context is bound as in the case of forward axis. In that case, the sequence can contain both nodes and atomic values.

 
[PrimaryExpr Predicates "[" Expr "]"]Expr
==
let $fs:sequence := [PrimaryExpr Predicates]Expr return
let $fs:last := fn:count($fs:sequence) return
let $fs:position := Numeric return
if (($fs:position > 0) and ($fs:position <= $fs:last))
   then fn:item-at($fs:sequence,$fs:position)
   else ()

Finally, a stand-alone forward or reverse step is normalized through the auxiliary normalization rule for Axis.

 
[ForwardStep]Expr
==
[ForwardStep]Axis
 
[ReverseStep]Expr
==
[ReverseStep]Axis

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
Type1 <: node
statEnv |- axis Axis of Type1 : Type2
Axis principal PrincipalNodeKind
statEnv |- test NodeTest with PrincipalNodeKind of Type2 : Type3

statEnv |- Axis NodeTest : Type3

Note

Note that the second judgment in the inference rule imposes that the context item be a node type, hence making sure the dynamic error in case the context node is an atomic value does not occur.

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
Value1 matches node
dynEnv |- axis Axis of Value1 => Value2
Axis principal PrincipalNodeKind
dynEnv |- test NodeTest with PrincipalNodeKind of Value2 => Value3

dynEnv |- Axis NodeTest => fs:distinct-doc-order(Value3)

Note

Note that the second judgment in the inference rule makes sure the axis nodetest expression is not evaluated in case the context item is not bound to a node.

Dynamic Errors

If the context item is not a node, the evaluation of an axis node test expression raises a dynamic error.

dynEnv.varValue($fs:dot) = AtomicValue

dynEnv.varValue |- Axis NodeTest raises typeError

4.2.1.1 Axes

Introduction

Axes
[88 (XQuery)]   ForwardAxis   ::=   ("child" "::")
| ("descendant" "::")
| ("attribute" "::")
| ("self" "::")
| ("descendant-or-self" "::")
| ("following-sibling" "::")
| ("following" "::")
[89 (XQuery)]   ReverseAxis   ::=   "parent" "::"
| "ancestor" "::"
| "preceding-sibling" "::"
| "preceding" "::"
| "ancestor-or-self" "::"

Core Grammar

The core grammar productions for XPath axis are:

Axes
[54 (Core)]   ForwardAxis   ::=   ("child" "::")
| ("descendant" "::")
| ("attribute" "::")
| ("self" "::")
| ("descendant-or-self" "::")
| ("following-sibling" "::")
| ("following" "::")
| ("namespace" "::")
[55 (Core)]   ReverseAxis   ::=   "parent" "::"
| "ancestor" "::"
| "preceding-sibling" "::"
| "preceding" "::"
| "ancestor-or-self" "::"

Notation

Normalization of axis uses the following auxiliary mapping rule: []Axis.

Normalization

Normalization for all axis is specified as follows.

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]Axis
==
[let $e := . in parent::node()/child:: NodeTest [.<<$e]]Expr
 
[following:: NodeTest]Axis
==
[ancestor-or-self::node()/following-sibling::node()/descendant-or-self::NodeTest]Expr

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

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

Reverse axes:

 
[preceding-sibling:: NodeTest]Axis
==
[let $e := . in parent::node()/child:: NodeTest [.>>$e]]Expr
 
[preceding:: NodeTest]Axis
==
[ancestor-or-self::node()/preceding-sibling::node()/descendant-or-self::NodeTest]Expr

Otherwise, the reverse axis is part of the core.

 
[parent:: NodeTest]Axis
==
parent:: NodeTest
 
[ancestor:: NodeTest]Axis
==
ancestor:: NodeTest
 
[ancestor-or-self:: NodeTest]Axis
==
ancestor-or-self:: NodeTest
4.2.1.2 Node Tests

Introduction

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

Node Tests
[90 (XQuery)]   NodeTest   ::=   KindTest | NameTest
[91 (XQuery)]   NameTest   ::=   QName | Wildcard
[92 (XQuery)]   Wildcard   ::=   "*"
| (NCName ":" "*")
| ("*" ":" NCName)

Core Grammar

The core grammar productions for node tests are:

Node Tests
[56 (Core)]   NodeTest   ::=   KindTest | NameTest
[57 (Core)]   NameTest   ::=   QName | Wildcard
[58 (Core)]   Wildcard   ::=   "*"
| (NCName ":" "*")
| ("*" ":" NCName)

4.2.2 Predicates

Introduction

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

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

Notation

Normalization of predicates uses the following auxiliary mapping rule: []Predicates.

Normalization

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

 
[Expr]Predicates
==
typeswitch (Expr)
  case $v as fs:numeric return op:numeric-equal($v, $fs:position)
  default $v return fn:boolean($v)

Note that the semantics of predicates whose parameter is a numeric value also works for other numeric than integer values, in which case the op:numeric-equal returns false when compared to a position. For example the expression //a[3.4] is allowed and always returns the empty sequence)

Editorial note 
NEW Issue: The static semantics for the case where the parameter of a predicate is a numeric value is still an open issue.

4.2.3 Unabbreviated Syntax

The corresponding Section in the [XPath/XQuery] document just contains examples.

4.2.4 Abbreviated Syntax

Abbreviated Syntax

Normalization

Here are normalization rules for the abbreviated syntax.

 
[ .. ]Expr
==
[parent::node()]Axis
 
[ @ NameTest ]Expr
==
attribute :: NameTest
 
[ NodeTest ]Expr
==
[child :: NodeTest]Axis

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

4.3.1 Constructing Sequences

Constructing Sequences
[40 (XQuery)]   Expr   ::=   ExprSingle ("," ExprSingle)*
[62 (XQuery)]   RangeExpr   ::=   AdditiveExpr ( "to" AdditiveExpr )?

Core Grammar

The core grammar productions for sequence expressions are:

Core Sequence Expressions
[31 (Core)]   Expr   ::=   ExprSingle ("," ExprSingle)*

Normalization

A sequence expression is normalized into a sequence of normalized single expressions:

 
[Expr1 , Expr2]Expr
==
[Expr1]Expr, [Expr2]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 |- Expr2 : Type2

statEnv |- Expr1 , Expr2 : Type1, Type2

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 |- Expr1, Expr2 => Value1, Value2

Dynamic Errors

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

Normalization

The range operator is normalized to the op:to operator.

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

Static Type Analysis

The static semantics of the op:to operator is defined in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Evaluation

The dynamic semantics of the op:to operator is defined in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Errors

The error semantics of the op:to operator is defined in [XQuery 1.0 and XPath 2.0 Functions and Operators].

4.3.2 Combining Sequences

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

Combining Sequences
[66 (XQuery)]   UnionExpr   ::=   IntersectExceptExpr ( ("union" | "|") IntersectExceptExpr )*
[67 (XQuery)]   IntersectExceptExpr   ::=   ValueExpr ( ("intersect" | "except") ValueExpr )*
[68 (XQuery)]   ValueExpr   ::=   ValidateExpr | PathExpr

Notation

The union, intersect, and except expressions are normalized into function calls to the appropriate functions. 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 [6 Additional Semantics of Functions].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics for function calls is given in [4.1.5 Function Calls].

4.4 Arithmetic Expressions

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

Arithmetic Expressions
[63 (XQuery)]   AdditiveExpr   ::=   MultiplicativeExpr ( ("+" | "-") MultiplicativeExpr )*
[64 (XQuery)]   MultiplicativeExpr   ::=   UnaryExpr ( ("*" | "div" | "idiv" | "mod") UnaryExpr )*
[65 (XQuery)]   UnaryExpr   ::=   ("-" | "+")* UnionExpr
[42 (XPath)]   ValueExpr   ::=   PathExpr

Notation

The mapping function []ArithOp is defined by the following table:

ArithOp[ArithOp]ArithOp
"+"fs:plus
"-"fs:minus
"*"fs:times
"div"fs:div
"mod"fs:mod

Normalization

Editorial note 
Proposal (Kris). The following rules eliminate let bindings that are not necessary.

The normalization rules for all the arithmetic operators except idiv first atomize each argument by applying fn:data and then apply the internal function fs:convert-operand defined in [6.2.5 The fn:data function] to each argument. If the first argument to this function has type xdt:untypedAtomic, then the first argument is cast to a double, otherwise it is returned unchanged. The overloaded internal function corresponding to the arithmetic operator is then applied to the two converted arguments. The table above maps the operators to the corresponding internal function. The mapping from the overloaded internal functions to the corresponding monomorphic function is given in [B.2 Mapping of Overloaded Internal Functions].

 
[Expr1 ArithOp Expr2]Expr
==
[ArithOp]ArithOp (fs:convert-operand(fn:data([Expr1]Expr), 1.0E0),
fs:convert-operand(fn:data([Expr2]Expr), 1.0E0))

The normalization rules for the idiv operator are similar, but instead of casting arguments with type xdt:untypedAtomic to xs:double, they are cast to xs:integer.

 
[Expr1 idiv Expr2]Expr
==
fs:idiv (fs:convert-operand(fn:data([Expr1]Expr), 1.0E0),
fs:convert-operand(fn:data([Expr2]Expr), 1.0E0))

The unary operators are mapped similarly.

 
[+ Expr]Expr
==
fs:plus(0, fs:convert-operand(fn:data([Expr]Expr), 1.0E0))
 
[- Expr]Expr
==
fs:minus(0, fs:convert-operand(fn:data([Expr]Expr), 1.0E0))

Core Grammar

There are no core grammar rules for value comparisons as they are normalized to other core expressions.

Static Type Analysis

The static semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics for function calls is given in [4.1.5 Function Calls].

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

Comparison Expressions
[61 (XQuery)]   ComparisonExpr   ::=   RangeExpr ( (ValueComp
| GeneralComp
| NodeComp
| OrderComp) RangeExpr )?
[81 (XQuery)]   ValueComp   ::=   "eq" | "ne" | "lt" | "le" | "gt" | "ge"
[80 (XQuery)]   GeneralComp   ::=   "=" | "!=" | "<" | "<=" | ">" | ">="
[82 (XQuery)]   NodeComp   ::=   "is" | "isnot"
[83 (XQuery)]   OrderComp   ::=   "<<" | ">>"

4.5.1 Value Comparisons

Notation

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

ValueOp[ValueOp]ValueOp
"eq"fs:eq
"ne"fs:ne
"lt"fs:lt
"le"fs:le
"gt"fs:gt
"ge"fs:ge

Normalization

The normalization rules for the value comparison operators first atomize each argument by applying fn:data and then apply the internal function fs:convert-operand defined in [6.2.5 The fn:data function]. If the first argument to this function has type xdt:untypedAtomic, then the first argument is cast to a string, otherwise it is returned unchanged. The overloaded internal function corresponding to the value comparison operator is then applied to the two converted arguments. The table above maps the value operators to the corresponding internal function. The mapping from the overloaded internal functions to the corresponding monomorphic function is given in [B.2 Mapping of Overloaded Internal Functions].

 
[Expr1 ValueOp Expr2]Expr
==
[ValueOp]ValueOp (fs:convert-operand(fn:data([Expr1]Expr), "string"),
fs:convert-operand(fn:data([Expr2]Expr), "string") )

Core Grammar

There are no core grammar rules for value comparisons as they are normalized to other core expressions.

Static Type Analysis

The static semantics for function calls is given in [4.1.5 Function Calls]. The comparison functions all have return type xs:boolean, as specified in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics rules for function calls is given in [4.1.5 Function Calls].

4.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 []GeneralOp is defined by the following table:

GeneralOp[GeneralOp]GeneralOp
"="fs:eq
"!="fs:ne
"<"fs:lt
"<="fs:le
">"fs:gt
">="fs:ge

Normalization

The normalization rule for a general comparison expression first atomizes each argument by applying fn:data and then applies the existentially quantified some expression to each sequence. The internal function fs:convert-operand is applied to each pair of atomic values. If the first argument to this function has type xdt:untypedAtomic, then the first argument is cast to type of the second argument. If the second argument has type xdt:untypedAtomic the first argument is cast to a string. The overloaded internal function corresponding to the general comparison operator is then applied to the two converted values.

 
[Expr1 GeneralOp Expr2]Expr
==
some $v1 in fn:data([Expr1]Expr) satisfies
some $v2 in fn:data([Expr2]Expr) satisfies
let $u1 := fs:convert-operand($v1, $v2) return
let $u2 := fs:convert-operand($v2, $v1) return
[GeneralOp]GeneralOp ($u1, $u2)

Core Grammar

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

4.5.3 Node Comparisons

Normalization

The normalization rules for node comparisons map each argument expression and then apply the internal function corresponding to the node comparison operator.

 
[Expr1 is Expr2]Expr
==
   op:node-equal([Expr1]Expr, [Expr2]Expr)
 
[Expr1 isnot Expr2]Expr
==
   fn:not(op:node-equal([Expr1]Expr, [Expr2]Expr))

Core Grammar

There are no core grammar rules for node comparisons as they are normalized to other core expressions.

Static Type Analysis

The static semantics for function calls is given in [4.1.5 Function Calls]. The node comparison functions all have return type xs:boolean, as specified in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics rules for function calls is given in [4.1.5 Function Calls].

4.5.4 Order Comparisons

Normalization

The normalization rules for order comparisons map each argument expression and then apply the internal function corresponding to the node comparison operator.

 
[Expr1 << Expr2]Expr
==
op:node-before([Expr1]Expr, [Expr2]Expr)
 
[Expr1 >> Expr2]Expr
==
op:node-after([Expr1]Expr, [Expr2]Expr)

Core Grammar

There are no core grammar rules for order comparisons as they are normalized to other core expressions.

Static Type Analysis

The static semantics for function calls is given in [4.1.5 Function Calls]. The order comparison functions all have return type xs:boolean, as specified in [XQuery 1.0 and XPath 2.0 Functions and Operators].

Dynamic Evaluation

The dynamic semantics for function calls is given in [4.1.5 Function Calls].

Dynamic Errors

The error semantics rules for function calls is given in [4.1.5 Function Calls].

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

Logical Expressions
[55 (XQuery)]   OrExpr   ::=   AndExpr ( "or" AndExpr )*
[56 (XQuery)]   AndExpr   ::=   InstanceofExpr ( "and" InstanceofExpr )*

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
==
fn:boolean([Expr1]Expr) and fn:boolean([Expr2]Expr)
 
[Expr1 or Expr2]Expr
==
fn:boolean([Expr1]Expr) or fn:boolean([Expr2]Expr)

Static Type Analysis

The logical expressions require that each subexpression have type xs:boolean. The result type is also xs:boolean.

statEnv |- Expr1 : xs:boolean      statEnv |- Exprn : xs:boolean

statEnv |- Expr1 and Expr2 : xs:boolean

statEnv |- Expr1 : xs:boolean      statEnv |- Exprn : xs:boolean

statEnv |- Expr1 or Expr2 : xs:boolean

Dynamic Evaluation

The dynamic semantics of logical expressions is non-deterministic. In the expression, Expr1 and Expr2, if either expression raises an error or evaluates to false, the entire expression may raise an error or evaluate to false. In the expression, Expr1 or Expr2, if either expression raises an error or evaluates to true, the entire expression may raise an error or evaluate to true.

dynEnv |- Expri => false      1 <= i <= 2

dynEnv |- Expr1 and Expr2 => false

dynEnv |- Expr1 => true      dynEnv |- Expr2 => true

dynEnv |- Expr1 and Expr2 => true

dynEnv |- Expri => true      1 <= i <= 2

dynEnv |- Expr1 or Expr2 => true

dynEnv |- Expr1 => false      dynEnv |- Expr2 => false

dynEnv |- Expr1 or Expr2 => false

Dynamic Errors

dynEnv |- Expri raises Error      1 <= i <= 2

dynEnv |- Expr1 and Expr2 raises Error

dynEnv |- Expri raises Error      1 <= i <= 2

dynEnv |- Expr1 or Expr2 raises Error

4.7 Constructors

[XPath/XQuery] supports two forms of constructors: a "direct" form that supports literal XML syntax for elements, attributes, and text nodes, and a "computed" form that can be used to construct element and attribute nodes, possibly with computed names, and also document and text nodes.

4.7.1 Direct Element Constructors

Introduction

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

Constructors
[79 (XQuery)]   Constructor   ::=   ElementConstructor
| XmlComment
| XmlPI
| CdataSection
| CompDocConstructor
| CompElemConstructor
| CompAttrConstructor
| CompNSConstructor
| CompTextConstructor
| CompXmlPI
| ComputedXmlComment
[97 (XQuery)]   ElementConstructor   ::=   "<" QName AttributeList ("/>" | (">" ElementContent* "</" QName S? ">"))
[108 (XQuery)]   ElementContent   ::=   ElementContentChar
| "{{"
| "}}"
| ElementConstructor
| EnclosedExpr
| CdataSection
| CharRef
| PredefinedEntityRef
| XmlComment
| XmlPI
[109 (XQuery)]   AttributeList   ::=   (S (QName S? "=" S? AttributeValue)?)*
[110 (XQuery)]   AttributeValue   ::=   ('"' (EscapeQuot | QuotAttrValueContent)* '"')
| ("'" (EscapeApos | AposAttrValueContent)* "'")
[113 (XQuery)]   EnclosedExpr   ::=   "{" Expr "}"

Core Grammar

The core grammar productions for constructors are:

Constructors
[51 (Core)]   Constructor   ::=   XmlComment
| XmlPI
| CdataSection
| CompDocConstructor
| CompElemConstructor
| CompAttrConstructor
| CompNSConstructor
| CompTextConstructor
| CompXmlPI
| ComputedXmlComment
[73 (Core)]   EnclosedExpr   ::=   "{" Expr "}"
ElementContent
[108 (XQuery)]   ElementContent   ::=   ElementContentChar
| "{{"
| "}}"
| ElementConstructor
| EnclosedExpr
| CdataSection
| CharRef
| PredefinedEntityRef
| XmlComment
| XmlPI

Notation

The auxiliary mapping rules []ElementContent, []ElementContent-unit, []Attribute, []AttributeContent, []AttributeContent-unit, []NamespaceAttr, and []NamespaceAttrs, are used for the normalization of the content of direct element and attribute constructors.

Normalization

We start with the rules for normalizing a direct element constructor's content. We distinguish between direct element constructors that contain only one element-content unit and those that contain more than one element-content unit. An element-content unit is a contiguous sequence of literal characters (character references, escaped braces, and predefined entity references), one enclosed expression, one direct element constructor, one CDATA section, one XML comment, or one XML processing instruction. Here are three direct element constructors that each contain one element-content unit:

<date>{ xsd:date("2003-03-18") }</date>

<name>Dizzy Gillespe</name>

<comment><!-- Just a comment --></comment>

The first contains one enclosed expression, the second contains one contiguous sequence of characters, and the third contains one XML comment.

The next example contains six element-content units:

<address>
  <!-- Dizzy's address -->
  { 123 }-0A <street>Roosevelt Ave.</street> Flushing, NY { 11368 }
</address>

It contains one XML comment, followed by one enclosed expression that contains the integer 123, one contiguous sequence of characters ("-0A "), one direct XML element constructor, one contiguous sequence of characters (" Flushing, NY"), and one enclosed expression that contains the integer 11368. Evaluating this expression yields this element value:

<address><!-- Dizzy's address -->123-0A <street>Roosevelt Ave.</street> Flushing, NY 11368</address>

Adjacent element-content units are convenient because they permit arbitrary interleaving of text and atomic data. During evaluation, atomic values are converted to text nodes containing the string representations of the atomic values, and then adjacent text nodes are concatenated together. In the example above, the integer 123 is converted to a string and concatenated with "-0A" and the result is a single text node containing "123-0A".

In general, we do not want to convert all atomic values to text nodes, especially when performing static-type analysis, because we lose useful type information. For example, if we normalize the first example above as follows, we lose the important information that the user constructed a date value, not just a text node containing an arbitrary string:

<date>{ xsd:date("2003-03-18") }</date>
 (normalization that loses type information) == 
element date { text { "2003-03-18" } } 

So to preserve useful type information, we distinguish between direct element constructor's that contain one element-content unit and those that contain more than one (because multiple element-content units commonly denote concatenatation of atomic data and text). Here is the normalization of the first and fourth examples above:

<date>{ xsd:date("2003-03-18") }</date>
 ==
element date { xsd:date("2003-03-18") } 

<address>
  <!-- Dizzy's address -->
  { 123 }-0A <street>Roosevelt Ave.</street> Flushing, NY { 11368 }
</address>
 ==
element address { 
  attribute zip { "11368" }, 
  fs:item-sequence-to-node-sequence( 
    comment { " Dizzy's address "},
    123, 
    text { "-0A "}, 
    element street {"Roosevelt Ave."},
    text { " Flushing, NY"  },
    11368
  )
}
Editorial note 
Mary 2003-03-21: Michael Kay has suggested that instead of distinguishing between direct element constructor's that contain one element-content unit and those that contain more than one element-content unit, we should add a new kind of enclosed expression delimited with {| |} that does not apply the conversion rules and therefore preserves the type information. For example,
<date>{| xsd:date("2003-03-18") |}</date>
 ==
element date { xsd:date("2003-03-18") } 

Given the distinction between direct element constructors that we made above, we give two normalization rules for a direct element constructor's content. If the direct element constructor contains exactly one element-content unit, we simply normalize that unit by applying the normalization rule for the element content:

 
[ ElementContent1 ]ElementContent-unit
==
[ ElementContent1 ]ElementContent

If the direct element constructor contains more than one element-content unit, we normalize each unit individually and construct a sequence of the normalized results interleaved with empty text nodes. The empty text nodes guarantee that the results of evaluating consecutive element-content units can be distinguished. Then we apply the function fs:item-sequence-to-node-sequence, Section [3.7.1 Direct Element Constructors] in [XQuery 1.0: A Query Language for XML] specifies the rules for converting a sequence of atomic values and nodes into a sequence of nodes before element construction. The special function fs:item-sequence-to-node-sequence implements these conversion rules.

 
[ElementContent1 ..., ElementContentn]ElementContent-unit, n > 1
==
fs:item-sequence-to-node-sequence([ ElementContent1 ]ElementContent , text { "" }, ..., text { "" }, [ ElementContentn]ElementContent)

We need to distinguish between multiple element-content units, because the rule for converting sequences of atomic values into strings apply to sequences within distinct enclosed expressions. The empty text nodes are eliminated during evaluation of fs:item-sequence-to-node-sequence 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. For example, here is an expression, its normalization, and the resulting XML value:

<example>{ 1 }{ 2 }</example>
 ==
element example { fs:item-sequence-to-node-sequence ((1, text {""}, 2)) }
 ==>
<example>12</example>

In the absence of the empty text node, the expression would evaluate to the following incorrect value:

<example>{ 1 }{ 2 }</example>
 (incorrect normalization) ==
element example { fs:item-sequence-to-node-sequence ((1, 2)) }
 (incorrect value) ==>
<example>1 2</example>

Now that we have explained the normalization rules for direct element content, we give the rules for the two forms of direct XML element constructors. Note that the direct attribute constructors are normalized twice: the []NamespaceAttrs normalizes the namespace-declaration attributes and []AttributeContent maps all other attributes.

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

Next, we give the normalization rules for each element-content unit. The normalization rule for a contiguous sequence of characters assumes:

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

  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 rule takes the longest consecutive sequence of individual characters that include literal characters, escaped curly braces, character references, and predefined entity references and normalizes the character sequence as a text node containing the string of characters..

 
[(Char | "{{" | "}}" | CharRef | PredefinedEntityRef)+]ElementContent
==
text { fn:codepoints-to-string((Char | "{{" | "}}" | CharRef | PredefinedEntityRef)+) }

XML processing instructions and comments in element content are normalized by applying the standard normalization rules for expressions, which appear in [4.7.2 Other Direct Constructors].

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

An enclosed expression in element content is normalized by normalizing each individual expression in its expression sequence and then constructing a sequence of the normalized values:

 
[ { Expr1, ..., Exprn } ]ElementContent
==
[ Expr1 ]Expr , ..., [ Exprn]Expr

Core Grammar

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

Static Type Analysis

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

Dynamic Evaluation

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

Dynamic Errors

There are no additional error semantics rules for direct XML element or attribute constructors.

4.7.1.1 Attributes

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

[109 (XQuery)]   AttributeList   ::=   (S (QName S? "=" S? AttributeValue)?)*
[110 (XQuery)]   AttributeValue   ::=   ('"' (EscapeQuot | QuotAttrValueContent)* '"')
| ("'" (EscapeApos | AposAttrValueContent)* "'")

Normalization

Direct attribute may contain namespace-declaration attributes. The normalization rules for attributes ignore namespace-declaration attributes -- they are handled by the normalization rules in [4.7.1.2 Namespaces].

As with literal XML elements, we need to distinguish between direct attribute constructors that contain one attribute-content unit and those that contain multiple attribute-content units, because the rule for converting sequences of atomic values into strings are applied to sequences within distinct enclosed expressions. If the direct attribute constructor contains exactly one attribute-content unit, we simply normalize that unit by applying the normalization rule for the attribute content:

 
[ AttributeValueContent1 ]AttributeContent-unit
==
[AttributeValueContent1]AttributeContent

If the direct attribute constructor contains more than one attribute-content unit, we normalize each unit individually and construct a sequence of the normalized results interleaved with empty text nodes. The empty text nodes guarantee that the results of evaluating consecutive attribute-content units can be distinguished. Then we apply the function fs:item-sequence-to-untypedAtomic, which applies the appropriate conversion rules to the normalized attribute content:

 
[ AttributeValueContent1 ..., AttributeValueContentn ]AttributeContent-unit, n > 1
==
fs:item-sequence-to-untypedAtomic([ AttributeValueContent1 ]AttributeContent , text { "" }, ..., text {""}, [ 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.

 
[
QName1 S? = S? '"' AttributeValue0 '"'
QNamen S? = S? '""' AttributeValuen '"'
]AttributeContent
==
([QName1 S? = S? '"' AttributeValue0 '"']Attribute
...,
[QNamen S? = S? '"' AttributeValuen '"']Attribute)

Namespace-declaration attributes, i.e., those attributes whose prefix is xmlns are ignored by mapping them to the empty sequence.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']Attribute
(Prefix = xmlns)
==
()

All attributes that are not namespace-declaration attributes are mapped to computed attribute constructors.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']Attribute
not(Prefix = xmlns)
==
attribute [Prefix:LocalPart ]Expr { [AttributeValue]AttributeContent}

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 include 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
==
fn:codepoints-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)
4.7.1.2 Namespaces

Normalization

Direct attribute may contain namespace-declaration attributes. The normalization rules for namespace-declaration attributes ignore all non-namespace attributes -- they are handled by the normalization rules in [4.7.1.1 Attributes].

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

 
[
QName1 S? = S? '"' AttributeValue0 '"'
QNamen S? = S? '""' AttributeValuen '"'
]NamespaceAttrs
==
([QName1 S? = S? '"' AttributeValue0 '"']NamespaceAttr
...,
[QNamen S? = S? '"' AttributeValuen '"']NamespaceAttr)

Attributes whose prefix is not xmlns are ignored by mapping them to the empty sequence.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']Attribute
not (Prefix = xmlns)
==
()

Namespace-declaration attributes are normalized to computed namespace constructors.

 
[Prefix:LocalPart S? = S? '"' AttributeValue '"']Attribute
(Prefix = xmlns)
==
namespace [Prefix:LocalPart ]Expr { [AttributeValue]AttributeContent}
4.7.1.3 Content
4.7.1.4 Whitespace in Element Content

Section [3.7.1.4 Whitespace in Element Content] 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.

4.7.1.5 Type of a Constructed Element

4.7.2 Other Direct Constructors

Other Constructors
[105 (XQuery)]   CdataSection   ::=   "<![CDATA[" Char* "]]>"
[106 (XQuery)]   XmlPI   ::=   "<?" PITarget Char* "?>"
[18 (XQuery)]   PITarget   ::=   NCName
[107 (XQuery)]   XmlComment   ::=   "<!--" Char* "-->"

Core Grammar

The core grammar productions for other constructors and comments are:

[69 (Core)]   CompTextConstructor   ::=   "text" "{" Expr? "}"
[67 (Core)]   CompXmlPI   ::=   (("pi" NCName "{") | ("pi" "{" Expr "}" "{")) Expr? "}"
[68 (Core)]   ComputedXmlComment   ::=   "comment" "{" Expr "}"

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* "]]>]ElementContent
==
[Char*]ElementContent

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

 
[<? NCName Char* ?>"]Expr
==
processing-instruction 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
==
comment { [Char*]AttributeContent }

Static Type Analysis

There are no additional static type rules for CDATA or direct processing-instruction constructors.

Dynamic Evaluation

There are no additional dynamic evaluation rules for CDATA or direct processing-instruction constructors.

Dynamic Errors

There are no additional error semantics rules for CDATA or direct processing-instruction constructors.

4.7.3 Computed Constructors

Computed Constructors
[99 (XQuery)]   CompElemConstructor   ::=   (("element" QName "{") | ("element" "{" Expr "}" "{")) Expr? "}"
[101 (XQuery)]   CompAttrConstructor   ::=   (("attribute" QName "{") | ("attribute" "{" Expr "}" "{")) Expr? "}"
[98 (XQuery)]   CompDocConstructor   ::=   "document" "{" Expr "}"
[104 (XQuery)]   CompTextConstructor   ::=   "text" "{" Expr? "}"
[102 (XQuery)]   CompXmlPI   ::=   (("pi" NCName "{") | ("pi" "{" Expr "}" "{")) Expr? "}"
[103 (XQuery)]   ComputedXmlComment   ::=   "comment" "{" Expr "}"
[100 (XQuery)]   CompNSConstructor   ::=   ("namespace" NCName "{") Expr "}"
4.7.3.1 Computed Element Constructors

Notation

Computed namespace constructors may only occur directly within computed element constructors. Computed namspace constructors may occur explicitly in the query or may be the result of normalizing namespace-declaration attributes. To simplify typing and evaluation, we assume that the mapping function []SplitNamespaces reorders the expressions in the element constructor so that all namespace constructors preceed all other expressions. We do not define this mapping function formally.

Normalization

Computed element constructors are normalized by mapping their name and content expression.

 
[element QName { Expr }]Expr
==
element [QName]Expr { [ [Expr]SplitNamespaces ]Expr }

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 or a xs:string. If the name expression returns a string, that string is implicitly cast to a QName by using the fn:QName-in-context function with its $use-default parameter set to true. The resulting expanded QName is used as the name of the constructed element.

 
[element { Expr1 } { Expr2 }]Expr
==
let $fs:new1 as (xs:QName | xs:string) := [Expr1]Expr return
let $fs:new3 :=
     typeswitch ($fs:new1)
     case $fs:new2 as xs:QName return $fs:new2
     case $fs:new2 as xs:string return fn:QName-in-context($fs:new2, fn:true())
     default return fn:error()
return element { $fs:new3 }{ [[Expr2]SplitNamespaces ]Expr }

Static Type Analysis

The normalization rules leave us with only the computed form of the element constructor. The computed constructor also has two forms: one in which the element name is a literal QName, and the other in which the element name is a computed expression.

We start with the static rule for an element constructor with a computed name expression, because it is the simplest rule. Because the element's name cannot be known until runtime, the element is given the wildcard type, element * of type xdt:untypedAny. The computed name expression must have type xs:QName and the content expression must have a type of zero-or-more attributes followed by zero-or-more element, text, comment, or processing-instruction nodes.

statEnv |- Expr1 : xs:QName
statEnv |- Expr2 : attribute *, (element | text | comment | processing-instruction) *

statEnv |- element { Expr1 } { Expr2 } : element * of type xdt:untypedAny

In the first rule for a computed element constructor with a literal QName, we consider the case in which the validation mode is set to "skip", which means that all type information in the element is ignored and the new element is labeled with the type xdt:untypedAny. The content expression must have a type of zero-or-more attributes followed by zero-or-more element, text, comment, or processing-instruction nodes. The result type is an element of type xdt:untypedAny.

statEnv.validationMode = "skip"
statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- Expr2 : attribute *, (element | text | comment | processing-instruction) *

statEnv |- element QName { Expr } : element ExpandedQName of type xdt:untypedAny

In the remaining rules, the validation mode is either "lax" or "strict", and the static rules for element constructors check that the type of the element's content expression are valid with respect to the type of the element being constructed.

Recall that in the static semantics of arithmetic, general comparison, and function arguments, the static rules are liberal when an expression with type xdt:untypedAtomic is used in the context where an atomic typed expression is required. In these cases, it is not possible to determine statically whether the evaluation-time cast of the xdt:untypedAtomic value to the required type will succeed, but the rules optimistically assume that they will. In all other cases, the static rules are conservative and require that the type of the argument expression be a subtype of the required type. We apply a similar static semantics to element constructors in which the required type of the constructed element is simple, i.e., a subtype of xdt:anyAtomicType*

The first rule below applies to element constructors whose required type is simple. If the content expression is a sequence of expressions all of which have type untypedAtomic or text, we apply a liberal static rule (i.e., assume the run-time validation will succeed) and assign the appropriate static type:

statEnv.validationMode = "lax" or statEnv.validationMode = "strict"
statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- element ExpandedQName in context statEnv.validationContext static lookup ElementName of type TypeName
statEnv |- of type TypeName resolves to Type      Type <: (attribute*, xdt:anyAtomicType)
statEnv + validationContext(TypeName) |- Expr : Type1      Type1 <: (attribute*, (xdt:untypedAtomic | text)*)

statEnv |- element QName { Expr } : element ExpandedQName of type TypeName

The second rule also applies to element constructors whose required type is simple and whose content expression is not a sequence of expressions of type xdt:untypedAtomic or text. In this case, the static rule is conservative and requires that the type of the context expression be a subtype of the element's required type.

statEnv.validationMode = "lax" or statEnv.validationMode = "strict"
statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- element ExpandedQName in context statEnv.validationContext static lookup ElementName of type TypeName
statEnv |- of type TypeName resolves to Type      Type <: (attribute*, xdt:anyAtomicType*)
statEnv + validationContext(TypeName) |- Expr : Type1      not(Type1 <: (xdt:untypedAtomic | text)* )
statEnv |- Type1 <: Type

statEnv |- element QName { Expr } : element ExpandedQName of type TypeName

The third rule applies to element constructors whose required type is complex. In this case, the static type rule is conservative: the type of the element's content expression must be a subtype of its required type.

statEnv.validationMode = "lax" or statEnv.validationMode "strict"
statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- element ExpandedQName in context statEnv.validationContext static lookup ElementName of type TypeName
statEnv |- of type TypeName resolves to Type      not(Type <: (attribute*, xdt:anyAtomicType*))
statEnv + validationContext(TypeName) |- Expr : Type1
statEnv |- Type1 <: Type

statEnv |- element QName { Expr } : element ExpandedQName of type TypeName

Dynamic Evaluation

The following dynamic-semantics rules construct an element from its name and content expression. The dynamic semantics of the element constructor expression is the most complex semantics in XQuery. Here is how to read the rule below.

First, the element's name is expanded into a qualified name.

Second, the element's content expression is partitioned into the computed namespace constructors and all other expressions, and the computed namespace constructors are evaluated, yielding a sequence of namespace annotations. The static environment is extended to include the new namespace annotations, which are all active.

Third, the function fs:item-sequence-to-node-sequence is applied to the element's content expression (excluding computed namespace constructors); this function call is evaluated in the new static and dynamic environment. Recall from the section on normalization that during normalization, we do not convert the content of direct element constructors that contain one element-content unit. This guarantees that useful type information is preserved for static analysis. Since the conversion function fs:item-sequence-to-node-sequence was not applied to all element constructors during normalization, we have to apply it at evaluation time. (Obviously, it is possible to elide the application of fs:item-sequence-to-node-sequence injected during normalization and the application injected during evaluation.) The resulting value Value0 must match zero-or-more attributes followed by zero-or-more element, text, processing-instruction or comment nodes.

Fourth, The namespace annotations are concatenated with the list of active namespaces in the namespace environment statEnv.namespace and the namespaces corresponding to the element's name and all attributes names. The resulting sequence is the sequence of namespace annotations for the element.

Lastly, recall that an element constructor automatically validates the constructed element node, using the validation mode and validation context from its static context. The last step in evaluation is to construct a new element with type annotation xdt:untypedAny and with content Value0 and then validate the element using the validation mode and context from the static environment.

statEnv |- fs:expand(QName) = ExpandedQName
Expr = ComputedNamespaceConstructor1, ..., ComputedNamespaceConstructorn, (Expr0)
statEnv, dynEnv |- ComputedNamespaceConstructor1, => NamespaceAnnotation1
...
statEnv, dynEnv |- ComputedNamespaceConstructorn, => NamespaceAnnotationn
NamespaceAnnotation1 = namespace NCName1 { URI1 }
statEnv1 = statEnv + namespace(NCName => (active, URI1))
...
NamespaceAnnotationn = namespace NCNamen { URIn }
statEnvn = statEnvn-1 + namespace(NCName => (active, URIn))
statEnvn, dynEnv |- fs:item-sequence-to-node-sequence (Expr0); => Value0
Value0 matches (attribute*, (element | text | processing-instruction | comment)*)
NamespaceAnnotations = (NamespaceAnnotation1, ... NamespaceAnnotationn), fs:active_ns(statEnv.namespace), fs:get_ns_from_items(statEnv, Value0)
statEnvn, dynEnv |- validate statEnv.validationMode statEnv.validationContext { element ExpandedQName of type xdt:untypedAny { Value0 } { NamespaceAnnotations } } => Value1

statEnv dynEnv |- element QName { Expr } => Value1

The dynamic evaluation of an element constructor with a computed name is similar.

dynEnv |- Expr1 => Value0      statEnv |- Value0 matches xs:QName
Expr2 = ComputedNamespaceConstructor1, ..., ComputedNamespaceConstructorn, (Expr3)
statEnv, dynEnv |- ComputedNamespaceConstructor1, => NamespaceAnnotation1
...
statEnv, dynEnv |- ComputedNamespaceConstructorn, => NamespaceAnnotationn
NamespaceAnnotation1 = namespace NCName1 { URI1 }
statEnv1 = statEnv + namespace(NCName => (active, URI1))
...
NamespaceAnnotationn = namespace NCNamen { URIn }
statEnvn = statEnvn-1 + namespace(NCName => (active, URIn))
statEnvn, dynEnv |- fs:item-sequence-to-node-sequence (Expr3); => Value1
statEnvn |- Value1 matches (attribute*, (element | text | processing-instruction | comment)*)
NamespaceAnnotations = (NamespaceAnnotation1, ... NamespaceAnnotationn), fs:active_ns(statEnv.namespace), fs:get_ns_from_items(statEnv, Value1)
statEnvn, dynEnv |- validate statEnv.validationMode statEnv.validationContext { element { Value0 } of type xdt:untypedAny { Value1 } } => Value2

statEnv dynEnv |- element { Expr1 } { Expr2 } { NamespaceAnnotations } => Value2

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to element constructors. In addition, an element constructor with a computed name raises a type error if the name value is not a xs:QName.

dynEnv |- Expr1 => Value1      statEnv |- not (Value matches xs:QName)

dynEnv |- element { Expr1 } { Expr2 } raises typeError

Both forms of element constructors raises a type error if the element's content is not a sequence of attributes followed by a sequence of element, text, comment, or processing-instruction nodes.

dynEnv |- Expr2 => Value2
statEnv |- not (Value matches (attribute *, (element | text | comment | processing-instruction )*))

dynEnv |- element { Expr1 } { Expr2 } raises typeError

dynEnv |- Expr2 => Value2
statEnv |- not (Value matches (attribute *, (element | text | comment | processing-instruction )*))

dynEnv |- element QName { Expr2 } raises typeError

4.7.3.2 Computed Attribute Constructors

Normalization

Computed attribute constructors are normalized by mapping their name and content expression in the same way that computed element constructors are normalized.

 
[attribute QName { Expr }]Expr
==
attribute [QName]Expr { [Expr]Expr }
 
[attribute { Expr1 } { Expr2 }]Expr
==
let $fs:new1 as (xs:QName | xs:string) := [Expr1]Expr return
let $fs:new3 :=
     typeswitch ($fs:new1)
     case $fs:new2 as xs:QName return $fs:new2
     case $fs:new2 as xs:string return fn:QName-in-context($fs:new2, fn:true())
     default return fn:error()
return attribute { $fs:new3 } { [Expr2]Expr }

Core Grammar

The core grammar rules for computed element and attribute constructors are:

Core computed element and attribute construtors
[64 (Core)]   CompElemConstructor   ::=   (("element" QName "{") | ("element" "{" Expr "}" "{")) Expr? "}"
[66 (Core)]   CompAttrConstructor   ::=   (("attribute" QName "{") | ("attribute" "{" Expr "}" "{")) Expr? "}"

Static Type Analysis

The normalization rules leave us with only the computed form of the attribute constructors. The computed constructor also has two forms: one in which the attribute name is a literal QName, and the other in which the attribute name is a computed expression.

We start with the static rule for an attribute constructor with a computed name expression, because it is the simplest rule. The computed name expression must have type xs:QName. The result type is an attribute of type xdt:untypedAtomic.

statEnv |- Expr1 : xs:QName

statEnv |- attribute { Expr1 } { Expr2 } : attribute * of type xdt:untypedAtomic

In the first rule for a computed attribute constructor with a literal QName, we consider the case in which the validation mode is set to "skip", which means that all type information in the attribute is ignored and the new attribute is labeled with the type xdt:untypedAtomic.

statEnv.validationMode = "skip"
statEnv |- fs:expand(QName) = ExpandedQName

statEnv |- attribute QName { Expr } : element ExpandedQName of type xdt:untypedAtomic

In the remaining rules, the validation mode is either "lax" or "strict", and the static rules for attribute constructors check that the type of the attribute's content expression are valid with respect to the type of the attribute being constructed.

As in element constructors, the static rules are liberal when a single xdt:untypedAtomic content expression is provided as an argument and conservative, otherwise.

If the content expression is a sequence of expressions all of which are untypedAtomic, we apply a liberal static rule (i.e., assume the validation will succeed) and assign the appropriate static type:

statEnv.validationMode = "lax" | "strict"
statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- attribute ExpandedQName in statEnv.validationContext => AttributeName TypeReference
statEnv |- Expr : Type1      Type1 <: xdt:untypedAtomic *

statEnv |- attribute QName { Expr } : attribute ExpandedQName TypeReference

In the second case, the static type rule is conservative: the type of the attribute's content expression must be a subtype of its required type.

statEnv.validationMode = "lax" | "strict"
statEnv |- fs:expand(QName) = ExpandedQName
statEnv |- attribute ExpandedQName in statEnv.validationContext => AttributeName of type TypeName      statEnv |- of type TypeName resolves to Type
statEnv |- Expr : Type1      not(Type1 <: xdt:untypedAtomic *)
statEnv |- Type1 <: Type

statEnv |- attribute QName { Expr } : attribute ExpandedQName of type TypeName

Dynamic Evaluation

The following rules construct an attribute from its name and content expression. The rules are similar to those for element constructors. First, the attribute's name is expanded into a qualified name. Second, the function fs:item-sequence-to-untypedAtomic is applied to the content expression and this function call is evaluated in the dynamic environment. Recall from the section on normalization that during normalization, we do not convert the content of direct attribute constructors that contain one attribute-content unit. This guarantees that useful type information is preserved for static analysis. Since the conversion function fs:item-sequence-to-untypedAtomic was not applied to all attribute constructors during normalization, we have to apply it at evaluation time. (As before, it is possible to elide the application of fs:item-sequence-to-untypedAtomic injected during normalization and the application injected during evaluation.) The resulting value Value0 must match zero-or-more attributes followed by zero-or-more element, text, processing-instruction or comment nodes.

statEnv |- fs:expand(QName) = ExpandedQName
dynEnv |- fs:item-sequence-to-untypedAtomic(Expr) => Value

dynEnv |- attribute QName { Expr } => attribute ExpandedQName { Value }

dynEnv |- Expr => Value0      statEnv |- Value0 matches xs:QName
dynEnv |- fs:item-sequence-to-untypedAtomic(Expr) => Value

dynEnv |- attribute { Expr } { Expr } => attribute { Value0 } { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to attribute constructors. In addition, an attribute constructor with a computed name raises a type error if the name value is not a xs:QName.

dynEnv |- Expr1 => Value1      statEnv |- not (Value matches xs:QName)

dynEnv |- attribute { Expr1 } { Expr2 } raises typeError

4.7.3.3 Document Node Constructors

Normalization

A document node constructor contains an expression, which must evaluate to a sequence of element, text, comment, or processing-instruction nodes. Section [3.7.2.3 Document Node Constructors] in [XQuery 1.0: A Query Language for XML] specifies the rules for converting a sequence of atomic values and nodes into a sequence of nodes before document construction. The special function fs:item-sequence-to-node-sequence([6.1.2 The fs:item-sequence-to-node-sequence function]) implements this conversion.

 
[document { Expr }]Expr
==
document { fs:item-sequence-to-node-sequence([Expr]Expr) }

Core Grammar

The core grammar rule for a computed document constructor is:

Core computed document construtor
[63 (Core)]   CompDocConstructor   ::=   "document" "{" Expr "}"

Static Type Analysis

The static semantics checks that the type of the argument expression is a sequence of element, text, processing-instruction, and comment nodes. The type of the entire expression is a document with the given content type.

statEnv |- Expr : Type      Type <: (element | text | processing-instruction | comment)*

statEnv |- document { Expr } : document { Type }

Dynamic Evaluation

The dynamic semantics checks that the argument expression evaluates a value that is a sequence of element, text, processing-instruction, or comment nodes. The entire expression evaluates to a new document node value.

dynEnv |- Expr => Value      dynEnv |- Value matches (element | text | processing-instruction | comment)*

dynEnv |- document { Expr } => document { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to document node constructors. In addition, if the argument expression evaluates to a value that is not a sequence of element, text, processing-instruction, or comment nodes, a type error is raised.

dynEnv |- Expr => Value      dynEnv |- not (Value matches (element | text | processing-instruction | comment )*)

dynEnv |- document { Expr } raises typeError

4.7.3.4 Text Nodes Constructors

Normalization

A text node constructor contains an expression, which must evaluate to an xs:string value. Section [3.7.2.4 Text Node Constructors ] 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 fs:item-sequence-to-untypedAtomic([6.1.3 The fs:item-sequence-to-untypedAtomic function]) implements this conversion.

 
[text { Expr }]Expr
==
text { fs:item-sequence-to-node-sequence([Expr]Expr) }

Core Grammar

The core grammar rule for a computed text constructor is:

Core computed text construtor
[69 (Core)]   CompTextConstructor   ::=   "text" "{" Expr? "}"

Static Type Analysis

The static semantics checks that the argument expression has type xs:string. The type of the entire expression is simply the text node type.

statEnv |- Expr : xs:string

statEnv |- text { Expr } : text

Dynamic Evaluation

The dynamic semantics checks that the argument expression evaluates a value of type xs:string. The entire expression evaluates to a new text node.

dynEnv |- Expr => Value      dynEnv |- Value matches xs:string

dynEnv |- text { Expr } => text { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to text node constructors. In addition, if the argument expression evaluates to a value that is not a string, a type error is raised.

dynEnv |- Expr => Value      dynEnv |- not (Value matches xs:string)

dynEnv |- text { Expr } raises typeError

Editorial note: Mary 
Because of the normalization rules for text nodes, which apply fs:item-sequence-to-untypedAtomic, the above static and dynamic type checks turn out to be redundant, but for completeness, they are included.
4.7.3.5 Computed Processing Instruction Constructors

Normalization

Computed processing-instruction constructors are normalized by mapping their name and content expression in the same way that computed element and attribute constructors are normalized.

 
[pi QName { Expr }]Expr
==
pi [QName]Expr { fs:item-sequence-to-untypedAtomic ([Expr]Expr ) }
 
[pi { Expr1 } { Expr2; }]Expr
==
let $fs:new1 as (xs:QName | xs:string) := [Expr1]Expr return
let $fs:new3 :=
     typeswitch ($fs:new1)
     case $fs:new2 as xs:QName return $fs:new2
     case $fs:new2 as xs:string return fn:QName-in-context($fs:new2, fn:true())
     default return fn:error()
return pi { $fs:new3 } { fs:item-sequence-to-untypedAtomic ([Expr2]Expr) }

Core Grammar

The core grammar rule for computed processing-instruction constructors is:

[67 (Core)]   CompXmlPI   ::=   (("pi" NCName "{") | ("pi" "{" Expr "}" "{")) Expr? "}"

Static Type Analysis

The static typing rules for processing-instruction constructors are straightforward.

statEnv |- Expr : xs:string

statEnv |- pi NCName { Expr } : processing-instruction

statEnv |- Expr1 : xs:QName      statEnv |- Expr2 : xs:string

statEnv |- pi { Expr1 } { Expr2 } : processing-instruction

Dynamic Evaluation

The dynamic evaluation rules for computed processing instructions are straightforward.

dynEnv |- Expr => Value      dynEnv |- Value matches xs:string

dynEnv |- pi NCName { Expr } => processing-instruction NCName { Value }

dynEnv |- Expr1 => Value1      dynEnv |- Value1 matches xs:QName
dynEnv |- Expr2 => Value2      dynEnv |- Value2 matches xs:string

dynEnv |- pi { Expr1 } { Expr2 } => processing-instruction Value1 { Value2 }

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to computed processing-instruction constructors.

4.7.3.6 Computed Comment Constructors

Normalization

Computed processing-instruction constructors are normalized by mapping their content expression.

 
[comment { Expr }]Expr
==
comment { [Expr]Expr }

Core Grammar

The core grammar rule for computed comment constructors is:

[68 (Core)]   ComputedXmlComment   ::=   "comment" "{" Expr "}"

Static Type Analysis

Dynamic Evaluation

Dynamic Errors

Static Type Analysis

The static typing rule for computed comment constructors is straightforward.

statEnv |- Expr : xs:string

statEnv |- comment { Expr } : comment

Dynamic Evaluation

The dynamic evaluation rule for computed comment constructors is straightforward.

dynEnv |- Expr => Value      dynEnv |- Value matches xs:string

dynEnv |- comment { Expr } => comment { Value }

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to computed comment constructors.

4.7.3.7 Computed Namespace Constructors

Normalization

Computed namespace constructors are normalized by mapping their name and content expression in the same way as computed processing-instruction constructors.

 
[namespace NCName { Expr }]Expr
==
namespace [NCName]Expr { fs:item-sequence-to-untypedAtomic ([Expr]Expr ) }

Core Grammar

The core grammar rule for computed namespace constructors is:

[65 (Core)]   CompNSConstructor   ::=   ("namespace" NCName "{") Expr "}"

Static Type Analysis

A computed namespace constructor may only occur within a computed element constructor. The result of evaluating a computed element constructor is a namespace annotation, which annotates the element thats results from evaluating the containing computed element constructor. Because the computed namespace constructor has no effect on the type of the element that it annotates, it is given the empty-sequence type.

statEnv |- Expr : xs:string

statEnv |- namespace NCName { Expr } : empty

Dynamic Evaluation

The dynamic evaluation rules for a computed namespace constructor are given in the evaluation rules for computed element constructors in [4.7.3.1 Computed Element Constructors].

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to computed namespace constructors.

4.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 declaration which specify the type expected for the variable.

[For/FLWR] Expressions
[42 (XQuery)]   FLWORExpr   ::=   (ForClause | LetClause)+ WhereClause? OrderByClause? "return" ExprSingle
[43 (XQuery)]   ForClause   ::=   "for" "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle ("," "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle)*
[45 (XQuery)]   LetClause   ::=   "let" "$" VarName TypeDeclaration? ":=" ExprSingle ("," "$" VarName TypeDeclaration? ":=" ExprSingle)*
[122 (XQuery)]   TypeDeclaration   ::=   "as" SequenceType
[44 (XQuery)]   PositionalVar   ::=   "at" "$" VarName
[46 (XQuery)]   WhereClause   ::=   "where" Expr
[47 (XQuery)]   OrderByClause   ::=   ("order" "by" | "stable" "order" "by") OrderSpecList
[48 (XQuery)]   OrderSpecList   ::=   OrderSpec ("," OrderSpec)*
[49 (XQuery)]   OrderSpec   ::=   ExprSingle OrderModifier
[50 (XQuery)]   OrderModifier   ::=   ("ascending" | "descending")? (("empty" "greatest") | ("empty" "least"))? ("collation" StringLiteral)?
[25 (XPath)]   ForExpr   ::=   SimpleForClause "return" ExprSingle
[26 (XPath)]   SimpleForClause   ::=   "for" "$" VarName "in" ExprSingle ("," "$" VarName "in" ExprSingle)*

4.8.1 FLWOR 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:

[For/FLWR] Clauses
[75 (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

The [For/FLWR] expressions include the FLWRExpr of XQuery and the ForExpr of XPath. The normalization rule for ForExpr is simple: It simply unrolls a ForExpr that binds multiple variables into nested ForExprs, each of which bind one variable.

 
[for Variable0 in Expr0, ..., Variablen in Exprn return Expr ]Expr
==
for Variable0 in [Expr0]Expr return
...
for Variablen in [Exprn]Expr return
[Expr]Expr

Full FLWRExpr 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 | OrderByClause) FLWRExpr ]Expr
==
[(ForClause | LetClause | WhereClause | OrderByClause)]FLWR([FLWRExpr]Expr)
 
[ (ForClause | LetClause | WhereClause | OrderByClause) return Expr ]Expr
==
[(ForClause | LetClause | WhereClause | OrderByClause)]FLWR([Expr]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 Variable1 TypeDeclaration1? PositionalVar1? in Expr1,..., Variablen TypeDeclarationn? PositionalVarn? in Exprn ] FLWR(Expr)
==
for Variable1 TypeDeclaration1? PositionalVar1? in [Expr1]Expr return
  ···
     for Variablen TypeDeclarationn? PositionalVarn? in [ Exprn ]Expr return Expr

Each individual for clause, is then normalized to always have a type declaration.

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 Variable1 TypeDeclaration1? := Expr1, ···, Variablen TypeDeclarationn? := Exprn]FLWR(Expr)
==
let Variable1 TypeDeclaration1? := [Expr1 ]Expr return
  ···
    let Variablen TypeDeclarationn? := [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 $i as xs:integer 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 $i as xs:integer 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>)

4.8.2 For expression

Core Grammar

After normalization, single for expressions are described by the following core grammar production.

For Expressions
[34 (Core)]   ForClause   ::=   "for" "$" VarName TypeDeclaration? PositionalVar? "in" ExprSingle
[35 (Core)]   PositionalVar   ::=   "at" "$" VarName
[82 (Core)]   TypeDeclaration   ::=   "as" 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 union over all item types in Type1 (see also [7.5 Judgments for sequences of item types]). With the variable component of the static environment statEnv extended with Variable1 as type prime(Type1) (and Variablepos as type xs:integer, if it is present), 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)

statEnv |- Expr1 : Type1
statEnv + varType(Variable1 : prime(Type1), Variablepos : xs:integer) |- Expr2 : Type2

statEnv |- for Variable1 at Variablepos in Expr1 return Expr2 : Type2 · quantifier(Type1)

In the case a type declaration is present, the static semantics also checks that the type of the input expression is a subtype of the declared type and extends the static environment by typing Variable1 with type Type0. This semantics is specified by the following typing rule.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv + varType(Variable1 : Type0)) |- Expr2 : Type2

statEnv |- for Variable1 as SequenceType in Expr1 return Expr2 : Type2 · quantifier(Type1)

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv + varType(Variable1 : Type0, Variablepos : xs:integer) |- Expr2 : Type2

statEnv |- for Variable1 as SequenceType at Variablepos in Expr1 return Expr2 : Type2 · quantifier(Type1)

Example

For example, if $example is bound to the sequence 10.0, 1.0E1, 10 of type xsd:decimal, xsd:float, xsd:integer, then the query

  for $s in $example
  return $s * 2

is typed as follows:

  (1) prime(xsd:decimal, xsd:float, xsd:integer) =
      xsd:decimal | xsd:float | xsd:integer
  (2) quantifier(xsd:decimal, xsd:float, xsd:integer) = +
  (3) $s : xsd:decimal | xsd:float | xsd:integer
  (4) $s * 2 : 
      xsd:decimal | xsd:float | xsd:integer
  (5) result-type :
      ( xsd:decimal | xsd:float | xsd:integer ) +

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 Variable1 TypeDeclaration? in Expr1 return Expr2 => ()

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. If the optional positional variable Variablepos is present, it is bound to the position of the item in the input sequence, i.e., the value i.

dynEnv |- Expr1 => Item1 ,..., Itemn
dynEnv + varValue(Variable => Item1) |- Expr2 => Value1
···
dynEnv + varValue(Variable => Itemn) |- Expr2 => Valuen

dynEnv |- for Variable in Expr1 return Expr2 => Value1 ,..., Valuen

dynEnv |- Expr1 => Item1 ,..., Itemn
dynEnv + varValue(Variable => Item1, Variablepos => 1) |- Expr2 => Value1
···
dynEnv + varValue(Variable => Itemn, Variablepos => n) |- Expr2 => Valuen

dynEnv |- for Variable at Variablepos in Expr1 return Expr2 => Value1 ,..., Valuen

In the case a type declaration is present, the dynamic semantics also checks that each item in the result of evaluating Expr1 matches the declared type. This semantics is specified as the following dynamic rule.

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
Item1 matches Type0
dynEnv + varValue(Variable => Item1) |- Expr2 => Value1
···
Itemn matches Type0
dynEnv + varValue(Variable => Itemn) |- Expr2 => Valuen

dynEnv |- for Variable as SequenceType in Expr1 return Expr2 => gr_Value1; ,..., Valuen

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
Item1 matches Type0
dynEnv + varValue(Variable => Item1, Variablepos => 1) |- Expr2 => Value1
···
Itemn matches Type0
dynEnv + varValue(Variable => Itemn, Variablepos => n) |- Expr2 => Valuen

dynEnv |- for Variable as SequenceType at Variablepos in Expr1 return Expr2 => Value1 ,..., Valuen

It is important to note that the definition allows non-deterministic evaluation of the resulting sequence, since the judgements above the inference rule can be evaluated in any order.

Dynamic Errors

If evaluation of the first expression raises an error, the entire expression raises an error. This rule applies to expressions with or without the type declaration or positional variable.

dynEnv |- Expr1 raises Error

dynEnv |- for Variable1 TypeDeclaration1? PositionalVar1? in Expr1 return Expr2 raises Error

If any evaluation of the body of the for expression raises an error, then the entire expression raises an error. This rule applies to for expressions with or without the type declaration.

dynEnv |- Expr1 => Item1 ,..., Itemn
dynEnv + varValue(Variable => Itemi) |- Expr2 raises Error      1 <= i <= n

dynEnv |- for Variable TypeDeclaration? in Expr1 return Expr2 raises Error

dynEnv |- Expr1 => Item1 ,..., Itemn
dynEnv + varValue(Variable => ItemiVariablepos => i) |- Expr2 raises Error      1 <= i <= n

dynEnv |- for Variable TypeDeclaration? at Variablepos in Expr1 return Expr2 raises Error

In the case a type declaration is present, a type error is raised if any item in the result of evaluating Expr1 does not match the declared type.

dynEnv |- Expr1 => Item1 ,..., Itemn
Type0 = [ SequenceType ]sequencetype
not (Itemi matches Type0)      1 <= i <= n

dynEnv |- for Variable as SequenceType PositionalVar1? in Expr1 return Expr2 raises typeError

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:

  
  (<i>1</i>,
   <negi>-1</negi>,
   <i>2</i>,
   <negi>-2</negi>)

4.8.3 Let Expression

Core Grammar

After normalization, single let expressions are described by the following core grammar production.

Let Expressions
[36 (Core)]   LetClause   ::=   "let" "$" VarName TypeDeclaration? ":=" ExprSingle

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 declaration is present, the static semantics also checks that the type of the input expression is a subtype of the declared type and extends the static environment by typing Variable1 with type Type0. This semantics is specified as the following typing rule.

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
Type1 <: Type0
statEnv + varType(Variable1 : Type0 ) |- Expr2 : Type2

statEnv |- let Variable1 as SequenceType := 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 declaration is present, the dynamic semantics also checks that the result of evaluating Expr1 matches the declared 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 Variable1 as SequenceType := Expr1 return Expr2 => Value2

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to let expressions. In addition, in the case that a type declaration is present, a type error is raised if the result of evaluating Expr1 does not match the declared type.

dynEnv |- Expr1 => Value1
Type0 = [ SequenceType ]sequencetype
not (Value1 matches Type0)

dynEnv |- let Variable1 as SequenceType := Expr1 return Expr2 raises typeError

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.

4.8.4 Order By and Return Clauses

[For/FLWR] Expressions
[37 (Core)]   OrderByClause   ::=   ("order" "by" | "stable" "order" "by") OrderSpecList
[38 (Core)]   OrderSpecList   ::=   OrderSpec ("," OrderSpec)*
[39 (Core)]   OrderSpec   ::=   ExprSingle OrderModifier
[40 (Core)]   OrderModifier   ::=   ("ascending" | "descending")? (("empty" "greatest") | ("empty" "least"))? ("collation" StringLiteral)?

Introduction

The formal semantics of order by is not fully specified. The static semantics is object by normalizing the order by clause as a simple for loop. The dynamic semantics is not specified formally as it would require the introduction of a notion of tuples which are not supported in the [XPath/XQuery] data model. The dynamic semantics of the order by clause can be found in [XQuery 1.0: A Query Language for XML].

Notation

To define normalization of OrderBy, the following auxiliary mapping rule is used.

 
[OrderSpecList]OrderSpecList
==
Expr

which specify that OrderSpecList is mapped to Expr.

Normalization

An OrderByClause is normalized to a let clause, nested for loops, and atomization. Note that if evaluated dynamically, the order by normalization proposed here would not deal with the sorting semantics, but still this normalization will provide the correct static type.

 
[ stable? order by OrderSpecList]FLWR(Expr)
==
let $fs:new0 := [OrderSpecList]OrderSpecList return Expr

Each OrderSpec is normalized the auxiliary atomization normalization rule.

 
[ Expr OrderModifier, OrderSpecList]OrderSpecList
==
for $fs:new in fn:data(Expr) [OrderSpecList]OrderSpecList
 
[ Expr OrderModifier]OrderSpecList
==
for $fs:new in fn:data(Expr) return ()

4.9 Unordered Expressions

Introduction

The fn:unordered function returns its input sequence in any order.

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 [7.5 Judgments for sequences of item types]. The type of each argument is determined, and then prime(.) and quantifier(.) are applied to the sequence type (Type1, Type2).

statEnv |- Expr1 : Type1

statEnv |- fn: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

dynEnv |- fn:unordered(Expr1) => Value2

It is important to remark that the permutes to judgments is non deterministic. There are many sequences which can be a permutation of a given sequence. Any of those permutations would satisfy the above semantics.

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to the unordered expression.

4.10 Conditional Expressions

Introduction

A conditional expression supports conditional evaluation of one of two expressions.

Conditional Expression
[54 (XQuery)]   IfExpr   ::=   "if" "(" Expr ")" "then" ExprSingle "else" ExprSingle

Normalization

 
[if (Expr1) then Expr2 else Expr3]Expr
==
  if (fn:boolean([ Expr1 ]Expr)) then [Expr2]Expr else [Expr3]Expr

Core Grammar

The core grammar rule for the conditional expression is:

Core Conditional Expression
[43 (Core)]   IfExpr   ::=   "if" "(" Expr ")" "then" ExprSingle "else" ExprSingle

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.

dynEnv |- Expr1 => true      dynEnv |- Expr2 => Value2

dynEnv |- if Expr1 then Expr2 else Expr3 => Value2

dynEnv |- Expr1 => false      dynEnv |- Expr3 => Value3

dynEnv |- if Expr1 then Expr2 else Expr3 => Value3

Dynamic Errors

If the conditional's boolean expression raises an error, then the conditional expression raises an error.

dynEnv |- Expr1 raises Error

dynEnv |- if Expr1 then Expr2 else Expr3 raises Error

If the conditional's boolean expression Expr1 evaluates to true, and Expr2 raises an error, then the conditional expression raises an error. Conversely, if the conditional's boolean expression evaluates to false, and Expr3 raises an error, then the conditional raises an error.

dynEnv |- Expr1 => true      dynEnv |- Expr2 raises Error

dynEnv |- if Expr1 then Expr2 else Expr3 raises Error

dynEnv |- Expr1 => false      dynEnv |- Expr3 => Error

dynEnv |- if Expr1 then Expr2 else Expr3 raises Error

4.11 Quantified Expressions

Introduction

[XPath/XQuery] defines two quantification expressions:

Quantified Expression
[51 (XQuery)]   QuantifiedExpr   ::=   (("some" "$") | ("every" "$")) VarName TypeDeclaration? "in" ExprSingle ("," "$" VarName TypeDeclaration? "in" ExprSingle)* "satisfies" ExprSingle
[27 (XPath)]   QuantifiedExpr   ::=   (("some" "$") | ("every" "$")) VarName "in" ExprSingle ("," "$" VarName "in" ExprSingle)* "satisfies" ExprSingle

Normalization

The quantified expressions are normalized into nested core quantified expressions, each of which binds one variable.

 
[some Variable1 in Expr1, ..., Variablen in Exprn satisfies Expr]Expr
==
some Variable1 in [Expr1]Expr satisfies
   some Variable2 in [Expr2]Expr satistfies
         ...
     some Variablen in [Exprn]Expr satistfies
     [Expr]Expr
 
[every Variable1 in Expr1, ..., Variablen in Exprn satisfies Expr]Expr
==
every Variable1 in [Expr1]Expr satisfies
   every Variable2 in [Expr2]Expr satistfies
         ...
     every Variablen in [Exprn]Expr satistfies
     [Expr]Expr

Core Grammar

The quantified expressions are in the core.

Static Type Analysis

The static semantics of the quantified expressions uses the prime operator on types, which is explained in [7.5 Judgments for sequences of item types].

statEnv |- Expr1 : Type1
statEnv + varType(Variable1 : prime(Type1)) |- Expr2 : xs:boolean

statEnv |- some Variable1 in Expr1 satisfies Expr2 : xs:boolean

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv + varType(Variable1 : Type0) |- Expr2 : xs:boolean

statEnv |- some Variable1 as SequenceType in Expr1 satisfies Expr2 : xs:boolean

statEnv |- Expr1 : Type1
statEnv + varType(Variable1 : prime(Type1)) |- Expr2 : xs:boolean

statEnv |- every Variable1 in Expr1 satisfies Expr2 : xs:boolean

statEnv |- Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
prime(Type1) <: Type0
statEnv + varType(Variable1 : Type0) |- Expr2 : xs:boolean

statEnv |- every Variable1 as SequenceType in Expr1 satisfies Expr2 : xs:boolean

Dynamic Evaluation

The existentially quantified "some" expression yields true if any evaluation of the satisfies expression yields true. The existentially quantified "some" expression yields false if every evaluation of the satisfies expression is false.

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
dynEnv(Variable1 => Itemi)) |- Expr2 => true

dynEnv |- some Variable1 in Expr1 satisfies Expr2 => true

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
Type0 = [ SequenceType ]sequencetype
Itemi matches Type0
dynEnv(Variable1 => Itemi)) |- Expr2 => true

dynEnv |- some Variable1 as SequenceType in Expr1 satisfies Expr2 => true

dynEnv |- Expr1 => Item1 ... Itemn
dynEnv(Variable1 => Item1)) |- Expr2 => false
...
dynEnv(Variable1 => Itemn)) |- Expr2 => false

dynEnv |- some Variable1 in Expr1 satisfies Expr2 => false

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
dynEnv(Variable1 => Item1)) |- Expr2 => false
Item1 matches Type0
...
dynEnv(Variable1 => Itemn)) |- Expr2 => false
Itemn matches Type0

dynEnv |- some Variable1 as SequenceType in Expr1 satisfies Expr2 => false

The universally quantified "every" expression yields false if any evaluation of the satisfies expression yields false. The universally quantified "every" expression yields true if every evaluation of the satisfies expression is true.

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
dynEnv(Variable1 => Itemi)) |- Expr2 => false

dynEnv |- every Variable1 in Expr1 satisfies Expr2 => false

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
Type0 = [ SequenceType ]sequencetype
Itemi matches Type0
dynEnv(Variable1 => Itemi)) |- Expr2 => false

dynEnv |- every Variable1 as SequenceType in Expr1 satisfies Expr2 => false

dynEnv |- Expr1 => Item1 ... Itemn
dynEnv(Variable1 => Item1)) |- Expr2 => true
...
dynEnv(Variable1 => Itemn)) |- Expr2 => true

dynEnv |- every Variable1 in Expr1 satisfies Expr2 => true

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
dynEnv(Variable1 => Item1)) |- Expr2 => true
Item1 matches Type0
...
dynEnv(Variable1 => Itemn)) |- Expr2 => true
Itemn matches Type0

dynEnv |- every Variable1 as SequenceType in Expr1 satisfies Expr2 => true

Dynamic Errors

An existentially quantified expression raises an error if:

  • evaluation of the first expression raises an error,
  • any evaluation of the satisfies expression raises an error.

An existentially quantified expression raises a type error if evaluation of the first expression yields a value, and some item in this value does not match the declared type of the variable.

dynEnv |- Expr1 raises Error

dynEnv |- some Variable1 TypeDeclaration ? in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
dynEnv(Variable1 => Itemi)) |- Expr2 raises Error

dynEnv |- some Variable1 TypeDeclaration? in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
1 <= i <= n
not(Itemi matches Type0)

dynEnv |- some Variable1 as SequenceType in Expr1 satisfies Expr2 raises typeError

dynEnv |- Expr1 raises Error

dynEnv |- every Variable1 in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 => Item1 ... Itemn
1 <= i <= n
dynEnv(Variable1 => Itemi)) |- Expr2 raises Error

dynEnv |- every Variable1 in Expr1 satisfies Expr2 raises Error

dynEnv |- Expr1 => Item1 ... Itemn
Type0 = [ SequenceType ]sequencetype
1 <= i <= n
not(Itemi matches Type0)

dynEnv |- every Variable1 as SequenceType in Expr1 satisfies Expr2 raises typeError

4.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 [3.4.1 SequenceType].

4.12.1 Instance Of

SequenceType expressions
[57 (XQuery)]   InstanceofExpr   ::=   TreatExpr ( "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 $fs:new as SequenceType return fn:true()
  default $fs:new return fn:false()

4.12.2 Typeswitch

SequenceType expressions
[52 (XQuery)]   TypeswitchExpr   ::=   "typeswitch" "(" Expr ")" CaseClause+ "default" ("$" VarName)? "return" ExprSingle
[53 (XQuery)]   CaseClause   ::=   "case" ("$" VarName "as")? SequenceType "return" Expr

Introduction

The typeswitch expression 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, which is bound the value 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 is assigned a specific type for the corresponding branch.

Notation

To define normalization of case clauses to the [XPath/XQuery] core, the following auxiliary mapping rule is used.

 
[CaseClause]Case
==
CaseClause

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

Normalization

Normalization of a typeswitch expression guarantees that every branch has an associated Variable. The following normalization rule adds a newly created variable that 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 and that is not used in any of the sub-expressions.

 
[   case SequenceType return Expr ]Case
==
  case $fs:new1 as SequenceType return [ Expr ]Expr
 
[   case Variable as SequenceType return Expr ]Case
==
  case Variable as SequenceType return [ Expr ]Expr
 
[ default return Expr ]Case
==
default $fs:new1 return [ Expr ]Expr
 
[ default Variable return Expr ]Case
==
default Variable return [ Expr ]Expr
 
[
typeswitch ( Expr0 )
  CaseClause1
    ···
  CaseClausen
  default (Variable)? return Exprn+1
]Expr
==
typeswitch ( [ Expr0 ]Expr )
[CaseClause1]Case
    ···
[CaseClausen]Case
[  default (Variable)? return Exprn+1 ]Case

Core Grammar

The core grammar productions for typeswitch are:

[41 (Core)]   TypeswitchExpr   ::=   "typeswitch" "(" Expr ")" CaseClause+ "default" ("$" VarName)? "return" ExprSingle
[42 (Core)]   CaseClause   ::=   "case" ("$" VarName "as")? SequenceType "return" Expr

Notation

The following auxiliary grammar production is used to identify branches of the typeswitch.

CaseRules
[76 (Formal)]   CaseRules   ::=   ("case" "$" VarName "as" SequenceType "return" Expr CaseRules) | ("default" "$" VarName "return" Expr)

Notation

The following judgment

dynEnv |- Value1 against CaseRules => Value2

is used in the dynamic semantics of typeswitch. It indicates that under the environment dynEnv, with the input value of the typeswitch being Value1, the given case rules yields the value Value2.

Notation

The following judgment

statEnv |- Type1 case CaseClause : Type

is used in the static of typeswitch. It indicates that under the environment statEnv, and with the input type of the typeswitch being Type1, the given case rule yields the type Type.

Static Type Analysis

The static typing rules for the typeswitch expression are simple. Each case clause and the default clause of the typeswitch is typed independently. The type of the entire typeswitch expression is the union of the types of all the clauses.

statEnv |- Expr0 : Type0
statEnv |- Type0 case case Variable1 as SequenceType1 return Expr1 : Type1
    ···
statEnv |- Type0 case case Variablen as SequenceTypen return Exprn : Typen
statEnv |- Type0 case default Variablen+1 return Exprn : Typen+1

statEnv |-  
(typeswitch (Expr0)
  case Variable1 as SequenceType1 return Expr1
    ···
  case Variablen as SequenceTypen return Exprn
  default Variablen+1 return Exprn+1)
: (Type1 | ... | Typen+1)

To type one case clause, the case variable is assigned the type of the case clause CaseType and the body of the clause is typed in the extended environment. Thus, the type of a case clause is independent of the type of the input expression.

CaseType = [ SequenceType ]sequencetype
statEnv(Variable : CaseType ) |- Expr : Type

Type0 case case Variable as SequenceType return Expr : Type

To type the default clause, the variable is assigned the type of the input expression and the body of the default clause is typed in the extended environment.

statEnv(Variable : Type0 ) |- Expr : Type

Type0 case default Variable return Expr : Type

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

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to the typeswitch expression. In particular, if evaluation of the input expression or evaluation of any case rule raises an error, then the typeswitch expression raises an error.

4.12.3 Cast

[60 (XQuery)]   CastExpr   ::=   ComparisonExpr ( "cast" "as" SingleType )?
[123 (XQuery)]   SingleType   ::=   AtomicType "?"?

Cast expressions change the type and value of an expression against a given type.

Core Grammar

The core grammar production for cast as is:

[84 (Core)]   SingleType   ::=   AtomicType "?"?

Introduction

The expression "cast as AtomicType ( Expr )" can be used to explicitly convert the result of an expression from an tomic 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.

Normalization

The normalization of cast applies atomization to its argument. The type declaration asserts that the result is a single atomic value. Normalization differs whether the type is followed by ? or not.

 
[cast as AtomicType (Expr)]Expr
==
let $v as atomic value := fn:data([ Expr ]Expr) return
  cast as AtomicType ($v)
 
[cast as AtomicType? (Expr)]Expr
==
let $v as atomic value? := fn:data([ Expr ]Expr) return
  typeswitch ($v)
    case empty return ()
    default return cast as AtomicType ($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.

statEnv |- Expr : AtomicType1
AtomicType1 cast allowed AtomicType2 => Y or AtomicType1 cast allowed AtomicType2 => M

statEnv |- cast as AtomicType2 (Expr) : AtomicType2

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.

dynEnv |- Expr => Value1
cast as AtomicType2 ( Value1 ) => AtomicType2(Value1) of type AtomicType2

dynEnv |- cast as AtomicType ( Expr ) => 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 raises an error.

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to the cast expression. In particular, if Expr1 raises an error, then the cast expression raises an error. In addition, if the casting table returns "N", the cast is not allowed, and the dynamic semantics always raises an error.

dynEnv |- Expr1 => AtomicValue1 of type AtomicType1
AtomicType1 cast allowed AtomicType2 => N

dynEnv |- cast as AtomicType2 ( Expr1 ) raises dynError

4.12.4 Castable

[59 (XQuery)]   CastableExpr   ::=   CastExpr ( "castable" "as" SingleType )?

Castable expressions check whether a value can be cast to a given type.

Core Grammar

The core grammar production for cast as is:

Normalization

The normalization of castable simply maps its expression argument.

 
[Expr castable as AtomicType]Expr
==
let $v as atomic value := fn:data([ Expr ]Expr) return
$v castable as AtomicType
 
[Expr castable as AtomicType]Expr
==
let $v as atomic value? := fn:data([ Expr ]Expr) return
$v castable as AtomicType?

Static Type Analysis

The type of a castable expression is always a boolean.


statEnv |- Expr castable as AtomicType : xs:boolean

Dynamic Evaluation

If casting succeeds, then the 'castable' expression evaluates to true.

dynEnv |- Expr => Value1
cast as AtomicType ( Value1 ) => Value2

dynEnv |- Expr castable as AtomicType => true

If casting raises a dynamic error, 'castable as' evaluates to false.

cast as AtomicType2 ( Expr1 ) raises dynError

dynEnv |- Expr1 castable as AtomicType2 => false

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to the castable expression.

4.12.5 Constructor Functions

Constructor functions provide an alternative syntax for casting.

Normalization

Constructor functions are normalized to explicit cast as operations.

 
[AtomicType(Expr)]Expr
==
[cast as AtomicType (Expr)]Expr

4.12.6 Treat

[58 (XQuery)]   TreatExpr   ::=   CastableExpr ( "treat" "as" SequenceType )?

Introduction

The expression "Expr treat as SequenceType", 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.

 
[Expr treat as SequenceType]Expr
==
typeswitch ([ Expr ]Expr) as $fs:new
  case SequenceType return $fs:new
  default return fn:error()

4.13 Validate Expressions

[77 (XQuery)]   ValidateExpr   ::=   "validate" SchemaMode? SchemaContext? "{" Expr "}"
[12 (XQuery)]   SchemaMode   ::=   "lax" | "strict" | "skip"
[78 (XQuery)]   SchemaContext   ::=   ("context" SchemaContextLoc) | "global"
[135 (XQuery)]   SchemaContextPath   ::=   SchemaGlobalContext "/" (SchemaContextStep "/")*
[14 (XQuery)]   SchemaGlobalContext   ::=   QName | SchemaGlobalTypeName
[15 (XQuery)]   SchemaContextStep   ::=   QName

Core Grammar

The core grammar production for validate is:

[49 (Core)]   ValidateExpr   ::=   "validate" SchemaMode? 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 Part 1]. The argument to a validate expression must be either element or document node. 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.

Static Type Analysis

Static typing of the validate operation is defined by the following rule. Note the use of a subtyping check to ensure the input of the validation is either an element or a well-formed document node (i.e., with only one root element and no text nodes).

statEnv |- SchemaMode is SchemaMode'
statEnv |- SchemaContext? is TypeName1
statEnv1 = statEnv(validationMode(SchemaMode') + validationContext(TypeName1))
statEnv1 |- Expr : Type1
statEnv1 |- Expr <: (element | document { ElementType })
statEnv1 |- Type1 validates as Type2

statEnv |- validate SchemaMode? SchemaContext? { Expr } : Type2

Dynamic Evaluation

An important effect of validation is that it removes existing type annotations from nodes ("erasure"), and it revalidates the corresponding data model instance, possibly adding new type annotations to nodes ("annotation"). Both erasure and annotation are described formally in [7.7 Judgments for the validate expression]. Indeed, the conjunction of erasure and annotation provides a formal model for a large part of actual schema validation. The semantics of the validate expression is specified as follows.

When the validation mode is either given explicitly as "skip" or is set to "skip" in statEnv.validationMode, the dynamic semantics simply erases all existing type annotations and re-labels all element nodes with xdt:untypedAny and all attribute nodes with xdt:untypedAtomic.

statEnv |- SchemaMode? is "skip"
Expr => ElementValue1
ElementValue1 erases to ElementValue2

dynEnv |- validate SchemaMode? SchemaContext? { Expr } => ElementValue2

statEnv |- SchemaMode? is "skip"
Expr => document { ElementValue1 }
document { ElementValue1 } erases to document { ElementValue2 }

dynEnv |- validate SchemaMode? SchemaContext? { Expr } => document { ElementValue2 }

When the validation mode is either given explicitly as "lax" or "strict" or is set to "lax" or "strict" in statEnv.validationMode, the dynamic semantics erases all existing type annotations and then re-validates against the definition of the given element in the given schema context.

statEnv |- SchemaMode? is "lax" or SchemaMode? is "strict"
statEnv |- SchemaContext? is TypeName1
dynEnv.varValue |- Expr => ElementValue1
ElementValue1 erases to ElementValue2
statEnv |- element ElementName in context TypeName1 static lookup ElementName of type TypeName
annotate as element ElementName of type TypeName (ElementValue2) => ElementValue3

dynEnv |- validate SchemaMode? SchemaContext? { Expr } => ElementValue3

statEnv |- SchemaMode? is "lax" or SchemaMode? is "strict"
statEnv |- SchemaContext? is TypeName1
dynEnv.varValue |- Expr => document { ElementValue1 }
document { ElementValue1 } erases to document { ElementValue2 }
statEnv |- element ElementName in context TypeName1 static lookup ElementName of type TypeName
annotate as document { element ElementName } of type TypeName (document { ElementValue2 }) => document { ElementValue3 }

dynEnv |- validate SchemaMode? SchemaContext? { Expr } => document { ElementValue3 }

Note that validation depends upon the order of types in a union type, but that type matching does not.

Dynamic Errors

The default rules for propogating errors, described in [3.5 Errors Handling] apply to the validate expression.

5 Modules and Prologs

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.

Query Module
[30 (XQuery)]   Module   ::=   MainModule | LibraryModule
[31 (XQuery)]   MainModule   ::=   Prolog QueryBody
[32 (XQuery)]   LibraryModule   ::=   ModuleDecl Prolog
[33 (XQuery)]   ModuleDecl   ::=   "module" "namespace" NCName "=" StringLiteral Separator
[34 (XQuery)]   Prolog   ::=   (Version Separator)? ((NamespaceDecl
| XMLSpaceDecl
| DefaultNamespaceDecl
| DefaultCollationDecl
| BaseURIDecl
| SchemaImport
| ModuleImport
| VarDecl
| ValidationDecl
| FunctionDecl) Separator)*
[39 (XQuery)]   QueryBody   ::=   Expr

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 [XPath/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.

Prolog Declarations
[77 (Formal)]   PrologDeclList   ::=   PrologDecl*
[78 (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.

Editorial note 
Jerome: What do the default namespace and type environments contain? I believe at least the default namespace environment should contain the "xs", "fn" and "op" prefixes, as well as the default namespaces bound to the empty namespace. Should the default type environment contain wildcard types? See Issue 458 (FS-Issue-0115).

() => statEnvDefault

PrologDeclList => statEnv1
statEnv1 |- PrologDecl => statEnv2

PrologDecl PrologDeclList => statEnv2

5.1 Version Declaration

The version number does not have any effect on the language semantics at this point.

5.2 Namespace Declarations

Namespace Declarations
[117 (XQuery)]   NamespaceDecl   ::=   "declare" "namespace" NCName "=" StringLiteral
[118 (XQuery)]   DefaultNamespaceDecl   ::=   (("declare" "default" "element") | ("declare" "default" "function")) "namespace" StringLiteral

Context Processing

A namespace declaration adds a new (prefix,uri) binding in the namespace component of the static environment. All namespace declarations in the prolog are passive declarations. Namespace declaration attributes of element constructors are active declarations.

statEnv1 = statEnv + namespace(NCName => (passive, String))

statEnv |- declare namespace NCName = String => statEnv1

5.3 Default Namespace Declarations

Context Processing

A default element namespace declaration changes the default element namespace prefix binding in the namespace component of the static environment.

statEnv1 = statEnv + namespace(fsdefaultelem => (passive, String))

statEnv |- default element namespace = String => 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 => (passive, String))

statEnv |- default function namespace = String => statEnv1

Note that for namespaces, later declarations can override earlier declarations of the same prefix.

5.4 Schema Imports

Schema Imports
[142 (XQuery)]   SchemaImport   ::=   "import" "schema" SchemaPrefix? StringLiteral ("at" StringLiteral)?
[143 (XQuery)]   SchemaPrefix   ::=   ("namespace" NCName "=") | ("default" "element" "namespace")

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 [XPath/XQuery] 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? TypeReference)

statEnv |- define element ElementName Substitution? Nillable? TypeReference => statEnv1

statEnv1 = statEnv + attrDecl(AttributeName => define attribute AttributeName TypeReference)

statEnv |- define attribute AttributeName TypeReference => 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.

5.5 Module Imports

Editorial note 
Issue: The semantics of Module Import is not formally specified. See Issue XXX.

5.6 Variable Definitions

Editorial note 
Issue: The semantics of Variables Definitions in the XQuery prolog is not formally specified. See Issue XXX.

5.7 Validation Declaration

Editorial note 
Issue: The semantics of Validation Declaration in the XQuery prolog is not formally specified. See Issue XXX.

5.8 Xmlspace Declaration

[114 (XQuery)]   XMLSpaceDecl   ::=   "declare" "xmlspace" ("preserve" | "strip")

The impact of xmlspace declaration is not formally specified in this document.

5.9 Default Collation

[115 (XQuery)]   DefaultCollationDecl   ::=   "declare" "default" "collation" StringLiteral

The impact of default collation is not formally specified in this document. See Issue 503 (FS-Issue-0160).

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

Function Definitions
[120 (XQuery)]   ParamList   ::=   Param ("," Param)*
[121 (XQuery)]   Param   ::=   "$" VarName TypeDeclaration?

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? ) as SequenceType EnclosedExpr ]Expr
==
define function [QName] ( [ParamList?]Param ) as 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 ) as 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 ) as 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 ) as 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 [4.1.5 Function Calls].

6 Additional Semantics of Functions

A number of functions play a role in defining the formal semantics of [XPath/XQuery], and some other functions from the [XQuery 1.0 and XPath 2.0 Functions and Operators] document need special static typing rules.

6.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. Their dynamic semantics are defined in the same informal style as in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document. The static semantics of some formal-semantics functions require custom typing rules.

6.1.1 The fs:distinct-doc-order function

fs:distinct-docorder( $nodes as node * ) as node *

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 fn:distinct-nodes and sorting by document order.

Static Type Analysis

statEnv |- Expr : Type

statEnv |- fs:distinct-doc-order ( Expr ) : prime(Type) · quantifier(Type)

6.1.2 The fs:item-sequence-to-node-sequence function

fs:item-sequence-to-node-sequence( $items as item * ) as node *

Th fs:item-sequence-to-node-sequence function converts a sequence of item values to nodes by applying the rules in Section [3.7.2.1 Computed Element Constructors] in [XQuery 1.0: A Query Language for XML].

Notation

The type function items_to_nodes(Type) converts all atomic types in a type to the text type. The items_to_nodes function is defined by induction as follows.

items_to_nodes(AtomicTypeName)  =  text
items_to_nodes(NodeType)  =  NodeType
items_to_nodes(Type1 , Type2)  =  items_to_nodes(Type1) , items_to_nodes(Type2)
items_to_nodes(Type1 & Type2)  =  items_to_nodes(Type1) & items_to_nodes(Type2)
items_to_nodes(Type1 | Type2)  =  items_to_nodes(Type1) | items_to_nodes(Type2)
items_to_nodes(Type ?)  =  items_to_nodes(Type) ?
items_to_nodes(Type *)  =  items_to_nodes(Type) *
items_to_nodes(Type +)  =  items_to_nodes(Type) +

Static Type Analysis

statEnv |- Expr : Type

statEnv |- fs:item-sequence-to-node-sequence ( Expr) : items_to_nodes(Type)

6.1.3 The fs:item-sequence-to-untypedAtomic function

fs:item-sequence-to-untypedAtomic( $items as item * ) as xdt:untypedAtomic

The fs:item-sequence-to-untypedAtomic function converts a sequence of item values to a string of type xdt:untypedAtomic by applying the rules in Section [3.7.2.2 Computed Attribute Constructors] in [XQuery 1.0: A Query Language for XML].

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.

6.1.4 The fs:convert-simple-operand function

fs:convert-simple-operand( $actual as
      item *, $expected as
      xdt:anyAtomicType ) as xdt:anyAtomicType
      *

The formal-semantics function fs:convert-simple-operand is used to convert the value of an $actual parameter such that it fits the type of $expected (or some sequence of that type).

The dynamic semantics of this function are as follows:

  • If statEnv.xpath1.0_compatibility is true and $expected is of type xs:string (or a type derived from xs:string) but $actual is not of type xs:string (or a type derived from xs:string), then returns the value of fn:string($actual).

  • If statEnv.xpath1.0_compatibility is true and $expected is of numeric type (or a type derived from a numeric type) but $actual is not of numeric type, then returns the value of fn:number($actual).

  • If statEnv.xpath1.0_compatibility is false and $actual is of type xdt:untypedAtomic * then returns the sequence obtained by casting each item of $actual to the type of $expected.

  • Otherwise, return $actual.

Static Type Analysis

The following static semantics rules correspond to the four dynamic semantics rules given above.

statEnv.xpath1.0_compatibility = true
statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
statEnv |- Type2 <: xs:string *

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : xs:string

statEnv.xpath1.0_compatibility = true
statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
statEnv |- Type2 <: fs:numeric *

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : xs:double

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 : Type1
Type1 <: xdt:untypedAtomic*
statEnv |- Expr2 : Type2
statEnv |- Type2 <: xdt:anyAtomicType

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : Type2 · quantifier(Type1)

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 : Type1
not(Type1 <: xdt:untypedAtomic*)

statEnv |- fs:convert-simple-operand(Expr1, Expr2) : Type1

6.1.5 The fs:convert-operand function

fs:convert-operand( $actual as item *, $expected as xdt:anyAtomicType ) as xdt:anyAtomicType ?

The formal-semantics function fs:convert-operand converts the operands of arithmetic and comparison operators as follows:

  1. If $actual is the empty sequence, returns the empty sequence.

  2. If statEnv.xpath1.0_compatibility is false and $actual is of type xdt:untypedAtomic, then

    1. if $expected is of type xdt:untypedAtomic, returns $actual cast to xs:string;

    2. if $expected is of numeric type, returns $actual cast to xs:double

    3. otherwise returns $actual cast to the type of $expected.

  3. If statEnv.xpath1.0_compatibility is true, and $actual is not of numeric type, then returns the value of the expression fn:number(fn:subsequence($actual,1,1)).

    Editorial note 
    New Issue: According to Michael Kay this converts too much (for example dates) to numbers in backwards compatibility mode. One fix would be to make the test inclusive yet sufficiently general to capture all the actual 1.0 cases, i.e., say something like "$actual : (node* | xdt:untypedAtomic* | xs:string*)". [Kris]
  4. Otherwise, the operand is returned unchanged.

Static Type Analysis

No conversion is needed for numeric (or empty) operands.

statEnv |- Expr1 : Type1
Type1 <: (xs:decimal|xs:float|xs:double)?

statEnv |- fs:convert-operand(Expr1, Expr2) : Type1

Pairs of untyped atomic operands are converted to strings (except in backwards compatibility mode handled below).

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 : xdt:untypedAtomic?
statEnv |- Expr2 : xdt:untypedAtomic

statEnv |- fs:convert-operand(Expr1, Expr2) : xs:string?

When an untyped operand is paired with a numeric operand then it is converted to xs:double (except in backwards compatibility mode handled below).

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 : xdt:untypedAtomic?
statEnv |- Expr2 : Type
statEnv |- Type <: fs:numeric

statEnv |- fs:convert-operand(Expr1, Expr2) : xs:double?

Finally, an untyped atomic operand not dealt with by the above rules is converted to the type of the other operand (except in backwards compatibility mode handled below).

statEnv.xpath1.0_compatibility = false
statEnv |- Expr1 : xdt:untypedAtomic?
statEnv |- Expr2 : Type2
not(Type2 <: (xdt:untypedAtomic|fs:numeric))

statEnv |- fs:convert-operand(Expr1, Expr2) : Type2

In backwards compatibility mode a non-numeric operand is converted to xs:double after sequences have been reduced to their first element.

statEnv.xpath1.0_compatibility = true
statEnv |- Expr1 : Type1
not(Type1 <: (xdt:untypedAtomic|xs:decimal|xs:float|xs:integer)?)
statEnv |- fn:number(fn:subsequence(Expr1,1,1)) : Type

statEnv |- fs:convert-operand(Expr1, Expr2) : Type

Editorial note 
This rule does not seem quite right...to discuss. [Kris]

6.1.6 The arithmetic operator pseudo-functions: fs:minus, fs:plus, fs:times, fs:idiv, fs:div, and fs:mod

These functions are overloaded placeholders with signatures and semantics as specified in the table in Appendix [B.2 Mapping of Overloaded Internal Functions].

6.1.7 The comparison pseudo-functions: fs:eq, fs:ne, fs:lt, fs:le, fs:gt, and fs:ge

These functions are overloaded placeholders with signatures and semantics as specified in the table of Appendix [B.2 Mapping of Overloaded Internal Functions].

6.2 Standard functions with specific typing rules

Introduction

This section gives static typing rules for those functions from [XQuery 1.0 and XPath 2.0 Functions and Operators] where the standard typing rule based on the function signature is insufficient. All functions that are not mentioned here have static semantics as descrbed by the generic static rule of section [4.1.5 Function Calls]. The rules in this section always give more precise type information than the generic rule.

6.2.1 The fn:error function

Static Type Analysis

The fn:error function always has the none type.


statEnv |- fn:error() : none

6.2.2 The fn:distinct-nodes and fn:distinct-values functions

Static Type Analysis

The fn:distinct-nodes function expects a sequence of nodes as input and returns a sequence of prime types, which are defined in [7.5 Judgments for sequences of item types].

statEnv |- Expr : Type
statEnv |- Type <: node*

statEnv |- fn:distinct-nodes(Expr) : prime(Type) · quantifier(Type)

The fn:distinct-values function expects a sequence of atomic values as input and returns a sequence of prime types, which are defined in [7.5 Judgments for sequences of item types].

statEnv |- Expr : Type
statEnv |- Type <: xdt:anyAtomicType*

statEnv |- fn:distinct-values(Expr) : prime(Type) · quantifier(Type)

6.2.3 The fn:collection and fn:doc functions

Editorial note 
Proposal (Mary). The static semantics of these functions is currently under discussion. (See Issue 480 (FS-Issue-0137))

Static Type Analysis

The fn:collection function as described in the [XQuery 1.0 and XPath 2.0 Functions and Operators] document, takes a string-valued expression, which denotes a URI, and returns a value.

If the argument to fn:collection is a literal String expression and that string is defined in statEnv.collectionType, then we can look up the corresponding type in statEnv.collectionType.

statEnv |- statEnv.collectionType(String) = Type

statEnv |- fn:collection(String) : Type

Otherwise, if the argument is not a literal string or is a string but not defined in statEnv.collectionType, then we don't know anything about the URI, and the static type is node*:

statEnv |- statEnv.collectionType(String) not defined

statEnv |- fn:collection(Expr) : node *

statEnv |- not(Expr = String)

statEnv |- fn:collection(Expr) : node *

The static type of the fn:doc function has similar static rules, but also requires that the static type of the URI be a document:

statEnv |- statEnv.docType(String) = Type      statEnv |- statEnv.docType(String) = Type      statEnv |- Type <: document

statEnv |- fn:doc(String) : Type

Otherwise, if the argument is not a literal string or is not defined in the domain of statEnv.docType, then we don't know anything about the URI, and the static type is document:

statEnv |- statEnv.docType(String) not defined

statEnv |- fn:doc(Expr) : document

statEnv |- not(Expr = String)

statEnv |- fn:doc(Expr) : document

6.2.4 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 [7.5 Judgments for sequences of item types]. 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. Because an intersection may always be empty, the result type needs to be made optional.

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

statEnv |- op:intersect(Expr1, Expr2) : prime(Type1, Type2); · quantifier(Type1,Type2); · ?

The static semantics of op:except follows. The type of the second argument is ignored as it does not contribute to the result type. As 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) · ?

6.2.5 The fn:data function

Introduction

The fn:data function converts a sequence of items to a sequence of atomic values.

Notation

Infering the type for the fn:data function is done by applying the data; function as a Filter, using the same approach as for the XPath steps.

statEnv |- data on Type1 : Type2

Static Type Analysis

The general rule for fn:data is to apply the filter data on to the prime type of its argument type, then apply the quantifier to the result:

statEnv |- Expr : Type
statEnv |- data on prime(Type) : Type1

statEnv |- fn:data(Expr) : Type1 · quantifier(Type)

When applied to none, data on yields none.


statEnv |- data on none : none

When applied to empty, data on yields empty.


statEnv |- data on empty : empty

When applied to the union of two types, data on is applied to each of the two types. The resulting types are combined into a factored type. This rule is necessary because data on may return a sequence of atomic types.

statEnv |- data on Type1 : Type1'
statEnv |- data on Type2 : Type2'

statEnv |- data on (Type1|Type2) : prime(Type1'|Type2') · quantifier(Type1'|Type2')

When applied to an atomic type, the fn:data filter simply returns the atomic type:

Type <: xdt:anyAtomicType

statEnv |- data on Type : Type

When applied to comment, processing instruction, text, and document node types, the fn:data filter returns xdt:untypedAtomic

Type <: comment | processing-instruction | text | document

statEnv |- data on Type : xdt:untypedAtomic

When applied to element node types with type annotation xdt:untypedAny, the data on filter returns xdt:untypedAtomic.

statEnv |- ElementType static lookup (of type xdt:untypedAny)

statEnv |- data on ElementType : xdt:untypedAtomic

When applied to an attribute type, the data on filter returns the attribute's simple type.

statEnv |- AttributeType static lookup (of type TypeName)
statEnv |- (of type TypeName) expands to TypeName1 { Type }

statEnv |- data on AttributeType : Type

When applied to an element type whose type annotation denotes a simple type or a complex type of simple content, the fn:data filter returns the element's simple type.

statEnv |- ElementType static lookup TypeReference
statEnv |- TypeReference expands to Type
Type <: (attribute *, Type1)      Type1 <: xs:anySimpleType

statEnv |- data on ElementType : Type1

When applied to an element type whose type annotation denotes a complex type of mixed content, the data on filter returns xdt:untypedAtomic.

statEnv |- ElementType static lookup (of type TypeName)
statEnv.typeDefn(TypeName) = define type TypeName Derivation? Mixed { Type1? }

statEnv |- data on ElementType : xdt:untypedAtomic

The data on filter is not defined on any element type whose type annotation denotes a complex type of complex content and therefore raises a static error.

Example

Consider the following variables and its corresponding static type.

    $x : (element price { attribute currency { xs:string }, xs:decimal }
         | element price_code { xs:integer })

Applying the fn:data function on that variable results in the following type.

    fn:data($x) : (xs:decimal | xs:integer)

Because the input type is a choice, applying the data on filter results in a choice of simple types for the output of the fn:data function.

6.2.6 The fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions

Static Type Analysis

The typing rules for the fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions preserve their input type, which must be a numeric.

statEnv |- Expr : Type
Type <: fs:numeric

statEnv |- F (Expr) : Type

for F one of the fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions.

6.2.7 The fn:subsequence, and fn:remove functions

Static Type Analysis

The typing rules for the fn:subsequence and fn:remove functions return the factored type of the functions' input sequence.

statEnv |- Expr : Type
statEnv |- Expr1 : xs:integer      statEnv |- Expr2 : xs:integer

statEnv |- fn:subsequence(Expr, Expr1, Expr2) : prime(Type') · quantifier(Type')

statEnv |- Expr : Type
statEnv |- Expr1 : xs:integer

statEnv |- fn:remove(Expr, Expr1) : : prime(Type') · quantifier(Type')

6.2.8 The fn:min fn:max, fn:avg, and fn:sum functions

Static Type Analysis

These functions all return a single value of the same numeric type as the type of their input sequence.

statEnv |- Expr : Type
statEnv |- prime(Type) <: fs:numeric

statEnv |- F (Expr) : prime(Type)

where F is one of the fn:min, fn:max, fn:avg, and fn:sum functions.

7 Auxiliary Judgments

This section defines auxiliary judgments used in the course of defining the formal semantics.

7.1 Judgments for schema contexts

7.1.1 Mode is

Notation

The judgment

statEnv |- SchemaMode? is SchemaMode1

holds when the possibly optional schema mode resolves to the given schema mode.

Semantics

An absent schema mode resolves to the schema mode in statEnv.validationMode.

statEnv.validationMode = SchemaMode

statEnv |- is SchemaMode

A present schema mode resolves to itself.


statEnv |- SchemaMode is SchemaMode

7.1.2 Context is

Notation

The judgment

statEnv |- SchemaContext? is TypeName

holds when the possibly optional schema context resolves to the given type name.

Semantics

An absent schema context resolves to the schema context in statEnv.validationContext.

statEnv.validationContext = TypeName

statEnv |- is TypeName

A present schema context resolves to the type name denoted by the schema context path. A type name simply resolves to itself.


statEnv |- type(TypeName) is TypeName

An element name is resolved to the type name of the global element with the given element name. The rest of the context is resolved recursively in the context of the given type name.

SchemaContext = ElementName/SchemaContext1?
statEnv |- statEnv.elemDecl(ElementName) => define element ElementName substitutes for BaseElementName Nillable? of type TypeName
type(TypeName)/SchemaContext1 is TypeName1

statEnv |- SchemaContext is TypeName1

A type name followed by an element name is resolved to the type name of the local element in the first type name. The rest of the context is resolved recursively in the context of the local element's type name.

SchemaContext = type(TypeName)/gr_ElementName;/SchemaContext1?
statEnv |- statEnv.localElemDecl(ElementName, TypeName) => element ElementName Nillable? of type TypeName1
type(TypeName1)/SchemaContext1? is TypeName2

statEnv |- SchemaContext is TypeName2

If an element name is not defined in the given type name, then it is resolved to the type name of a global element.

SchemaContext = type(TypeName)/ElementName/SchemaContext1?
statEnv |- statEnv.localElemDecl(ElementName, TypeName) not defined
ElementName/SchemaContext1? is TypeName2

statEnv |- SchemaContext is TypeName2

7.2 Judgments for accessing types

Introduction

This section defined several auxiliary judgments to access components of the [XPath/XQuery] type system. The first two judgements (derives from and substitutes for) are used to access the type and element name hierarchies from the schema. The other judgments (lookup, static lookup, extended by, adjusts to and expands to) are used to lookup the meaning of element or attribute types from the schema. These judgments are used in many expressions, notably in the specification of type matching (See [7.4 Judgments for type matching]), validation (See [7.7 Judgments for the validate expression]), and the static semantics for step expressions (See [7.3 Judgments for step expressions and filtering]).

7.2.1 Derives

Notation

The judgment

statEnv |- TypeName derives from TypeName

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

Example

For example, assuming the extended XML Schema given in section [2.3.5 Example of a complete Schema], then the following judgments hold.

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

Note

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

Semantics

This judgment is specified by the following rules.

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

Every type name derives from itself.


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

7.2.2 Substitutes

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

Notation

The judgment

statEnv |- ElementName substitutes for ElementName

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

Example

For example, assuming the extended XML Schema given in section [2.3.5 Example of a complete Schema], then the following judgments hold.

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

Note

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

Semantics

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

Every element name substitutes for itself.


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

statEnv |- ElementName substitutes for BaseElementName

Substitution is transitive.

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

statEnv |- ElementName1 substitutes for ElementName3

7.2.3 Element and attribute type lookup

The lookup judgments are used to obtain the appropriate type annotations from any given attribute or element type, given an element or attribute name.

Notation

The judgment

statEnv |- ElementName lookup ElementType yields Nillable? TypeReference

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

Example

For example, assuming the extended XML Schema given in section [2.3.5 Example of a complete Schema], then the following judgments hold.

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

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

Semantics

This judgment is specified by the following rules.

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

statEnv |- ElementName1 substitutes for ElementName2
statEnv.elemDecl(ElementName1) => define element ElementName1 Substitution? Nillable? TypeReference

statEnv |- ElementName1 lookup element ElementName2 yields Nillable? TypeReference

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


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

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


statEnv |- ElementName lookup element TypeReference yields TypeReference

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


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

Notation

The judgment

statEnv |- AttributeName lookup AttributeType yields TypeReference

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

Example

For example, assuming the extended XML Schema given in section [2.3.5 Example of a complete Schema], then the following judgments hold.

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

Semantics

This judgment is specified by the following rules.

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

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

statEnv |- AttributeName lookup attribute AttributeName yields TypeReference

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


statEnv |- AttributeName lookup attribute AttributeName TypeReference yields TypeReference

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


statEnv |- AttributeName lookup attribute TypeReference yields TypeReference

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


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

7.2.4 Static element and attribute type lookup

The static lookup judgments are used to obtain the appropriate type reference from any given attribute or element type.

Notation

The judgment

statEnv |- ElementType in context TypeName? static lookup Nillable? TypeReference

holds when the element type accessed in the given type context is nillable and has the given type reference.

Semantics

This judgment is specified by the following rules.

If the schema context is global (i.e., the context argument is absent), the element type must be a reference to a global element, in which case static lookup yields the type reference in the global element declaration with the given element name.

statEnv.elemDecl(ElementName) => define element ElementName Substitution? Nillable? TypeReference

statEnv |- element ElementName in context static lookup Nillable? TypeReference

If the the schema context is not global (i.e., the context argument is present), static lookup yields the type reference of the local element with the given name defined in the given context.

statEnv.localElemDecl(ElementName, TypeName) => element ElementName Nillable? TypeReference

statEnv |- element ElementName in context TypeName static lookup Nillable? TypeReference

If the the schema context is not global (i.e., the context argument is present), but the element is not defined in the given context, then it must be a global element.

statEnv.localElemDecl(ElementName, TypeName) not defined
statEnv.elemDecl(ElementName) => define element ElementName Substitution? Nillable? TypeReference

statEnv |- element ElementName in context TypeName static lookup Nillable? TypeReference

In the case of a local element type, lookup yields the corresponding type reference.


statEnv |- element ElementName Nillable? TypeReference in context TypeName? static lookup Nillable? TypeReference

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


statEnv |- element Nillable? TypeReference in context TypeName? static lookup TypeReference

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


statEnv |- element in context TypeName? static lookup of type xs:anyType

Notation

The judgment

statEnv |- AttributeType in context TypeName? static lookup TypeReference

holds when the attribute type accessed in the given type context up has the given type reference.

Semantics

This judgment is specified by the following rules.

If the schema context is global (i.e., the context argument is absent), the attribute type must be a reference to a global attribute, in which case static lookup yields the type reference in the global attribute declaration with the given attribute name.

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

statEnv |- attribute AttributeName in context static lookup TypeReference

If the the schema context is not global (i.e., the context argument is present), static lookup yields the type reference of the local attribute with the given name defined in the given context.

statEnv.localAttrDecl(AttributeName, TypeName) => attribute AttributeName TypeReference

statEnv |- attribute AttributeName in context TypeName static lookup TypeReference

If the the schema context is not global (i.e., the context argument is present), static lookup yields the type reference of the local attribute with the given name defined in the given context.

statEnv.localAttrDecl(AttributeName, TypeName) => attribute AttributeName TypeReference

statEnv |- attribute AttributeName in context TypeName static lookup TypeReference

If the the schema context is not global (i.e., the context argument is present), but the attribute is not defined in the given context, then it must be a global attribute.

statEnv.localAttrDecl(AttributeName, TypeName) not defined
statEnv.elemDecl(AttributeName) => define attribute AttributeName TypeReference

statEnv |- attribute AttributeName in context TypeName static lookup TypeReference

In the case of a local attribute type, lookup yields the corresponding type reference.


statEnv |- attribute AttributeName TypeReference in context TypeName? static lookup TypeReference

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


statEnv |- attribute TypeReference in context TypeName? static lookup TypeReference

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


statEnv |- attribute in context TypeName? static lookup of type xs:anySimpleType

7.2.5 Extension

Notation

The judgment

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

7.2.6 Type adjustment

Any element may optionally include the four built-in attributes xsi:type, xsi:nil, xsi:schemaLocation, or xsi:noNamespaceSchemaLocation. The adjust judgment is used to build a complete type description from a (possibly mixed) type description.

Notation

The judgment

statEnv |- 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 |- Type1 mixes to Type2
statEnv |- Type2 extended by BuiltInAttributes is Type3
statEnv |- Type3 extended by (processing-instruction? & comment?)* is Type4

statEnv |- mixed Type1 adjusts to Type4

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

statEnv |- Type1 extended by BuiltInAttributes is Type2
statEnv |- Type2 extended by (processing-instruction? & comment?)* is Type3

statEnv |- Type1 adjusts to Type3

The definition of BuiltInAttributes appears in [7.7.1 Builtin attributes].

7.2.7 Type expansion

The expands to judgment is used to compute the union of all types derived by extension from a given type. In the case the type is nillable it also makes sure the content model allows the empty sequence.

Notation

The judgment

statEnv |- Nillable? TypeReference expands to Type

holds when expanding the (nillable) type reference results in the given type.

Semantics

This judgment is specified by the following rules.

If the type is nillable, then its expansion is optional.

statEnv |- TypeReference expands to Type

statEnv |- nillable TypeReference expands to Type?

The type definition for the type reference is contained in its expansion.

statEnv.typeDefn(TypeName) => define type TypeName extends BaseTypeName Mixed? { Type1? }
statEnv |- Mixed? Type1 adjusts to Type2

statEnv |- of type TypeName expands to Type2

If there is a type deriving from the given type, then it is contained in its expansion.

statEnv |- of type TypeName1 expands to Type2
statEnv |- Type2 adjusts to Type1

statEnv |- of type TypeName1 expands to (Type1 | Type2)

Editorial note 
MF (13 Mar 2003) : I'm not sure about the expansion rule above. Jerome, please check.

Note

Note that the expand judgment can result in many possible types, depending on how much expansion is performed. We are only interested in the biggest expansion, which is defined by the following auxiliary judgment.

Notation

The judgment

statEnv |- Nillable? TypeReference fully expands to Type

holds when the (nillable) type reference fully expands to the given type.

Semantics

Nillable? TypeReference fully expands to Type1 holds if and only if, Nillable? TypeReference expands to Type1 and there exists no type Type2 such that Nillable? TypeReference expands to Type2 and Type1 <: Type2.

7.3 Judgments for step expressions and filtering

Introduction

Step expressions are one of the elementary operations in [XPath/XQuery]. Steps select nodes reachable from the root of an XML tree. Defining the semantics of step expressions requires a detailed analysis of all the possible cases of axis and node tests.

This section introduces auxiliary judgments used to define the semantics of step expressions. The first judgment captures the notion of principal node kind in XPath. The second and third judgments describe how an axis or a node test filters a type and is used to define the static semantics of Step Expressions. The fourth judgment describes how an axis or a node test filters a sequence of nodes and is used to define the dynamic semantics of Step Expressions. A fifth judgment that accesses the value of an attribute is introduced for convenience.

7.3.1 Principal Node Kind

Notation

The following auxiliary grammar production describe principal node types (See [XML Path Language (XPath) 2.0]).

PrincipalNodeKind
[70 (Formal)]   PrincipalNodeKind   ::=   "element" | "attribute" | "namespace"

Notation

The judgment

Axis principal PrincipalNodeKind

holds when PrincipalNodeKind is the principal node kind for Axis.

Example

For example, the following judgments hold.

  child::       principal  element
  descendant::  principal  element
  preceding::   principal  element
  attribute::   principal  attribute
  namespace::   principal  namespace

Semantics

This judgment is specified by the following rules.

The principal node type for the attribute axis is attribute.


attribute:: principal attribute

The principal node type for the namespace axis is namespace.


namespace:: principal namespace

The principal node type for all other axis is element.

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

Axis principal element

7.3.2 Auxiliary judgments for axis

7.3.2.1 Static semantics of axis

Notation

The following judgment

statEnv |- axis Axis of Type1 : Type2

holds when applying the axis Axis on type Type1 yields the type Type2.

Example

For example, assuming the extended XML Schema given in section [2.3.5 Example of a complete Schema], then the following judgments hold.

  axis child::      of  element of type xsd:string  :  text
  axis child::      of  element items of type Items :  element item of type [Anon1]*

  axis child::      of  element purchaseOrder       : 
    element shipTo of type USAddress,
    element billTo of type USAddress,
    element ipo:comment?,
    element items of type Items

  axis attribute::  of  element of type xsd:string  :  empty

Semantics

This judgment is specified by the following rules.

The first set of rules are used to process the content each individual item type in the input content model. Note that those rules always apply to prime types (see [7.5 Judgments for sequences of item types]).


statEnv |- axis Axis of none : none

statEnv |- axis Axis of Type1 : Type3
statEnv |- axis Axis of Type2 : Type3

statEnv |- axis Axis of Type1|Type2 : Type3|Type4

The following rules specifies how the judgment applies to each Axis.

Applying the self axis to a node type results in the same node type.


statEnv |- axis self:: of NodeType : NodeType

In the case of an element type, the static type of the child axis is obtained by static lookup and expansion of the resulting type, then removal of the types which are attributes. If the extracted type is a simple type, the child axis has type text.

statEnv |- ElementType in context static lookup Nillable? TypeReference
Nillable? TypeReference fully expands to (AttributeType, ChildType)
statEnv |- ChildType <: xdt:anyAtomicType*

statEnv |- axis child:: of ElementType : text

In the case of an element type with complex content type, the static type of the child axis is obtained by static lookup and expansion of the resulting type, then removal of the types which are attributes.

ElementType in context static lookup Nillable? TypeReference
Nillable? TypeReference expands to (AttributeType, ChildType)
statEnv |- ChildType <: node*

statEnv |- axis child:: of ElementType : prime(ChildType) · quantifier(ChildType)

In the case of an attribute type, the static type of the child axis is empty.


statEnv |- axis child:: of AttributeType : empty

In the case of a text node type, the static type of the child axis is empty.


statEnv |- axis child:: of text : empty

In the case of a comment node type, the static type of the child axis is empty.


statEnv |- axis child:: of comment : empty

In the case of a processing-instruction node type, the static type of the child axis is empty.


statEnv |- axis child:: of processing-instruction : empty

In case of a document node type, the static type of the child axis is the factored type of the document node type;.


statEnv |- axis child:: of document { Type } : prime(Type & processing-instructions* & comment*) · quantifier(Type & processing-instructions* & comment*)

In case of an element type, the static type of the attribute axis is obtained by static lookup and expansion of the resulting type, then removal of the types which are not attributes.

statEnv |- element ElementName static lookup Nillable? TypeReference
Nillable? TypeReference expands to (AttributeType, ChildType)

statEnv |- axis attribute:: of ElementType : prime(AttributeType) · quantifier(AttributeType)

In case of an attribute type, the static type of the attribute axis is empty.


statEnv |- axis attribute:: of AttributeType : empty

In case of a text node type, the static type of the attribute axis is empty.


statEnv |- axis attribute:: of text : empty

In case of a comment node type, the static type of the attribute axis is empty.


statEnv |- axis attribute:: of comment : empty

In case of a processing-instruction node type, the static type of the attribute axis is empty.


statEnv |- axis attribute:: of processing-instruction : empty

In case of a document node type, the static type of the attribute axis is the empty.


statEnv |- axis attribute:: of document { Type } : empty

The type for the parent of an element type, a text node type, a PI node type, or a comment node type is either an element, a document, or empty.


statEnv |- axis parent:: of element : (element | document)?


statEnv |- axis parent:: of text : (element | document)?


statEnv |- axis parent:: of processing-instruction : (element | document)?


statEnv |- axis parent:: of comment : (element | document)?

The type for the parent of an attribute node is an element, or empty.


statEnv |- axis parent:: of AttributeType : element?

The type for the parent of a document node type is always empty.


statEnv |- axis parent:: of DocumentType : empty

The type for the namespace axis is always empty.


statEnv |- axis namespace:: of NodeType : empty

The types for the descendant axis is obtained as the closure of the type of the child axis. This is expressed by the following inference rule.

statEnv |- axis child:: of Type : Type1
statEnv |- axis child:: of prime(Type1) : Type2
...
statEnv |- axis child:: of prime(Typen) : Typen+1
statEnv |- prime(Typen+1) <: prime(Type1) | ... | prime(Typen)

statEnv |- axis descendant:: of Type : (prime(Type1) | ... | prime(Typen))*

Note

Note that the last condition above the rule is used to terminate recursion. The rules in fact computes the nth type Typen such that applying the child axis one more time does not add any item type to the union. This condition is guaranteed to hold at one point, since the number of item types is bounded by all of the item types defined in the in-scope schema definitions.

The type for the descendant-or-self axis is the union of the type for the self axis and for the descendant axis.

statEnv |- axis descendant:: of Type1 : Type2

statEnv |- axis descendant-or-self:: of Type1 : (prime(Type1) | prime(Type2))*

The type for the ancestor axis is computed similarly as for the descendant axis.


statEnv |- axis ancestor:: of NodeType : element*

Note that this rule will always result in the type (element | document)* type, but this formulation is prefered for consistency, and in case the static typing for the parent axis gets improved in a future version.

statEnv |- axis parent:: of Type : Type1
statEnv |- axis parent:: of prime(Type1) : Type2
...
statEnv |- axis parent:: of prime(Typen) : Typen+1
statEnv |- prime(Typen+1) <: prime(Type1) | ... | prime(Typen)

statEnv |- axis ancestor:: of Type : (prime(Type1) | ... | prime(Typen))*

The type for the ancestor-or-self axis is the union of the type for the self axis and for the ancestor axis.

statEnv |- axis ancestor:: of Type1 : Type2

statEnv |- axis ancestor-or-self:: of Type1 : (prime(Type1) | prime(Type2))*

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

statEnv |- axis AxisName:: of NodeType : empty otherwise.

Note

Note that in case an axis is applied on a generic node type, it is interpreted in the type system as the union type element | attribute | text | comment | processing-instruction as described in [3.4.1.1 SequenceType Matching].

7.3.2.2 Dynamic semantics of axis

Notation

The following judgment

dynEnv |- axis Axis of Value1 => Value2

holds when applying the axis Axis on Value1 yields Value2:

Example

For example, the following judgments hold.

  axis child::      of    element sizes { text { "1 2 3" } }  =>  text { "1 2 3" }

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

Semantics

This judgment is specified by the following rules.

The first set of rules are used to process the axis judgment on each individual item in the input sequence.


dynEnv |- axis Axis of () => ()

dynEnv |- axis Axis of Value1 => Value3
dynEnv |- axis Axis of Value2 => Value4

dynEnv |- axis Axis of Value1,Value2 => Value3,Value4

The following rules specifies how the value filter judgment is applied on each Axis.

The self axis just returns the context node.


dynEnv |- axis Axis self:: of NodeValue => NodeValue

The child, parent, attribute and namespace axis are specified as follows.


dynEnv |- axis Axis child:: of element ElementName { AttributeValue,ElementValue } => ChildValue


dynEnv |- axis Axis attribute:: of ElementName { AttributeValue,ElementValue } => AttributeValue


dynEnv |- axis Axis parent:: of NodeValue => dm:parent(NodeValue)

Editorial note 
The use of the dm: should be removed. This can be removed when adding the notion of store in the dynamic rules.

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

dynEnv |- axis Axis child:: of NodeValue => Value1
dynEnv |- axis Axis descendant:: of Value1 => Value2

dynEnv |- axis Axis descendant:: of NodeValue => Value1, Value2

dynEnv |- axis Axis self:: of NodeValue => Value1
dynEnv |- axis Axis descendant:: of Value1 => Value2

dynEnv |- axis Axis descendant-or-self:: of NodeValue => Value1, Value2

dynEnv |- axis Axis parent:: of NodeValue => Value1
dynEnv |- axis Axis ancestor:: of Value1 => Value2

dynEnv |- axis Axis ancestor:: of NodeValue => Value1, Value2

dynEnv |- axis Axis self:: of NodeValue => Value1
dynEnv |- axis Axis ancestor:: of Value1 => Value2

dynEnv |- axis Axis ancestor-or-self:: of NodeValue => Value1, Value2

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

dynEnv |- axis Axis of NodeValue => () otherwise.

7.3.3 Auxiliary judgments for node tests

7.3.3.1 Static typing of node tests

Notation

The following judgment

statEnv |- test NodeTest with PrincipalNodeKind of Type1 : Type2

holds when applying the node test NodeTest on the type Type1 in the context of the given principal node kind, yields the type Type2.

Example

For example, assuming the extended XML Schema given in section [2.3.5 Example of a complete Schema], then the following judgments hold.

  test shipTo with "element"  of
    element shipTo of type USAddress,
    element billTo of type USAddress,
    element ipo:comment?,
    element items of type Items
  : element shipTo of type USAddress

Semantics

This judgment is specified by the following rules.

The first set of rules are similar to those for axis, and are used to process the content each individual item type in the input content model. Note that those rules always apply to prime types (see [7.5 Judgments for sequences of item types]).


statEnv |- test NodeTest with PrincipalNodeKind of none : none

statEnv |- test NodeTest with PrincipalNodeKind of Type1 : Type2
statEnv |- test NodeTest with PrincipalNodeKind of Type2 : Type4

statEnv |- test NodeTest with PrincipalNodeKind of Type1|Type2 : Type3|Type4

The following rules specify how the test judgment apply to 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. The static type computed for the expression $v/self::foo is element foo of type xs:anyType, which makes use of foo in the nametest to compute a more specific type. Also note that each case of name matching restricts the principal node kind appropriately.

Editorial note 
Issue: The formal semantics of node tests is still under revision to support the new syntax for type tests and for sequences types. See Issue 559. Additional editorial improvements should also apply to that sections, notably: 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. This part also needs to deal with substitution groups. For instance, say that element b is in the substitution group of element a, then if the current node has static type element(a), then 'self::b' should have type element(b)?, not ()!
QName2 = Prefix2:LocalPart2
fn:get-namespace-from-QName( QName1) = statEnv.namespace(Prefix2)
fn:get-local-name-from-QName( QName1 ) = LocalPart2

statEnv |- test QName2 with "element" of element QName1 TypeSpecifier? : element QName1 TypeSpecifier?

QName2 = Prefix2:LocalPart2
LocalPart1 = LocalPart2

statEnv |- test QName2 with "element" of element *:LocalPart1 TypeSpecifier? : element QName2 TypeSpecifier?

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

statEnv |- test QName2 with "element" of element Prefix1:* TypeSpecifier? : element Prefix1:LocalPart2 TypeSpecifier?


statEnv |- test QName2 with "element" of element TypeSpecifier? : element QName2 TypeSpecifier?

fn:get-local-name-from-QName( QName1 ) = LocalPart2

statEnv |- test *:LocalPart2 with "element" of element QName1 TypeSpecifier? : element QName1 TypeSpecifier?

LocalPart1 = LocalPart2

statEnv |- test *:LocalPart2 with "element" of element *:LocalPart1 TypeSpecifier? : element *:LocalPart2 TypeSpecifier?


statEnv |- test *:LocalPart2 with "element" of element Prefix1:* TypeSpecifier? : element Prefix1:LocalPart2 TypeSpecifier?


statEnv |- test *:LocalPart2 with "element" of element TypeSpecifier? : element *:LocalPart2 TypeSpecifier?

fn:get-namespace-from-QName( QName1) = statEnv.namespace(Prefix2)

statEnv |- test Prefix2:* with "element" of element QName1 TypeSpecifier? : element QName1 TypeSpecifier?


statEnv |- test Prefix2:* with "element" of element *:LocalPart1 TypeSpecifier? : element Prefix2:LocalPart1 TypeSpecifier?

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

statEnv |- test Prefix2:* with "element" of element Prefix1:* TypeSpecifier? : element Prefix1:* TypeSpecifier?


statEnv |- test Prefix2:* with "element" of element TypeSpecifier? : element Prefix2:* TypeSpecifier?


statEnv |- test * with "element" of element prefix:local TypeSpecifier? : element prefix:local TypeSpecifier?

Similar typing rules apply to attributes:

QName2 = Prefix2:LocalPart2
fn:get-namespace-from-QName( QName1) = statEnv.namespace(Prefix2)
fn:get-local-name-from-QName( QName1 ) = LocalPart2

statEnv |- test QName2 with "attribute" of attribute QName1 TypeReference? : attribute QName1 TypeReference?

QName2 = Prefix2:LocalPart2
LocalPart1 = LocalPart2

statEnv |- test QName2 with "attribute" of attribute *:LocalPart1 TypeReference? : attribute QName2 TypeReference?

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

statEnv |- test QName2 with "attribute" of attribute Prefix1:* TypeReference? : attribute Prefix1:LocalPart2TypeReference?


statEnv |- test QName2 with "attribute" of attribute TypeReference? : attribute QName2 TypeReference?

fn:get-local-name-from-QName( QName1 ) = LocalPart2

statEnv |- test *:LocalPart2 with "attribute" of attribute QName1 TypeReference? : attribute QName1 TypeReference?

LocalPart1 = LocalPart2

statEnv |- test *:LocalPart2 with "attribute" of attribute *:LocalPart1 TypeReference? : attribute *:LocalPart2 TypeReference?


statEnv |- test *:LocalPart2 with "attribute" of attribute Prefix1:* TypeReference? : attribute Prefix1:LocalPart2TypeReference?


statEnv |- test *:LocalPart2 with "attribute" of attribute TypeReference? : attribute *:LocalPart2 TypeReference?

fn:get-namespace-from-QName( QName1) = statEnv.namespace(Prefix2)

statEnv |- test Prefix2:* with "attribute" of attribute QName1 TypeReference? : attribute QName1 TypeReference?


statEnv |- test Prefix2:* with "attribute" of attribute *:LocalPart1 TypeReference? : attribute Prefix2:LocalPart1 TypeReference?

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

statEnv |- test Prefix2:* with "attribute" of attribute Prefix1:* TypeReference? : attribute Prefix1:* TypeReference?


statEnv |- test Prefix2:* with "attribute" of attribute TypeReference? : attribute Prefix2:* TypeReference?


statEnv |- test * of attribute prefix:local TypeReference? with "attribute" : attribute prefix:local TypeReference?

Comments, processing instructions, and text:


statEnv |- test processing-instruction() with PrincipalNodeKind of processing-instruction : processing-instruction


statEnv |- test processing-instruction(String) with PrincipalNodeKind of processing-instruction : processing-instruction


statEnv |- test comment() with PrincipalNodeKind of comment : comment


statEnv |- test text() of with PrincipalNodeKind text : text


statEnv |- test node() with PrincipalNodeKind of NodeType : NodeType

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

statEnv |- test node() with PrincipalNodeKind of NodeType : empty
7.3.3.2 Dynamic semantics of node tests

Notation