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