- From: Michael Dyck <jmdyck@ibiblio.org>
- Date: Sat, 17 Apr 2004 16:56:15 -0700
- To: public-qt-comments@w3.org
This is a resend of the submission I made a couple days ago:
http://lists.w3.org/Archives/Public/public-qt-comments/2004Apr/0072.html
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
Received on Saturday, 17 April 2004 19:58:38 UTC