- From: Michael Dyck <jmdyck@ibiblio.org>
- Date: Thu, 15 Apr 2004 02:13:22 -0700
- To: public-qt-comments@w3.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