This section provides the background necessary to understand the
Formal Semantics, introduces the notations that are used, and
explains its relationship to other documents.
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: An XML Query Language] 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].
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: 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: An XML Query Language]
document, and are marked with "(XQuery)". For
instance, the following production describes FLWOR expressions
in XQuery.
[For/FLWOR] Expressions
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.
[For/FLWOR] Expressions
XQuery Core grammar productions describe the XQuery Core. The
Core grammar is given in [A Normalized core and formal grammars]. Core
productions are identified by a number, which corresponds to
their number in [A Normalized core and formal grammars], and are marked with
"(Core)". For instance, the following production
describes the simpler form of the "FLWOR"
expression in the XQuery Core.
Core FLWOR Expressions
The Formal Semantics manipulates "objects"
(values, types, expressions, etc.) for which there is no
existing grammar production in the [XQuery 1.0: An XML Query Language] 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.
Type Definitions
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 judgments (see the next section). As a
convenience, non-terminals used in judgments link to the
appropriate grammar production.
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
Object is a positive
integer
holds if the object Object is a positive
integer.
A judgment may hold (if it is true) or not hold (if it is
false). For instance '1 is a positive integer'
holds and '-1 is a positive integer' does not
hold.
Notation
Here are two other example judgments.
The judgment
holds if the expression Expr yields (or evaluates to)
the value Value.
The judgment
holds if the expression Expr has the type
Type.
Most other judgments used in this document are short
English sentences intended to reflect their meaning. For
instance, the judgment
holds if PrincipalNodeKind is the principal node kind
for the axis Axis.
A judgment can contain symbols and
patterns.
Symbols are purely syntactic and are used to write the
judgment itself. Symbols are chosen to reflect a judgment's
meaning, and are written in bold fonts. For example, 'is a
positive integer', '=>' and
':' are symbols, the second and third of which
should be read "yields", and "has
type" respectively.
Patterns are used to represent objects, constructed from a
given grammar production. In patterns, italicized words usually
correspond to non-terminals in the grammar. The name of those
non-terminals is significant, and may be instantiated only to an
"object" (a value, a type, an expression, etc.)
that can be substituted legally for that non-terminal. For
example, 'Expr' is a pattern that stands for every
[XPath/XQuery] expressions, 'Expr1 + Expr2' is a pattern
that stands for every addition expression, 'element a {
Value }' is a pattern that stands for every value in the
[XPath/XQuery] data model that is an 'a' element.
Non-terminals in a pattern may appear with subscripts
(e.g. Expr1, Expr2) to distinguish different instances
of the same sort of pattern. In some cases, non-terminals in a
pattern may have a name that is not exactly the name of that non
terminal, 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.
When instantiating 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
value '3' (on the right-hand side of the =>
symbol).
In some cases, inference rules may need to use
the fact that a certain judgment does not hold.
not(Judgment) holds
if andonly if Judgment does not hold.
In some cases, a pattern may be instantiated to
a value within a finite set of pre-determined values. We may
write that set of possible values using the in
judgment. For instance, the judgment
holds if the pattern Color has either the value
blue or the value green.
In some cases, a judgment may use the "=" sign
to indicate that a given value is equal to another value, or
that a pattern is equal to a given value. For instance, the
judgment
Color = blue
holds if the pattern Color has the value
blue.
An index to all the judgments used in this specification is
provided in [B Index of judgments].
2.1.3 Notations for environments
An environment component 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 component
or update it.
If "envComp" is an environment component, then
"envComp(symbol)" denotes the
"object" to which symbol is mapped.
The notation is intentionally similar to function application,
because an environment component can be considered a function
from the argument symbol to the
"object" to which the symbol is
mapped.
This document uses environments that group
related environment components. If "env" is an
environment containing the environment component
"envComp", that environment component is denoted
"env.envComp". The value that symbol
is mapped to in that environment component is denoted
"env.envComp(symbol)".
The two main environments used in the Formal Semantics are: a
dynamic environment (dynEnv), which models the [XPath/XQuery]
dynamic context, and a static environment (statEnv), which
models the [XPath/XQuery] static context. Both are defined in
[3.1 Expression Context].
For example, dynEnv.varValue denotes the dynamic environment
component that maps variables to values and
dynEnv.varValue(Variable) denotes the value of the variable
Variable in the dynamic context.
Environments 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 dynEnv,
the expression Expr yields the value Value.
Environments can be updated, using the following
notation:
"env + envComp(symbol =>
object) "
denotes the new environment that is identical to
env except that the environment component
envComp has been updated to map
symbol to object. The notation
symbol =>
object indicates that
symbol is mapped to object in
the new environment.
In case the environment component contains only a
constant value (e.g., the ordering mode which can only be
either ordered or unordered), the following notation is
used to set its value.
"env + envComp(
object
) ".
The following shorthand is also allowed:
"env + envComp(
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 + envComp(
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 component 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.
2.1.4 Notations for inference rules
Inference rules are used to specify how to infer whether a
given 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, as follows:
|
premise1
...
premisen
|
|
|
conclusion
|
All premises and the conclusion are judgments. From a logical
point of view, an inference rule is a deduction that if the
premises hold, then the conclusion holds as well. In that sense,
the previous inference rule has a similar meaning as the
following logical statement.
IF premise1
AND ...
AND premisen
THEN conclusion
Here is a simple example of inference rule, which uses
specific instances of the example judgment 'Expr
=> Value' from above:
|
$x => 0
3 => 3
|
|
|
$x + 3 => 3
|
This inference rule expresses the following property:
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. For
instance:
This inference rule expresses the following property:
evaluating the literal expression '3' always yields the value
'3'.
The two above rules are expressed in terms of specific
expressions and values, but usually rules are more abstract.
That is, the judgments are not fully instantiated. Here is a
rule that says that for any variable $VarName that yields
the integer value Integer, adding '0' yields the same
integer value:
|
$VarName => Integer
|
|
|
$VarName + 0 => Integer
|
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, in the context of a
particular instantiation of a rule, one can talk about
"the value of $VarName" instead of the value
bound to the first (second, etc) occurrence of
$VarName.
Here is an example of a rule occurring 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 sequence expression "Expr1 ,
Expr2" has the static type "Type1,
Type2", which is the sequence of types Type1
and Type2. Note that this 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.
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
statEnv. Finally, the type Type2 of Expr2 is
computed in that new environment.
In some cases, ellipses may be used in inference rules to
handle an arbitrary number of judgments. In those cases, some of
the patterns may have indices as subscript. If the same index is
used several times within the same rule, the number of judgment
in each case must be the same. For instance, the following rule
holds for any number of expressions, from Expr1 to
Exprn, with the same number of types Type1 to
Typen.
This inference rule is equivalent to having an unbounded
number of rules, the first of which has 1 judgment, the second
of which has 2 judgments, etc. For instance, the above rule
holds if and only if one of the following rules hold.
or
etc.
When ellipses are used, the value for the index always
ranges from 1 to an arbitrary number n.
2.1.5 Putting it together
In isolation, each inference rule describes a fragment of the
semantics for a given judgment. Put together, inference rules
describe possible inferences that can be used to decide whether
a particular judgment holds.
For a given judgment, if that judgment can be inferred to be
true by applying any sequence of inferences based on premises
which are known to be true, the inference succeeds. In most
cases, the inference will proceed by proving intermediate
judgments, following the consequences from one judgment to the
next by applying successive inference rules.
Such inference is a mechanism which can be used to describe
both static type analysis and dynamic evaluation. More
specifically, performing static typing consists in proving that
the following judgment holds for a given expression
Expr.
If the judgment holds for a given type Type, this type
is a possible static type for the expression. If there exists no
type for which this judgment holds, then static typing
fails and a static type error is returned to the user.
Consider the following expression.
Using the static typing rules given for expressions in the
rest of this document, one can deduce that the expression is of
type xs:integer through the following inference.
statEnv |- 1 : xs:integer (from typing of literals)
statEnv |- 2 : xs:integer (from typing of literals)
--------------------------------------------------- (sequence)
statEnv |- 1,2 : xs:integer, xs:integer
statEnv |- 3 : xs:integer
----------------------------------------------------- (sequence)
statEnv |- 1,2,3 : xs:integer, xs:integer, xs:integer
declare function fn:count($x as item()*) as xs:integer
statEnv |- xs:integer,xs:integer,xs:integer <: item()*
---------------------------------------------------------- (function call)
statEnv |- fn:count((1,2,3)) : xs:integer
Conversly, consider the following expression.
Using the static typing rules given for expressions in the rest
of this document, one can apply inference rules up to the
following point.
....
----------------------------------------------------- (sequence)
statEnv |- 1,2,3 : xs:integer, xs:integer, xs:integer
However, there is no rule that can infer the type of
fn:nilled((1,2,3)), because the static typing rules
for function calls will only hold if the type of the function
parameters is a subtype of the expected type. However, here
(xs:integer,xs:integer,xs:integer) is not a node
type, which is the expected type for the function
fn:nilled.
Note that in some cases, the inference can only proceed
through the appropriate changes to the environment. For
instance, consider the following expression.
let $x := 1 return ($x,$x)
Using the static typing rules given for expressions in the
rest of this document, one can deduce that the expression is of
type (xs:integer,xs:integer) through the following
inference.
statEnv0.varType = ()
-------------------------- (literal)
statEnv0 |- 1 : xs:integer
statEnv1 = statEnv0 + varType($x => xs:integer)
statEnv1.varType($x) = xs:integer
--------------------------------- (variable reference)
statEnv1 |- $x : xs:integer
statEnv1.varType($x) = xs:integer
--------------------------------- (variable reference)
statEnv1 |- $x : xs:integer
------------------------------------------- (sequence)
statEnv1 |- ($x,$x) : xs:integer,xs:integer
-------------------------------------------------------------- (let)
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.
2.3 XML Values
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.
2.3.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, 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], xs:untypedAtomic, or
xs: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
xs: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.
Values
Notation
In the production for AtomicValueContent, each symbol
in the right-hand side corresponds to one of the primitive
datatypes. For example, String corresponds to
xs:string, and Boolean corresponds to
xs:boolean. (The mapping is obvious, except that
"expanded-QName" corresponds to xs:QName) Although there are
no explicit productions for these symbols, we assume that each
is a non-terminal that derives a set of syntactic objects,
each of which corresponds to a value in the value space of the
corresponding datatype. For instance, the non-terminal
String derives a set of syntactic objects, which appear
in examples as "", "a",
"John", etc.; each one corresponds to a string
value in the xs:string value space. For familiarity, these
objects have been given the same appearance as
StringLiterals from the XQuery and Core grammars;
however, these are formal objects, with a distinct role in the
FS.
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 xs:untyped,
untyped attributes have the type annotationXQ xs:untypedAtomic, and untyped
atomic values have the type annotationXQ xs:untypedAtomic.
An element has an optional "nilled" marker. This
marker is present only 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.
2.3.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:untyped {
text { "The cat weighs " },
element weight of type xs:untyped {
attribute units of type xs:untypedAtomic {
"lbs" of type xs: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:untyped {
attribute xsi:type of type xs:untypedAtomic {
"xs:integer" of type xs: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
Before validation, this element is represented as:
element sizes of type xs: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
Before validation, this element is represented as:
element sizes of type xs: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
Before validation, this element is represented as:
element sizes of type xs:untyped {
attribute xsi:nil of type xs:untypedAtomic { "true" of type xs: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 xs: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
}
2.4 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.4.1 XML Schema and the [XPath/XQuery] Type System
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 [D 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.
2.4.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. 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.
Item Types
An element or attribute type has a name or wildcard, 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. "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 a union of the corresponding node types (e.g.,
element,attribute,text,comment and processing-instruction
nodes) and therefore do not appear in the grammar. The
semantics of sequence types is described in [3.5.4 SequenceType Matching].
Examples
The following is a text node type
The following is a type for all elements
element * of type xs:anyType
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
The following is a type for elements with anonymous type
fs:anon1:
element sizes of type fs:anon1
2.4.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 (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].
Types
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 two
sequences of items, Value1 and Value2, with
Value