The presentation of this document has been augmented to identify changes from a previous version. Three kinds of changes are highlighted: new, added text, changed text, and deleted text.
This document is also available in these non-normative formats: XML and Revisions to LC Draft.
Copyright © 2005 W3C® (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
This document defines formally the semantics of XQuery 1.0 [XQuery 1.0: A Query Language for XML] XPath 2.0 [XML Path Language (XPath) 2.0].
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. 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.
XQuery 1.0, XPath 2.0, and their formal semantics has been defined jointly by the XML QueryWorking Groupand the XSL WorkingGroup(both part of the XML Activity).
Thisdraft includes corrections and changes based on publiccomments on the Last Call Working Draft dated 03June 2005. These decisions are recorded in the Bugzilla database (http://www.w3.org/Bugs/Public/). A list of changes since the Last Call Working Draft of 03June 2005 can be found in [F Revision Log].
A number of technical and editorial issues are still being processedby the Working Groups. Some of the main technicalchanges that arestill not implemented in this working draft include improvementsto the formalnotations (Bugs[1605],[1614],[1618], [1730], [1790]), fixesto bugs inthe semantics of function calls (Bugs [1582],[1583],[1820]), function and variable declarations (Bugs [1743],[1964], [1965]), and fixes to the semantics of constructors (Bugs [1628],[1629],[1641]).
This draft is being providedto permit public review of the changes thathave beenmade as a result of the Last Callcomments. Comments on the changes should be made against the pertinent Last Call comment (instructions can be found at http://www.w3.org/XML/2005/04/qt-bugzilla). If access to that system is not feasible, you may send your comments to the W3C mailing list, public-qt-comments@w3.org (archived at http://lists.w3.org/Archives/Public/public-qt-comments/). Please start the subject line with “[FS]” so comments can be classified correctly.
The XMLQuery and XSL Working Groups expect to progress this document to Candidate Recommendation status in the very nearfuture.
The patent policy for this document is the 5 February 2004 W3C Patent Policy. Patent disclosures relevant to this specification may be found on the XML Query Working Group's patent disclosure page and the XSL Working Group's patent disclosure page. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) with respect to this specification should disclose the information in accordance with section 6 of the W3C Patent Policy.
1 Introduction
1.1 Normative and Informative Sections
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 URIs, Namespaces, and Prefixes
2.3 XML Values
2.3.1 Formal values
2.3.2 Examples of values
2.4 The [XPath/XQuery] Type System
2.4.1 XML Schema and the [XPath/XQuery] Type System
2.4.2 Item types
2.4.3 Content models
2.4.4 Top level definitions
2.4.5 Example of a complete Schema
2.5 Functions and operators
3 Basics
3.1 Expression Context
3.1.1 Static Context
3.1.1.1 Resolving QNames to Expanded QNames
3.1.2 Dynamic Context
3.2 Processing Model
3.2.1 Processing model
3.2.2 Normalization judgment
3.2.3 Static typing judgment
3.2.4 Dynamic evaluation judgment
3.3 Error Handling
3.4 Concepts
3.4.1 Document Order
3.4.2 Atomization
3.4.3 Effective Boolean Value
3.4.4 Input Sources
3.4.5 URI Literals
3.5 Types
3.5.1 Predefined Schema Types
3.5.2 Typed Value and String Value
3.5.3 SequenceType Syntax
3.5.4 SequenceType Matching
3.6 Comments
4 Expressions
4.1 Primary Expressions
4.1.1 Literals
4.1.2 Variable References
4.1.3 Parenthesized Expressions
4.1.4 Context Item Expression
4.1.5 Function Calls
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 Filter Expressions
4.3.3 Combining Node 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.6 Logical Expressions
4.7 Constructors
4.7.1 Direct Element Constructors
4.7.1.1 Attributes
4.7.1.2 Namespace Declaration Attributes
4.7.1.3 Content
4.7.1.4 Whitespace in Element Content
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 Node Constructors
4.7.3.5 Computed Processing Instruction Constructors
4.7.3.6 Computed Comment Constructors
4.7.4 In-scope Namespaces of a Constructed Element
4.8 [For/FLWOR] 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 Ordered and 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
4.13.1 Validating an Element Node
4.13.2 Validating a Document Node
4.14 Extension Expressions
5 Modules and Prologs
5.1 Version Declaration
5.2 Module Declaration
5.3 Boundary-space Declaration
5.4 Default Collation Declaration
5.5 Base URI Declaration
5.6 Construction Declaration
5.7 Ordering Mode Declaration
5.8 Empty Order Declaration
5.9 Copy-Namespaces Declaration
5.10 Schema Import
5.11 Module Import
5.12 Namespace Declaration
5.13 Default Namespace Declaration
5.14 Variable Declaration
5.15 Function Declaration
5.16 Option Declaration
6 Conformance
6.1 Static Typing Feature
6.1.1 Static Typing Extensions
7 Additional Semantics of Functions
7.1 Formal Semantics Functions
7.1.1 The fs:convert-operand function
7.1.2 The fs:convert-simple-operand function
7.1.3 The fs:distinct-doc-order function
7.1.4 The fs:distinct-doc-order-or-atomic-sequence function
7.1.5 The fs:item-sequence-to-node-sequence function
7.1.6 The fs:item-sequence-to-untypedAtomic function
7.1.7 The fs:item-sequence-to-untypedAtomic-PI function
7.1.8 The fs:item-sequence-to-untypedAtomic-text function
7.1.9 The fs:item-sequence-to-untypedAtomic-comment function
7.1.10 The fs:apply-ordering-mode function
7.1.11 The fs:to function
7.2 Standard functions with specific typing rules
7.2.1 The fn:last context function
7.2.2 The fn:position context function
7.2.3 The fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions
7.2.4 The fn:boolean function
7.2.5 The fn:collection and fn:doc functions
7.2.6 The fn:data function
7.2.7 The fn:distinct-values function
7.2.8 The fn:unordered function
7.2.9 The fn:error function
7.2.10 The fn:min, fn:max, fn:avg, and fn:sum functions
7.2.11 The fn:remove function
7.2.12 The fn:reverse function
7.2.13 The fn:subsequence function
7.2.14 The op:union, op:intersect, and op:except operators
7.2.15 The fn:insert-before function
7.2.16 The fn:zero-or-one, fn:one-or-more, and fn:exactly-one functions
8 Auxiliary Judgments
8.1 Judgments for accessing types
8.1.1 Derives from
8.1.2 Substitutes for
8.1.3 Element and attribute name lookup (Dynamic)
8.1.4 Element and attribute type lookup (Static)
8.1.5 Extension
8.1.6 Mixed content
8.1.7 Type adjustment
8.1.8 Builtin attributes
8.1.9 Type expansion
8.1.10 Union interpretation of derived types
8.2 Judgments for step expressions and filtering
8.2.1 Principal Node Kind
8.2.2 Auxiliary judgments for axes
8.2.2.1 Static semantics of axes
8.2.2.1.1 Inference rules for all axis
8.2.2.1.2 Inference rules for the self axis
8.2.2.1.3 Inference rules for the child axis
8.2.2.1.4 Inference rules for the attribute axis
8.2.2.1.5 Inference rules for the parent axis
8.2.2.1.6 Inference rules for the namespace axis
8.2.2.1.7 Inference rules for the descendant axis
8.2.2.1.8 Inference rules for the descendant-or-self axis
8.2.2.1.9 Inference rules for the ancestor axis
8.2.2.1.10 Inference rules for the ancestor-or-self axis
8.2.2.2 Dynamic semantics of axes
8.2.3 Auxiliary judgments for node tests
8.2.3.1 Static semantics of node tests
8.2.3.1.1 Name Tests
8.2.3.1.2 Kind Tests
8.2.3.2 Dynamic semantics of node tests
8.2.3.2.1 Name Tests
8.2.3.2.2 Kind Tests
8.3 Judgments for type matching
8.3.1 Matches
8.3.2 Subtype and Type equality
8.4 Judgments for FLWOR and other expressions on sequences
8.5 Judgments for function calls
8.5.1 Type promotion
8.6 Judgments for validation modes and contexts
8.6.1 Elements in validation mode
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 Importing Schemas
C.1 Introduction
C.1.1 Features
C.1.2 Organization
C.1.3 Main mapping rules
C.1.4 Special attributes
C.1.4.1 use, default, and fixed
C.1.4.2 minOccurs, maxOccurs, minLength, maxLength, and length
C.1.4.3 mixed
C.1.4.4 nillable
C.1.4.5 substitutionGroup
C.1.5 Anonymous type names
C.2 Schemas as a whole
C.2.1 Schema
C.2.2 Include
C.2.3 Redefine
C.2.4 Import
C.3 Attribute Declarations
C.3.1 Global attributes declarations
C.3.2 Local attribute declarations
C.4 Element Declarations
C.4.1 Global element declarations
C.4.2 Local element declarations
C.5 Complex Type Definitions
C.5.1 Global complex type
C.5.2 Local complex type
C.5.3 Complex type with simple content
C.5.4 Complex type with complex content
C.6 Attribute Uses
C.7 Attribute Group Definitions
C.7.1 Attribute group definitions
C.7.2 Attribute group reference
C.8 Model Group Definitions
C.9 Model Groups
C.9.1 All groups
C.9.2 Choice groups
C.9.3 Sequence groups
C.10 Particles
C.10.1 Element reference
C.10.2 Group reference
C.11 Wildcards
C.11.1 Attribute wildcards
C.11.2 Element wildcards
C.12 Identity-constraint Definitions
C.13 Notation Declarations
C.14 Annotation
C.15 Simple Type Definitions
C.15.1 Global simple type definition
C.15.2 Local simple type definition
C.15.3 Simple type content
D References
D.1 Normative References
D.2 Non-normative References
D.3 Background References
E Auxiliary Judgments for Validation (Non-Normative)
E.1 Judgments for the validate expression
E.1.1 Type resolution
E.1.2 Interleaving
E.1.3 Attribute filtering
E.1.4 Erasure
E.1.4.1 Simply erases
E.1.4.2 Erases
E.1.5 Annotate
E.1.5.1 Simply annotate
E.1.5.2 Nil-annotate
E.1.5.3 Annotate
F Revision Log (Non-Normative)
F.1 15 September 2005
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:
[XQuery 1.0: A Query Language for XML] introduces the XQuery 1.0 language, defines its capabilities from a user-centric view, and defines the language syntax.
[XML Path Language (XPath) 2.0] introduces the XPath 2.0 language, defines its capabilities from a user-centric view, and defines the language syntax.
[Functions and Operators] lists the functions and operators defined for the [XPath/XQuery] language and specifies the required types of their parameters and return value.
[Data Model] formally specifies the data model used by [XPath/XQuery] to represent the content of XML documents. The [XPath/XQuery] language is formally defined by operations on this data model.
[Data Model Serialization] specifies how [XPath/XQuery] data model values are serialized into XML.
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. This document defines the formal semantics for XPath 2.0 only when the XPath 1.0 backward compatibility rules are not in effect.
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 characteristic of a functional language is that variables are always passed by value, and a variable's 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. Static type analysis infers the output type of an expression based on the type of its input expressions. In addition to inferring the type an expression for the user, static typing allows early detection of type errors, and can be used as the basis for certain classes of optimization. The [XPath/XQuery] type system captures most of the features of [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. [7 Additional Semantics of Functions] defines the static semantics of several functions in [Functions and Operators] and gives the dynamic and static semantics of several supporting functions used in this document. The remaining sections, [8 Auxiliary Judgments] and [C Importing Schemas], contain material that supports the formal semantics of [XPath/XQuery]. [8 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 judgments are used in the definition of expressions in [4 Expressions]. Lastly, [C 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.
Certain aspects of language processing are described in this specification as implementation-defined or implementation-dependent.
[Definition: Implementation-defined indicates an aspect that may differ between implementations, but must be specified by the implementor for each particular implementation.]
[Definition: Implementation-dependent indicates an aspect that may differ between implementations, is not specified by this or any W3C specification, and is not required to be specified by the implementor for any particular implementation.]
A language aspect described in this specification as implementation-defined or implementation dependent may be further constrained by the specifications of a host language in which XPath or XQuery is embedded.
This document contains the normative static semantics of [XPath/XQuery]. The static semantics rules in [3 Basics], [4 Expressions], [5 Modules and Prologs], and [7 Additional Semantics of Functions] are normative. [3.1.1 Static Context] is normative, because it defines the static context used in the static typing rules. [8 Auxiliary Judgments] is normative, because it contains all the judgments necessary for defining SequenceType Matching.
The dynamic semantics of [XPath/XQuery] are normatively defined in [XQuery 1.0: A Query Language for XML] and [XML Path Language (XPath) 2.0]. In this document, the dynamic semantic rules in [3 Basics], [4 Expressions], and [5 Modules and Prologs], the examples, and the material labeled as "Note" are provided for explanatory purposes and are not normative.
The mapping rules from XML Schema to the XQuery type system provided in [C Importing Schemas], and the formal semantics of XML Schema validation in [E Auxiliary Judgments for Validation] are informative and do not handle every feature of XML Schema.
This section provides the background necessary to understand the Formal Semantics, introduces the notations that are used, and explains its relationship to other documents.
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 inferred 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 introduces 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.3 XML Values].
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: productions from the [XPath/XQuery] grammar itself, productions for a subset of the [XPath/XQuery] language called the XQuery Core which is used throughout this document, and other productions used for formal specification only such as for the XQuery type system.
XQuery grammar productions describe the XQuery language and expressions. XQuery productions are identified by a number, which corresponds to their number in the [XQuery 1.0: A Query Language for XML] document, and are marked with "(XQuery)". For instance, the following production describes FLWOR expressions in XQuery.
| [33 (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 their number in [XML Path Language (XPath) 2.0], and are marked with "(XPath)". For instance, the following production describes for expressions in XPath.
| [4 (XPath)] | ForExpr |
::= | SimpleForClause "return" ExprSingle |
XQuery Core grammar productions describe the XQuery Core. The Core grammar is given in [A Normalized core grammar]. Core productions are identified by a number, which corresponds to their number in [A Normalized core grammar], and are marked with "(Core)". For instance, the following production describes the simpler form of the "FLWOR" expression in the XQuery Core.
| [32 (Core)] | FLWORExpr |
::= | (ForClause | LetClause) "return" ExprSingle |
The Formal Semantics manipulates "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 [Data Model], and to describe the [XPath/XQuery] type system. Formal Semantics productions are identified by a number, and are marked by "(Formal)". For instance, the following production describes global type definitions in the [XPath/XQuery] type system.
| [40 (Formal)] | Definition |
::= | ("define" "element" ElementName Substitution? Nillable? TypeReference) |
Note that grammar productions that are specific to the Formal Semantics (i.e., marked with "(Formal)") are not part of [XPath/XQuery]. They are not accessible to the user and are only used in the course of defining the languages' semantics.
Grammar non-terminals are used extensively in this document to represent objects in inference rules (see the next section). As a convenience, non-terminals used in inference rules link to the appropriate grammar production.
The basic building block of the formal specification is called a judgment. A judgment expresses whether a property holds or not.
For example:
Notation
The judgment
holds if the object Painting is beautiful.
Notation
Here are three judgments that are used extensively in this document.
The judgment
holds if the expression Expr yields (or evaluates to) the value Value.
The judgment
holds when the expression Expr has the type Type.
Most other judgments used in this document are short english sentences intended to reflect their meaning, and written in bold fonts. For instance, the judgment
holds PrincipalNodeKind isthe principal nodekind for the axis Axis.
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'.
Patterns may have a name that is not exactly the name of a grammar production but is based on it. For instance, a BaseTypeName is a pattern that 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.
In some cases, inference rules may need to use the fact that a certain judgment does not hold. We may write not(Judgment) the judgment which holds iff Judgment does not hold.
In some cases, an "object" may take a value within a finite set of pre-determined values. We may write those set of possible value using the in judgment. For instance, the judgment
which holds, if the object Color has either the value blue or the value green.
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, written respectively 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 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'.
An inference rule may have no premises above the line, which 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. 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 occurrence of a given 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 valuebound to thefirst(second, etc) occurrence ofVariable.
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 accessed later on during evaluation when that variable is accessed.
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 access information in 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 similar to function application, because an environment can be considered 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 "group" is an environment group with the environment component "env", then that environment is denoted "group.env" and the value that symbol is mapped to is denoted "group.env(symbol)".
The two main environment groups used in the Formal Semantics are: a dynamic environment group (dynEnv), which models to the [XPath/XQuery]'s dynamic context, and a static environment group (statEnv), which models the [XPath/XQuery]'s static context. Both are defined in [3.1 Expression Context].
For example, dynEnv.varValue denotes the dynamic environment that maps variables to values and dynEnv.varValue(Variable) denotes the value of the variable Variable in the dynamic context.
Environment groups are used in a judgment to capture some of the context in which the judgment is computed, and most judgments are computed assuming that some environment is given. This assumption is denoted by prefixing the judgment with "env |-". The "|-" symbol is called a "turnstile" and is used in almost all inference rules.
For instance, the judgment
is read as: Assuming the dynamic environment group dynEnv, the expression Expr yields the value Value.
Environment groups can be updated, using the following notation:
"group + env(symbol => object) " denotes the new environment group that is identical to group except that the env environment has been updated to map symbol to object. The notation symbol => object indicates that symbol is mapped to object in the new environment.
The following shorthand is also allowed: "group + env( 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 " (group + env( symbol1 => object1) + ... ) + env(symboln => objectn)".
Updating an environment creates a copy of the original environment and overrides any previous binding that might exist for the same name and the same group in that environment. Updating the environment is used to capture the scope of a symbol (e.g., for variables, namespace prefixes, etc). For instance, in the following expression
let $x := 1 return let $x := $x + 2 return $x - 3
each let expression changes the dynamic context by binding a new variable to a new value. Each different context is represented by a different environment. The original environment, in which the expression 1 is evaluated, does not contain any binding for variable $x. This environment is updated a first time with a binding of variable $x to the value 1, and this environment is used for the evaluation of the expression $x + 2. Then it is
updated a second time with a binding of variable $x to the value 3, and this environment is used for the evaluation of the expression$x - 3.
Also, note that there are no operations to remove entries from environments. This is never necessary as updating an environment effectively creates a new extended copy of the original environment, leaving the original environment accessible wherever it is in scope along with the updated copy.
Putting the above notations together, here is an example of an inference rule that occurs later in this document:
This rule is read as follows: if two expressions Expr1 and Expr2 are known to have the static 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 |- let $VarName := Expr1 return Expr2 : Type2 |
This rule is read as follows: First, because the variable is a QName, it is first expanded into an expanded QName. Second, the type Type1 for the "let" input expression Expr1 is computed. Then the "let" variable with expanded name, expanded-QName with type Type1 is added into the varType component of the static environment group statEnv. Finally, the type Type2 of Expr2 is computed in that new environment.
Each inference rule describes a fragment of the semantics for a given expression. Here is how those rules are combined. Consider the following expression.
let $x := 1 return ($x,$x)
We have just seen the static typing rule for the let clause and sequence construction. To handle this expression completely, we need inference rules for integer literals and variable access. Those two rules are as follows.
|
||
|
|
||
|
With this set of rules, we can compute the type of the expression above in a bottom-up fashion, i.e., starting with the sub-expressions. The resulting type inference proceeds as follows.
statEnv0 = ()
statEnv0 |- 1 : xs:integer
statEnv1 = ($x -> 1)
statEnv1 |- $x : xs:integer
statEnv1 |- $x : xs:integer
statEnv1 |- ($x,$x) : xs:integer,xs:integer
statEnv0 |- let $x := 1 return ($x,$x) : xs:integer,xs:integer
This example illustrates how each rule is applied to individual sub-expressions, and how the environment is used to maintain the relevant context information.
The Formal Semantics does not formally specify the adjustment of relative URIs according to a base URI. All URIs used in this document are assumed to be absolute URIs.
The Formal Semantics uses the following namespace prefixes.
fn: for functions and operators from the [Functions and Operators] document.
xs: for XML Schema components and built-in types.
xdt: for [XPath/XQuery] built-in types.
All these prefixes are assumed to be bound to the appropriate URIs.
In addition, the Formal Semantics uses the following special prefixes for specification purposes.
dm: for accessors of the [Data Model].
op: for operators in [Functions and Operators].
fs: for functions and types defined in the formal semantics.
These prefixes are always italicized to emphasize that the corresponding functions, variables, and types are abstract: they are not and cannot be made accessible in [XPath/XQuery]. None of these special prefixes are given a URI.
The [XPath/XQuery] language is defined over values of the [XPath/XQuery] data model. The [XPath/XQuery] data model is defined normatively in [Data Model]. We define the formal notation that is used in this document to describe and manipulate values in inference rules. Formal values are used for specification purposes only and are not exposed to the [XPath/XQuery] user.
This section gives the grammar for formal values, along with a summary of the corresponding data model properties. In the context of this document, all constraints on values that are specified in [Data Model] are assumed to hold.
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, labeled with the name of that atomic type. An atomic type is either a primitive or derived atomic type according to XML Schema [Schema Part 2], xdt:untypedAtomic, or xdt:anyAtomicType.
A node is either an element, an attribute, a document, a text, a comment, or a processing-instruction node.
Element nodes have a type annotationXQ and contain a complex value or a simple value. Attribute nodes have a type annotationXQ and contain a simple value. Text nodes always contain one string value of type xdt:untypedAtomic, therefore the corresponding type annotation is omitted in
the formal notation of a text node. Document nodes do not have a type annotation and contain a sequence of element, text, comment, or processing-instruction nodes.
A simple value is a sequence of atomic values.
A complex value is a sequence of attribute nodes followed by a sequence of element, text, comment, or processing-instruction nodes.
A type annotationXQ 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 using the fs: Formal Semantics prefix: fs:anon0, fs:anon1, etc.
Formal values are defined by the following grammar.
| [7 (Formal)] | Value |
::= | Item |
| [21 (Formal)] | Item |
::= | NodeValue |
| [22 (Formal)] | AtomicValue |
::= | AtomicValueContent TypeAnnotation? |
| [1 (Formal)] | AtomicValueContent |
::= | String |
| [2 (Formal)] | TypeAnnotation |
::= | "of" "type" TypeName |
| [9 (Formal)] | ElementValue |
::= | "element" ElementName "nilled"? TypeAnnotation? "{" Value "}" ("{" NamespaceBindings "}")? |
| [10 (Formal)] | AttributeValue |
::= | "attribute" AttributeName TypeAnnotation? "{" SimpleValue "}" |
| [8 (Formal)] | SimpleValue |
::= | AtomicValue |
| [11 (Formal)] | DocumentValue |
::= | "document" "{" Value "}" |
| [13 (Formal)] | CommentValue |
::= | "comment" "{" String "}" |
| [14 (Formal)] | ProcessingInstructionValue |
::= | "processing-instruction" QName "{" String "}" |
| [12 (Formal)] | TextValue |
::= | "text" "{" String "}" |
| [20 (Formal)] | NodeValue |
::= | ElementValue |
| [3 (Formal)] | ElementName |
::= | QName |
| [6 (Formal)] | AttributeName |
::= | QName |
| [23 (Formal)] | TypeName |
::= | QName |
| [15 (Formal)] | NamespaceBindings |
::= | NamespaceBinding ("," NamespaceBinding)* |
| [17 (Formal)] | NamespaceBinding |
::= | "namespace" NCName "{" String "}" |
Notation
In that grammar, "String" indicates the value space of xs:string, "Decimal" indicates the value space of xs:decimal, etc.
Element (resp. attributes) without type annotations, are assumed to have the type annotation xs:anyType (resp. xs:anySimpleType). Atomic values without type annotations, are assumed to have a type annotation which is the base type for the corresponding value. For instance, "Hello, World!" is equivalent to "Hello, World!" of type xs:string.
Untyped elements (e.g., from well-formed documents) have the type annotationXQ xdt:untyped, untyped attributes have the type annotationXQ xdt:untypedAtomic, and untyped atomic values have the type annotationXQ 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 the element has no content and an attribute xsi:nil set to "true".
An element also has a sequence of namespace bindings, which are the set of in-scope namespaces for that element. Each namespace binding is a prefix, URI pair. Elements without namespace bindings are assumed to have an empty set of in-scope namespaces.
Note:
In [XPath], the in-scope namespaces of an element node are represented by a collection of namespace nodes arranged on a namespace axis, which is optional and deprecated in [XML Path Language (XPath) 2.0]. XQuery does not support the namespace axis and does not represent namespace bindings in the form of nodes.
In examples, we omit the namespace bindings when they are empty. For example, the following two values are the same (note that the xs and xdt prefixes are built-in):
element weight of type xs:integer { text { "42" } } {}
element weight of type xs:integer { text { "42" } }
The same rule about constructing sequences apply to the values described by that grammar. Notably sequences are automatically flattened. For example, the sequence (10, (1, 2), (), (3, 4)) is equivalent to the sequence (10, 1, 2, 3, 4). Those rules are described in more details in [Data Model].
When the context is clear, we may omit the type annotationXQ on literal values. For instance:
"Hello World!" instead of "Hello World!" of type xs:string 10 instead of 10 of type xs:integer
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 xdt:untyped {
text { "The cat weighs " },
element weight of type xdt:untyped {
attribute units of type xdt:untypedAtomic {
"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 xdt:untyped {
attribute xsi:type of type xdt:untypedAtomic {
"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 xdt:untyped {
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 xdt:untyped {
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 fs:anon1 {
1 of type xs:integer,
2 of type xs:integer,
3 of type xs:integer
}
where fs:anon1 stands for the internal anonymous name generated by the system for the sizes element.
A nillable element with xsi:type set to true:
<sizes xsi:nil="true"/>
Before validation, this element is represented as:
element sizes of type xdt:untyped {
attribute xsi:nil of type xdt:untypedAtomic { "true" of type xdt:untypedAtomic }
}
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:boolean { true of type xs:boolean }
}
An element with a union type
<sizes>1 two 3 four</sizes>
Before validation, this element is represented as:
element sizes of type xdt:untyped {
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
}
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.
The [XPath/XQuery] type system is based on [Schema Part 1] and [Schema Part 2]. [Schema Part 1] and [Schema Part 2] specify normatively the type information available in [XPath/XQuery]. We define the formal notation that is used in this document to describe and manipulate types in inference rules. Formal types are used for specification purposes only and 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, and minLength, maxLength on list types for the occurrences that correspond to the DTD operators +, *, and ?. Choices are represented using the DTD operator |. All groups are represented using the interleaving operator (&).
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 and identity constraints are not formally represented in the [XPath/XQuery] type system. However, an [XPath/XQuery] implementation supporting XML Schema import and validation must take simple type facets and identity constraints into account.
This document describe types in the [XPath/XQuery] types system, as well as the operations and properties over those types which are used to define the [XPath/XQuery] static typing feature. The two most important properties are whether a data instances matches a type, and whether a type is a subtype of another. Those properties are described in [8.3 Judgments for type matching]. This document does not describe all other possible properties over those types.
The mapping from XML Schema into the [XPath/XQuery] type system is given in [C Importing Schemas]. The rest of this section is organized as follows. [2.4.2 Item types] describes item types, [2.4.3 Content models] describes content models, and [2.4.4 Top level definitions] describe top-level type declarations.
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. We distinguish between document nodes, attribute nodes, and nodes that can occur in element content (elements, comments, processing instructions, and text nodes), as we need to refer to element content types later in the formal semantics.
| [26 (Formal)] | FormalItemType |
::= | AtomicTypeName | NodeType |
| [29 (Formal)] | AtomicTypeName |
::= | QName |
| [27 (Formal)] | NodeType |
::= | DocumentType |
| [28 (Formal)] | ElementContentType |
::= | ElementType |
| [30 (Formal)] | ElementType |
::= | "element" ElementName? TypeSpecifier? |
| [31 (Formal)] | TypeSpecifier |
::= | Nillable? TypeReference |
| [32 (Formal)] | AttributeType |
::= | "attribute" AttributeName? TypeReference? |
| [33 (Formal)] | Nillable |
::= | "nillable" |
| [37 (Formal)] | TypeReference |
::= | "of" "type" TypeName |
| [49 (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 for any element or any attribute. In addition, an element type has an optional nillable flag that indicates whether the element can be nilled or not.
A document type has an optional content type. If no content type is given, then the type is treated as being the wildcard type for documents, i.e., a sequence of text and element nodes. For consistency with element nodes, PIs and comments are not indicated in that wildcard type, but may occur in instances.
Note
Generic node types (e.g., node()) such as used in the SequenceType production, 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.5.4 SequenceType Matching].
Examples
The following is a text node type
text
The following is a type for all elements
element
The following is a type for all elements of type string
element of type xs:string
The following is a type for a nillable element of type string and with name size
element size nillable of type xs:string
The following is a reference to a global attribute declaration
attribute sizes
The following is a type for elements with anonymous type fs:anon1:
element sizes of type fs:anon1
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 (written empty), or empty choice (written none).
The type empty matches the empty sequence. The type none matches no values. none is the identity for choice, that is (Type | none) = Type. The type none is the static type for [7.2.9 The fn:error function].
| [24 (Formal)] | Type |
::= | FormalItemType |
| [25 (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 captures the semantics of all groups in XML Schema, but it more general has it applies to arbitrary types. All groups in XML Schema are restricted to apply only on global or local element declarations with minOccurs 0 or 1, and maxOccurs 1.
The "&" operator builds the "interleaved product" of two types. The type Type1 & Type2 matches any sequence that is an interleaving of two sequences of items, the first one matching Type1 and the second matching Type2. Where the interleaving of two sequences of items Value1 and Value2 is any sequence Value0 such that there is an ordered partition of Value0 into the two sub-sequences Value1 and Value2.
For example, consider the types Type1 = xs:integer,xs:integer,xs:integer and Type2 = xs:string,xs:string. Value1 = (1,2,3) matches the type Type1 and
Value2 = ("a","b") matches the type Type2. Any of the following Value0 are interleavings of Value1 and Value2, and therefore match the type (Type1 & Type2):
Value0 = (1,2,3,"a","b")
Value0 = (1,2,"a",3,"b")
Value0 = (1,2,"a","b",3)
Value0 = (1,"a",2,3,"b")
Value0 = (1,"a",2,"b",3)
Value0 = (1,"a","b",2,3)
Value0 = ("a",1,2,3,"b")
Value0 = ("a",1,2,"b",3)
Value0 = ("a",1,"b",2,3)
Value0 = ("a","b",1,2,3)
Types precedence order. To improve readability when writing types, we assume the following precedence order between operators on types.
| # | Operator | Associativity |
|---|---|---|
| 1 | | (choice) | left-to-right |
| 2 | & (interleaving) | right-to-left |
| 3 | , (sequence) | left-to-right |
| 4 | *, +, ? (occurrence) | left-to-right |
Parenthesis can be used to enforce precedence. For instance
xs:string | xs:integer, xs:float*
is equivalent to
xs:string | (xs:integer, (xs:float*))
and a different precedence can be obtained by writing
((xs:string | xs:integer), xs:float)*
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 global 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)*
Top level definitions correspond to global element declarations, global attribute declarations and type definitions in XML Schema.
| [41 (Formal)] | Definitions |
::= | Definition* |
| [40 (Formal)] | Definition |
::= | ("define" "element" ElementName Substitution? Nillable? TypeReference) |
| [42 (Formal)] | Substitution |
::= | "substitutes" "for" ElementName |
| [34 (Formal)] | TypeDerivation |
::= | ComplexTypeDerivation | AtomicTypeDerivation |
| [35 (Formal)] | ComplexTypeDerivation |
::= | Derivation? Mixed? "{" Type? "}" |
| [36 (Formal)] | AtomicTypeDerivation |
::= | "restricts" AtomicTypeName |
| [38 (Formal)] | Derivation |
::= | ("restricts" TypeName) |
| [39 (Formal)] | Mixed |
::= | "mixed" |
A type definition has a name (possibly anonymous) and a type derivation. In the case of a complex type, the derivation indicateswether it is derived by extension or restriction, its basetype, and its content model, withan optional flag indicating if it has mixed content. For instance, the following complextype
<complexType name="UKAddress">
<complexContent>
<extension base="ipo:Address">
<sequence>
<element name="postcode" type="ipo:UKPostcode"/>
</sequence>
<attribute name="exportCode" type="positiveInteger" fixed="1"/>
</extension>
</complexContent>
</complexType>
is represented as follows
define type UKAddress extends ipo:Address {
attribute exportCode of type ipo:UKPostcode,
element postcode of type positiveInteger
};
In the case of simple types derived by union or list, the derivation is always a restriction from the base typexs:anySimpleType, and has acontent which is a union
of the membertypes, or a repetion of the item type. For instance, thetwo following simple type declarations
<xsd:simpleType name="listOfMyIntType"> <xsd:list itemType="myInteger"/> </xsd:simpleType> <xsd:simpleType name="zipUnion"> <xsd:union memberTypes="USState FrenchRegion"/> </xsd:simpleType>
are represented asfollows
define type listOfMyIntType restricts xs:anySimpleType {
myInteger*
}
define type zipUnion restricts xs:anySimpleType {
USState | FrenchRegion
}
In the case of an atomic type, it just indicates its base type. For instance, the followingtype definition
<xsd:simpleType name="SKU">
<xsd:restriction base="xsd:string">
<xsd:pattern value="\d{3}-[A-Z]{2}"/>
</xsd:restriction>
</xsd:simpleType>
is respresented as follow
define type SKU restrict xsd:string;
When the type derivation is omitted, the type d