Last Call Comments for xquery-semantics.

XQuery 1.0 and XPath 2.0 Formal Semantics
W3C Working Draft 20 February 2004

4.1.5 Function Calls
Dynamic Evaluation
rule 2 (imported function)

The last premise is incorrect. It would re-evaluate the whole function
call in the imported module's environment. Instead, it should be more
like:
    dynEnv1 |- expanded-QName( Value1', ..., Valuen' ) => Value'

-Michael Dyck

XQuery 1.0 and XPath 2.0 Formal Semantics
W3C Working Draft 20 February 2004

The Formal grammar and the Core grammar both define the following
non-terminals:
    AttributeName
    ElementName
    ItemType
    TypeName

Because the inference rules use symbols from both the Formal and Core
languages, this would seem to cause an ambiguity. Now, it's true that
the Formal and Core definitions of AttributeName are the same (both
simply derive QName). Similarly for ElementName. And it's also true that
ItemType doesn't occur in the inference rules (though are you certain it
won't in a future draft?). But TypeName has different Formal and Core
definitions (Formal allows AnonymousTypeNames, Core doesn't), and it
does occur in the inference rules, so I think there is an ambiguity
there. But regardless of whether there is or isn't a formal ambiguity,
there's presumably the opportunity for confusion, which could be removed
simply by renaming some symbols.

(Note that, in addition to the above symbols, the Formal and *XQuery*
languages also both define AttributeValue. However, because the
appearance of XQuery constructs in inference rules is fairly limited, I
suppose an ambiguity does not arise. But again, it would reduce the
chance of confusion if you renamed one of them.)

-Michael Dyck

Dear FS Editors,

Below is a list of some possible issues with FS Feb 2004 Working
Draft, with occasional suggestions, ordered by FS sections.

Hopefully, it does not come too late to be useful...  My apologies if
there are too many already known issues and false alarms down there.

Sincerely,

Vladimir Gapeyev

------------------------------------------------------------------------


[General]

Shouldn't normative inference rules have formal identifiers by which they
can be referenced, similar to those of grammar productions?


[2.5.1 Namespaces, last para]

The term "host language" appears here and nowhere else in the spec!
Should it just say "language" or "XQuery or XPath"?


[3.1, just before 3.2]

The statement in this section that $fs:dot, $fs:position and $fs:last are
_built-in_ variables in FS is confusing when one considers their use
in the normalization rules of Section 4: One could assume that if the
variables are built-in they somehow magically contain appropriate
values whenever referenced.  However, the normalization rules treat
them as regular variables, by binding them in for and let expressions
whenever their value is changed -- no magic!

Suggestion:

Perhaps the def of these variables should be moved to Section 4 where
it would just say that they are special variables used in
normalization rules that are assumed to be distinct from any user
variables.  They are supposed to mimic the functionality of '.',
fn:position, fn:last, and this is achieved by careful formulation of
the normalization rules, no magic.

In light of this I wonder, if in addition to the rule
       [ . ] == $fs:dot
one also needs the rules
       [ fn:last() ] == $fs:last
       [ fn:position() ] == $position
?



[3.1, just before 3.2]

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

This appears to be at odds with the last para of 2.5.1 saying that
entities with fs prefix are abstract, introduced just for the purposes
of this spec and are not supposed to be provided in the host language.
So, under the 2.5.1 proviso, defining the fs prefix in a user query should
lead to absolutely no trouble!


[3.1.1 Static Context, last 2 para before 3.1.1.1]

These paragraphs define functions fs:active-ns and
fs:get_ns_from_items, which perhaps better be done in 6.1.

The descriptions of the functions aren't very clear...

[fs:active-ns] Perhaps should say "fs:active-ns(statEnv) returns all
prefix mappings from statEnv.namespace that are of 'active' kind."

[fs:get_ns_from_items]: The expanded-QName and URI appear in the def
from nowhere and their role is unclear!  It also should say that the
return are prefix-to-namespace mappings with kind indication, not just
namespaces.


[4.2 Path Expressions, just before 4.2.1]

It appears that according to the spec the last normalization rule,
the one for [ StepExpr1 "/" StepExpr2 ]_Expr is supposed to handle all
"seminormalized" path expressions of the form StepExpr1 / StepExpr2 /
.... / StepExpr_n.

However, RelativePathExpr is defined as
[71 (XQuery)] RelativePathExpr ::= StepExpr (("/" | "//") StepExpr)*,
i.e. it can contain one or more StepExpr, while the rule in question
handles the case of exactly two.

Perhaps this can be fixed just by changing StepExpr2 to
RelativePathExpr in the rule.


[4.2 Path Expressions]

It is said in "Core Grammar" section: "The grammar for path
expressions in the Core starts with the StepExpr production".
According to the productions [52,58,59(Core)] in 4.2.1. it should be
rather said "starts with AxisStep production".


[4.2.1 Steps -- Dynamic Evaluation, also Static Type Analysis]

The eval rule for the judgment dynEnv |- Axis NodeTest => Value refers
to the variable $fs:dot.  Somehow it does not feel right to make the
Core semantics depend on the name of an auxiliary variable, especially
if one takes the position (see also comments for [3.1]) that $fs:dot
is a usual Core variable, albeit introduced for special purposes
during normalization.

Suggestion:

Extend the Core syntax to contain an explicit step application
construct.  In more detail:

(1) Introduce an expression form Expr / AxisStep (or PrimaryExpr /
AxisStep, or even $Var / AxisStep -- if more restrictive syntax is
desired).  The semantics is that Expr evaluates to a single node (to
be checked by the type system) which is an explicit context node for
AxisStep.  [Of course, if the use of "/" is objectionable, the syntax
can be different.]

(2) Modify the single-step normalization rules to read:
     [ ForwardStep ]_Expr == $fs:dot / [ ForwardStep ]_Axis

(3) Now, the above evaluation rule would look like

  dynEnv |- Expr => Value1
  <-- the rest of clauses unchanged -->
----------------------------------------------------------------
  dynEnv |- Expr / Axis NodeTest => fs:distinct-doc-order(Value3)



[4.2.1.1, Axes]

The text and normalization rules indicate that
preceding/following(-sibling) axes are not on the Core, but the
grammar rules [(Core) 60,61] still contain them. (Also in Appendix
A.1)


[4.2.1.1, Axes]  For ForwardAxis, the grammar [91(XQuery)] does not define
namespace:: axis, while [60 (Core)] does!  Consequently, the normalization
rule that follows normalizes from non-existing syntax.

[This could be a problem with XQuery, rather than FS spec, since XQ
Datamodel does define the kind of namespace nodes.  On the other hand, if
namespace:: is to be removed from FS, it currently also appears in
[7.2.1, Principal Node Kinds]

There is also cross-spec-numbering discrepancy: FS [91(XQuery)] is
XQuery[89]


[4.2.1.1] The normalization rules for sibling axes are given as follows:

[following-sibling:: NodeTest]_Axis
==
[let $e := . in parent::node()/child:: NodeTest [.<<$e]]_Expr

[preceding-sibling:: NodeTest]_Axis
==
[let $e := . in parent::node()/child:: NodeTest [.>>$e]]_Expr

I think their bodies should be swapped!  E.g., in the 1st, if I get it
right, in [.<<$e] predicate, $e refers to the original node and . ranges
over all siblings, so the predicate is true for siblings that _precede_
$e.

Also, it could make sense to be a notch more explicit by writing
[following-sibling:: NodeTest]_Axis
==
[let $e := . in $e/parent::node()/child:: NodeTest [.>>$e]]_Expr
                ^^

[4.3.2 Filter Expressions]

Subsection "Core Grammar" should be renamed "Normalization".


[4.7.3.1. Computed Element Constructors, both Dynamic Evaluation rules]

In extended static environments statEnv_1, ... , statEnv_n, there are
missing indexes in NCName, should be NCName_1 .... NCName_n


[5. Modules and Prologs, Intro]

It says: "Namespace declarations and schema imports always precede
function definitions, as specified by the following grammar
productions."  However, the production [33 (XQuery)] Prolog allows to
intermix them freely.


[5.8 Schema import]

In the rule:

statEnv |- Definition* =>type statEnv1
statEnv1 |- Definition1 =>type statEnv2
---------------------------------------
Definition1 Definition* =>type statEnv2

--- input statEnv is missing in the conclusion


[5.8 Schema Import]
(Also see comments for [F] below.)

I am afraid the schema importing formalization in [5.8] and [F] is not
robust w.r.t. namespace prefix bindings possibly defined in the
imported schema.  Namely, the import is formalized by the rule

[schema String (at String)?]_Schema
statEnv |- Definition* =>type statEnv1
-------------------------------------------------------------
statEnv |- import schema String (at String)? =>stat statEnv1

and a representative rule for the second judgment above the line is

statEnv |- TypeName of elem/type expands to expanded-QName
statEnv1 = statEnv +
            typeDefn(expanded-QName => define type TypeName TypeDerivation
)
----------------------------------------------------------------------------
statEnv |- define type TypeName TypeDerivation =>type statEnv1

where statEnv maps a resolved expanded-QName of TypeName to a
definition containing unresolved TypeName and where TypeDerivation can
contain other unresolved Qnames (see current defs in [F]).  But, even
though TypeName is supposed to reside in the target namespace of the
imported schema, statEnv may lack a prefix mapping necessary for
resolving it into expanded-QName, since the first rule above does not
add it by default!  (And even if the version of the import statement
is used that binds schema's namespace to a prefix, this prefix can
only coincidentally be the same as the one in TypeName.)  Moreover, if
the schema defined other prefixes (e.g. for namespaces of the imported
schemas), they can occur in TypeDerivation, and there is no provision
in the current formalization for them to get into statEnv.

I can see two possible approaches for cleaning this up:

(1) Specify that schema import, in addition to Definitions (with
    unresolved QNames), also returns a set of prefix-to-namespace
    bindings that can now be incorporated into statEnv.

(2) Specify that the definitions returned by schema import actually
    contain only resolved QNames.

The obvious (killer?) shortcoming of (1) is that it implicitly
introduces prefixes that explicitly appear only in the schema and can
even shadow earlier prefixes defined by the query programmer.

Approach (2) appears to be more sound, although it would require
significant changes to the specification, at least:

  - Definitions productions in [2.3.4] need to be duplicated to
    similar defs that refer only to resolved QNames.  (Although, since
    those productions describe entities not available in the source
    language, maybe the modified version is the only one that is
    needed?)

  - statEnv needs to be modified to contain definitions with
    _resolved_ names.


[6.1 Formal Semantics Functions]

Here is a summary list of fs-prefixed functions that appear throughout
the spec but do not have subsections in 6.1, which is perhaps an
unintended omission:

fs:active-ns, fs:get_ns_from_items, fs:count, fs:is-same-node,
fs:node-before, fs:node-after, fs:local-variables, fs:local-functions


[7.1.9 Type expansion]

(1) The inference rule given here is for the case when type TypeName
    is defined by extension.  There must be another one for s
    derivation by restriction.

(2) The inference rule contains the judgment

   statEnv |- Type2 is Type1 extended with union interpretation of
TypeName

where Type1 is defined in the previous judgment to be the extension
fragment that TypeName's extension adds to the type BaseTypeName.
I believe, however, Type1 should be the concatenation of
BaseTypeName's definition and TypeName's extension fragment.

Suggestion:

It might help to obtain Type1 as the result of the following "derives"
judgment:
           statEnv |- TypeName derives Type
which produces the type model for TypeName that composes the effects
of all type derivations on the path from the root of the type
hierarchy down to TypeName.

Rules(still need to be tinkered with to handle Mixed? correctly):

statEnv |- TypeName of elem/type expands to expanded-QName
statEnv.typeDefn(expanded-QName) =>
          define type TypeName extends BaseTypeName Mixed? { Type0? }
statEnv |- BaseTypeName derives BaseType
   Type = BaseType, Type0
----------------------------------------------------------------------
 statEnv |- TypeName derives Type

statEnv |- TypeName of elem/type expands to expanded-QName
statEnv.typeDefn(expanded-QName) =>
          define type TypeName restricts BaseTypeName Mixed? { Type0? }
statEnv |- BaseTypeName derives BaseType
   <<? affirm that Type0 is a subtype of BaseType  ?>>
   Type = Type0
----------------------------------------------------------------------
 statEnv |- TypeName derives Type

Note that using these two rules would automatically resolve the issue
(1) above.


[7.1.10 Union interpretation of derived types]

The inference rule should contain the judgment to obtain
expanded-QName from TypeName0.


[7.2.2.2 Dynamic semantics of axes]

In most rules, the judgments are written like
     dynEnv |- axis Axis child:: of NodeValue => Value1
                    ^^^^
--- "Axis" should be dropped.


[A. Normalized core grammar]

There seems to be quite a few unreachable non-terminals in the grammar:

- QuantifiedExpr [43 (Core)] -- perhaps it should be mentioned in [34
  (Core)] for ExprSingle

- OrderByClause [39 (Core)] -- Perhaps it should appear in [35 (Core)]
   production for FLWORExp

- PrimaryExpr [53 (Core)] -- perhaps should appear in [51 (Core)] for
  ValueExpr

- ComputedConstructor [57 (Core)] -- perhaps should appear in
  PrimaryExpr [53 (Core)]


[F.2 Schemas as a whole]

The rule
    [Pragma]pragma(targetNCName) == Definition*
in [F.2.1] for, presumably, handling Schema's "include" | "import" |
"redefine" features, does not make sense: its rhs comes from nowhere!

On the other hand, [F.2.2-4] say that handling of "include" | "import"
| "redefine" is not specified in this document since it is assumed to
be handled by the XML Schema processor.

Suggestion:

Perhaps [F.2] should just say that the helper function
open-schema-document(SchemaName) encapsulates the functionality of a
Schema processor, which is assumed to handle "include" | "import" |
"redefine" features.  I.e., the result of
open-schema-document(SchemaName) is described by Content production
[(56) Formal].

Then there is no need for [Pragma]_pragma rule, and Schema mapping
 rules at the end of [F.2.1.] should be

   [schema SchemaName (at SchemaNamespace)?]_Schema
        ==
   [open-schema-document(SchemaName,
SchemaNamespace)]_definition(targetNCName)


[F.2 Schemas as a whole]

This section mentions targetURI (that comes from the imported schema)
and targetNCName (that parameterizes all the mapping rules), which are
supposedly related, but the relationship is nowhere spelled out.

Also, in the presence of Schema <import> and relatives, there can be
multiple target URIs...

Perhaps a good way to tackle both difficulties would be to say that
open-schema-document() is also assumed to resolve all QNames defined
and referenced in the imported schema.  The mapping rules in the rest
of the section then refer to the fully resolved names and don't need to
be parameterized by targetNCName.


[F.7, F.8 Attribute and model group definitions]

These sections say that the corresponding features are not handled by the
mapping, and refer to Issue 501 (FS-Issue-0158).  But the Issues document
marks the issue as resolved!

This is a resend of the submission I made a couple days ago:

I have added a unique identifier for each comment, and fixed a few typos
of my own.

Also, I forgot to mention that most if not all of these comments are
editorial.
---------------------

XQuery 1.0 and XPath 2.0 Formal Semantics
W3C Working Draft 20 February 2004


Lines beginning with '%' uniquely identify each comment.
Lines beginning with '#' are quotes from the spec.
Lines beginning with '>' are suggested replacement text.

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

TRANS-SECTION COMMENTS

% 001
'not' in judgments:
Note that there are no inference rules that tell us how to conclude
that a judgment involving 'not' holds, so presumably you must explain
how to do so.
I suspect this will be easier if you change occurrences of
#   env |- not( something )
to
 >   not( env |- something )
________

% 002
When a double-quoted symbol appears in the EBNF, the symbol should
appear without the quotes when in occurs in an inference rule or
mapping rule. For the most part, the spec adheres to this, but it
occasionally lapses. In particular, when the following quoted symbols
appear in rules, the quotes should probably be removed.
     "element"
     "attribute"
     "lax"
     "strict"
     "skip"
     "/"
________

% 003
# Object in { a, b, ... }
The 'in' and braces are meta-syntactic, so they should be bolded.
Or prehaps better would be to rewrite it as
 > Object = a or Object = b or ...
(with bold 'or's).
________

% 004
# statEnv |- statEnv.mem(a) ...
The "statEnv |-" is redundant, delete it.
 > statEnv.mem(a) ...
________

% 005
# Type <: Type
All '<:' judgments should start with 'statEnv |-'
________

% 006
# Value matches Type
All 'matches' judgments should start with 'statEnv |-'.
________

% 007
# VarRef of var expands to Variable
Change to:
 > VarRef = $ VarName
 > VarName of var expands to Variable
________

% 008
# Variable
Not defined. Change to 'expanded-QName'?
________

% 009
# Value
Sometimes a Value (or more specifically, a pattern whose name is a
symbol deriveable from Value) will appear where an Expr is allowed.
This seems kind of sloppy.
________

% 010
# String
As a specific case of the preceding, most occurrences of 'String' in
the rules should probably be 'StringLiteral'.
________

% 011
# . . .
Change to:
 > ...
________

% 012
# fn:local-name-from-QName
Change to:
 > fn:get-local-name-from-QName
________

% 013
# fn:namespace-uri-from-QName
Change to:
 > fn:get-namespace-uri-from-QName

% 014
Also, all uses of the function are of the form:
# fn:namespace-uri-from-QName( ... ) = statEnv.namespace(...)
but this is malformed: the LHS is a URI, but the RHS is a
(namespace-kind, URI) pair.

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

SECTION-SPECIFIC COMMENTS

Abbreviations:
"Sem"  = "Semantics"
"SCP"  = "Static Context Processing"
"STA"  = "Static Type Analysis"
"DCP"  = "Dynamic Context Processing"
"DEv"  = "Dynamic Evaluation"
"DErr" = "Dynamic Errors"
"LHS"  = "left-hand side"  (or "above the '=='" in mapping rules)
"RHS"  = "right-hand side" (or "below the '=='" in mapping rules)

To identify a particular premise of an inference rule, I give its
position (e.g. "premise 3"). In counting, I skip any premise that is
merely an ellipsis.

------------------------------------------------------------------------
2.1.2 Notations for judgments

% 015
# Symbols are purely syntactic and are used to write the judgment
# itself.
There are actually (at least) two kinds of symbols, which you might call
"base-syntactic" and "meta-syntactic". Base-syntactic symbols arise
from the EBNF grammar. Meta-syntactic symbols arise from the "judgment
declarations" in Notation sections. Because a judgment can combine both
kinds of symbols, it's important to be able to distinguish them.
Usually, base-syntactic symbols are presented in normal typeface,
whereas meta-syntactic symbols are presented in boldface.  However,
sometimes they aren't. It would be good if the spec were consistent.
In particular, add bold to:
     =>
     |-
     : (Unless it's the colon in a QName or Wildcard.)
     = (Except a few cases, e.g. "namespace foo =".)
     fn:local-name-from-QName()
     fn:namespace-uri-from-QName()
________

% 016
# Patterns are written with italicized words.

Do you have a reference for this terminology?  "Pattern" sounds like the
wrong word to me. A regular expression is a pattern. The RHS of an EBNF
production is a pattern. Even a judgment is a form of pattern. But a
name is not a pattern.  Personally, I'd call it a metavariable.
________

% 017
# By convention, all patterns in the Formal Semantics correspond to
# grammar non-terminals, and are used to represent entities that can be
# constructed through application of the corresponding grammar
# production. ...
# In a few cases, patterns may have a name that is not exactly the name
# of a grammar production but is based on it.

Then there some other cases, where the pattern name isn't a grammar
non-terminal or a slight modification of one:
     AttributeAll
     Error
     URI-or-EmptyNamespace
     Variable  (replace with expanded-QName?)

------------------------------------------------------------------------
2.1.3 Notations for inference rules

% 018
Note:
# In effect, inference rules are just a notation that describes a
# bottom-up algorithm.

They don't necessarily describe an algorithm, because the precedure
might not terminate. Also note (as in 7.3.1) that the rules do not
necessarily give a simple means to compute a result.

Moreover, I wouldn't say the procedure is bottom-up, because types
and values can't bubble up the tree until environments have bubbled
down.

------------------------------------------------------------------------
2.1.4 Notations for environments

% 019
para 4
# This document uses environment groups that group related environments.

I think you'd be better off if you changed your terminology somewhat:
Instead of saying that statEnv and dynEnv are "environment groups"
whose members are "environments", say that statEnv and dynEnv are
"environments", whose members may be "mappings" (or "dictionaries", if
you like). Note that after section 3, statEnv and dynEnv *are* generally
referred to as "environments".)
________

% 020
para 4
# If "env" is an environment group with the member "mem", then that
# environment is denoted "env.mem" and the value that it maps symbol to
# is denoted "env.mem(symbol)".

Note that this ignores members that are not mappings/dictionaries.
________

% 021
para 4
# the value that it maps symbol to is denoted "env.mem(symbol)".

So should one say
# env.mem(a) = b
or
# env.mem(a) => b
? The first, I think. There are about 20 occurrences of the second form,
which should be changed to the first.
________

% 022
Updating
# If the "object" is a type then the following notation relates a symbol
# to a type: "env + mem(symbol : object) ".
I think it would be better to keep the environment notation more
self-consistent, and use '=>' in this case too.

------------------------------------------------------------------------
2.1.5 Putting it together

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

You should at least talk about how attempting to prove a premise in one
rule involves finding another rule with a matching conclusion (for some
definition of the word "matching"), instantiating (some of) its
patterns, and then trying to prove that conclusion.

------------------------------------------------------------------------
2.2.1 Formal Values

% 024
Grammar
# [26 (Formal)]  AtomicValue
# [16 (Formal)]  ElementValue
# [17 (Formal)]  AttributeValue
Looking at some of the inference rules, it seems that a TypeAnnotation
is optional (or can be empty).
E.g., 7.2.4 / Sem / rule 2 / premise 3:
# Value3 = attribute QName { SimpleValue }
________

% 025
Grammar
# [16 (Formal)]  ElementValue
Looking at the inference rules, it seems that the
# "{" NamespaceAnnotations ")"
part is optional.
________

% 026
Grammar
# [22 (Formal)]  NamespaceAnnotations =
# NamespaceAnnotation ... NamespaceAnnotation
This is sloppy. Change to
 > NamespaceAnnotation ( "," NamespaceAnnotation )*

------------------------------------------------------------------------
2.3.3 Content models

% 027
Grammar
# [28 (Formal)]  Type
This production leads to a fairly ambiguous grammar. I realize that this
is common practice when defining the domains for a formal semantics, but
the specification includes lots of examples of "serialized" Types, and
it might be useful if these were parseable. I suggest that any use of a
type "operator" must be parenthesized:
 > Type ::= ItemType
 >          | Type Occurrence
 >          | "(" Type ( "&" Type )+ ")"
 >          | "(" Type ( "," Type )+ ")"
 >          | "(" Type ( "|" Type )+ ")"
 >          | "empty"
 >          | "none"

------------------------------------------------------------------------
2.3.4 Top level definitions

% 028
Grammar
# [39 (Formal)] ComplexTypeDerivation ::= ... Mixed?
# [35 (Formal)] TypeSpecifier ::= Nillable? ...
# [44 (Formal)] Definition ::= ... Substitution? Nillable?

The symbol '?' is both base-syntactic (to denote a zero-or-one type) and
meta-syntactic (to denote an optional [base-syntactic] phrase). It's
sometimes difficult to tell which kind each is. They should at least be
easily distinguishable. But the meta-syntactic '?' complicates the
matching of premises to conclusions (in other rules), so I think things
would be even better if meta-syntactic '?' were eliminated.

For example, consider the symbol 'Mixed'. In the grammar, and in the
inference rules, it always occurs followed by a '?'. So replace
occurrences (in the grammar and inference rules) of 'Mixed?' with a
new symbol, say 'MixedOption', and replace the production
# Mixed ::= "mixed"
with
 > MixedOption ::= "mixed"?
or
 > MixedOption ::= | "mixed"
I believe these symbols can be handled this way:
     Derivation
     Mixed
     Nillable
     PositionalVar
     Substitution
     TypeDeclaration

When the symbol sometimes occurs with the '?' and sometimes without,
you proceed as above, except that the production for the new symbol
augments rather than replaces the original production. E.g., replace
occurrences of 'ElementName?' with 'ElementNameOption', keep the
'ElementName' production, and add the production
 > ElementNameOption ::= ElementName?
Some symbols that can be handled this way:
     AttributeName
     ElementName
     TypeSpecifier
     ValidationMode

------------------------------------------------------------------------
2.4.1 Processing model

% 029
# Static analysis is further divided into four sub-phases. Each phase
# consumes the result of the previous phase and generates output for
# the next phase. ...
# Static analysis consists of the following sub-phases
# 1. Parsing
# 2. Static Context Processing
# 3. Normalization
# 4. Static type analysis

In fact, as section 5 tells us, some Normalization happens as part of
SCP, and some as part of STA.  And SCP happens as part of STA. So
"sub-phases" 2, 3, and 4 are not as assembly-line as you indicate.

------------------------------------------------------------------------
------------------------------------------------------------------------
3.1.1 Static Context

% 030
statEnv.docType:
# corresopnds
Change to "corresponds".
________

% 031
statEnv.namespace
# The namespace environment maps a namespace prefix (NCName) onto a
# namespace kind and a namespace URI (URI) or the empty namespace
# (#EMPTY-NAMESPACE).

How does a prefix get mapped to #EMPTY-NAMESPACE?

------------------------------------------------------------------------
3.1.1.1 Resolving QNames to Expanded QNames

% 032
para 1
# Element and type QNames may be in the empty namespace,

I looked in
-- the 'Namespaces in XML' spec,
-- the 'XQuery Data Model' spec, and
-- the 'XQuery Language' spec,
and as far as I can see, none of them support the term "the empty
namespace". Moreover, QNames aren't in namespaces, NCNames are.

# that is, there is no URI associated with their namespace prefix.

I don't think you mean this. If an element or type QName has a namespace
prefix, then it will match the first rule in the Semantics section (with
the prefix bound to NCName1). If there's no URI associated with the
prefix, then statEnv.namespace(NCName1) will fail, and you'll get a
static error. If you really wanted the stated behaviour, you'd need this
rule:
 > statEnv.namespace(NCName1) undefined
 > -------------------------------------
 > statEnv |- NCName1:NCName2 of elem/type expands to
 >                                             (#EMPTY-NAMESPACE,NCName2)
But I don't think you want that.

Instead, the rules that involve #EMPTY-NAMESPACE appear to be using it
to handle names that belong to no namespace. If that's what you mean,
then change your terminology. And change '#EMPTY-NAMESPACE' to
'#NO-NAMESPACE-URI' or something.
________

% 033
Notation
# statEnv |- QName of elem/type expands to expanded-QName
Some occurrences of this judgment-form have 'TypeName' in the 'QName'
position.  But TypeName derives both QName and AnonymousTypeName.  In
cases where the TypeName is an AnonymousTypeName, it will be able to
match the conclusion of any rule. Which means that the '=>type' judgment
does not hold for definitions of anon types, which means that schema
import doesn't work.

Possible fix: Split this judgment-form into two, one for 'elem' and one
for 'type', and then in the latter, change 'QName' to 'TypeName'.  Then
add a rule for 'AnonymousTypeName of type expands to'.
________

% 034
Sem / rule 1,3 / premise 1
# statEnv.namespace(NCName1) = URI-or-EmptyNamespace

Section 3.1.1 tells us that statEnv.namespace maps an NCName to a pair
consisting of a namespace kind (passive/active) and a namespace URI (or
#EMPTY-NAMESPACE). Thus the judgment should be:
 > statEnv.namespace(NCName1) = (NamespaceKind, URI-or-EmptyNamespace)
________

% 035
Sem / rule 5,7 / premise 1
# statEnv.namespace(NCName1) = URI
Ditto above.
 > statEnv.namespace(NCName1) = (NamespaceKind, URI)

------------------------------------------------------------------------
3.1.2

% 036
dynEnv.funcDefn
# The initial function environment (statEnvDefault.funcDefn) ...
Change 'statEnvDefault' to 'dynEnvDefault'.
________

% 037
dynEnv.docValue:
# corresopnds
Change to "corresponds".

------------------------------------------------------------------------
3.4.4 SequenceType Matching

% 038
Normalization / rule 19, 25 / LHS

Each of these rules appears to have a judgment thrown in before the '=='
sign. This should presumably be explained, or else notated differently.

------------------------------------------------------------------------
3.5.2 Handling Dynamic Errors

% 039
rule 1
I realize this rule is only supposed to specify the default behaviour,
but how do you prevent it from being true in the non-default cases?
________

% 040
rules 2, 3
You're using what appears to be formal notation to convey an informal
rule, which is unwise.

For any given statEnv, you can always find some binding for 'symbol' and
'component' such that the lookup fails, so the premise always holds, so
every expression raises statError and dynError.

------------------------------------------------------------------------
------------------------------------------------------------------------
4.1.1 Literals

% 041
all rules
Occurrences of 'IntegerLiteral', 'DecimalLiteral', 'DoubleLiteral',
'StringLiteral' should be italicized
________

% 042
3rd DEv / rule 1 / conclusion
# dynEnv |- DoubleLiteral => xs:double(DoubleLiteral)
'=>' should be bold
________

% 043
4th DEv / rule 1 / conclusion
# dynEnv |- StringLiteral => xs:string(StringLiteral)
'=>' should be bold.

------------------------------------------------------------------------
4.1.2 Variable References

% 044
DEv / rule 1,2 / premise 1
# dynEnv |- VarName of var expands to expanded-QName
Change 'dynEnv' to 'statEnv'.
________

% 045
DEv / rule 2 / premise 4
# dynEnv1 |- $ VarName => Value
The '1' should be a subscript.

------------------------------------------------------------------------
4.1.5 Function Calls

% 046
Notation / rule 1 / RHS
Change 'Expr' to '[ Expr ]_Expr'.
(Or you could do it in the Normalization rule, but it's easier here.)
________

% 047
Normalization / rule 2
# QName ( A1, ..., An) )
Delete extra right-paren
________

% 048
STA / rule 1 / premise 2
# statEnv |- Expr1 : Type1 ... Exprn : Typen
This is structured as a single premise but should presumably be two plus
an ellipsis-premise.
________

% 049
STA / rule 3 / premise 1,2
# not(Typex = (...)
Occurrences of 'not' should be in bold.
________

% 050
STA / rule 3 / premise 1,2
# not(Typex = (...)
Append a right paren.
________

% 051
STA / rule 3 / premise 7,8
# Type1' can be promoted to Type1''
Prepend 'statEnv |-'
________

% 052
STA+DEv+DErr
Occurrences of 'FuncDecl' should be italicized.
Also, there should be a Formal EBNF production for FuncDecl.
________

% 053
DEv / rule 1
Several of the premises refer to statEnv, but the conclusion doesn't.
(This happens with lots of the DEv rules in the spec.) Theoretically,
this would allow the inference engine to fabricate any statEnv that
satisfied the premises.  But presumably, want the same statEnv that the
FunctionCall "received" during STA.  This needs to be explained, and
possibly denoted somehow.
________

% 054
DEv / rule 1,2,3 / premise 4
DErr / rule 3,4 / premise 4
# dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen
This is structured as a single premise but should presumably be two plus
an ellipsis-premise.
________

% 055
DEv / rule 1 / premise 8
# dynEnvDefault = ( ... ) ] |-
Change to
 > dynEnvDefault + varValue( ...) |-
In addition to the obvious changes, note the deletion of right-bracket.
________

% 056
DErr / rule 2 / premise 3
# FuncDeclj = define function expanded-QName(Type1, ..., Typen) as Type
# for all 1 <= j <= m
This appears to require that all signatures for a given func name be
identical. Put j subscripts on the 'Type' patterns.
________

% 057
DErr / rule 3 / premise 9
# dynEnv [ varValue = (...) ] |-
Change to
 > dynEnv + varValue(...) |-

------------------------------------------------------------------------
4.2.1 Steps

% 058
STA / rule 1 / premise 2
# Type1 <: node
DEv / rule 1 / premise 2
# Value1 matches node

'node' does not appear to be a valid Type.  If you meant 'node()',
that's still not a valid (Formal) Type, though it is a valid (XQuery)
ItemType.
________

% 059
STA / rule 1 / premise 3, 4, conclusion
DEv / rule 1 / premise 3, 4, conclusion
Occurrences of 'Axis' should be italicized.
________

% 060
STA / rule 1 / premise 4, 5
DEv / rule 1 / premise 4, 5
Occurrences of 'PrincipalNodeKind' should be italicized.
________

% 061
DErr / rule 1 / conclusion
# dynEnv.varValue |- ...
Delete '.varValue'.

------------------------------------------------------------------------
4.2.1.2 Node Tests

% 062
Grammar
# [95 (XQuery)] Wildcard ::= "*" | (NCName ":" "*") | ("*" ":" NCName)
# [64 (Core)]   Wildcard ::=
Change occurrences of 'NCName' to 'Prefix' and 'LocalPart' respectively,
or 'Wildcard' won't match patterns that use those names.

------------------------------------------------------------------------
4.3.1 Constructing Sequences

% 063
Normalization, STA, DEv
Change occurrences of 'Expr' to 'ExprSingle'.

------------------------------------------------------------------------
4.6 Logical Expressions

% 064
Normalization, STA, DEv, DErr
Change occurrences of 'Expr' to 'AndExpr' or 'ComparisonExpr' as
appropriate.

------------------------------------------------------------------------
4.7.1 Direct Element Constructors

% 065
Grammar
# [26 (XQuery)]  ElementContentChar ::=  Char - [{}<&] - [{}<&]
# [27 (XQuery)]  QuotAttContentChar ::=  Char - ["{}<&] - ["{}<&]
# [28 (XQuery)]  AposAttContentChar ::=  Char - ['{}<&] - ['{}<&]
In each case, eliminate the repetition.

------------------------------------------------------------------------
4.7.3.1 Computed Element Constructors

% 066
Often, this section does not recognize that the 'content expression' of
a CompElemConstructor is not an Expr but a CompElemBody.  So anything of
the form:
# element QName { Expr }
should be changed to
 > element QName { CompElemBody }
and the changes propagated (i.e., the rules made to handle
CompElemNamespaces).
________

% 067
STA / rules 2,3,4 / premise 1
# statEnv |- QName in context ...
This judgment matches both
# statEnv |- ElementName? in context ...
declared in 7.6.2, and
# statEnv |- AttributeName? in context ...
declared in 7.6.3. Is this intentional? Maybe the judgment-forms should
be distinct (add an 'elem' or 'attr' keyword in bold).
________

% 068
STA / rule 2 / premise 5
# ValidationContext1 = statEnv.validationContext "/" QName
The slash should not be in quotes.
Even so, I can't parse the premise, because ValidationContext/QName
doesn't fit the EBNF for ValidationContext.
________

% 069
DEv / rule 1 / premise 1, conclusion
# Expr = CompElemNamespace1, ..., CompElemNamespacen, (Expr0)
DEv / rule 2 / premise 3
# Expr2 = CompElemNamespace1, ..., CompElemNamespacen, (Expr3)

The equation is invalid; an Expr cannot match the RHS. The LHS should be
a CompElemBody.
________

% 070
DEv / rule 1 / premise 2,3
DEv / rule 2 / premise 4,5
# CompElemNamespace = namespace NCName { URI }
The EBNF for a CompElemNamespace says that the NCName can be omitted,
but these jusgments don't allow for that.
________

% 071
DEv / rule 1 / premise 6
# statEnvn, dynEnv |- ...
It's not clear what the notation means.
________

% 072
DEv / rule 1 / premise 8
DEv / rule 2 / premise 10
# NamespaceAnnotations = (CompElemNamespace1, ... CompElemNamespacen,
Delete parens, or else change the EBNF for NamespaceAnnotations to
require/allow parens.
Also, put a comma after the ellipsis
________

% 073
DEv / rule 1,2 / last premise
# element   QName    of type xs:anyType { Value0 } { NSAnnotations }
# element { Value0 } of type xs:anyType { Value1 } { NSAnnotations }
These are meant to be ElementValues, but:
(a) the context allows an Expr, not an ElementValue, and
(b) (for rule 2) the element-name must be a QName, not computed.
________

% 074
DEv / rule 1,2 / conclusion
# statEnv dynEnv |-
Insert comma, presumably.
________

% 075
DEv / rule 2 / premise 8
# fs:item-sequence-to-node-sequence (Expr3); => Value
Delete semicolon.

------------------------------------------------------------------------
4.7.3.2 Computed Attribute Constructors

% 076
STA / rules 2, 3 / premise 1
# statEnv |- QName in context ...
As in 4.7.3.1, this matches both judgment-forms
# statEnv |- ElementName in context ...
# statEnv |- AttributeName in context ...
________

% 077
DEv / rule 1 / conclusion
# attribute expanded-QName of type xdt:untypedAtomic { Value }
EBNF for AttributeValue says QName, not expanded-QName, and
SimpleValue, not Value.
________

% 078
DEv / rule 2
Change 'Expr' to 'Expr1' or 'Expr2' as appropriate.
________

% 079
DEv / rule 2 / conclusion
# attribute { Value0 } of type xdt:untypedAtomic { Value }
Where you have "{ Value0 }", AttributeValue only allows QName.
________

% 080
DErr / rule 3 / premise 1
# statEnv.statEnv
Delete 'statEnv.'

------------------------------------------------------------------------
4.7.3.3 Document Node Constructors

% 081
DEv, DErr / all rules
# dynEnv |- Value matches Type
Change 'dynEnv' to 'statEnv', according to 7.3.1.

------------------------------------------------------------------------
4.7.3.4 TextNodesConstructors

% 082
DEv, DErr / all rules
# dynEnv |- Value matches Type
Change 'dynEnv' to 'statEnv', according to 7.3.1.

------------------------------------------------------------------------
4.7.3.5 Computed Processing Instruction Constructors

% 083
DEv, DErr / all rules
# dynEnv |- Value matches Type
Change 'dynEnv' to 'statEnv', according to 7.3.1.

------------------------------------------------------------------------
4.7.3.6 Computed Comment Constructors

% 084
DEv, DErr / all rules
# dynEnv |- Value matches Type
Change 'dynEnv' to 'statEnv', according to 7.3.1.

------------------------------------------------------------------------
4.8 [For/FLWR] expressions

% 085
In rules throughout 4.8.x, change 'Expr' to 'ExprSingle' as
appropriate, to conform to the EBNF.

------------------------------------------------------------------------
4.8.2 For expression

% 086
STA / all rules
# ... varType(VarRef : Type) ...

According to Section 3.1.1, the domain of statEnv.varType is
expanded-QName, but a VarRef is not an expanded-QName. You'll need to
add some stuff:
 > VarRef = "$" VarName
 > VarName of var expands to expanded-QName
 > ... varType( expanded-QName : Type )
________

% 087
STA / rule 2 / premise 2
STA / rule 4 / premise 4
# statEnv + varType(VarRef1 : T, VarRefpos : xs:integer)
Change the comma to a semicolon.
________

% 088
STA / rule 3,4 / premise 3
# prime(Type1) <: Type0
Prepend 'statEnv |-'.
________

% 089
STA / rule 3 / premise 4
# statEnv + varType(VarRef1 : Type0)) |- ...
Delete extra right paren.
________

% 090
DEv / rule 3 / premise 4,5
DEv / rule 5 / premise 6,8
# varValue(Variable => Itemn, Variablepos => n)
Change the comma to a semicolon
________

% 091
DEv / rule 4 / conclusion
# => gr_Value1; ,..., Valuen
Change 'gr_Value1;' to italicized Value sub 1.
________

% 092
DErr / rule 1 / conclusion
# for Variable1
Change to
 > for VarRef
________

% 093
DErr / rule 3 / premise 4
# Variable => ItemiVariablepos => i
Insert semicolon and space:
 > Variable => Itemi; Variablepos => i

------------------------------------------------------------------------
4.9 Unordered Expressions

% 094
Notation
# dynEnv |- Value1 permutes to Value2
Should be centered.

------------------------------------------------------------------------
4.10 Conditional Expressions

% 095
Throughout, change occurrences of 'Expr2' & 'Expr3' to 'ExprSingle2' &
'ExprSingle3', to conform to the EBNF.
________

% 096
DEv+DErr / all rules / conclusions
# dynEnv |- if Expr1 then Expr2 else Expr3 ...
Add parens around Expr1.
________

% 097
DErr / rule 3 / premise 2
# dynEnv |- Expr3 => Error
Change to:
 > dynEnv |- Expr3 raises Error

------------------------------------------------------------------------
4.11 Quantified Expressions

% 098
Why are Quantified Expressions in the Core? Couldn't they be normalized
into For expressions?

% 099
In rules throughout this section, change 'Expr' to 'ExprSingle' as
appropriate, to conform to the EBNF.

% 100
Also, in each rule, put a linebreak after the 'of var expands to'
premise.
________

% 101
DEv + DErr / most rules / premise 1
# dynEnv |- Expr1 => Item1 ... Item
Add commas around ellipsis.
________

% 102
DEv + DErr / most rules
# 1 <= i <= n
Put this premise next to a premise that uses 'i'.
________

% 103
DEv / all rules
# dynEnv(Variable1 => Itemx))
Not only does this have an extra right paren,
but it also treats dynEnv as a mapping.
Change to
 > dynEnv + varValue(Variable1 => Itemx)
________

% 104
DEv / rule 3 / premise 5
# dynEnv(VarRef1 => Itemn))
(Similar to above, but with a VarRef.)
Change to
 > dynEnv + varValue(Variable1 => Itemn)
________

% 105
DEv / rule 4 / premise 6
# statEnv |- VarRef1 of var expands to Variable1
This repeats premise 3. Delete it
________

% 106
DErr / rule 1 / conclusion
# TypeDeclaration ?
Delete space before '?'.

------------------------------------------------------------------------
4.12.2 Typeswitch

% 107
2nd notation
# statEnv |- Type1 case CaseClause : Type
# dynEnv |- Value1 against CaseRules => Value
Should be centered
________

% 108
STA / rule 1 / premise 4
# statEnv |- Type0 case default VarRefn+1 return Exprn : Typen+1
STA / rule 3 / conclusion
# Type0 case default VarRef return Expr : Type

A 'default' clause is not a CaseClause, which is all that the 'case'
judgement is declared to handle.
________

% 109
STA / rule 2 / premise 2
STA / rule 3 / premise 1
# statEnv( VarRef : Type ) ...
Change to
 > VarRef = $ VarName
 > VarName of var expands to expanded-QName (or Variable)
 > statEnv + varType( expanded-QName : Type ) ...
________

% 110
STA / rules 2+3 / conclusion
Prepend "statEnv |-".
________

% 111
DEv / rule 1 / conclusion
# dynEnv |- typeswitch (Expr) CaseRules => Value1
The symbol 'CaseRules' does not exist in the XQuery or Core grammar,
only in the Formal.  (Maybe the Core grammar should use the CaseRules
syntax.)
________

% 112
DEv / rule 2 / conclusion
# case VarRef SequenceType
Insert 'as':
 > case VarRef as SequenceType
________

% 113
DEv / rule 3 / conclusion
# case SequenceType VarRef
Change to:
 > case VarRef as SequenceType

------------------------------------------------------------------------
4.12.3 Cast

% 114
Notation
# AtomicType1 cast allowed AtomicType2 = { Y, M, N }

Prepend 'statEnv |-'.

% 115
And instead of putting "{ Y, M, N }" in the judgment, introduce a Formal
non-terminal (e.g. Castability):
 > [xx (Formal)] Castability ::= Y | M | N
________

% 116
Notation / rule 1 / premise 3, conclusion
# ... = X, where X in { Y, M, N }
# ... = X
Change to
 > ... = Castability
________

% 117
Notation
# Type2 ( Value1 ) casts to Value2
Prepend "dynEnv |-"
________

% 118
STA, DE, DErr / all rules
# ... cast allowed ...
Prepend 'statEnv |-'
________

% 119
DEv / rule 1 / premise 3
# ( Value1 ) cast as AtomicType2 => Value2
Prepend "dynEnv |-".
________

% 120
DEv / rule 1 / conclusion
# AtomicType ( Expr ) casts to Value2
DEv / rule 2 / premise 3
# AtomicType2 ( Value1 ) casts to Value2

AtomicType is not actually a Type (i.e., not deriveable from symbol
Type), so these judgments don't match the judgment-form declared in the
Notation section. Change to QName?
________

% 121
DErr / rule 1 / premise 1
# AtomicValue1 of type AtomicTypeName
Change 'AtomicValue' to 'AtomicValueContent'.

------------------------------------------------------------------------
4.12.4 Castable

% 122
throughout
# Expr castable as AtomicType
Change 'Expr' to 'CastExpr'.
________

% 123
Normalization / rule 2 / LHS
# [Expr castable as AtomicType]_Expr
Presumably, AtomicType should be followed by a '?', otherwise it's the
same LHS as rule 1.
________

% 124
DEv / rule 1 / premise 2
# ( Value1 ) cast as AtomicType=> Value2
Prepend 'dynEnv |-'.
________

% 125
DEv / rule 2 / premise 1
# ( Expr1 ) cast as AtomicType2 raises dynError
Prepend 'dynEnv |-'.

------------------------------------------------------------------------
4.13 Validate Expressions:

% 126
Normalization / rules 1,2 / LHS
Each is missing [ ]_Expr around LHS
________

% 127
STA / rule 1 / premise 2
DEv / rule 1 / premise 2
DEv / rule 2 / premise 2
# statEnv(validationMode(ValidationMode) +
#         validationContext(ValidationContext))

This syntax is not supported by 2.1.4. Change to:
 > statEnv + validationMode(ValidationMode)
 >         + validationContext(ValidationContext)
________

% 128
STA / rule 1 / premise 5
# prime(Type) = ElementType1 ... ElementType2
Put choice bars around ellipsis.
________

% 129
STA / rule 1 / last premise
# Type1 = ElementName1 | ... | ElementNamen
'ElementName' is not a valid Type.
Did you mean ElementType instead?
________

% 130
DEv / rules 1,2 / premise 5
# ElementValue2 = ElementName2 ...
Insert 'element'
 > ElementValue2 = element ElementName2 ...
Also, in rule 1, delete the semicolon at the end of the line.
________

% 131
DEv / rules 1,2 / premise 7
# annotate as ...
Prepend "statEnv |-" or "statEnv1 |-" (not sure which).

------------------------------------------------------------------------
------------------------------------------------------------------------
5 Modules and Prologs

% 132
Notation
# [81 (Formal)] PrologDeclList ::= (PrologDecl Separator)*

The rules in SCP and DCP assume that PrologDeclList is left-recursive:
 > PrologDeclList ::= () | PrologDeclList PrologDecl Separator
but the rules in 5.2's SCP and DCP assume that it's right-recursive:
 > PrologDeclList ::= () | PrologDecl Separator PrologDeclList
Since section 5,2 needs to construct a new PrologDeclList by prepending
a PrologDecl to an existing PrologDeclList, I think it wins. So maybe
the left-recursive rules should be changed. E.g.:
 >
 > SCP:
 >     --------------------------------------------------
 >     statEnv |- () =>stat statEnv
 >
 >     PrologDecl1 = [PrologDecl]_PrologDecl
 >     statEnv  |- PrologDecl1    =>stat statEnv1
 >     statEnv1 |- PrologDeclList =>stat statEnv2 ; PrologDeclList1
 >     --------------------------------------------------
 >     statEnv  |- PrologDecl ; PrologDeclList =>stat statEnv2;
 >                                          PrologDecl1 ; PrologDeclList1
 >
 > STA:
 >     statEnvDefault |- PrologDeclList =>stat statEnv ; PrologDeclList1
 >     statEnv |- [QueryBody]_Expr : Type
 >     --------------------------------------------------
 >     PrologDeclList QueryBody : Type
 >
 > DCP:
 >     --------------------------------------------------
 >     dynEnv |- () =>dyn dynEnv
 >
 >     dynEnv  |- PrologDecl     =>dyn dynEnv1
 >     dynEnv1 |- PrologDeclList =>dyn dynEnv2
 >     --------------------------------------------------
 >     dynEnv |- PrologDecl ; PrologDeclList =>dyn dynEnv2
 >
 > DEv:
 >     dynEnvDefault |- PrologDeclList1 =>dyn dynEnv
 >     dynEnv |- [QueryBody]_Expr => Value
 >     --------------------------------------------------
 >     PrologDeclList QueryBody => Value
________

% 133
Notation
# [82 (Formal)] PrologDecl
You forgot FunctionDecl!
________

% 134
Notation / normalization
# [PrologDecl]_PrologDecl == PrologDecl
Use subscripts to distinguish the two PrologDecls, otherwise it looks
like the []_PrologDecl function is the identity function.
________

Notation / judgment-form 1
# PrologDeclList =>stat statEnv; PrologDeclList1

% 135
(1) The use of a meta-syntactic semicolon is probably a poor choice,
     especially when base-syntactic semicolons are nearby. How about
     a bolded word like "with"?

% 136
(2) It isn't clear what the resulting PrologDeclList1 is for.

% 137
(3) There isn't a corresponding judgment-form declared for =>dyn:
     PrologDeclList =>dyn dynEnv
________

% 138
Notation / judgment-form 3
# dynEnv |- PrologDecl =>stat dynEnv
Change '=>stat' to '=>dyn'.
________

% 139
SCP / rule 2
# PrologDecl1 = [PrologDecl]_PrologDecl
When you have a normalization-invocation in an inference rule, you
should perhaps make the judgment look more like the "longhand" judgment
shown in 2.4.2 / Notation:
 > statEnv |- [PrologDecl]_PrologDecl == PrologDecl1
________

% 140
SCP / rule 1 / conclusion
DCP / rule 1 / conclusion
# () =>stat statEnvDefault; ()
# () =>dyn  dynEnvDefault
These use '()' to denote a (syntactically) empty PrologDeclList. This is
prehaps not a good idea, since there is possible confusion with '()'
denoting a (semantically) empty sequence in the base language. In other
rules, empty syntax is denoted by the empty string. See, e.g.,
7.6.2 / Semantics / rule 1 / conclusion, where an an omitted ElementName
in an 'ElementName? in context' judgment results in the judgment
# statEnv |- in context global ...
________

% 141
SCP / rule 2 / premise 3
# statEnv1 |- PrologDecl1 =>stat statEnv2 ; PrologDecl1
Delete '; PrologDecl1'. When applied to a single PrologDecl, '=>stat'
just produces a statEnv.
________

% 142
STA / rule 1 / premise 2
# statEnv |- [QueryBody]_Expr : Type
Maybe split into
 > statEnv |- [QueryBody]_Expr == Expr2
 > statEnv |- Expr2 : Type
________

% 143
DEv / rule 1 / premise 1
# PrologDeclList1 =>dyn dynEnv
Presumably, the subscript 1 refers to the normalized prolog that =>stat
"returned" during STA of the module. But as far as the notation is
concerned, it just looks like PrologDeclList1 is "free".
________

% 144
DEv / rule 1 / premise 2.
# dynEnv |- [QueryBody]_Expr => Value
Maybe split into
 > statEnv |- [QueryBody]_Expr == Expr2
 > dynEnv |- Expr2 => Value

------------------------------------------------------------------------
5.2 Module Declaration

% 145
Notation
# URI =>module_statEnv statEnv
# URI =>module_dynEnv dynEnv
It seems to me that these mappings should be components of the
static and dynamic environments, respectively.
________

% 146
SCP+DCP / rule 1 / premise 1
# (declare namespace NCName = String PrologDeclList) =>stat statEnv
Delete the parens around the namespace decl, and insert a semicolon
between the String and PrologDeclList:
 > declare namespace NCName = String ; PrologDeclList =>stat statEnv
________

% 147
SCP+DCP / rule 1 / premise 2
# module namespace NCName = String PrologDeclList
Insert a semicolon again. But even, it's not a judgment
________

% 148
DCP / rule 1 / premise 1
# ... =>stat dynEnv
Change '=>stat' to '=>dyn'.

------------------------------------------------------------------------
5.4 Default Collation Declaration

% 149
SCP / rule 1 / premise
# statEnv1 = statEnv + collations( String)
Change 'collations' to 'defaultCollation'.
However, Section 3.1.1 tells us that statEnv.defaultCollation is a pair
of functions, not a String. So first, look up the collation's URI in the
static environment:
 > func-pair = statEnv.collations(String)
 > statEnv1 = statEnv + defaultCollation(func-pair)
________

% 150
DCP / rule 1 / conclusion
# dynEnv |- default collation String =>dyn dynEnv
Insert "declare" before "default".

------------------------------------------------------------------------
5.7 Default Namespace Declaration

% 151
SCP / rules 1, 2, 3 / conclusion
# statEnv |- declare default element namespace = String =>stat statEnv1
Delete '=' after 'namespace'.

------------------------------------------------------------------------
5.8 Schema Import

% 152
Notation / judgment-form 1
# statEnv1 |- Definition* =>type statEnv2
The meta-syntactic '*' is used to denote a sequence of Definitions, but
this overloads '*' unnecessarily. Instead, a new symbol 'Definitions'
would be less confusion-prone.
 > [xx (Formal)]  Definitions ::= Definition*
(And propagate to F.1.3 Main mapping rules and F.2.1 Schema.)
________

% 153
SCP / rules 1,2,3 / premise 1
# ... schema String (at String)? ...
Without subscripts, you're forcing the two String's to bind to the same
object, which you don't want.  Moreover, the schema location hint can be
more involved than just "(at String)?". To take care of both of these
problems, define
 > [xx (XQuery+Core)] ImportLocationHints ::=
 >                           (("at" StringLiteral) ("," StringLiteral)*)?
use that in [149 (XQuery)] and [108 (Core)], and in the inference rules,
change every occurrence of
# (at String)?
to
 > ImportLocationHints
________

% 154
SCP / rule 3:
# default_elem_namespace( String (at String)?)
Delete "(at String)?", as default_elem_namespace doesn't care about it.
________

% 155
SCP / rule 5 / conclusion
# Definition1 Definition* =>type statEnv2
Prepend "statEnv |-".

------------------------------------------------------------------------
5.9 Module Import

% 156
SCP / rule 1 / premise 1
# String =>module_statEnv statEnv2
Change 'String' to 'String1', I think
________

% 157
SCP / rule 1 / premise 2
# statEnv3 = statEnv1(fs:local-variables(statEnv2, String1)
#                   + fs:local-functions(statEnv2, String1))
This is vague, ad hoc syntax. The following is still ad hoc, but at
least is more specific (re varType + funcDefn) and fits better with the
syntax established by 2.1.4:
 > statEnv3 = statEnv1 + varType( fs:local-variables(a,b) )
 >                     + funcDefn( fs:local-functions(a,b) )
________

% 158
DCP / rule 1 / premise 1
# String =>module_dynEnv dynEnv2
Delete it.
________

% 159
DCP / rule 1 / premise 2
# dynEnv2 = dynEnv1 + varValue(expanded-QName => #IMPORTED(URI))
Add subscript 1 to 'expanded-QName'.
________

% 160
DCP / rule 1 / premise 3, conclusion
# (expanded-QName2, Type2) ??? (expanded-QNamen, Typen)
Put commas around ellipsis.
________

% 161
DCP / rule 2 / premise 1
# String =>module_dynEnv dynEnv2
Delete it.
________

% 162
DCP / rule 2 / premise 2
# dynEnv + funcDefn1(...)
The subscript 1 is in the wrong place. Change to
 > dynEnv1 + funcDefn(...)
________

% 163
DCP / rule 2 / premise 2,3, conclusion
# expanded-QName1(Type1,1, ..., Type1,n)
# expanded-QName2(Type2,1, ..., Type2,n)
# expanded-QNamek(Typek,1, ..., Typek,n)
# expanded-QName1(Type1,1, ..., Type1,n)
# expanded-QNamek(Typek,1, ..., Typek,n)
Note that this appears to require that all functions imported from a
module have the same number of arguments (n). Moreover, with all these
subscripts and ellipses, the rule is hard to follow. To fix both of
these problems, define a Formal symbol for function signatures:
 > [xx (Formal)] FuncSignature ::=
 >                           expanded-QName "(" ( Type ("," Type)* )? ")"

Then you can say:

 > dynEnv2 = dynEnv1 + funcDefn( FuncSignature1 => #IMPORTED(URI) )
 > dynEnv2 ; URI |- FuncSignature2 ??? FuncSignaturek
 >                                             =>import_functions dynEnv3
 > ------------------------------------------------
 > dynEnv1 ; URI |- FuncSignature1 ??? FuncSignaturek
 >                                             =>import_functions dynEnv3
________

% 164
DCP / rule 2 / premise 3, conclusion
Put commas around the (top-level) ellipsis.
________

% 165
DCP / rule 3 / premise 1
# String =>module_dynEnv dynEnv2
Change 'String' to 'String1',
________

% 166
DCP / rule 3 / premise 2,3
# dynEnv1 |-
# dynEnv3 |-
Change to
 > dynEnv1 ; String1 |-
 > dynEnv3 ; String1 |-
to match the conclusion of rule 2.
________

% 167
DCP / rule 3 / conclusion
# statEnv1 |- import module ... =>dyn statEnv4
Change each 'statEnv' to 'dynEnv'.

------------------------------------------------------------------------
5.10 Namespace

% 168
DCP / rule 1 / conclusion
# declare namespace NCName =>dyn dynEnv
Insert '= String' after 'NCName'.

------------------------------------------------------------------------
5.11 Variable Declaration

% 169
SCP / all rules / last premise
# varType( Variable => Type )
Change '=>' to ':' if you want to follow 2.1.4.
________

% 170
DCP / all rules / conclusion
# =>stat dynEnv
Change '=>stat' to '=>dyn'.

------------------------------------------------------------------------
5.12 Function Declaration

% 171
Normalization + SCP + STA + DCP
# define function QName
should be
 > declare function QName
________

% 172
Normalization / rule 3 / LHS
Add 'PrologDecl' subscript to right bracket.
________

% 173
SCP / para 1
# withtin
Change to 'within'.
________

% 174
SCP / rule 1 / premise 2 + conclusion
STA / rule 1 / conclusion
STA / rule 2 / conclusion
DCP / rule 1 / premise 4 + conclusion
DCP / rule 2 / conclusion
# [SequenceType1]sequencetype, ??? [SequenceTypen]sequencetype
Put comma after ellipsis.
________

% 175
SCP / rule 1 / premise 2
# funcType(expanded-QName => ( [SequenceType1]sequencetype, ???
funcType is supposed to map an expanded-QName to a set of FuncDecls,
but this maps it to a sequence of Types.
________

% 176
SCP / rule 1 / premise 3
# statEnv2 = statEnv + funcType1(expanded-QName)
Seems to be a leftover. Delete it.
In the conclusion, change 'statEnv2' to 'statEnv1'.
________

% 177
SCP / rules 1 / conclusion
Prepend 'statEnv |-'.
________

% 178
STA / rule 1 / premise 1
# ... varType( VarRef : T; ...
The domain of statEnv.varType is exapnded-QName, not VarRef, so:
 > VarRef = $ VarName
 > VarName of var expands to expanded-QName
 > ... varType( expanded-QName : T; ...
________

% 179
STA / rule 1+2 / conclusion
# statEnv |- define function QName ...
This doesn't appear to be a judgment.
________

% 180
DCP / rule 1 / premise 4 + conclusion
# dynEnv'
This is the only place where a prime is appended to an environment name.
For greater consistency, use a subscript '1' instead.
________

% 181
DCP / rule 1 / premise 4
# funcDefn(expanded-QName => ... )
The domain of dynEnv.funcDefn is not just an expanded-QName, but a whole
FuncSignature (expanded-QName and sequence of (parameter) Types).
________

% 182
DCP / rule 2 / conclusion
# Variable1 as SequenceType1
# Variablen as SequenceTypen
Change 'Variable' to 'VarRef'.

------------------------------------------------------------------------
------------------------------------------------------------------------
6.1.3 The fs:convert-operand function

% 183
STA / rule 3,4,5 / premise 2
# statEnv |- Expr1 <: Type1
Change '<:' to ':'.

------------------------------------------------------------------------
6.2.1 The fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions

% 184
STA / rule 1 / premise 3
# convert_untypedAtomic(....) can be promoted to Type1
Maybe change to
 > Type2 = convert_untypedAtomic(....)
 > statEnv |- Type2 can be promoted to Type1
________

% 185
STA / rule 1 / premise 4
# xs:integer xs:decimal
Insert comma after 'xs:integer'.

------------------------------------------------------------------------
6.2.2 The fn:collection and fn:doc functions

% 186
STA / rule 2,5 / premise 1
# statEnv |- statEnv.map(String) not defined
Change 'not defined' to 'undefined' for consistency. Or change
occurrences of 'undefined' to 'not defined'.
________

% 187
STA / rule 2,3 / conclusion
# statEnv |- fn:collection(Expr) : node *
'node *' does not appear to be a valid Type.
________

% 188
STA / rule 3,6
# statEnv |- not(Expr = String)
This is an attempt to express "Expr is not a literal string". However,
note that
     Expr = String
doesn't mean
     'Expr' is a literal string
but rather
     'Expr' and 'String' are instantiated to the same object
Because 'String' has no other reference in the rule, the inference
engine is free to instantiate it to any object. In particular, it can
*always* instantiate it to something different from 'Expr', causing the
premise to hold, and thus the conclusion to hold (even when it
shouldn't).

I don't think you've defined the notation that would express this
correctly.
________

% 189
SAT / rule 4 / premises 1,2
# statEnv |- statEnv.docType(String) = Type
# statEnv |- statEnv.docType(String) = Type
The two premises are the same. Delete one of them.

------------------------------------------------------------------------
6.2.3 The fn:data function

% 190
Notation / judgement-form 1
# statEnv |- data on Type1 : Type2
Put the colon in bold.
________

% 191
STA / rule 8 / premise 1
STA / rule 9 / premise 1,2
STA / rule 11 / premise 1
# statEnv |- ... type lookup (of type TypeName)
The parens are ungrammatical.  Note that
   7.1.9 / Sem / rule 2 / conclusion
   E.1.1 / Sem / rule 2 / conclusion
don't have them.
________

% 192
STA / rule 11 / premise 3
# define type TypeName Derivation? Mixed { Type1? }
Change 'Mixed' to just 'mixed'.

------------------------------------------------------------------------
6.2.5 The fn:error function

% 193
STA / rule 1 / premise 1
# statEnv |- Expr : item ?
"item?" does not appear to be a valid Type.

% 194
Anyway, if fn:error() always has the 'none' type, why does the rule need
a premise?

------------------------------------------------------------------------
6.2.6 The fn:min, fn:max, fn:avg, and fn:sum functions

% 195
Sem / rule 1,2,3 / premise 3
# Type1 can be promoted to T
Prepend 'statEnv |-'.

------------------------------------------------------------------------
6.2.7 The fn:remove function

% 196
STA / rule 1 / conclusion
# fn:remove(Expr,Expr1) : : prime(Type) ? quantifier(Type)
Change ': :' to just ':'.

------------------------------------------------------------------------
6.2.8 The fn:reverse function

% 197
STA / rule 1 / conclusion
# fn:reverse(Expr) : : prime(Type) ? quantifier(Type)
Change ': :' to just ':'.

------------------------------------------------------------------------
6.2.10 The op:union, op:intersect, and op:except operators

% 198
STA / rule 2 / conclusion
# prime(Type1, Type2); ? quantifier(Type1,Type2); ? ?
Delete two semicolons.

------------------------------------------------------------------------
------------------------------------------------------------------------
7.1.3 Element and attribute name lookup (Dynamic)

% 199
2nd Sem / rule 1 / premise 1
3rd Sem / rule 1,2 / premise 1
# ... statEnv.attrDecl(AttributeName) ...
The domain of statEnv.attrDecl is expanded-QName, so change to:
 > statEnv |- AttributeName of attr expands to expanded-QName
 > ... statEnv.attrDecl(expanded-QName) ..

------------------------------------------------------------------------
7.1.4 Element and attribute type lookup (Static)

% 200
1st Sem / rule 2 / conclusion
# statEnv |- element ElementName type lookup Nillable? xdt:untyped
Insert 'of type' before xdt
________

% 201
2nd Sem / rule 1,2 / premise 1
# ... statEnv.attrDecl(AttributeName) ...
The domain of statEnv.attrDecl is expanded-QName, so change to:
 > statEnv |- AttributeName of attr expands to expanded-QName
 > ... statEnv.attrDecl(expanded-QName) ..
________

% 202
2nd Sem / rule 2 / conclusion
# statEnv |- attribute AttributeName type lookup xdt:untypedAtomic
Insert 'of type' before xdt

------------------------------------------------------------------------
7.1.5 Extension

% 203
Sem / rule 1 / premise 1,2
# Type1 = AttributeAll1 , ElementContent1
What does it mean? 'AttributeAll' doesn't match any symbol name, and
ElementContent isn't in the Formal language. Is 'ElementContent'
supposed to be 'ElementContentType'?
And similarly in 7.1.6 / Sem / rule 1 / premise 1.

------------------------------------------------------------------------
7.1.6 Mixed Content

% 204
Sem / rule 1 / conclusion
# ( ElementContent & text* | xdt:anyAtomicType *)
This relies on the relative precedence of type-operators '&' and '|',
which has not been defined, and probably shouldn't be. Just use parens.

------------------------------------------------------------------------
7.1.7 Type adjustment

% 205
Sem / rule 1 / premise 3
# statEnv |- Type3 & processing-instruction* & comment* is Type4
What kind of judgment is this?

------------------------------------------------------------------------
7.1.9 Type Expansion

% 206
Notation / judgment-form 1
# statEnv |- Nillable? TypeReference expands to Type
Given the use of this judgment in 7.2.3.1.2, it would be better to
change 'Nillable? TypeReference' to 'TypeSpecifier'.

------------------------------------------------------------------------
7.2.2.1 Static semantics of axes

% 207
Sem / rule 8 / premise 2
Sem / rule 17 / premise 2
# Nillable? TypeReference expands to ...
Prepend 'statEnv |-'.
________

% 208
Sem / rule 8 / premise 3, 4
# Type1 has-node-content Type1'
Prepend 'statEnv |-'.
________

% 209
Sem / rule 16 / conclusion
# processing-instructions*
Delete final 's'.
________

% 210
Sem / rule 17 / premise 3, 4
# Type1 has-attribute-content Type1'
Prepend 'statEnv |-'.
________

% 211
Sem / rule 23 / conclusion
# document { Type }
Italicize 'Type'.

------------------------------------------------------------------------
7.2.2.2 Dynamic semantics of axes

% 212
Sem / rules 3-10
# axis Axis self:: of NodeValue
# axis Axis child:: of element ...
# axis Axis attribute:: of ElementName ...
# etc
In each case, delete "Axis" before the actual axis name.
________

% 213
Sem / rule 5 / conclusion
# dynEnv |- axis Axis attribute:: of ElementName ...
Insert 'element' before 'ElementName'.
________

% 214
Sem / rule 11
# In all the other cases, the axis application results in an empty
# sequence.
# dynEnv |- axis Axis of NodeValue => () otherwise.
The premises are unformalized.

------------------------------------------------------------------------
7.2.3.1.1 (Static semantics of) Name Tests

% 215
rule 13 / conclusion
rule 26 / conclusion
# prefix:local
Change to italicized 'Prefix:LocalPart'.
________

% 216
rule 22 / premise 1
# fn:namespace-uri-from-QName(QName1)
Change 'QName1' to 'expanded-QName1', and add
 > QName1 of attr expands to expanded-QName1

------------------------------------------------------------------------
7.2.3.1.2 (Static semantics of) Kind Tests

% 217
throughout / many rules / conclusion
# dynEnv |-
Change 'dynEnv' to 'statEnv'
________

% 218
It would be nice if the division-headers of this section ('Document kind
test', 'Element kind test', etc.) stood out more than the big bold
'Semantics' headers.

------------------------------------------
(Static semantics of) Document kind test

% 219
Sem / rule 3 / premise 2
# (Type1 <: DocumentType or DocumentType <: Type1)
Put 'or' in bold, since it's meta.
________

% 220
Sem / rule 3,4 / conclusion
# document-node (Type)
This is not a valid Type.  Change to
 > document { Type }

------------------------------------------
(Static semantics of) Element kind test

% 221
The "Semantics" header should be either one or two paras earlier.
________

% 222
Sem / rule 3 / conclusion
Sem / rule 4 / premise 1
# element * TypeSpecifier
This is not a valid Type. (Wildcards are allowed in XQuery Tests, not in
Formal Types.) Delete the '*'.
________

% 223
Sem / rule 5 /  premise 1, 2, 3, conclusion
# ElementNameOrWildcard TypeSpecifier
This is being used as if it's a Type, but it isn't. Change all to
 > element ElementName? TypeSpecifier

------------------------------------------
(Static semantics of) Attribute kind test

% 224
The "Semantics" header should be either one or two paras earlier.
________

% 225
Sem / rule 3 / conclusion
Sem / rule 4 / premise 1
# attribute * TypeSpecifier
Change to:
 > attribute TypeReference
and propagate.
________

% 226
Sem / rule 5 / premise 1, 2, 3, conclusion
# AttribNameOrWildcard TypeSpecifier
Change to:
 > attribute AttributeName? TypeReference
and propagate.

------------------------------------------
(Static semantics of) Processing instruction, comment, and text kind tests.

% 227
What, no "Semantics" header?
________

% 228
rule 4 / conclusion
# test text() of with PrincipalNodeKind text
Move the 'of':
 > test text() with PrincipalNodeKind of text
________

% 229
rule 6
# If none of the above rules apply, then the node test returns the empty
# sequence and the following rule applies:
# statEnv |- test node() with PrincipalNodeKind of NodeType : empty
The premises are unformalized.

------------------------------------------------------------------------
7.2.3.2.1 (Dynamic semantics of) Name Tests

% 230
Sem / all rules / premise 1
# fn:node-kind( NodeValue ) = PrincipalNodeKind
Italicize 'PrincipalNodeKind'.
________

% 231
Sem / rule 3 / premise 3
# fn:namespace-uri-from-QName( QName )
Change 'QName' to 'expanded-QName', and add
 > QName of attr expands to expanded-QName
________

% 232
Sem / rule 3 / conclusion
#  test prefix:* with PrincipalNodeKind of NodeValue
Change 'prefix' to italicized 'Prefix'.
________

% 233
Sem / rule 4 / premise 3, conclusion
# local
Change 'local' to italicized 'LocalPart'.

------------------------------------------------------------------------
7.2.3.2.2 (Dynamic semantics of) Kind Tests

Processing instruction, comment, and text kind tests.

% 234
Sem / rule 2 / premise 3, 4
# String
Italicize 'String'.
________

% 235
Sem / rule 9
# If none of the above rules applies then the node test returns the
# empty sequence, and the following dynamic rule is applied:
# dynEnv |- test node() with PrincipalNodeKind of NodeValue => ()
The premises are unformalized.

------------------------------------------------------------------------
7.2.4 Attribute filtering

% 236
Sem / rules 1,2 / premise 1
# dynEnv |- Value1 of attribute:: => Value2
What kind of judgment is this?
________

% 237
Sem / rules 1,2 / premise 2
# dynEnv |- Value2 of "attribute", QName => ...
Again, what kind of judgment is this?

------------------------------------------------------------------------
7.3.1 Matches

% 238
Sem / rule 1 / conclusion
# AtomicValue of type AtomicTypeName
Change 'AtomicValue' to 'AtomicValueContent'.
________

% 239
Sem / rule 2,3,4 / conclusion
# String
Italicize 'String'.
________

% 240
Sem / rule 8 / conclusion
# attribute AttributeName of type TypeName { Value }
Change '{ Value }' to '{ SimpleValue }'.
________

% 241
Sem / rule 15 / conclusion
# statEnv |- empty matches Type*
'empty' is not a Value.  Do you mean '()'?

------------------------------------------------------------------------
7.3.2 Subtype and Type equality

% 242
Note / para 1
# values which are not available at static type checking type.
Change second 'type' to 'time'?

------------------------------------------------------------------------
7.5.1 Type promotion

% 243
1st Notation / judgment-form 1
# Type1 can be promoted to Type2
Prepend 'statEnv |-'.
________

% 244
1st Sem / rule 8 / premise 2
# prime(Type2) can be promoted to prime(Type2')
Prepend 'statEnv |-'.
________

% 245
2nd Notation / judgment-form 2
# Value1 against Type2 promotes to Value2
Prepend 'statEnv |-'
________

% 246
2nd Semantics / rule 1 / premise 1, conclusion
Prepend 'statEnv |-'
________

% 247
2nd Semantics / rule 2 / premise 3
# statEnv |- Type1 != Type2
Is statEnv needed for this judgment?
________

% 248
2nd Semantics / rule 2 / premise 4
# cast as Type2 (Value1) => Value2
Change to
 > statEnv |- (Value1) cast as Type2 => Value2

------------------------------------------------------------------------
7.6.2 Elements in validation context

% 249
Sem / rule 1 / premise 3,4
Sem / rule 3 / premise 2
Sem / rule 6 / premise 3
# statEnv |- statEnv.elemDecl(expanded-QName) => define ElementType
statEnv,elemDecl maps an expanded-QName to a Definition, but
'define ElementType' is not a valid Definition. Change it to
'define element ElementName Substitution? Nillable? TypeReference'
and then construct ElementType out of those parts?
________

% 250
Sem / rule 2 / premise 1
Sem / rule 6 / premise 2
# element of TypeName
Insert 'type' before 'TypeName'.
________

% 251
Sem / rule 2 / premise 2
# statEnv |- test element() with "element" of Type1 : Type2
Put 'with' in bold.
________

% 252
Sem / rule 2 / conclusion
Sem / rule 6 / conclusion
Sem / rule 7 / conclusion
Sem / rule 8 / premise 2 + conclusion
Sem / rule 9 / premise 2 + conclusion
#   in context type(TypeName)
#   in context ElementName2
#   in context (SchemaGlobalContext "/" ... "/" SchemaContextStepN)
#   in context (SchemaGlobalContext "/" ... "/" SchemaContextStepN) "/" ElementName2
#   in context SchemaContextStep
#   in context SchemaContextStep "/" ElementName2
These assume a syntax for ValidationContext that does not match the
EBNF.  Also, the slashes should not be in quotes.
Similar problems in 7.6.3.
________

% 253
Sem / rule 3, 6, 7, 8, 9
# ValidationMode = "strict" or "lax"
It would be better to say
 > ( ValidationMode = "strict" ) or ( ValidationMode = "lax" )
or
 > ValidationMode in { "strict", "lax" }
At very least, 'or' should be in bold, since it's meta.
Similar problems in 7.6.3.
________

% 254
Sem / rule 6 / premise 3
Sem / rule 7 / premise 5
Sem / rule 8 / premise 4
Sem / rule 9 / permise 4
# test ElementName with "element" of Type
An ElementName is not a valid NodeTest.
Also, put 'with' in bold.

------------------------------------------------------------------------
7.6.3 Attributes in validation context

% 255
Sem / rule 1 / premise 1,2
Sem / rule 3,4 / premise 1
# ... statEnv.attrDecl(AttributeName) ...
The domain of statEnv.attrDecl is expanded-QName, so change to:
 > statEnv |- AttributeName of attr expands to expanded-QName
 > ... statEnv.attrDecl(expanded-QName) ..
________

% 256
Sem / rule 1 / premises 1,3
Sem / rule 3 / premise 1
# statEnv |- statEnv.attrDecl(AttributeName) => define AttributeType
statEnv,attrDecl maps an expanded-QName to a Definition, but
'define AttributeType' is not a valid Definition. Change it to
'define attribute AttributeName TypeReference' and then construct
AttributeType out of those parts?
________

% 257
Sem / rule 2 / premise 1
Sem / rule 6 / premise 2
# statEnv |- axis attribute:: of element of TypeName : Type1
Insert 'type' before 'TypeName'.
________

% 258
Sem / rule 5 / conclusion
# resolves to element AttributeName
Change 'element' to 'attribute'?
________

% 259
Sem / rule 6 / premise 3
Sem / rule 7 / premise 5
Sem / rule 8 / premise 5
Sem / rule 9 / premise 5
# test AttributeName
An AttributeName is not a valid NodeTest.  Maybe you want just QName.
________

% 260
Sem / rule 7
# statEnv |- statEnv.elemDecl(expanded-QName2) => define ElementType2
'define ElementType' is not a valid Definition. Change it to
'define element ElementName Substitution? Nillable? TypeReference'
and then construct ElementType out of those parts?

------------------------------------------------------------------------
------------------------------------------------------------------------
A.1 Core BNF

% 261
Named Terminals
# [18 (Core)]  ElementContentChar ::=  Char - [{}<&] - [{}<&]
# [19 (Core)]  QuotAttContentChar ::=  Char - ["{}<&] - ["{}<&]
# [20 (Core)]  AposAttContentChar ::=  Char - ['{}<&] - ['{}<&]
Eliminate repetition (as in 4.7.1)

------------------------------------------------------------------------
------------------------------------------------------------------------
E.1.1 Type resolution

% 262
Notation / judgment-form 1
# statEnv |- (TypeReference | TypeDerivation) resolves to ...
The '|' is meta. It would be better to declare the judgment-form twice,
once for TypeReference and once for TypeDerivation.

------------------------------------------------------------------------
E.1.3.1 Simply erases

% 263
Sem / rule 2 / premise 1,2
# statEnv |- SimpleValue1 simply erases to String1 SimpleValue1 != ()
Each is structured as a single premise, but presuambly should be two.
________

% 264
Sem / rule 3 / conclusion
# AtomicValue of type AtomicTypeName
Change 'AtomicValue' to 'AtomicValueContent'

------------------------------------------------------------------------
E.1.4.1 Simply annotate

% 265
Notation
# statEnv |- simply annotate as SimpleType ( SimpleValue ) => ...
SimpleValue is in the EBNF but not SimpleType.
________

% 266
Sem / rule 2 / premise 1
# statEnv |- (...) fails
Change to:
 > not( statEnv |- ... )

------------------------------------------------------------------------
E.1.4.3 Annotate

% 267
Sem / rule 1 / conclusion
# annotate as () (()) => ()
Change the first '()' (the Type) to 'empty'.
________

% 268
Sem / rule 10,11,12 / last premise
# nil-annotate as Type Nillable?
Change to:
 > nil-annotate as Nillable? Type
________

% 269
Sem / rule 11 / premise 1
# Value filter @xsi:type => TypeName
The 'filter' judgment "yields" a SimpleValue, but a TypeName is not a
SimpleValue.
________

% 270
Sem / rule 11 / premise 2
# statEnv |- XsiTypeReference = of type TypeName
Is statEnv needed for this judgment?
________

% 271
Sem / rule 15 / premise 1
# String as xs:anySimpleType
Syntactically, what is the 'as xs:anySimpleType'?

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

-Michael Dyck

XQuery 1.0 and XPath 2.0 Formal Semantics
W3C Working Draft 20 February 2004

I think the normalization rules for some and every are incorrrect: the 
call of the function fn:boolean is missing in the satisfies clause. I 
would write the normalization rule like this:

[some VarRef1 in Expr1, ..., VarRefn in Exprn satisfies Expr]Expr
==
some VarRef1 in [Expr1]Expr satisfies
   some VarRef2 in [Expr2]Expr satisfies
         ...
     some VarRefn in [Exprn]Expr satisfies
      fn:boolean([Expr]Expr)


Same for every.


Minor typo: the two last 'satisfies' keyword are mispelled: satist
fies(note the t before f)

Best regards,
Lionel

Section 3.1.1		
Technical	

The static context should allow $fs:dot and friends to be predefined by
an implementation with an implementation-provided static type in the
outermost static variable declaration context.

Section 3.4.4		
Technical	

Why does normalization of [document-node(ElementTest)]sequencetype
include text in the result? This seems wrong since text should be part
of the original type, shouldn't it? Also, you should not have the node
types written with ().

Section 3.4.4		
Technical	

"  
[processing-instruction()]sequencetype 
== 
processing-instruction ? 
": 

Why ? ?

Section 3.4.1		
Editorial/Technical	

Why is xdt:untypedAtomic not part of the definition of xs:anySimpleType.
Please explain. Also, why is xs:anySimpleType not defined as
xdt:anyAtomicType*?

Section 3.1.2		
Technical	

Please replace "It is a static error to define a variable in the "fs"
namespace." with "Since there is no namespace URI associated to the fs
prefix, users cannot refer to such variables"

Note that a user should be allowed to define a prefix called fs with any
namespace he/she chooses. The point of not associating a namespace with
the definitional prefixes is that there will be no need to check for a
clash or disallow them.

Section 3.4.1		
Editorial/Technical	

Could "( element? & text? & comment? & processing-instruction? )* " be
written as the simpler "(  element | text | comment |
processing-instruction )* "?

MS-FS-LC1-037	
Section 3.1.1		
Editorial	

Replace "expaned " with "expanded "

MS-FS-LC1-038	
Section 3.1.1		
Editorial	

"in-scope type definitions": Do we need to change this name as we did
for "static in-scope namespaces"?

[Note this comment has been addressed at the F2F and is submitted for
completeness reasons.]

MS-FS-LC1-040	
Section 3.1.1		
Editorial	

typeDefn, attrDecl, elemDecl: Mention that they are containing the
imported schema components.

MS-FS-LC1-041	
Section 3.1.1		
Editorial	

Default collation should be a member of the collation environment.

MS-FS-LC1-042	
Section 3.1.1		
Editorial	

Replace "corresopnds " with "corresponds "

MS-FS-LC1-043	
Section 3.1.1		
Editorial	

Please rename " fs:get_ns_from_items" to " fs:get_static_ns_from_items"
to avoid confusion with dynamic in-scope namespaces

MS-FS-LC1-046	
Section 3.1.2		
Editorial	

$fs:dot can be referred to by the user using the XPath expression ".".
Please add.

MS-FS-LC1-049	
Section 3.4.1		
Editorial	

There are still references to xdt:untypedAny. Should be replaced with
xdt:untyped.

MS-FS-LC1-050	
Section 3.4.1		
Editorial	

"derived derived " -> "derived "

MS-FS-LC1-051	
Section 3.4.1		
Editorial	

The definition of fs:numerics seems broken. Also, do we really need to
make it a type or can we just do the explosion into all the possible
types?

MS-FS-LC1-052	
Section 3.4.3		
Editorial	

"SequenceTypes can be used in [XPath/XQuery] to refer to a type imported
from a schema ": Obviously it can refer to other types such as comment
or element(a, b) that are not imported from a schema!

MS-FS-LC1-054	
Section 3.4.4		
Editorial	

Also show NCName rule (not only string) for pi or do it in mapping to
the Core syntax!

Section 3.1.2		
Technical	

Why should the function body be part of the dynamic context. This seems
to imply that I can change the function definition at runtime or based
on an input value. I understand that we do not need the body of a
function during compilation of a query, but I would assume that you do
not have dynamic semantics with respect to function resolution. Maybe we
need a special linking environment to contain this information?

Section 3.1.1		
Technical	

Why can't the default function namespace be the empty namespace? Call it
out either way.

Section 3.1.1		
Editorial/Technical	

Are the namespace and collation environments already base URI adjusted?
Please call out either way. Note that the term URI means an absolute URI
which seems to indicate that base URIs have been applied.

Section 2.3.4		
Editorial/Technical	

Why is <xsd:attribute name="country" type="xsd:NMTOKEN" fixed="US"/>
mapped to an optional attribute? The instance always will have this
attribute with the fixed value.

Section 2.3.4		
Editorial/Technical	

" define type Section mixed {
    (element h1 of type xsd:string |
     element p of type xsd:string |
     element div of type Section)*
  }
": The Type grammar production does not allow "(", ")". Needs to be
fixed in the Type grammar production.

Section 2.3.4		
Editorial/Technical	

"A type declaration with simple content derived by restriction

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

": 

How does this work? If SKU is complex, how can it restrict from an
atomic type? If it is a restriction from an atomic type, then the
{xs:string} should not be there.

Section 2.3.2		
Editorial/Technical	

"A name alone corresponds to a reference to a global element or
attribute declaration. ": 

This is confusing. Why should this be used as a schema lookup? Shouldn't
this be part of the schema import and inference results and denote
something along the line of 

element a == element a of type xs:anyType?! 

Also affects the example and others: 
The following is a reference to a global attribute declaration
  attribute sizes

Especially with the resolution of the ISSD lookup semantics, we think
that the static type system should use explicit types and use another
syntax in the static type system for references such as ref a/ref-attr
a...

Section 2.3.4		
Editorial/Technical	

"When the type derivation is omitted, the type derives by restriction
from xs:anyType, as in:": Doesn't it derive from xdt:anyAtomicType?
since it is an atomic type?

Section 2.3.1		
Editorial/Technical	

Representation of content models: You are missing sequences (,).

Section 2.3.3		
Technical	

Please provide the precedence rules for the ItemType grammar. Especially
since no parens are allowed. For example, 

element a, element b | element b, element a 

can be interpreted in different ways.

Section 2.2		
Editorial/Technical	

Please mention namespace nodes as an XPath 2.0 specific node.

Section 2.3.1		
Editorial/Technical

"For the purpose of static typing, the [XPath/XQuery] type system only
describes minOccurs, maxOccurs combinations that correspond to the DTD
operators +, *, and ?. ": Also add that one looks at minLength/maxLength
for list types.

MS-FS-LC1-003	
Section 2.1.1		
Editorial	

Introduce the notion and purpose of XQuery Core before talking about its
syntactic notation.

MS-FS-LC1-004	
Section 2.1.1		
Editorial	

Please replace "language's semantics" with "languages' semantics" (there
are two!)

MS-FS-LC1-005	
Section 2.1.2		
Editorial	

"Expr raises Error": Add note that bold names refer to other judgments.
In this case it is an auxiliary judgment.

MS-FS-LC1-006	
Section 2.1.3		
Editorial	

Final Note is more confusing than helpful. It is not an algorithm since
the rules are descriptive. Please remove.

MS-FS-LC1-007	
Section 2.1.4		
Editorial	

Using "env" for environment group is confusing.

MS-FS-LC1-008	
Section 2.1.4		
Editorial	

The scoping of some of the environments (variables, namespaces) is not
understandable from the single sentence "Updating the environment
captures the scope of a symbol ". Please improve or give better example.

MS-FS-LC1-009	
Section 2.1.5		
Editorial	

Composition of several inference rules should be explained.

MS-FS-LC1-010	
Section 2.2		
Editorial	

Please do not use the term "value" as a synonym for "item" or "sequence
of items" (see similar comments on other documents). Thus rename the
section of 2.2 to "XML items" and perform other such alignments
throughout the document.

MS-FS-LC1-012	
Section 2.2		
Editorial	

Please replace "Elements have a type annotation and contain a value"
with "Elements have a type annotation and contain a sequence of items"

MS-FS-LC1-013	
Section 2.2		
Editorial	

Replace "Text nodes always contain one string value of type
xdt:untypedAtomic, therefore the corresponding type annotation is
omitted." with "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."

MS-FS-LC1-014	
Section 2.2.1		
Editorial	

Replace "Notably sequences cannot be nested." with "Notably sequences
are automatically flattened." Since you can write nested sequences
syntactically: they are just flattened.

MS-FS-LC1-015	
Section 2.2.2		
Editorial	

Replace "true as xsd:boolean " with "true as xs:boolean "

MS-FS-LC1-019	
Section 2.3.2		
Editorial	

Replace "Generic node types (e.g., node()), " with "Generic node types
such as used in the SequenceType production (e.g., node()), "

MS-FS-LC1-020	
Section 2.3.2		
Editorial	

Replace "The following is a type for a nillable element of type string"
with "The following is a type for a nillable element of type string with
name size"

MS-FS-LC1-022	
Section 2.3.3		
Editorial	

Replace "with lower bound 0 or 1, and upper bound 1." with "with
minOccurs 0 or 1, and maxOccurs 1."

MS-FS-LC1-023	
Section 2.3.3		
Editorial	

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

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

" with

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

  (element a & element b) 

which is equivalent to 

    element a, element b
  | element b, element a

"

MS-FS-LC1-025	
Section 2.3.4		
Editorial	

"element street of type xsd:string*": Explain that this is sequence of
element with name street! People may bind * to xsd:string. Also, please
use xs:string and not xsd:string.

MS-FS-LC1-029	
Section 2.4.1		
Editorial	

"In XQuery, static the input context may be defined by the processing
environment and by declarations in the Query Prolog ": Fix the sentence.

MS-FS-LC1-030	
Section 2.4.1		
Editorial	

"Evaluation works by bottom-up application of evaluation rules over
expressions, starting with evaluation of literals and variables.": From
a query processing point of view, the expressions (such as path
expressions) are actually evaluated top-down. Please explain based on an
example and call out that the bottom-up application actually still may
lead to a top-down evaluation of an expression such as /a/b/c[@d=42].

MS-FS-LC1-031
Section 2.4.1		
Editorial/Conformance	

"Statically typed implementations are required to find and report type
errors during static analysis, as specified in this document. ": 
This should be qualified as subject to implementations inferring more
precise types. Also, some people read it as that the error messages are
normatively given in the specification. Please write this clearer.

MS-FS-LC1-032	
Section 2.4.2		
Editorial	

Please call out that some of the parts of the syntax is hotlinked (since
it is not easily visible on a printed page or even on a browser).

MS-FS-LC1-033	
Section 2.4.2		
Editorial	
"FWLR" -> "FLWOR"

MS-FS-LC1-034	
Section 2.5.1		
Editorial	

"xdt: for XML Schema components and built-in types.": Actually the
XQuery/XPath built-in types. Please fix.

MS-FS-LC1-035	
Section 2.5.2		
Editorial	

"fn:distinct-nodes(node*) as node*": Has been cut. Please use a function
that still exists. Also please use the F&O formatting for generic types.

Section 1.1 Normative and informative Sections	
Technical	

Make mapping of XSD into type system normative as far as specified.
Otherwise we specify normative static semantics on top of non-normative
basics.

MS-FS-LC1-001 
Section 1 Introduction	
Editorial	

In section starting with "[XPath/XQuery] is a typed language. ": Make a
better distinction between static type inference (inferring the static
type) and static type checking for discovering errors.

There are a number of places in the Formal Semantics spec where it
chooses a static type that is more general than the most specific type 
that is deducible.

While we understand that an implementation is free to extend static typing
to produce more specific types than the Formal Semantics spec says [1],
we think it is important for the spec to choose the most specific type 
possible.

Examples of places in the Formal Semantics where a more-specific type is 
desirable:

----------------------------------------------------

1. SECTION 4.8.2 for expression

431: for expression type

Under static type analysis, when a type declaration is present,
the static environment should be extended to typing VarRef1 with type 
Type1, NOT type0.

----------------------------------------------------

2. SECTION 4.8.3, let expression

432: let expression type
bug

The let expression variable has its declared type, instead of its actual 
type,
entered into the static environment.

Under static type analysis, when a type declaration is present,
the static environment should be extended to typing VarRef1 with type 
Type1, NOT type0.

----------------------------------------------------

3. SECTION 5.12, Function Declaration

454: function return type vs declared return type

Example:
declare function foo() as xdt:anyAtomicType {return 3;}
foo() + 4

When doing static type analysis on foo() +4, should foo()'s static
type be xdt:anyAtomicType or xs:integer ?

According to the current spec, foo()'s static type is xdt:anyAtomicType.
Then foo() +4 raises static type error.

foo()'s static type should be xs:integer so that foo() +4 does
NOT raise static type error.

----------------------------------------------------

4. SECTION 6.2.8, fn:reverse function

442: explain why factored type is used here
bug/editorial

It may not be obvious why the static Type analysis for fn:reverse()
function actually returns the factored type of the function's
input sequence.

For example, consider:
fn:reverse((1, 'abc')).

The input sequence type is (xs:integer, xs:string).
After applying fn:reverse(), its most precise type should be (xs:string, 
xs:integer).

If we compute the factored type, its type
is (xs:string|xs:integer)+ , which is NOT as precise as
(xs:string, xs:integer).

Suggest: either return the most precise type (preferred solution),
or add some text to explain why a factored type is used here.

----------------------------------------------------

[1] From the Formal Semantics spec:

3.6.7 Static Typing Extensions

For some expressions, the static typing rules defined in the Formal 
Semantics are not very precise (see, for instance, the type inference 
rules for the ancestor axes — parent, ancestor, and ancestor-or-self— 
and for the function fn:root function. Some implementations may wish to 
support more precise static typing rules.

A conforming implementation may provide a static typing extensionXQ, 
which is a type inference rule that infers a more precise static type 
than that inferred by the type inference rules in the Formal Semantics. 
Given an expression Expr, the type of Expr given by the extension must 
be a subtype of the type of Expr given by the Formal Semantics. "

These are Oracle's Formal Semantics Last Call comments, editorial.

By "bugs" we mean mistakes in the text. "bugs" differ from "editorial" 
in that "bugs" significantly change the meaning of the document.

Each comment has a header, with a number, the section, section title, an 
internal-to-Oracle comment number, and a 1-line summary.

----------------------------------------------------

B1. SECTION F9.3, Sequence Group

429: Sequence Vs Choice Group
bug

Immediately below schema mapping section, "Choice groups" should be 
"Sequence groups".


----------------------------------------------------

B2. SECTION 7.2.2.1, Static Semantics of axes

443: axis:child:: of document {Type} should include text *
bug

The inference rule for child axis of document node type should include 
text nodes as well.

statEnv |- axis child:: of document {Type} : Type & 
processing-instruction *&
comment*  & text*

Note text* is missing here.


----------------------------------------------------

B3. SECTION 7.2.3.2, Dynamic semantics of node tests

449: bug in the example conclusion
bug

For the 1st example,
element bar:c of type xs:int {5}

should be

element foo:d of type xs:int {5}

since we test for foo:*


----------------------------------------------------

B4. SECTION 3.5.3, Errors and Optimization

452: add 'NOT' in the last sentence of the section
bug

The last sentence of 3.5.3 says
"In the example above, a static type error would be
raised because a path expression may be applied to an atomic value"

It should be

"In the example above, a static type error would be
raised because a path expression may NOT be applied to an atomic value"


----------------------------------------------------


B5. SECTION 3.1.2, Dynamic Context

462: dynEnv.varValue can also map an expanded variable name to #EXTERNAL
bug

In addition to Value or #IMPORTED(URI), an expanded variable name can 
also be mapped to #EXTERNAL.


----------------------------------------------------


B6. SECTION 3.4.4, Sequence Type Matching
bug

453: normalization of  document-node(ElementTest)

There should be NO () after
processing-instruction, comment, text types
when defining normalization of document-node(ElementTest)
because XQuery formal semantic type has no () for 
processing-instruction, comment, text types.

----------------------------------------------------



B7. SECTION 4.7.1, Direct Element Constructor

404: Normalization rule for Direct element constructor
bug

The normalization rule for a Direct element constructor distinguishes
between the constructor having one element-content unit from the one having
more than one element-content unit as illustrated in 4.7.1 section.

The contructor containing one element-content unit preserves the typeinfo.

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

This rule appears to contradict the XQuery 1.0 language spec section 
3.7.1.5,
type of a constructed element.
In XQuery 1.0, there is no distinction between a construct having one
element-content unit vs the one having more than one element-content unit.

If we plan to implement Michael Kay's suggestion
(documented as an editorial note in 
 section 4.7.1),
then the XQuery 1.0 spec needs to be changed to accommodate this.


----------------------------------------------------



B8. SECTION 7.6.3, Atributes in validation context

466: inference rule for the case of no attribute name present
bug

The inference rule for the case of no attribute name present is not right.

The rule is stated as:

statEnv |- axis attribute:: of element of TypeName: Type1
------------------------------------------------------------
statEnv |- in context type(TypeName) with mode ValidationMode resolves to
prime(Type2)

The conclusion should refer to Type1, NOT Type2.

----------------------------------------------------

These are Oracle's Formal Semantics Last Call comments, editorial.

By "editorial" we mean typos, plus suggestions on markup and wording to 
make the spec more readable.

Each comment has a header, with a number, the section, section title, an 
internal-to-Oracle comment number, and a 1-line summary.

----------------------------------------------------

E1. SECTION F10: Particles

430: Typo
editorial

"Particles can be either and element reference ..."
"and" should be "an"

----------------------------------------------------

E2. SECTION 4.4: Arithmetic Expressions, Core Grammar

433: Typo
editorial

"There are no Core grammar rules for value comparisons  ..."
Should be:
"There are no Core grammar rules for arithmetic expressions ..."

----------------------------------------------------

E4. SECTION 4.12.4 Castable, Normalization

437: Castable normalization rule is specified twice (cut-paste error ?)
editorial

The "normalization of castable" expr rule is listed twice.

----------------------------------------------------

E5. SECTION 7.2.2.1, Static Semantics of axes

446: Suggest subsections under 7.2.2.1
editorial

Please subsection 7.2.2.1 based on the axes access section
(child axes, parent axes,  attribute axes etc.) for readability.

----------------------------------------------------

E6. SECTION 7.2.2.1, Static Semantics of axes

444: possibly missing words 'type of'
editorial

"The static type of the attribute axis is similar to the static the 
child axis."

Should be ?

"The static type of the attribute axis is similar to the static [type 
of] the child axis."

----------------------------------------------------

E7. SECTION 2.1.3, Notations for inference rules

448: inference rules need clearer markup
editorial

The inference rules are written as a collection of premises and a 
conclusion,
written respectively above and below a
dividing line.

Having seen these rules in different fonts, browsers, print-outs, it is 
clear
that some more markup is needed to make it easier to read the rules.

Suggest: draw a box around the entire rule and/or make some
other markup around the entire rule, such as background shading.

When there are multiple inference rules listed together,
it is very hard for the reader to mentally draw the boundary around
each inference rule. This is especially true for inference rules without
premises. When there are many inference rules, some of which have
no premises and some of which have premises, listed in a cluster under
a section, it is  hard for reader to separate the inference rules.
See especially 7.2.3.1.1, 7.2.3.1.2, 7.2.3.2.2

----------------------------------------------------

E8. SECTION 7.2.3.1.2, kind tests

450: possible mis-wording in 7.2.3.1.2, 3rd paragraph
editorial

"After normalization of the kind test an XQuery type, the expression's 
type is compared to the normalized XQuery type."

Should be ?

"After normalization of the kind test [as] an XQuery type, the 
expression's type is compared to the normalized XQuery type."

----------------------------------------------------

E9. SECTION 3.4.1, Predefined Types

458: xdt:untyped definition
editorial

The definition of xdt:untyped includes xdt:untypedAny.

Presumably this was overlooked when changing xdt:untypedAny to xdt:untyped.

----------------------------------------------------

E10. SECTION 6.1.4, The fs:convert-simple-operand function

465: reference to convert_untypedAtomic
editorial

fs:convert-simple-operand function makes a reference to a function
convert_untypedAtomic. Please make a reference to 6.2.6 where
convert_untypedAtomic is defined.

convert_untypedAtomic is also used in 6.2.1, with no reference to a 
definition.

----------------------------------------------------

E11. SECTION 3.6.7, Static Typing Extensions

464: There is no definition of '<:' in 3.6.7
editorial

Suggest: add a reference to the definition of '<:' in 7.3.2.

----------------------------------------------------

E12. SECTION 4.1.4, Context Item Expression

455: static type analysis missing for context item expression
editorial

In the introduction section, it states that the context item may
be either a node or an atomic value. However, it does NOT explcitly
state that this as an inference rule in a 'static type analysis' rule.

----------------------------------------------------

E13. SECTION 6.2.2, The fn:collection and fn:doc function

439: The first premise of the first inference rule for fn:doc() is done 
twice
editorial

StatEnv |- statEnv.docType(string) = Type

premise for fn:doc() first inference rule is listed twice

----------------------------------------------------

E14. SECTION 7.2.3.2, Dynamic semantics of node tests

469: Singular used when plural required
editorial

In the second paragraph under Semantics, the phrase "are similar to 
those for axis" should read "are similar to those for axes".

----------------------------------------------------

E15. SECTION 4.7.1, Direct Element Constructors

467: Two typos
editorial

Under Normalization, the paragraph beginning "So to preserve useful type 
information" includes the phrase "constructor's that contain"; the 
apostrophe between the "r" and "s" is incorrect, because the constructor 
being discussed does not posess "that contain"...it's merely a plural 
form of "constructor".

In the same paragraph, the last sentence reads "Here is the 
normalization of the first and fourth examples above:"  There are two 
things wrong with this sentence.  First, it's unclear whether "first" 
and "fourth" are counting in reverse document order ;^) or in document 
order starting at the subheading "Normalization".  More importantly, 
the  shaded text that follows that sentence makes it clear that the 
examples are not the "first and fourth", but either the "second and 
fourth" (if in reverse document order) or the "first and third" (if in 
document order from the subheading).

----------------------------------------------------

E16. SECTION 4.7.3.6, computed comment constructors

436: computed processing-instruction
editorial

Under the normalization section, the first 3 words
"Computed processing-instruction
should be
"Computed comment"

----------------------------------------------------

E17. SECTION 4, Expression

456: static type analysis for expressions with empty type
clarification

It is a static type error for most (but not all) expressions to have the 
empty type.

Is '3+()' a static type error ?
We expect NO, because + is normalized into fs:plus() (6.1.1), which can 
return empty type.

Does 'local namespace declaration' defined in 4.7.4 raise a static type 
error,
as the static type analysis yields empty type ?

----------------------------------------------------

E18. SECTION 3.4.1, predefined types

457: definition of fs:numeric
editorial

The definition of fs:numeric does not appear to be right.
The usage of '&' and ';' and usage of _ do not seem to be right.

It should be:

define type fs:numeric restricts xs:anyAtomicType
{ xs:decimal | xs:float | xs:double}

----------------------------------------------------

E19. SECTION 2.3.3, Content models

461: '&' operator and XML SChema All
editorial

The definition in Formal Semantics of '&' operator is,
(element a & element b) =
  element a, element b
| element b , element a

The text says "The interleaved product represents all groups in XML Schema.
But "all groups in XML Schema" would result in:

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

Suggest changing this text"

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

to e.g.

"The interleaved product represents all groups in XML Schema, restricted 
to apply only on global or local element declarations with lower bound 0 
or 1, and upper bound 1."

----------------------------------------------------

E20. SECTION 7.2.3.2.2, kind tests

451: The conclusion of the inference rule for comment() test is incomplete
editorial

When the Formal Semantics document is printed (using Netscape),
the inference rule for comment nodes is printed as:

not(fn:node-kind(NodeValue) = "comment")
-----------------------------------------------------
()

The ()  conclusion should be replaced as
dynEnv|- test comment() with PrincipalNodeKind of NodeValue => ()

When the Formal Semantics document is displayed directly in a browser 
(including Netscape),
the conclusion displays as expected.

----------------------------------------------------

E21. SECTION 6.2.7, 6.2.8, fn:remove and fn:reverse function

441: 'factored type' not defined
editorial

There is no definition of 'factored type'.
Suggest defining it in 7.4 where prime type and its computation is defined,
and then reference this definition wherever 'factored type' is used.

----------------------------------------------------

E22. SECTION 5.11 - variable declaration

434: no 'static type analysis' section
editorial

There is no 'static type analysis' section for Variable declaration.

----------------------------------------------------

E23. SECTION 6.2.6, The fn:min, fn:max, fn:avg, and fn:sum functions

468: Incomplete list of types for fn:mix and fn:max
editorial

Under the subheading "Semantics", the paragraph starting "Instead of 
writing a separate judgement",
the second sentence deals with fn:min and fn:max. 

That sentence has a list of data types that incorrectly omits the types 
xs:date, xs:time, and xs:dateTime. 

As evidenced by F&O section 15.4.3, fifth paragraph, sentence beginning 
"If date/time values do not have a timezone...",
F&O properly handles fn:max and fn:min applied to those three types. 

Please add these three types to the list in the second sentence. 
(Do not add it to sentences dealing with fn:avg and fn:sum, of course.)

----------------------------------------------------

E24. SECTION 2.3.2, Item types

460: element content nodes
editorial

Section 2.3.2 says:

"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 nodes later in the formal semantics."

The spec refers to "element content type" elsewhere, but not "element 
content NODES".

----------------------------------------------------

Hi,

a question dealing with the function fs:convert-operand as described in  <> .

When having statEnv <> .xpath1.0_compatibility <>  = false, type($actual) = String and type($expected) = Integer no conversion is done, right? 

Considering a general comparison of a string and an integer value. According to the formal semantics of the general comparison, convert-operand would be called for both values but no conversion would take place actually. So I end up with a comparison of a string and an integer that is not defined (no overloaded comparison function exists taken these two types). That would force me to throw a XP0004 or XP0006 error due top the incompatible types, right?

Thanks & Cheers
Daniel

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 6.2.9

The last inference rule for fn:subsequence indicates that the types of the 
second and third arguments must be xs:integer.  In fact, from F&O Section 
15.1.3, they must be of type xs:double.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 6.2.7

The inference rule for fn:remove doesn't seem correct.  For example, for 
fn:remove(1,1), the rule yields type xs:integer.  The result type should 
not simply use the quantifier of the type of the first argument, as the 
operation may remove an item from the sequence.

If quantifier(Type) is "1" or "?", the inferred type of the result should 
be prime(Type)?; if quantifier(type) is "+" or "*", the inferred type of 
the result should be prime(Type)*.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 6.2.6

The paragraph between the two inference rules for fn:sum indicates, "The 
second form of fn:sum takes one argument, with an implicit second argument 
of the integer value 0.  In this case, the result type is the union of 
target type T and xs:integer."  However, F&O section 15.3.5 states "If the 
converted sequence is empty, then the single-argument form of the function 
returns the xs:double value 0.0e0."

The inference rule here needs to be made consistent with the description 
in F&O.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 6.2.6

The paragraph before the first inference rule states, "When the function 
variable F is fn:min or fn:max, the target type T must be one of 
xs:decimal, xs:float, xs:double, xdt:yearMonthDuration, or 
xdt:dayTimeDuration."  However, according to F&O section 15.3.3 and 
15.3.4, these functions also accept arguments of type xs:date, xs:time and 
xs:dateTime.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 4.4

The normalization rule for the unary arithmetic operators is problematic 
for values of type xs:float and xs:double.  If the operand of unary minus 
is positive zero, the result produced using the usual IEEE.738 rules for 
arithmetic ought to be negative zero, but the result of the normalized 
operation 0.0-(+0.0) will be positive zero.  Similarly, if the operand of 
unary plus is negative zero, the result ought to be negative zero, but the 
result of the normalized operation 0.0+(-0.0) will be positive zero.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 3.1.2

The penultimate paragraph refers to the "fs" namespace, and indicates that 
it is a static error to define a variable in that namespace.  However, 
section 2.5.1 indicates that the "fs:" prefix is a notational device, and 
that there is no namespace that corresponds to it.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 2.4.1

The second paragraph before the last numbered list states, "Notice that 
the separation of logical processing into phases is not meant to imply 
that implementations must separate the static analysis phase from the 
dynamic evaluation phase; processors may choose to perform all phases 
simultaneously at evaluation-time and may even mix the phases in their 
internal implementations."

This sentence should be further clarified.  If the static typing feature 
is in effect, and an error was detected by that subphase, the dynamic 
evaluation phase must not occur.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Hello,

     The following is a comment from IBM on the Last Call working draft of 
Formal Semantics.


Section 2.1.3

Some inference rules are written as if the order of the premises is 
significant, using terms like "first", "second", "then" (see last 
paragraph of section 2.1.5, for example).  If the order is signficant, 
that should be stated here.  Otherwise, those inferences should not be 
written as if the order was significant.

Thanks,

Henry (on behalf of IBM)
------------------------------------------------------------------
Henry Zongaro      Xalan development
IBM SWS Toronto Lab   T/L 969-6044;  Phone +1 905 413-6044
mailto:

Both the Formal Semantics and the internal XQuery specification seem to
allow empty text nodes, but this conflicts with the Data Model:

   6.7 Text Nodes
   6.7.1 Overview
   Text nodes must satisfy the following constraint:
     1. A text node must not contain the empty string as its content.

The formal semantics uses empty text nodes so it can suppress spaces
between adjacent enclosed expressions:

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

   4.7.1.1 Attributes
   Normalization
   [ AttributeValueContent1 ...,
     AttributeValueContentn]AttributeContent-unit, n > 1
   ==
   fs:item-sequence-to-untypedAtomic(
    [AttributeValueContent1]]AttributeContent , text { "" }, ...,
      text {""}, [ AttributeValueContentn]AttributeContent

Note also that the rule for Dynamic Evaluation of Text Node
Constructors does not check for an empty string.  Only the
static typing consider this by returning 'text?'.

Also, the informal XQuery specification has a problem here:

   3.7.3.4 Text Node Constructors
   2. If the result of atomization is an empty sequence, no text node
   is constructed. ...

However, it says nothing about a content expression that consists of
a single empty string.  I suggest removing the above sentence, and
modifying the 3rd rule:
   3. The individual strings resulting from the previous step are merged
   into a single string by concatenating them with a single space
   character between each pair.  If the resulting string is the empty
   string, no text node is constructed (and the expressions returns an
   empty sequence).  Otherwise, the resulting string becomes the content
   of the constructed text node.

Alternatively, change the data model to allow empty text nodes.  I don't
see any particular reason to prohibit them, even if they're not in the
XML infoset.  Just replace the sentence "In addition, document and
element nodes impose the constraint that two consecutive text nodes can
never occur as adjacent siblings" by adding "nor can any of their text
node children have the empty string as the content".

My recommendation:
1. Change the Data Model to allow empty text nodes.
2. Change the Text Node Constructor to allow empty string content.
3. Change element and ocument constructor normalization so that they
remove empty text nodes *and* combine adjacent text nodes.
-- 
	--Per Bothner
per@bothner.com

This is a request for the rationale as to why the quantifiers
	for "()" and "none" changed between Aug 2002 and May 2003.  In
	Aug 2002:

		quantifier(())   = 0
		quantifier(none) = 0

	In May 2003, this changed to:

		quantifier(())   = ?
		quantifier(none) = 1

	Why?  The current version seems rather odd.  Why should
	quantifier(none) be 1?

	- Paul
	  BEA Systems, Inc.

The normalization of FLWOR clauses seems wrong.
Specifically, the 'for' normalization in 4.8.1 following the
sentence:
   Therefore, a ForClause is normalized to nested for expressions:
appears to be incorrect.

Consider:

for $i in 0 to 9 for $j in 0 to 9 stable order by $j return 10*$i+j

This yields the tuple sequence:
(i=0,j=0), (i=0, j=1), (i=0, j=2) ...
so the sorted result should be:
0, 10, 20, ..., 1, 11, 21, ...

The "normalized" expression is:
for $i in 0 to 9 (for $j in 0 to 9 stable order by $j return 10*$i+j)

This performs 10 independents sorts, none of which change the order,
so the result is as if there was no order by clause:
0, 1, 2, ..., 10, 11, 12, ...
-- 
	--Per Bothner
per@bothner.com

MS-FS-LC1-058	
Section 4.1.3		
Editorial	

"It is a static error for any expression other than () to have the empty
type (see [4 Expressions].)": Make this statement less absolute: "Often
it is a static error for any expression to have the empty type. See [4
Expressions] for the detailed rules."

MS-FS-LC1-059	
Section 4.1.5		
Editorial	

"xdt:anyAtomic" -> "xdt:anyAtomicType"

MS-FS-LC1-061	
Section 4.1.5		
Editorial	

Instead of listing prototypical values, just explain what it is being
used for,

MS-FS-LC1-063	
Section 4.1.5		
Editorial	

Please clarify when dispatch based on provided union type is needed.
Most function dispatches are based on arity and not type and thus would
not lead to a successful application of this rule.

MS-FS-LC1-066	
General		
Editorial	
Please provide op: functions with links to their definition in the F&O
spec.

MS-FS-LC1-067	
Section 4.2.1/4.3.2		
Editorial	

It would be better to combine the rules into one section.

MS-FS-LC1-069	
Section 4.2.1		
Editorial	

The remainder of the static semantics of axis and node test is given in
section 7. But there is no link visible that takes one there and it is
not clear in this section how the semantics play out. Either move parts
up or add references.

MS-FS-LC1-105 
Section 4.3.3
Editorial	

Please link to section 6.2.10 where the op:union et al are defined
instead to 6.

MS-FS-LC1-112 
General
Editorial/Technical

Please also refer to the section where the dynamic semantics of the
functions is specified. Not only the function invocation!

MS-FS-LC1-115 
Section 4.7.1
Editorial	

"The next example contains six element-content units:": depends on the
XQuery boundary whitespace handling rules since you have boundary
whitespace in your query.

MS-FS-LC1-117 
Section 4.7.1
Editorial	

The section numbering needs to be better. Elements do not have their own
subsections but attributes do. Others are in separate 4.7.2.

MS-FS-LC1-124 
Section 4.7.3.4
Editorial

"The static semantics checks that the argument expression has type
xs:string." This is guaranteed by the normalization. So why do we need
this condition?

MS-FS-LC1-128 
Section 4.8	
Editorial

There are several places (including the title) where we refer to FLWR
instead of FLWOR. Please fix.

MS-FS-LC1-131 
Section 4.12.2
Editorial

Replace " an optional VarRef, which is bound the value of the input
expression" with " an optional VarRef, which is bound to the value of
the input expression"

Appendix B.2
Technical	

The table implies static types but the semantic described is the dynamic
semantics. This needs to be rectified (for example, what if the static
type of A is xs:integer? ? What is the result of () eq () (static error
if static typing? () dynamically.).

MS-FS-LC1-109	
Appendix B.2		
Editorial	

Please replace "Gregorian" with "Australian" :-)

MS-FS-LC1-111	
Appendix B.2
Editorial	

fs:minus: Decimal -> xs:decimal

Section 6.2.10		
Editorial	

Some spurious ; in judgment for op:intersection

Appendix B.2
Technical	

fs:is-same-node: Here you indicate static types. use this for the other
ops above as well and provide static and dynamic semantics. Also fix
node to be node().

Section 4.2.2		
Technical	

Dynamic dispatch of positional predicate is problematic for performing
implementations. See also comments MS-XQ-LC1-065, MS-FS-LC1-114.

Section 4.3.1
Technical	

Do we allow expr1 to expr2 where either expr1 or expr2 have a static
type of atomic? ? If so, we either need to extend the op:to signature or
make it clear that this is allowed during normalization.

Section 4.7.2
Technical	

CDATA should not be treated as a constructor. The XQuery parser should
take care of it before it gets to the F.S. level.

Section 4.7.1
Technical

The whole business of distinguishing element content to sometimes
preserve content type is incompatible with the dynamic semantics of the
construction. With the three current validation modes on construction,
we cannot infer statically some preserved type of the content. Please
remove this complexity from the spec.

Note: Even with preserve mode, we cannot preserve atomic type
information.

This will also simplify the static typing of construction and make the
section easier to understand.

Section 4.3.2
Technical	

In the case of a literal numeric, shouldn't we have also have a special
normalization rule for last()

Section 4.6.
Technical	

As mentioned in MS-FS-LC1-068, we should not use the full power of
fn:boolean() since we need to be able to statically dispatch on
predicates.

Section 4.7.2
Technical	

The construction of comments and Pis uses the attribute content
normalization that will perform entitization and escaping. This should
not occur when constructing comments and Pis. Instead certain characters
sequences (- -- etc) need to be treated specially in the context of
comment constructions.

Sections 4.7.3.1/2, 4.13
-	

We will not review these sections due to the changes with respect to
validation and construction. We expect them to be submitted separately
for a review once the changes have been made.

Section 4.7.3.3	
Technical

The document node constructor should not erase type information on its
content. It should keep that information (always).

Section 6.1.6
Technical

fs:item-sequence-to-node-sequence(): items_to_nodes() should collapse
atomictype*/+ to text and text*/+ to text.

Section 4.7.3.5	
Technical

Normalization is using two things not available in XQuery: A union
sequence type (just call this out), and casting from string to QName
(please fix). Since we raise an error if the QName is not an NCName, we
should instead use NCName (which happens to be a subtype of xs:string).
This would simplify the normalization and still give us type safety.

Section 4.8.4
Technical

The static type for order by seems wrong:
Assume that element person can contain multiple phone elements of type
xs:int. Then the following expression should be a static error:

for $p in /person order by $p/phone return $p

Since there is more than one phone per person. Also we need rules to
deal with type promotion of numeric, untyped and other types.

Section 4.12.4
Editorial/Technical

Replace 
"[Expr castable as AtomicType]Expr 
== 
let $v as xdt:anyAtomicType? := fn:data([ Expr ]Expr) return 
$v castable as AtomicType? " 
with 
"[Expr castable as AtomicType ?]Expr 
== 
let $v as xdt:anyAtomicType? := fn:data([ Expr ]Expr) return 
$v castable as AtomicType? "

Section 4.12.5
Technical

Constructor functions now cast to T?, thus we request the following
normalization:

[AtomicType(Expr)]Expr 
== 
[(Expr) cast as AtomicType? ]Expr

Section 4.7.4
Editorial/Technical

Since a namespace declaration only accepts string literals, the
normalization and static semantics judgment seem like overkill. There is
no need for the casting to untyped and then string and there is no need
to check for the input type (since the parser would have not allowed
anything else to go through).

Section 4.8.3
Editorial/Technical

Please add a sentence what happens if a variable with the name already
exists or add a reference to the variable name and scoping rules.

Section 4.7.3.4

Technical

 

"The type is zero-or-one, because no text node is constructed if the
argument of the text node constructor is the empty string.": Now the
empty text node is allowed. Please align with that decision.

Section 4.12.3/4
Technical

The current normalization of cast as/castable seems to raise a static
error if I have an expression E cast as T and E infers to be of static
type ET?. This means that most applications of cast as T will lead to
static errors. Shouldn't this be a dynamic error?

Section 4.1.5		
Editorial/Technical	

"SequenceType <: xs:anySimpleType" -> "SequenceType <:
xdt:anyAtomicType*" (no named union types or list types can be sequence
types!)

Section 4.1.5		
Technical	

"if the expected type is a union of atomic types then this check is
performed separately for each possibility": Remove. The expected type
cannot be a union of atomic types. Or did you mean the inferred type?

General		
Technical	

The formal semantics raises both static type errors and dynamic type
errors not differentiating that under static typing, no dynamic type
errors should occur. This needs to be made explicit. With static typing
on, all type errors need to be detected statically (conservative static
typing!).

Section 4.1.5		
Technical	

What happens if I have an inferred type of a union of atomic (xs:int |
xs:double) and I find a function expecting xs:double. The rule doing
promotion does not apply, the union rule also does not apply it seems.
Please clarify.
Also, is xs:integer? treated as an atomic type or a union of xs:integer
| empty() ?

Section 4.1.1
Editorial/Technical	

Mention that literal overflows are raised during parsing.

MS-FS-LC1-070
Sections 7.2.2.1/7.2.3.1
Editorial	

Add more whitespace before the inferences 
statEnv |- axis Axis of none : none 
statEnv |- axis Axis of empty : empty 

MS-FS-LC1-075 
Section 7.1.4
Editorial	

Sometimes the type lookup results in just a type name, sometimes it
returns "of type Typename". Please be consistent.

MS-FS-LC1-077 
Section 7.1.10
Editorial

Can you add a more complex example that shows restrictions and
derivation?

MS-FS-LC1-080	
Section 7.1.7
Editorial

"if the complex type is mixed, interleaves the type with a sequence of
text nodes and xdt:anyAtomicType.": Note that the atomic type is or'ed
and not part of the interleave adjustment.

MS-FS-LC1-081
Section 7.1.9
Editorial/Technical

"statEnv |- Type2 is Type1 extended with union interpretation of
TypeName 
statEnv |- Mixed? Type1 adjusts to Type2 
------------------------------------------------------------------------
--------
statEnv |- of type TypeName expands to Type2 
" -> Are the number mixed up?

MS-FS-LC1-084
Section 7.1.6
Editorial	

Please add example.

MS-FS-LC1-095	
Section 7.2.2.1
Editorial	

Please remove the "improved" version for ancestor axis unless we fix the
type inference for the parent axis!

MS-FS-LC1-096
Section 7.2.3.1.1
Editorial

"statEnv |- QName1 of elem/type expands to expanded-QName 
statEnv |- QName2 of elem/type expands to expanded-QName": 
Add subscripts to expanded-QName and add an equality condition of the
two expanded Qnames (same for attributes)

MS-FS-LC1-097	
Section 7.2.3.1.1
Editorial	

Please add more whitespace between inference rules. The current spacing
is unreadable.

MS-FS-LC1-098
Section 7.2.3.1.1
Editorial

Replace 
"statEnv |- test * with "element" of element prefix:local TypeSpecifier?
: element prefix:local TypeSpecifier?"
With
"statEnv |- test * with "element" of element QName TypeSpecifier? :
element QName TypeSpecifier?"

Not every QName has a prefix! (same holds for attributes)

MS-FS-LC1-099
Section 7.2.3.1.1
Editorial	

How do we deal with testing an element name foo against element() ? I
would assume that the inferred type is element(foo)? and not
element(foo). Same for a against a|b. The result should be a? and not a
or raise an error. Same issues with *:b test a:*: should be a:b? and not
a:b. Please clarify the use of ? for syntactic purposes and as
Occurrence indicator

MS-FS-LC1-100
Section 7.2.3.1.1
Editorial	

With the adoption of element(name) being the same as the name name test,
can we simplify the specification by making them map to the same rules?

MS-FS-LC1-101
Section 7.2.3.1.2
Editorial	

"Document kind test" etc: What should be the editorial status of these
words? Title? Sentence?

MS-FS-LC1-102
Section 7.2.3.1.2
Editorial	

What should the following inferred type be: Inferred:
document(element(A), Kindtest: document(element(*,T)). That seems to be
document(element(a,T)?). However, I think it should be
document(element(a,T))?

MS-FS-LC1-103
Section 7.2.3.1.2
Comment	

We have not reviewed Element and Attribute kind tests since they will be
changed due to the change in SequenceType semantics.

MS-FS-LC1-108
Section 7.4
Editorial

The quantifier composition | and . (dot) are the same. Just use one of
them.

Section 7.4

Technical

 

Prime(empty) = none: How can we get none as the prime type? Isn't that
leading to errors since none reflects the type of an error? Why not =
empty? For example, you say:

prime(element a | empty)                  = element a

But isn't this element a | none? And doesn't none propagate (so that we
propagate errors?)

Section 7.2.3.1.2
Technical

"
------------------------------------------------------------------------
--------
statEnv |- test node() with PrincipalNodeKind of NodeType : NodeType 

If none of the above rules apply, then the node test returns the empty
sequence and the following rule applies:

statEnv |- test node() with PrincipalNodeKind of NodeType : empty
": 

Remove the judgment. This is confusing and is in contradiction to the
rule before the sentence. As fallback, it also does not cover any of the
other kind tests!

Section 7.2.2.1
Technical

"
------------------------------------------------------------------------
--------
statEnv |- axis ancestor:: of NodeType : element* 

Note that this rule will always result in the type (element | document)*

": Seems to contradict each other. Please fix the judgment.

Section 7.2.2.1
Technical

Replace 
"statEnv |- axis descendant:: of Type1 : Type2 
------------------------------------------------------------------------
--------
statEnv |- axis descendant-or-self:: of Type1 : (prime(Type1) |
prime(Type2))* "
with
"statEnv |- axis descendant:: of Type1 : Type2 
------------------------------------------------------------------------
--------
statEnv |- axis descendant-or-self:: of Type1 : Type1 | Type2
"

Do the same for ancestor-or-self.

Section 7.2.2.1
Editorial/Technical

"statEnv |- ElementType type lookup Nillable? TypeReference 
Type = (Type1, Type2) 
statEnv |- Type1 <: attribute * 
statEnv |- Type2 <: ElementContentType * | xdt:anyAtomicType * 
------------------------------------------------------------------------
--------
statEnv |- Type has-attribute-content Type1 
" -> Why the type lookup?

Section 7.2.2.1
Technical	

has-attribute-content: Is the result type an interleave of all
attributes or a union?

Sections 7.1.7/7.1.8
Technical	

The typed BuiltInAttributes should not be added if the content type is
untyped, since the untyped content could contain such a named attribute
that is containing a different value.

Section 7.1.8
Technical	

"fs:anyURIlist" -> make it an anonymous type since there is no such
named type in XML Schema.

Section 7.1.6
Editorial/Technical

Since we now use the union expansion, do we still need to add "|
xdt:anyAtomicType"? Since we know will get the more precise subtypes
anyway...

Section 7.1.5/7.1.7
Technical

"Type2 extended by (processing-instruction? & comment?)*":

Extended by uses "," for adding element content. This clearly is
incorrect for adding PI and comment interleaves since they can appear in
lots of places. 

For example, assume that Type2 is ((a|b), c )& d.
Then the above would yield ((a|b), c )& d, (processing-instruction? &
comment?)*

Which is incorrect. It should yield:

((a|b) & (processing-instruction? & comment?)*, c &
(processing-instruction? & comment?)*) & (d & (processing-instruction? &
comment?)*)

Section 7.1.10
Technical	

The expanded type union should preserve whether the subtypes are mixed
or not so the later adjustment will add the text nodes.

Section 7.1.6
Technical	

" ElementContent & text* " does not match: If the Element content is a,
b, then (a,b) & text* does not match (a, text, b) even though mixed
content allows that. 

Please make it explicit or use a new mix operator.

Section 7.1.10
Technical	

"statEnv.typeDefn(expanded-QName) => define type TypeNameR,1 restricts
TypeName0 Mixed? { TypeR,1? }": There are many rules that look-up
different type definitions using the same expanded-QName. This looks
like a bug.

Section 7.1.7
Editorial/Technical

"statEnv |- Type1 mixes to Type2 
statEnv |- Type2 extended by BuiltInAttributes is Type3 
statEnv |- Type3 & processing-instruction* & comment* is Type4 ":
What is the meaning of the last is? Is that Type3 extended by pi and
comments? Also see comment on extended by...

Section 7.1.4
Technical	

Replace 
"statEnv |- ElementName of elem/type expands to expanded-QName 
statEnv.elemDecl(expanded-QName) undefined 
------------------------------------------------------------------------
--------
statEnv |- element ElementName type lookup Nillable? xdt:untyped "
with
"statEnv |- ElementName of elem/type expands to expanded-QName 
statEnv.elemDecl(expanded-QName) undefined 
------------------------------------------------------------------------
--------
statEnv |- element ElementName type lookup T"

where T is determined by the context (was the containing element of type
xdt:untyped or xs:anyType?). Depending on resolution of preserve mode on
data model, this comment also applies to attribute lookup.

Section 7.2.2.1
Technical	

Can we improve the following rule:
Type = Type1, Type2 
statEnv |- Type1 <: attribute * 
statEnv |- Type2 <: xdt:anyAtomicType + 
------------------------------------------------------------------------
--------
statEnv |- Type has-node-content text ? 

to take list types (+ needs to be *) and string types into account?

Section 7.2.2.1
Technical	

Why is it ElementContentType + and not ElementContentType * in judgment
has-node-content?

Section 7.2.2.1
Technical	

PI's and comments can occur before, after and inbetween the elements
given by the Type of the document. Thus the following rule:
 
------------------------------------------------------------------------
--------
statEnv |- axis child:: of document { Type } : Type &
processing-instructions* & comment* 

should be:
 
------------------------------------------------------------------------
--------
 statEnv |- axis child:: of document { Type } : (pi? & cmt?)* ,
interspersepicmt(Type),  (processing-instructions? & comment?) 

Or introduce a new symbol to denote the interspersing semantics instead
of misusing &.

Hi,

the latest XQuery Formal Semantics defines the fs:convert-operand()
function in Section 6.1.3 [1].  In a nutshell, fs:convert-operand()
casts its first argument to the type of a given sencond argument, if it
had been a subtype of xdt:untypedAtomic before.  Otherwise the first
argument is returned unchanged.

The type of fs:convert-operand(), however, is defined as

 fs:convert-operand($actual as item *,
                    $expected as xdt:anyAtomicType)
     as xdt:anyAtomicType ?  .

Note that it allows an arbitrarily long sequence of items as its first
argument.  The return value, however, is a sequence of at most length
one.

The specifications only consider the case where $actual has a length no
longer than one.  So the return value for $actual being a longer
sequence remains undefined.

fs:convert-operand() could easily be fixed by restricting $actual to an
optional item (item?).  This, however, would make queries such as XMark
11 [2] illegal:

for $p in fn:doc("auction.xml")/site/people/person return
  let $l :=
    for $i in document("auction.xml")/site/open_auctions/open_auction/initial
      where $p/profile/@income > (5000 * $i/text())
      return $i
    return
      element items {
        attribute name { $p/name/text() }
        text { count ($l) }
      }

Note the `5000 * $i/text()'.  $i/text() evaluates to node*.  The Formal
Semantics rule for Arithmetics [3] applies fn:data(), returning an
xdt:untypedAtomic* on the non-validated document.  If the first argument
of fs:convert-operand() were restricted to item? it could not be applied
to `$i/text()', making the above query illegal.
 
Regards

Jens Teubner

[1] 
[2] 
[3] 

-- 
Jens Teubner
University of Konstanz, Department of Computer and Information Science
D-78457 Konstanz, Germany
Tel: +49 7531 88-4379     Fax: +49 7531 88-3577


Statistics show that most people are in
the majority, while a few are in the minority.
                         -- Nitin Borwankar