W3C home > Mailing lists > Public > public-qt-comments@w3.org > April 2004

[FS] lots of comments on the Formal Semantics

From: Michael Dyck <jmdyck@ibiblio.org>
Date: Thu, 15 Apr 2004 02:13:22 -0700
To: public-qt-comments@w3.org
Message-id: <407E5232.261EBC7E@ibiblio.org>

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


Lines beginning with '#' are quotes from the spec.
Lines beginning with '>' are suggested replacement text.

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

TRANS-SECTION COMMENTS

'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 )
________

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"
    "/"
________

# 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).
________

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

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

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

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

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

# 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 kinds of sloppy.
________

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

# . . . 
Change to:
> ...
________

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

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

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

# 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()
________

# 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.
________

# 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:
    AttributeAll
    Error
    URI-or-EmptyNamespace
    Variable  (replace with expanded-QName?)

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

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

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 are "mappings" (or "dictionaries"), if
you like). Note that after section 3, statEnv and dynEnv *are* generally
referred to as "environments".)
________

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.
________

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.
________

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

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

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 }
________

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

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

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

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

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

# 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

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

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

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.
________

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'.
________

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)
________

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

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

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

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

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

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

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?
________

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

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

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

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

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

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

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

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

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

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

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.
________

STA / rule 3 / premise 1,2
Occurrences of 'not' should be in bold.
________

STA / rule 3 / premise 1,2
Append a right paren.
________

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

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

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.
________

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.
________

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

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.
________

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

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

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.
________

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

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

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

------------------------------------------------------------------------
4.2.1.2

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

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

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

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

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

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

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).
________

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).
________

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.
________

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.
________

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.
________

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

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
________

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.
________

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

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

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

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 ...
________

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )
________

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)
________

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

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

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

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

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

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.
________

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 ) ...
________

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

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.)
________

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

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

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

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

Prepend 'statEnv |-'.

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

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

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

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

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

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?
________

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

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

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

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.
________

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

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

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

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

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)
________

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

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

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.
________

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

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

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
________

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

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

(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"?

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

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

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

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
________

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 ...
________

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

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

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".
________

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

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

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.
________

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
________

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

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

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

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)
________

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

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

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

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

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.)
________

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
________

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

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

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

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

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) )
________

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

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

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

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

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

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
________

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

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

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

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

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

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

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

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

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

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

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

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

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

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.
________

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.
________

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

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

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; ...
________

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

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.
________

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).
________

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

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

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

------------------------------------------------------------------------
6.2.1

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
________

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

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

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'.
________

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

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.
________

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

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

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.
________

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

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

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

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

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

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

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

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

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

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

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

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)

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

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) ..
________

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 '*'.
________

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

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

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

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.

What, no "Semantics" header?
________

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

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

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

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
________

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

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.

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

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

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

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

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

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

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

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

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

------------------------------------------------------------------------
7.3.2

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

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

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

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

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

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

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

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

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?
________

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

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

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.
________

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.
________

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

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) ..
________

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?
________

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

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

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.
________

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

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

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

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.
________

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

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

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

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

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

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

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

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

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

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

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

-Michael Dyck
Received on Thursday, 15 April 2004 05:14:32 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 7 January 2015 15:45:19 UTC