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: 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].
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: A Query Language for XML]
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 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.
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: 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.
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 judgmentslink 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, and
written in bold fonts. 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. 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 usedto represent objects that can be
constructedfrom a given grammar production. In patterns,
italicizedwords correspond to non-terminals in the grammar.The
nameof those non-terminals is significant, and may be
instantiated only to an "object"(a value, a type,
anexpression, etc.) that can be
substitutedlegally for that
non-terminal. For example, 'Expr' is a pattern that stands
forevery [XPath/XQuery] expressions, 'Expr1 + Expr2'is a
patternthat standsfor every addition expression, 'element a {Value}'isa pattern that standsfor every value in the
[XPath/XQuery]data model that is an 'a' element.
Non-terminals in a patternmay appear with subscripts
(e.g. Expr1, Expr2) to distinguish different instances
of the same sort of pattern. Insome cases, non-terminals in a pattern may have a name that is not exactly the name of thatnon
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.
Wheninstantiatingthe
judgment, each pattern
mustbeinstantiated toan appropriate sort of
"object" (value,type, expression, etc). For
example,'3 =>
3'and'$x+0=> 3'
are bothinstances of the
judgment 'Expr
=> Value'. Notethatinthefirst
judgment,'3' corresponds toboththe expression '3' (on the
left-handside of the
=> symbol)and to the
value '3' (onthe right-handside of the
=>
symbol).
In some cases,inference rules may need to use
the factthat acertain judgment does not hold.
not( Judgment)holds
iffJudgmentdoes not hold.
Insome cases, a pattern may be instantiated to
avaluewithin a finite set of pre-determinedvalues. We may
writethat setof possiblevalues using the
in
judgment.For instance, the judgment
holdsif the patternColorhas either the value
blue
or the value green.
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 environmentsused in the Formal Semantics are: a
dynamic environment (dynEnv), which models the
[XPath/XQuery]'s dynamic context, and a static environment (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
component that maps variables to values and
dynEnv.varValue(Variable) denotes the value of the variable
Variable in the dynamic context.
Environmentsare 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.
Environmentscan 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 ornot. Inference rules express the logical
relationbetween judgments and describe how complex judgments
can be concluded from simpler premise judgments.
A logical inference ruleis 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.
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', thenthe 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 Variablethat yields
the integer value Integer, adding '0' yields the same
integer value:
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 value
bound to the first (second, etc) occurrence of VarRef.
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 sequenceexpression "Expr1 ,
Expr2" hasthe static type "Type1,
Type2", which is the sequence of types Type1
and Type2. Note that thisinference 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.
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 whetherthat a particular judgment hold.
For a given judgment, and a set of inference rules, if that
judgment can be inferred to betrue, the inference succeeds. In
mostcases, the inference will proceed by proving intermediatejudgments, following the consequences from one judgment to thenext by applying successiveinference rules.
Suchinference is a mechanism which can be used to describe
both statictype analysis and dynamic evaluation. Morespecifically, performing static typing consists in provingthat
thefollowingjudgmentholdsfor a givenexpression
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
restof this document, onecan 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 thatcan infer the type of
fn:nilled((1,2,3)), because the static typing rules
for function calls will only hold if the type ofthe 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 expectedtype for the function
fn:nilled.
Note that in some cases, the inference can only proceedthrough 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], 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.
Values
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 ispresent 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 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
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
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:
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
}
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 [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.
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 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 a union of thecorresponding node types (e.g.,
element,attribute,text,commentand 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 Value1matching Type1 and Value2 matchingType2. 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. The interleaved
product captures the semantics of all groups in XML
Schema, but is more general as 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.
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.
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.
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.4.4 Top level definitions
Top level definitions correspond to global element
declarations, global attribute declarations and type definitions
in XML Schema.
Type Definitions
A type definition has a name (possibly anonymous) and a type
derivation. In the case of a complex type, the derivation
indicates whether it is derived by extension or restriction, its
base type, and its content model, with an optional flag
indicating if it has mixed content.
Example
For instance, the following complex type
<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
};
Example
In the case of simple types derived by union or list, the
derivation is always a restriction from the base type
xs:anySimpleType, and has a content which is a union of the
member types, or a repetition of the item type. For instance, the two 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 as follows
define type listOfMyIntType restricts xs:anySimpleType {
myInteger*
}
define type zipUnion restricts xs:anySimpleType {
USState | FrenchRegion
}
Example
In the case of an atomic type, it just indicates its base
type. For instance, the following type definition
<xsd:simpleType name="SKU">
<xsd:restriction base="xsd:string">
<xsd:pattern value="\d{3}-[A-Z]{2}"/>
</xsd:restriction>
</xsd:simpleType>
is represented as follow
define type SKU restrict xsd:string;
Example
When the type derivation is omitted, the type derives by
restriction from xs:anyType. For instance:
define type Bib { element book* } =
define type Bib restricts xs:anyType { element book* }
Example
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 always have a name
and a reference to a (possibly anonymous) type. A global
element declaration also may declare a substitution group for
the element and whether the element is nillable.
Example
A type declaration with one element name of type
xs:string follows by one or more elements street of type
xs:string.
define type Address {
element name of type xs:string,
element street of type xs:string*
}
Example
A type declaration with complex content derived by
extension
define type USAddress extends Address {
element zip name of type xs:integer
}
Example
A type declaration with mixed content
define type Section mixed {
(element h1 of type xs:string |
element p of type xs:string |
element div of type Section)*
}
Example
A type declaration with simple content derived by
restriction
define type SKU restricts xs:string
Example
An element declaration
define element address of type Address
Example
An element declaration with a substitution
group
define element usaddress substitutes for address of type USAddress
Example
An element declaration which is nillable
define element zip nillable of type xs:integer
2.4.5 Example of a complete Schema
Here is a schema describing purchase orders from
[XML Schema Part 0].
<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>
Here is the mapping of the above schema into the [XPath/XQuery] type
system.
declare namespace xsd = "http://www.w3.org/2001/XMLSchema";
define element purchaseOrder of type 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 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 fs:anon1*
};
define type fs:anon1 {
element productName of type xsd:string,
element quantity of type fs:anon2,
element USPrice of type xsd:decimal,
element comment?,
element shipDate of type xsd:date?
};
define type fs:anon2 restricts xsd:positiveInteger;
define type SKU restrict xsd:string;
Note that the two anonymous types in the item
element declarations are mapping to types with names fs:anon1
and fs: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"/>
The above definitions are mapped into the [XPath/XQuery] type system as
follows:
define type NYCAddress extends USAddress {
element apt
}
define element apt of type fs:anon3
define type fs:anon3 restricts xsd:positiveInteger
define element usaddress substitutes for address of type USAddress
define element nycaddress substitutes for usaddress of type NYCAddress
2.5 Functions and operators
The [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; those functions are listed in
[B.1 Functions and Operators used in the Formal Semantics].
Many functions in the [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:unordered
returns its input sequence in an implementation-dependent
order. The signature of the fn:unordered function
takes arbitrary items as input and output:
fn:unordered($sourceSeq as item()*) as item()*
As defined, this signature provides little useful 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:unordered is applied on a sequence of
a elements, the result is also a sequence of
a elements.
In order to provide better static typing for those functions,
specific typing rules are given in [7 Additional Semantics of Functions].
