This document identifies the status of Last Call issues on XQuery 1.0 and XPath 2.0 Formal Semantics as of February 11, 2005.
The formal semantics has been defined jointly by the XML Query Working Group and the XSL Working Group (both part of the XML Activity).
The February 11, 2005 working draft includes a number of changes made in response to comments both received during the Last Call period that ended on Feb. 15, 2004. The working group is continuing to process these comments, and additional changes are expected.
Public comments on this document and its open issues are invited. Comments should be sent to the W3C mailing list public-qt-comments@w3.org. (archived at http://lists.w3.org/Archives/Public/public-qt-comments/) with “[FS]” at the beginning of the subject field.
Most issues are classified as either “substantive”, meaning the editor believes technical changes to the document are required to address them, or “editorial”, meaning that the issue is one of specification clarity not technical correctness.
An issue transitions through several states. Issues tracking begins when an issue is “raised”. After discussion, the Working Group may have “decided” how to resolve the issue. This decision is “announced” and hopefully “acknowledged” by external commenters. For the most part, once an issue is decided, it is considered closed.
Last call issues list for xquery-semantics (up to message 2004Mar/0246).
There are 90 issue(s).
90 raised (90 substantive), 0 proposed, 0 decided, 0 announced and 0 acknowledged.
Id | Title | Type | State | Doc. |
+qt-2004Apr0126 | [FS] 4.1.5 Function Calls: eval of imported function | substantive | raised | FS |
+qt-2004Apr0124 | [FS] overlap in Formal and Core symbols | substantive | raised | FS |
+qt-2004Apr0123 | [FS] A few comments on formal semantics | substantive | raised | FS |
+qt-2004Apr0107 | [FS] lots of comments on the Formal Semantics | substantive | raised | FS |
+qt-2004Apr0103 | [FS] Normalization of Quantified expression | substantive | raised | FS |
+qt-2004Apr0102 | [FS] MS-FS-LC1-056 | substantive | raised | FS |
+qt-2004Apr0101 | [FS] MS-FS-LC1-055 | substantive | raised | FS |
+qt-2004Apr0099 | [FS] MS-FS-LC1-053 | substantive | raised | FS |
+qt-2004Apr0098 | [FS] MS-FS-LC1-048 | substantive | raised | FS |
+qt-2004Apr0097 | [FS] MS-FS-LC1-045 | substantive | raised | FS |
+qt-2004Apr0096 | [FS] MS-FS-LC1-047 | substantive | raised | FS |
+qt-2004Apr0095 | [FS] Editorial comments on section 3 | substantive | raised | FS |
+qt-2004Apr0094 | [FS] MS-FS-LC1-044 | substantive | raised | FS |
+qt-2004Apr0093 | [FS] MS-FS-LC1-036 | substantive | raised | FS |
+qt-2004Apr0092 | [FS] MS-FS-LC1-039 | substantive | raised | FS |
+qt-2004Apr0100 | [FS] MS-FS-LC1-028 | substantive | raised | FS |
+qt-2004Apr0091 | [FS] MS-FS-LC1-026 | substantive | raised | FS |
+qt-2004Apr0090 | [FS] MS-FS-LC1-027 | substantive | raised | FS |
+qt-2004Apr0088 | [FS] MS-FS-LC1-018 | substantive | raised | FS |
+qt-2004Apr0087 | [FS] MS-FS-LC1-024 | substantive | raised | FS |
+qt-2004Apr0089 | [FS] MS-FS-LC1-017 | substantive | raised | FS |
+qt-2004Apr0086 | [FS] MS-FS-LC1-021 | substantive | raised | FS |
+qt-2004Apr0084 | [FS] MS-FS-LC1-011 | substantive | raised | FS |
+qt-2004Apr0083 | [FS] MS-FS-LC1-016 | substantive | raised | FS |
+qt-2004Apr0082 | [FS] Editorial comments on section 2 | substantive | raised | FS |
+qt-2004Apr0085 | [FS] MS-FS-LC1-002 | substantive | raised | FS |
+qt-2004Apr0081 | [FS] Editorial comments on section 1 (MS-FS-LC1-001) | substantive | raised | FS |
+qt-2004Apr0077 | ORA-FS-004-E: Formal Semantics comments, precise types | substantive | raised | FS |
+qt-2004Apr0076 | ORA-FS-003-E: Formal Semantics comments, bugs | substantive | raised | FS |
+qt-2004Apr0078 | ORA-FS-001-E: Formal Semantics comments, editorial | substantive | raised | FS |
+qt-2004Apr0063 | [XQuery] fs:convert-operand / General comparison | substantive | raised | FS |
+qt-2004Apr0015 | [FS] IBM-FS-107: Wrong types for arguments of fn:subsequence | substantive | raised | FS |
+qt-2004Apr0014 | [FS] IBM-FS-106: Quantifier of inferred type of fn:remove | substantive | raised | FS |
+qt-2004Apr0013 | [FS] IBM-FS-105: Inferred type of fn:sum with one argument | substantive | raised | FS |
+qt-2004Apr0012 | [FS] IBM-FS-104: fn:min, fn:max need to accept date/time arguments | substantive | raised | FS |
+qt-2004Apr0011 | [FS] IBM-FS-103: Normalization for unary arithmetic affects negative zero | substantive | raised | FS |
+qt-2004Apr0010 | [FS] IBM-FS-102: fs prefix does not refer to a namespace | substantive | raised | FS |
+qt-2004Apr0009 | [FS] IBM-FS-101: Logical separation of phases | substantive | raised | FS |
+qt-2004Apr0008 | [FS] IBM-FS-100: Significance of order of premises in inference rules | substantive | raised | FS |
+qt-2004May0037 | [FS] [XQuery] empty text nodes | substantive | raised | FS |
+qt-2004May0029 | FS quantifiers | substantive | raised | FS |
+qt-2004Jun0110 | [FS] for clause normalization | substantive | raised | FS |
+qt-2004Jun0107 | [FS] Editorial comments on Section 4 and a General Editorial remark | substantive | raised | FS |
+qt-2004Jun0106 | [FS] MS-FS-LC1-110 | substantive | raised | FS |
+qt-2004Jun0105 | [FS] Editorial Comments on Appendix B.2 | substantive | raised | FS |
+qt-2004Jun0104 | [FS] MS-FS-LC1-106 | substantive | raised | FS |
+qt-2004Jun0103 | [FS] MS-FS-LC1-113 | substantive | raised | FS |
+qt-2004Jun0101 | [FS] MS-FS-LC1-068 | substantive | raised | FS |
+qt-2004Jun0100 | [FS] MS-FS-LC1-087 | substantive | raised | FS |
+qt-2004Jun0099 | [FS] MS-FS-LC1-118 | substantive | raised | FS |
+qt-2004Jun0102 | [FS] MS-FS-LC1-116 | substantive | raised | FS |
+qt-2004Jun0097 | [FS] MS-FS-LC1-088 | substantive | raised | FS |
+qt-2004Jun0096 | [FS] MS-FS-LC1-114 | substantive | raised | FS |
+qt-2004Jun0098 | [FS] MS-FS-LC1-119 | substantive | raised | FS |
+qt-2004Jun0094 | [FS] MS-FS-LC1-120: Skipped Sections in 4 due to reworking of validation and construction | substantive | raised | FS |
+qt-2004Jun0093 | [FS] MS-FS-LC1-121 | substantive | raised | FS |
+qt-2004Jun0092 | [FS] MS-FS-LC1-122 | substantive | raised | FS |
+qt-2004Jun0091 | [FS] MS-FS-LC1-126 | substantive | raised | FS |
+qt-2004Jun0090 | [FS] MS-FS-LC1-130 | substantive | raised | FS |
+qt-2004Jun0089 | [FS] MS-FS-LC1-134 | substantive | raised | FS |
+qt-2004Jun0095 | [FS] MS-FS-LC1-133 | substantive | raised | FS |
+qt-2004Jun0087 | [FS] MS-FS-LC1-127 | substantive | raised | FS |
+qt-2004Jun0086 | [FS] MS-FS-LC1-129 | substantive | raised | FS |
+qt-2004Jun0085 | [FS] MS-FS-LC1-125 | substantive | raised | FS |
+qt-2004Jun0084 | [FS] MS-FS-LC1-132 | substantive | raised | FS |
+qt-2004Jun0083 | [FS] MS-FS-LC1-060 | substantive | raised | FS |
+qt-2004Jun0082 | [FS] MS-FS-LC1-062 | substantive | raised | FS |
+qt-2004Jun0080 | [FS] MS-FS-LC1-065 | substantive | raised | FS |
+qt-2004Jun0079 | [FS] MS-FS-LC1-064 | substantive | raised | FS |
+qt-2004Jun0081 | [FS] MS-FS-LC1-057 | substantive | raised | FS |
+qt-2004Jul0028 | [FS] Editorial comments on section 7 | substantive | raised | FS |
+qt-2004Jul0027 | [FS] MS-FS-LC1-107 | substantive | raised | FS |
+qt-2004Jul0026 | [FS] MS-FS-LC1-104 | substantive | raised | FS |
+qt-2004Jul0025 | [FS] MS-FS-LC1-094 | substantive | raised | FS |
+qt-2004Jul0024 | [FS] MS-FS-LC1-093 | substantive | raised | FS |
+qt-2004Jul0023 | [FS] MS-FS-LC1-092 | substantive | raised | FS |
+qt-2004Jul0022 | [FS] MS-FS-LC1-091 | substantive | raised | FS |
+qt-2004Jul0021 | [FS] MS-FS-LC1-090 | substantive | raised | FS |
+qt-2004Jul0020 | [FS] MS-FS-LC1-086 | substantive | raised | FS |
+qt-2004Jul0019 | [FS] MS-FS-LC1-083 | substantive | raised | FS |
+qt-2004Jul0018 | [FS] MS-FS-LC1-085 | substantive | raised | FS |
+qt-2004Jul0017 | [FS] MS-FS-LC1-082 | substantive | raised | FS |
+qt-2004Jul0016 | [FS] MS-FS-LC1-079 | substantive | raised | FS |
+qt-2004Jul0015 | [FS] MS-FS-LC1-076 | substantive | raised | FS |
+qt-2004Jul0014 | [FS] MS-FS-LC1-078 | substantive | raised | FS |
+qt-2004Jul0013 | [FS] MS-FS-LC1-074 | substantive | raised | FS |
+qt-2004Jul0012 | [FS] MS-FS-LC1-071 | substantive | raised | FS |
+qt-2004Jul0011 | [FS] MS-FS-LC1-072 | substantive | raised | FS |
+qt-2004Jul0010 | [FS] MS-FS-LC1-073 | substantive | raised | FS |
+qt-2004Aug0088 | Formal Semantics: fs:convert-operand() erroneous? | substantive | raised | FS |
XQuery 1.0 and XPath 2.0 Formal Semantics W3C Working Draft 20 February 2004 4.1.5 Function Calls Dynamic Evaluation rule 2 (imported function) The last premise is incorrect. It would re-evaluate the whole function call in the imported module's environment. Instead, it should be more like: dynEnv1 |- expanded-QName( Value1', ..., Valuen' ) => Value' -Michael Dyck
XQuery 1.0 and XPath 2.0 Formal Semantics W3C Working Draft 20 February 2004 The Formal grammar and the Core grammar both define the following non-terminals: AttributeName ElementName ItemType TypeName Because the inference rules use symbols from both the Formal and Core languages, this would seem to cause an ambiguity. Now, it's true that the Formal and Core definitions of AttributeName are the same (both simply derive QName). Similarly for ElementName. And it's also true that ItemType doesn't occur in the inference rules (though are you certain it won't in a future draft?). But TypeName has different Formal and Core definitions (Formal allows AnonymousTypeNames, Core doesn't), and it does occur in the inference rules, so I think there is an ambiguity there. But regardless of whether there is or isn't a formal ambiguity, there's presumably the opportunity for confusion, which could be removed simply by renaming some symbols. (Note that, in addition to the above symbols, the Formal and *XQuery* languages also both define AttributeValue. However, because the appearance of XQuery constructs in inference rules is fairly limited, I suppose an ambiguity does not arise. But again, it would reduce the chance of confusion if you renamed one of them.) -Michael Dyck
Dear FS Editors, Below is a list of some possible issues with FS Feb 2004 Working Draft, with occasional suggestions, ordered by FS sections. Hopefully, it does not come too late to be useful... My apologies if there are too many already known issues and false alarms down there. Sincerely, Vladimir Gapeyev ------------------------------------------------------------------------ [General] Shouldn't normative inference rules have formal identifiers by which they can be referenced, similar to those of grammar productions? [2.5.1 Namespaces, last para] The term "host language" appears here and nowhere else in the spec! Should it just say "language" or "XQuery or XPath"? [3.1, just before 3.2] The statement in this section that $fs:dot, $fs:position and $fs:last are _built-in_ variables in FS is confusing when one considers their use in the normalization rules of Section 4: One could assume that if the variables are built-in they somehow magically contain appropriate values whenever referenced. However, the normalization rules treat them as regular variables, by binding them in for and let expressions whenever their value is changed -- no magic! Suggestion: Perhaps the def of these variables should be moved to Section 4 where it would just say that they are special variables used in normalization rules that are assumed to be distinct from any user variables. They are supposed to mimic the functionality of '.', fn:position, fn:last, and this is achieved by careful formulation of the normalization rules, no magic. In light of this I wonder, if in addition to the rule [ . ] == $fs:dot one also needs the rules [ fn:last() ] == $fs:last [ fn:position() ] == $position ? [3.1, just before 3.2] It says: "Variables with the "fs" namespace prefix are reserved for use in the definition of the Formal Semantics. It is a static error to define a variable in the "fs" namespace." This appears to be at odds with the last para of 2.5.1 saying that entities with fs prefix are abstract, introduced just for the purposes of this spec and are not supposed to be provided in the host language. So, under the 2.5.1 proviso, defining the fs prefix in a user query should lead to absolutely no trouble! [3.1.1 Static Context, last 2 para before 3.1.1.1] These paragraphs define functions fs:active-ns and fs:get_ns_from_items, which perhaps better be done in 6.1. The descriptions of the functions aren't very clear... [fs:active-ns] Perhaps should say "fs:active-ns(statEnv) returns all prefix mappings from statEnv.namespace that are of 'active' kind." [fs:get_ns_from_items]: The expanded-QName and URI appear in the def from nowhere and their role is unclear! It also should say that the return are prefix-to-namespace mappings with kind indication, not just namespaces. [4.2 Path Expressions, just before 4.2.1] It appears that according to the spec the last normalization rule, the one for [ StepExpr1 "/" StepExpr2 ]_Expr is supposed to handle all "seminormalized" path expressions of the form StepExpr1 / StepExpr2 / .... / StepExpr_n. However, RelativePathExpr is defined as [71 (XQuery)] RelativePathExpr ::= StepExpr (("/" | "//") StepExpr)*, i.e. it can contain one or more StepExpr, while the rule in question handles the case of exactly two. Perhaps this can be fixed just by changing StepExpr2 to RelativePathExpr in the rule. [4.2 Path Expressions] It is said in "Core Grammar" section: "The grammar for path expressions in the Core starts with the StepExpr production". According to the productions [52,58,59(Core)] in 4.2.1. it should be rather said "starts with AxisStep production". [4.2.1 Steps -- Dynamic Evaluation, also Static Type Analysis] The eval rule for the judgment dynEnv |- Axis NodeTest => Value refers to the variable $fs:dot. Somehow it does not feel right to make the Core semantics depend on the name of an auxiliary variable, especially if one takes the position (see also comments for [3.1]) that $fs:dot is a usual Core variable, albeit introduced for special purposes during normalization. Suggestion: Extend the Core syntax to contain an explicit step application construct. In more detail: (1) Introduce an expression form Expr / AxisStep (or PrimaryExpr / AxisStep, or even $Var / AxisStep -- if more restrictive syntax is desired). The semantics is that Expr evaluates to a single node (to be checked by the type system) which is an explicit context node for AxisStep. [Of course, if the use of "/" is objectionable, the syntax can be different.] (2) Modify the single-step normalization rules to read: [ ForwardStep ]_Expr == $fs:dot / [ ForwardStep ]_Axis (3) Now, the above evaluation rule would look like dynEnv |- Expr => Value1 <-- the rest of clauses unchanged --> ---------------------------------------------------------------- dynEnv |- Expr / Axis NodeTest => fs:distinct-doc-order(Value3) [4.2.1.1, Axes] The text and normalization rules indicate that preceding/following(-sibling) axes are not on the Core, but the grammar rules [(Core) 60,61] still contain them. (Also in Appendix A.1) [4.2.1.1, Axes] For ForwardAxis, the grammar [91(XQuery)] does not define namespace:: axis, while [60 (Core)] does! Consequently, the normalization rule that follows normalizes from non-existing syntax. [This could be a problem with XQuery, rather than FS spec, since XQ Datamodel does define the kind of namespace nodes. On the other hand, if namespace:: is to be removed from FS, it currently also appears in [7.2.1, Principal Node Kinds] There is also cross-spec-numbering discrepancy: FS [91(XQuery)] is XQuery[89] [4.2.1.1] The normalization rules for sibling axes are given as follows: [following-sibling:: NodeTest]_Axis == [let $e := . in parent::node()/child:: NodeTest [.<<$e]]_Expr [preceding-sibling:: NodeTest]_Axis == [let $e := . in parent::node()/child:: NodeTest [.>>$e]]_Expr I think their bodies should be swapped! E.g., in the 1st, if I get it right, in [.<<$e] predicate, $e refers to the original node and . ranges over all siblings, so the predicate is true for siblings that _precede_ $e. Also, it could make sense to be a notch more explicit by writing [following-sibling:: NodeTest]_Axis == [let $e := . in $e/parent::node()/child:: NodeTest [.>>$e]]_Expr ^^ [4.3.2 Filter Expressions] Subsection "Core Grammar" should be renamed "Normalization". [4.7.3.1. Computed Element Constructors, both Dynamic Evaluation rules] In extended static environments statEnv_1, ... , statEnv_n, there are missing indexes in NCName, should be NCName_1 .... NCName_n [5. Modules and Prologs, Intro] It says: "Namespace declarations and schema imports always precede function definitions, as specified by the following grammar productions." However, the production [33 (XQuery)] Prolog allows to intermix them freely. [5.8 Schema import] In the rule: statEnv |- Definition* =>type statEnv1 statEnv1 |- Definition1 =>type statEnv2 --------------------------------------- Definition1 Definition* =>type statEnv2 --- input statEnv is missing in the conclusion [5.8 Schema Import] (Also see comments for [F] below.) I am afraid the schema importing formalization in [5.8] and [F] is not robust w.r.t. namespace prefix bindings possibly defined in the imported schema. Namely, the import is formalized by the rule [schema String (at String)?]_Schema statEnv |- Definition* =>type statEnv1 ------------------------------------------------------------- statEnv |- import schema String (at String)? =>stat statEnv1 and a representative rule for the second judgment above the line is statEnv |- TypeName of elem/type expands to expanded-QName statEnv1 = statEnv + typeDefn(expanded-QName => define type TypeName TypeDerivation ) ---------------------------------------------------------------------------- statEnv |- define type TypeName TypeDerivation =>type statEnv1 where statEnv maps a resolved expanded-QName of TypeName to a definition containing unresolved TypeName and where TypeDerivation can contain other unresolved Qnames (see current defs in [F]). But, even though TypeName is supposed to reside in the target namespace of the imported schema, statEnv may lack a prefix mapping necessary for resolving it into expanded-QName, since the first rule above does not add it by default! (And even if the version of the import statement is used that binds schema's namespace to a prefix, this prefix can only coincidentally be the same as the one in TypeName.) Moreover, if the schema defined other prefixes (e.g. for namespaces of the imported schemas), they can occur in TypeDerivation, and there is no provision in the current formalization for them to get into statEnv. I can see two possible approaches for cleaning this up: (1) Specify that schema import, in addition to Definitions (with unresolved QNames), also returns a set of prefix-to-namespace bindings that can now be incorporated into statEnv. (2) Specify that the definitions returned by schema import actually contain only resolved QNames. The obvious (killer?) shortcoming of (1) is that it implicitly introduces prefixes that explicitly appear only in the schema and can even shadow earlier prefixes defined by the query programmer. Approach (2) appears to be more sound, although it would require significant changes to the specification, at least: - Definitions productions in [2.3.4] need to be duplicated to similar defs that refer only to resolved QNames. (Although, since those productions describe entities not available in the source language, maybe the modified version is the only one that is needed?) - statEnv needs to be modified to contain definitions with _resolved_ names. [6.1 Formal Semantics Functions] Here is a summary list of fs-prefixed functions that appear throughout the spec but do not have subsections in 6.1, which is perhaps an unintended omission: fs:active-ns, fs:get_ns_from_items, fs:count, fs:is-same-node, fs:node-before, fs:node-after, fs:local-variables, fs:local-functions [7.1.9 Type expansion] (1) The inference rule given here is for the case when type TypeName is defined by extension. There must be another one for s derivation by restriction. (2) The inference rule contains the judgment statEnv |- Type2 is Type1 extended with union interpretation of TypeName where Type1 is defined in the previous judgment to be the extension fragment that TypeName's extension adds to the type BaseTypeName. I believe, however, Type1 should be the concatenation of BaseTypeName's definition and TypeName's extension fragment. Suggestion: It might help to obtain Type1 as the result of the following "derives" judgment: statEnv |- TypeName derives Type which produces the type model for TypeName that composes the effects of all type derivations on the path from the root of the type hierarchy down to TypeName. Rules(still need to be tinkered with to handle Mixed? correctly): statEnv |- TypeName of elem/type expands to expanded-QName statEnv.typeDefn(expanded-QName) => define type TypeName extends BaseTypeName Mixed? { Type0? } statEnv |- BaseTypeName derives BaseType Type = BaseType, Type0 ---------------------------------------------------------------------- statEnv |- TypeName derives Type statEnv |- TypeName of elem/type expands to expanded-QName statEnv.typeDefn(expanded-QName) => define type TypeName restricts BaseTypeName Mixed? { Type0? } statEnv |- BaseTypeName derives BaseType <<? affirm that Type0 is a subtype of BaseType ?>> Type = Type0 ---------------------------------------------------------------------- statEnv |- TypeName derives Type Note that using these two rules would automatically resolve the issue (1) above. [7.1.10 Union interpretation of derived types] The inference rule should contain the judgment to obtain expanded-QName from TypeName0. [7.2.2.2 Dynamic semantics of axes] In most rules, the judgments are written like dynEnv |- axis Axis child:: of NodeValue => Value1 ^^^^ --- "Axis" should be dropped. [A. Normalized core grammar] There seems to be quite a few unreachable non-terminals in the grammar: - QuantifiedExpr [43 (Core)] -- perhaps it should be mentioned in [34 (Core)] for ExprSingle - OrderByClause [39 (Core)] -- Perhaps it should appear in [35 (Core)] production for FLWORExp - PrimaryExpr [53 (Core)] -- perhaps should appear in [51 (Core)] for ValueExpr - ComputedConstructor [57 (Core)] -- perhaps should appear in PrimaryExpr [53 (Core)] [F.2 Schemas as a whole] The rule [Pragma]pragma(targetNCName) == Definition* in [F.2.1] for, presumably, handling Schema's "include" | "import" | "redefine" features, does not make sense: its rhs comes from nowhere! On the other hand, [F.2.2-4] say that handling of "include" | "import" | "redefine" is not specified in this document since it is assumed to be handled by the XML Schema processor. Suggestion: Perhaps [F.2] should just say that the helper function open-schema-document(SchemaName) encapsulates the functionality of a Schema processor, which is assumed to handle "include" | "import" | "redefine" features. I.e., the result of open-schema-document(SchemaName) is described by Content production [(56) Formal]. Then there is no need for [Pragma]_pragma rule, and Schema mapping rules at the end of [F.2.1.] should be [schema SchemaName (at SchemaNamespace)?]_Schema == [open-schema-document(SchemaName, SchemaNamespace)]_definition(targetNCName) [F.2 Schemas as a whole] This section mentions targetURI (that comes from the imported schema) and targetNCName (that parameterizes all the mapping rules), which are supposedly related, but the relationship is nowhere spelled out. Also, in the presence of Schema <import> and relatives, there can be multiple target URIs... Perhaps a good way to tackle both difficulties would be to say that open-schema-document() is also assumed to resolve all QNames defined and referenced in the imported schema. The mapping rules in the rest of the section then refer to the fully resolved names and don't need to be parameterized by targetNCName. [F.7, F.8 Attribute and model group definitions] These sections say that the corresponding features are not handled by the mapping, and refer to Issue 501 (FS-Issue-0158). But the Issues document marks the issue as resolved!
This is a resend of the submission I made a couple days ago: I have added a unique identifier for each comment, and fixed a few typos of my own. Also, I forgot to mention that most if not all of these comments are editorial. --------------------- XQuery 1.0 and XPath 2.0 Formal Semantics W3C Working Draft 20 February 2004 Lines beginning with '%' uniquely identify each comment. Lines beginning with '#' are quotes from the spec. Lines beginning with '>' are suggested replacement text. XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX TRANS-SECTION COMMENTS % 001 'not' in judgments: Note that there are no inference rules that tell us how to conclude that a judgment involving 'not' holds, so presumably you must explain how to do so. I suspect this will be easier if you change occurrences of # env |- not( something ) to > not( env |- something ) ________ % 002 When a double-quoted symbol appears in the EBNF, the symbol should appear without the quotes when in occurs in an inference rule or mapping rule. For the most part, the spec adheres to this, but it occasionally lapses. In particular, when the following quoted symbols appear in rules, the quotes should probably be removed. "element" "attribute" "lax" "strict" "skip" "/" ________ % 003 # Object in { a, b, ... } The 'in' and braces are meta-syntactic, so they should be bolded. Or prehaps better would be to rewrite it as > Object = a or Object = b or ... (with bold 'or's). ________ % 004 # statEnv |- statEnv.mem(a) ... The "statEnv |-" is redundant, delete it. > statEnv.mem(a) ... ________ % 005 # Type <: Type All '<:' judgments should start with 'statEnv |-' ________ % 006 # Value matches Type All 'matches' judgments should start with 'statEnv |-'. ________ % 007 # VarRef of var expands to Variable Change to: > VarRef = $ VarName > VarName of var expands to Variable ________ % 008 # Variable Not defined. Change to 'expanded-QName'? ________ % 009 # Value Sometimes a Value (or more specifically, a pattern whose name is a symbol deriveable from Value) will appear where an Expr is allowed. This seems kind of sloppy. ________ % 010 # String As a specific case of the preceding, most occurrences of 'String' in the rules should probably be 'StringLiteral'. ________ % 011 # . . . Change to: > ... ________ % 012 # fn:local-name-from-QName Change to: > fn:get-local-name-from-QName ________ % 013 # fn:namespace-uri-from-QName Change to: > fn:get-namespace-uri-from-QName % 014 Also, all uses of the function are of the form: # fn:namespace-uri-from-QName( ... ) = statEnv.namespace(...) but this is malformed: the LHS is a URI, but the RHS is a (namespace-kind, URI) pair. XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX SECTION-SPECIFIC COMMENTS Abbreviations: "Sem" = "Semantics" "SCP" = "Static Context Processing" "STA" = "Static Type Analysis" "DCP" = "Dynamic Context Processing" "DEv" = "Dynamic Evaluation" "DErr" = "Dynamic Errors" "LHS" = "left-hand side" (or "above the '=='" in mapping rules) "RHS" = "right-hand side" (or "below the '=='" in mapping rules) To identify a particular premise of an inference rule, I give its position (e.g. "premise 3"). In counting, I skip any premise that is merely an ellipsis. ------------------------------------------------------------------------ 2.1.2 Notations for judgments % 015 # Symbols are purely syntactic and are used to write the judgment # itself. There are actually (at least) two kinds of symbols, which you might call "base-syntactic" and "meta-syntactic". Base-syntactic symbols arise from the EBNF grammar. Meta-syntactic symbols arise from the "judgment declarations" in Notation sections. Because a judgment can combine both kinds of symbols, it's important to be able to distinguish them. Usually, base-syntactic symbols are presented in normal typeface, whereas meta-syntactic symbols are presented in boldface. However, sometimes they aren't. It would be good if the spec were consistent. In particular, add bold to: => |- : (Unless it's the colon in a QName or Wildcard.) = (Except a few cases, e.g. "namespace foo =".) fn:local-name-from-QName() fn:namespace-uri-from-QName() ________ % 016 # Patterns are written with italicized words. Do you have a reference for this terminology? "Pattern" sounds like the wrong word to me. A regular expression is a pattern. The RHS of an EBNF production is a pattern. Even a judgment is a form of pattern. But a name is not a pattern. Personally, I'd call it a metavariable. ________ % 017 # By convention, all patterns in the Formal Semantics correspond to # grammar non-terminals, and are used to represent entities that can be # constructed through application of the corresponding grammar # production. ... # In a few cases, patterns may have a name that is not exactly the name # of a grammar production but is based on it. Then there some other cases, where the pattern name isn't a grammar non-terminal or a slight modification of one: AttributeAll Error URI-or-EmptyNamespace Variable (replace with expanded-QName?) ------------------------------------------------------------------------ 2.1.3 Notations for inference rules % 018 Note: # In effect, inference rules are just a notation that describes a # bottom-up algorithm. They don't necessarily describe an algorithm, because the precedure might not terminate. Also note (as in 7.3.1) that the rules do not necessarily give a simple means to compute a result. Moreover, I wouldn't say the procedure is bottom-up, because types and values can't bubble up the tree until environments have bubbled down. ------------------------------------------------------------------------ 2.1.4 Notations for environments % 019 para 4 # This document uses environment groups that group related environments. I think you'd be better off if you changed your terminology somewhat: Instead of saying that statEnv and dynEnv are "environment groups" whose members are "environments", say that statEnv and dynEnv are "environments", whose members may be "mappings" (or "dictionaries", if you like). Note that after section 3, statEnv and dynEnv *are* generally referred to as "environments".) ________ % 020 para 4 # If "env" is an environment group with the member "mem", then that # environment is denoted "env.mem" and the value that it maps symbol to # is denoted "env.mem(symbol)". Note that this ignores members that are not mappings/dictionaries. ________ % 021 para 4 # the value that it maps symbol to is denoted "env.mem(symbol)". So should one say # env.mem(a) = b or # env.mem(a) => b ? The first, I think. There are about 20 occurrences of the second form, which should be changed to the first. ________ % 022 Updating # If the "object" is a type then the following notation relates a symbol # to a type: "env + mem(symbol : object) ". I think it would be better to keep the environment notation more self-consistent, and use '=>' in this case too. ------------------------------------------------------------------------ 2.1.5 Putting it together % 023 Editorial note # Jonathan suggests that we should explain 'chain' inference rules. # I.e., how several inference rules are applied recursively. You should at least talk about how attempting to prove a premise in one rule involves finding another rule with a matching conclusion (for some definition of the word "matching"), instantiating (some of) its patterns, and then trying to prove that conclusion. ------------------------------------------------------------------------ 2.2.1 Formal Values % 024 Grammar # [26 (Formal)] AtomicValue # [16 (Formal)] ElementValue # [17 (Formal)] AttributeValue Looking at some of the inference rules, it seems that a TypeAnnotation is optional (or can be empty). E.g., 7.2.4 / Sem / rule 2 / premise 3: # Value3 = attribute QName { SimpleValue } ________ % 025 Grammar # [16 (Formal)] ElementValue Looking at the inference rules, it seems that the # "{" NamespaceAnnotations ")" part is optional. ________ % 026 Grammar # [22 (Formal)] NamespaceAnnotations = # NamespaceAnnotation ... NamespaceAnnotation This is sloppy. Change to > NamespaceAnnotation ( "," NamespaceAnnotation )* ------------------------------------------------------------------------ 2.3.3 Content models % 027 Grammar # [28 (Formal)] Type This production leads to a fairly ambiguous grammar. I realize that this is common practice when defining the domains for a formal semantics, but the specification includes lots of examples of "serialized" Types, and it might be useful if these were parseable. I suggest that any use of a type "operator" must be parenthesized: > Type ::= ItemType > | Type Occurrence > | "(" Type ( "&" Type )+ ")" > | "(" Type ( "," Type )+ ")" > | "(" Type ( "|" Type )+ ")" > | "empty" > | "none" ------------------------------------------------------------------------ 2.3.4 Top level definitions % 028 Grammar # [39 (Formal)] ComplexTypeDerivation ::= ... Mixed? # [35 (Formal)] TypeSpecifier ::= Nillable? ... # [44 (Formal)] Definition ::= ... Substitution? Nillable? The symbol '?' is both base-syntactic (to denote a zero-or-one type) and meta-syntactic (to denote an optional [base-syntactic] phrase). It's sometimes difficult to tell which kind each is. They should at least be easily distinguishable. But the meta-syntactic '?' complicates the matching of premises to conclusions (in other rules), so I think things would be even better if meta-syntactic '?' were eliminated. For example, consider the symbol 'Mixed'. In the grammar, and in the inference rules, it always occurs followed by a '?'. So replace occurrences (in the grammar and inference rules) of 'Mixed?' with a new symbol, say 'MixedOption', and replace the production # Mixed ::= "mixed" with > MixedOption ::= "mixed"? or > MixedOption ::= | "mixed" I believe these symbols can be handled this way: Derivation Mixed Nillable PositionalVar Substitution TypeDeclaration When the symbol sometimes occurs with the '?' and sometimes without, you proceed as above, except that the production for the new symbol augments rather than replaces the original production. E.g., replace occurrences of 'ElementName?' with 'ElementNameOption', keep the 'ElementName' production, and add the production > ElementNameOption ::= ElementName? Some symbols that can be handled this way: AttributeName ElementName TypeSpecifier ValidationMode ------------------------------------------------------------------------ 2.4.1 Processing model % 029 # Static analysis is further divided into four sub-phases. Each phase # consumes the result of the previous phase and generates output for # the next phase. ... # Static analysis consists of the following sub-phases # 1. Parsing # 2. Static Context Processing # 3. Normalization # 4. Static type analysis In fact, as section 5 tells us, some Normalization happens as part of SCP, and some as part of STA. And SCP happens as part of STA. So "sub-phases" 2, 3, and 4 are not as assembly-line as you indicate. ------------------------------------------------------------------------ ------------------------------------------------------------------------ 3.1.1 Static Context % 030 statEnv.docType: # corresopnds Change to "corresponds". ________ % 031 statEnv.namespace # The namespace environment maps a namespace prefix (NCName) onto a # namespace kind and a namespace URI (URI) or the empty namespace # (#EMPTY-NAMESPACE). How does a prefix get mapped to #EMPTY-NAMESPACE? ------------------------------------------------------------------------ 3.1.1.1 Resolving QNames to Expanded QNames % 032 para 1 # Element and type QNames may be in the empty namespace, I looked in -- the 'Namespaces in XML' spec, -- the 'XQuery Data Model' spec, and -- the 'XQuery Language' spec, and as far as I can see, none of them support the term "the empty namespace". Moreover, QNames aren't in namespaces, NCNames are. # that is, there is no URI associated with their namespace prefix. I don't think you mean this. If an element or type QName has a namespace prefix, then it will match the first rule in the Semantics section (with the prefix bound to NCName1). If there's no URI associated with the prefix, then statEnv.namespace(NCName1) will fail, and you'll get a static error. If you really wanted the stated behaviour, you'd need this rule: > statEnv.namespace(NCName1) undefined > ------------------------------------- > statEnv |- NCName1:NCName2 of elem/type expands to > (#EMPTY-NAMESPACE,NCName2) But I don't think you want that. Instead, the rules that involve #EMPTY-NAMESPACE appear to be using it to handle names that belong to no namespace. If that's what you mean, then change your terminology. And change '#EMPTY-NAMESPACE' to '#NO-NAMESPACE-URI' or something. ________ % 033 Notation # statEnv |- QName of elem/type expands to expanded-QName Some occurrences of this judgment-form have 'TypeName' in the 'QName' position. But TypeName derives both QName and AnonymousTypeName. In cases where the TypeName is an AnonymousTypeName, it will be able to match the conclusion of any rule. Which means that the '=>type' judgment does not hold for definitions of anon types, which means that schema import doesn't work. Possible fix: Split this judgment-form into two, one for 'elem' and one for 'type', and then in the latter, change 'QName' to 'TypeName'. Then add a rule for 'AnonymousTypeName of type expands to'. ________ % 034 Sem / rule 1,3 / premise 1 # statEnv.namespace(NCName1) = URI-or-EmptyNamespace Section 3.1.1 tells us that statEnv.namespace maps an NCName to a pair consisting of a namespace kind (passive/active) and a namespace URI (or #EMPTY-NAMESPACE). Thus the judgment should be: > statEnv.namespace(NCName1) = (NamespaceKind, URI-or-EmptyNamespace) ________ % 035 Sem / rule 5,7 / premise 1 # statEnv.namespace(NCName1) = URI Ditto above. > statEnv.namespace(NCName1) = (NamespaceKind, URI) ------------------------------------------------------------------------ 3.1.2 % 036 dynEnv.funcDefn # The initial function environment (statEnvDefault.funcDefn) ... Change 'statEnvDefault' to 'dynEnvDefault'. ________ % 037 dynEnv.docValue: # corresopnds Change to "corresponds". ------------------------------------------------------------------------ 3.4.4 SequenceType Matching % 038 Normalization / rule 19, 25 / LHS Each of these rules appears to have a judgment thrown in before the '==' sign. This should presumably be explained, or else notated differently. ------------------------------------------------------------------------ 3.5.2 Handling Dynamic Errors % 039 rule 1 I realize this rule is only supposed to specify the default behaviour, but how do you prevent it from being true in the non-default cases? ________ % 040 rules 2, 3 You're using what appears to be formal notation to convey an informal rule, which is unwise. For any given statEnv, you can always find some binding for 'symbol' and 'component' such that the lookup fails, so the premise always holds, so every expression raises statError and dynError. ------------------------------------------------------------------------ ------------------------------------------------------------------------ 4.1.1 Literals % 041 all rules Occurrences of 'IntegerLiteral', 'DecimalLiteral', 'DoubleLiteral', 'StringLiteral' should be italicized ________ % 042 3rd DEv / rule 1 / conclusion # dynEnv |- DoubleLiteral => xs:double(DoubleLiteral) '=>' should be bold ________ % 043 4th DEv / rule 1 / conclusion # dynEnv |- StringLiteral => xs:string(StringLiteral) '=>' should be bold. ------------------------------------------------------------------------ 4.1.2 Variable References % 044 DEv / rule 1,2 / premise 1 # dynEnv |- VarName of var expands to expanded-QName Change 'dynEnv' to 'statEnv'. ________ % 045 DEv / rule 2 / premise 4 # dynEnv1 |- $ VarName => Value The '1' should be a subscript. ------------------------------------------------------------------------ 4.1.5 Function Calls % 046 Notation / rule 1 / RHS Change 'Expr' to '[ Expr ]_Expr'. (Or you could do it in the Normalization rule, but it's easier here.) ________ % 047 Normalization / rule 2 # QName ( A1, ..., An) ) Delete extra right-paren ________ % 048 STA / rule 1 / premise 2 # statEnv |- Expr1 : Type1 ... Exprn : Typen This is structured as a single premise but should presumably be two plus an ellipsis-premise. ________ % 049 STA / rule 3 / premise 1,2 # not(Typex = (...) Occurrences of 'not' should be in bold. ________ % 050 STA / rule 3 / premise 1,2 # not(Typex = (...) Append a right paren. ________ % 051 STA / rule 3 / premise 7,8 # Type1' can be promoted to Type1'' Prepend 'statEnv |-' ________ % 052 STA+DEv+DErr Occurrences of 'FuncDecl' should be italicized. Also, there should be a Formal EBNF production for FuncDecl. ________ % 053 DEv / rule 1 Several of the premises refer to statEnv, but the conclusion doesn't. (This happens with lots of the DEv rules in the spec.) Theoretically, this would allow the inference engine to fabricate any statEnv that satisfied the premises. But presumably, want the same statEnv that the FunctionCall "received" during STA. This needs to be explained, and possibly denoted somehow. ________ % 054 DEv / rule 1,2,3 / premise 4 DErr / rule 3,4 / premise 4 # dynEnv |- Expr1 => Value1 ... dynEnv |- Exprn => Valuen This is structured as a single premise but should presumably be two plus an ellipsis-premise. ________ % 055 DEv / rule 1 / premise 8 # dynEnvDefault = ( ... ) ] |- Change to > dynEnvDefault + varValue( ...) |- In addition to the obvious changes, note the deletion of right-bracket. ________ % 056 DErr / rule 2 / premise 3 # FuncDeclj = define function expanded-QName(Type1, ..., Typen) as Type # for all 1 <= j <= m This appears to require that all signatures for a given func name be identical. Put j subscripts on the 'Type' patterns. ________ % 057 DErr / rule 3 / premise 9 # dynEnv [ varValue = (...) ] |- Change to > dynEnv + varValue(...) |- ------------------------------------------------------------------------ 4.2.1 Steps % 058 STA / rule 1 / premise 2 # Type1 <: node DEv / rule 1 / premise 2 # Value1 matches node 'node' does not appear to be a valid Type. If you meant 'node()', that's still not a valid (Formal) Type, though it is a valid (XQuery) ItemType. ________ % 059 STA / rule 1 / premise 3, 4, conclusion DEv / rule 1 / premise 3, 4, conclusion Occurrences of 'Axis' should be italicized. ________ % 060 STA / rule 1 / premise 4, 5 DEv / rule 1 / premise 4, 5 Occurrences of 'PrincipalNodeKind' should be italicized. ________ % 061 DErr / rule 1 / conclusion # dynEnv.varValue |- ... Delete '.varValue'. ------------------------------------------------------------------------ 4.2.1.2 Node Tests % 062 Grammar # [95 (XQuery)] Wildcard ::= "*" | (NCName ":" "*") | ("*" ":" NCName) # [64 (Core)] Wildcard ::= Change occurrences of 'NCName' to 'Prefix' and 'LocalPart' respectively, or 'Wildcard' won't match patterns that use those names. ------------------------------------------------------------------------ 4.3.1 Constructing Sequences % 063 Normalization, STA, DEv Change occurrences of 'Expr' to 'ExprSingle'. ------------------------------------------------------------------------ 4.6 Logical Expressions % 064 Normalization, STA, DEv, DErr Change occurrences of 'Expr' to 'AndExpr' or 'ComparisonExpr' as appropriate. ------------------------------------------------------------------------ 4.7.1 Direct Element Constructors % 065 Grammar # [26 (XQuery)] ElementContentChar ::= Char - [{}<&] - [{}<&] # [27 (XQuery)] QuotAttContentChar ::= Char - ["{}<&] - ["{}<&] # [28 (XQuery)] AposAttContentChar ::= Char - ['{}<&] - ['{}<&] In each case, eliminate the repetition. ------------------------------------------------------------------------ 4.7.3.1 Computed Element Constructors % 066 Often, this section does not recognize that the 'content expression' of a CompElemConstructor is not an Expr but a CompElemBody. So anything of the form: # element QName { Expr } should be changed to > element QName { CompElemBody } and the changes propagated (i.e., the rules made to handle CompElemNamespaces). ________ % 067 STA / rules 2,3,4 / premise 1 # statEnv |- QName in context ... This judgment matches both # statEnv |- ElementName? in context ... declared in 7.6.2, and # statEnv |- AttributeName? in context ... declared in 7.6.3. Is this intentional? Maybe the judgment-forms should be distinct (add an 'elem' or 'attr' keyword in bold). ________ % 068 STA / rule 2 / premise 5 # ValidationContext1 = statEnv.validationContext "/" QName The slash should not be in quotes. Even so, I can't parse the premise, because ValidationContext/QName doesn't fit the EBNF for ValidationContext. ________ % 069 DEv / rule 1 / premise 1, conclusion # Expr = CompElemNamespace1, ..., CompElemNamespacen, (Expr0) DEv / rule 2 / premise 3 # Expr2 = CompElemNamespace1, ..., CompElemNamespacen, (Expr3) The equation is invalid; an Expr cannot match the RHS. The LHS should be a CompElemBody. ________ % 070 DEv / rule 1 / premise 2,3 DEv / rule 2 / premise 4,5 # CompElemNamespace = namespace NCName { URI } The EBNF for a CompElemNamespace says that the NCName can be omitted, but these jusgments don't allow for that. ________ % 071 DEv / rule 1 / premise 6 # statEnvn, dynEnv |- ... It's not clear what the notation means. ________ % 072 DEv / rule 1 / premise 8 DEv / rule 2 / premise 10 # NamespaceAnnotations = (CompElemNamespace1, ... CompElemNamespacen, Delete parens, or else change the EBNF for NamespaceAnnotations to require/allow parens. Also, put a comma after the ellipsis ________ % 073 DEv / rule 1,2 / last premise # element QName of type xs:anyType { Value0 } { NSAnnotations } # element { Value0 } of type xs:anyType { Value1 } { NSAnnotations } These are meant to be ElementValues, but: (a) the context allows an Expr, not an ElementValue, and (b) (for rule 2) the element-name must be a QName, not computed. ________ % 074 DEv / rule 1,2 / conclusion # statEnv dynEnv |- Insert comma, presumably. ________ % 075 DEv / rule 2 / premise 8 # fs:item-sequence-to-node-sequence (Expr3); => Value Delete semicolon. ------------------------------------------------------------------------ 4.7.3.2 Computed Attribute Constructors % 076 STA / rules 2, 3 / premise 1 # statEnv |- QName in context ... As in 4.7.3.1, this matches both judgment-forms # statEnv |- ElementName in context ... # statEnv |- AttributeName in context ... ________ % 077 DEv / rule 1 / conclusion # attribute expanded-QName of type xdt:untypedAtomic { Value } EBNF for AttributeValue says QName, not expanded-QName, and SimpleValue, not Value. ________ % 078 DEv / rule 2 Change 'Expr' to 'Expr1' or 'Expr2' as appropriate. ________ % 079 DEv / rule 2 / conclusion # attribute { Value0 } of type xdt:untypedAtomic { Value } Where you have "{ Value0 }", AttributeValue only allows QName. ________ % 080 DErr / rule 3 / premise 1 # statEnv.statEnv Delete 'statEnv.' ------------------------------------------------------------------------ 4.7.3.3 Document Node Constructors % 081 DEv, DErr / all rules # dynEnv |- Value matches Type Change 'dynEnv' to 'statEnv', according to 7.3.1. ------------------------------------------------------------------------ 4.7.3.4 TextNodesConstructors % 082 DEv, DErr / all rules # dynEnv |- Value matches Type Change 'dynEnv' to 'statEnv', according to 7.3.1. ------------------------------------------------------------------------ 4.7.3.5 Computed Processing Instruction Constructors % 083 DEv, DErr / all rules # dynEnv |- Value matches Type Change 'dynEnv' to 'statEnv', according to 7.3.1. ------------------------------------------------------------------------ 4.7.3.6 Computed Comment Constructors % 084 DEv, DErr / all rules # dynEnv |- Value matches Type Change 'dynEnv' to 'statEnv', according to 7.3.1. ------------------------------------------------------------------------ 4.8 [For/FLWR] expressions % 085 In rules throughout 4.8.x, change 'Expr' to 'ExprSingle' as appropriate, to conform to the EBNF. ------------------------------------------------------------------------ 4.8.2 For expression % 086 STA / all rules # ... varType(VarRef : Type) ... According to Section 3.1.1, the domain of statEnv.varType is expanded-QName, but a VarRef is not an expanded-QName. You'll need to add some stuff: > VarRef = "$" VarName > VarName of var expands to expanded-QName > ... varType( expanded-QName : Type ) ________ % 087 STA / rule 2 / premise 2 STA / rule 4 / premise 4 # statEnv + varType(VarRef1 : T, VarRefpos : xs:integer) Change the comma to a semicolon. ________ % 088 STA / rule 3,4 / premise 3 # prime(Type1) <: Type0 Prepend 'statEnv |-'. ________ % 089 STA / rule 3 / premise 4 # statEnv + varType(VarRef1 : Type0)) |- ... Delete extra right paren. ________ % 090 DEv / rule 3 / premise 4,5 DEv / rule 5 / premise 6,8 # varValue(Variable => Itemn, Variablepos => n) Change the comma to a semicolon ________ % 091 DEv / rule 4 / conclusion # => gr_Value1; ,..., Valuen Change 'gr_Value1;' to italicized Value sub 1. ________ % 092 DErr / rule 1 / conclusion # for Variable1 Change to > for VarRef ________ % 093 DErr / rule 3 / premise 4 # Variable => ItemiVariablepos => i Insert semicolon and space: > Variable => Itemi; Variablepos => i ------------------------------------------------------------------------ 4.9 Unordered Expressions % 094 Notation # dynEnv |- Value1 permutes to Value2 Should be centered. ------------------------------------------------------------------------ 4.10 Conditional Expressions % 095 Throughout, change occurrences of 'Expr2' & 'Expr3' to 'ExprSingle2' & 'ExprSingle3', to conform to the EBNF. ________ % 096 DEv+DErr / all rules / conclusions # dynEnv |- if Expr1 then Expr2 else Expr3 ... Add parens around Expr1. ________ % 097 DErr / rule 3 / premise 2 # dynEnv |- Expr3 => Error Change to: > dynEnv |- Expr3 raises Error ------------------------------------------------------------------------ 4.11 Quantified Expressions % 098 Why are Quantified Expressions in the Core? Couldn't they be normalized into For expressions? % 099 In rules throughout this section, change 'Expr' to 'ExprSingle' as appropriate, to conform to the EBNF. % 100 Also, in each rule, put a linebreak after the 'of var expands to' premise. ________ % 101 DEv + DErr / most rules / premise 1 # dynEnv |- Expr1 => Item1 ... Item Add commas around ellipsis. ________ % 102 DEv + DErr / most rules # 1 <= i <= n Put this premise next to a premise that uses 'i'. ________ % 103 DEv / all rules # dynEnv(Variable1 => Itemx)) Not only does this have an extra right paren, but it also treats dynEnv as a mapping. Change to > dynEnv + varValue(Variable1 => Itemx) ________ % 104 DEv / rule 3 / premise 5 # dynEnv(VarRef1 => Itemn)) (Similar to above, but with a VarRef.) Change to > dynEnv + varValue(Variable1 => Itemn) ________ % 105 DEv / rule 4 / premise 6 # statEnv |- VarRef1 of var expands to Variable1 This repeats premise 3. Delete it ________ % 106 DErr / rule 1 / conclusion # TypeDeclaration ? Delete space before '?'. ------------------------------------------------------------------------ 4.12.2 Typeswitch % 107 2nd notation # statEnv |- Type1 case CaseClause : Type # dynEnv |- Value1 against CaseRules => Value Should be centered ________ % 108 STA / rule 1 / premise 4 # statEnv |- Type0 case default VarRefn+1 return Exprn : Typen+1 STA / rule 3 / conclusion # Type0 case default VarRef return Expr : Type A 'default' clause is not a CaseClause, which is all that the 'case' judgement is declared to handle. ________ % 109 STA / rule 2 / premise 2 STA / rule 3 / premise 1 # statEnv( VarRef : Type ) ... Change to > VarRef = $ VarName > VarName of var expands to expanded-QName (or Variable) > statEnv + varType( expanded-QName : Type ) ... ________ % 110 STA / rules 2+3 / conclusion Prepend "statEnv |-". ________ % 111 DEv / rule 1 / conclusion # dynEnv |- typeswitch (Expr) CaseRules => Value1 The symbol 'CaseRules' does not exist in the XQuery or Core grammar, only in the Formal. (Maybe the Core grammar should use the CaseRules syntax.) ________ % 112 DEv / rule 2 / conclusion # case VarRef SequenceType Insert 'as': > case VarRef as SequenceType ________ % 113 DEv / rule 3 / conclusion # case SequenceType VarRef Change to: > case VarRef as SequenceType ------------------------------------------------------------------------ 4.12.3 Cast % 114 Notation # AtomicType1 cast allowed AtomicType2 = { Y, M, N } Prepend 'statEnv |-'. % 115 And instead of putting "{ Y, M, N }" in the judgment, introduce a Formal non-terminal (e.g. Castability): > [xx (Formal)] Castability ::= Y | M | N ________ % 116 Notation / rule 1 / premise 3, conclusion # ... = X, where X in { Y, M, N } # ... = X Change to > ... = Castability ________ % 117 Notation # Type2 ( Value1 ) casts to Value2 Prepend "dynEnv |-" ________ % 118 STA, DE, DErr / all rules # ... cast allowed ... Prepend 'statEnv |-' ________ % 119 DEv / rule 1 / premise 3 # ( Value1 ) cast as AtomicType2 => Value2 Prepend "dynEnv |-". ________ % 120 DEv / rule 1 / conclusion # AtomicType ( Expr ) casts to Value2 DEv / rule 2 / premise 3 # AtomicType2 ( Value1 ) casts to Value2 AtomicType is not actually a Type (i.e., not deriveable from symbol Type), so these judgments don't match the judgment-form declared in the Notation section. Change to QName? ________ % 121 DErr / rule 1 / premise 1 # AtomicValue1 of type AtomicTypeName Change 'AtomicValue' to 'AtomicValueContent'. ------------------------------------------------------------------------ 4.12.4 Castable % 122 throughout # Expr castable as AtomicType Change 'Expr' to 'CastExpr'. ________ % 123 Normalization / rule 2 / LHS # [Expr castable as AtomicType]_Expr Presumably, AtomicType should be followed by a '?', otherwise it's the same LHS as rule 1. ________ % 124 DEv / rule 1 / premise 2 # ( Value1 ) cast as AtomicType=> Value2 Prepend 'dynEnv |-'. ________ % 125 DEv / rule 2 / premise 1 # ( Expr1 ) cast as AtomicType2 raises dynError Prepend 'dynEnv |-'. ------------------------------------------------------------------------ 4.13 Validate Expressions: % 126 Normalization / rules 1,2 / LHS Each is missing [ ]_Expr around LHS ________ % 127 STA / rule 1 / premise 2 DEv / rule 1 / premise 2 DEv / rule 2 / premise 2 # statEnv(validationMode(ValidationMode) + # validationContext(ValidationContext)) This syntax is not supported by 2.1.4. Change to: > statEnv + validationMode(ValidationMode) > + validationContext(ValidationContext) ________ % 128 STA / rule 1 / premise 5 # prime(Type) = ElementType1 ... ElementType2 Put choice bars around ellipsis. ________ % 129 STA / rule 1 / last premise # Type1 = ElementName1 | ... | ElementNamen 'ElementName' is not a valid Type. Did you mean ElementType instead? ________ % 130 DEv / rules 1,2 / premise 5 # ElementValue2 = ElementName2 ... Insert 'element' > ElementValue2 = element ElementName2 ... Also, in rule 1, delete the semicolon at the end of the line. ________ % 131 DEv / rules 1,2 / premise 7 # annotate as ... Prepend "statEnv |-" or "statEnv1 |-" (not sure which). ------------------------------------------------------------------------ ------------------------------------------------------------------------ 5 Modules and Prologs % 132 Notation # [81 (Formal)] PrologDeclList ::= (PrologDecl Separator)* The rules in SCP and DCP assume that PrologDeclList is left-recursive: > PrologDeclList ::= () | PrologDeclList PrologDecl Separator but the rules in 5.2's SCP and DCP assume that it's right-recursive: > PrologDeclList ::= () | PrologDecl Separator PrologDeclList Since section 5,2 needs to construct a new PrologDeclList by prepending a PrologDecl to an existing PrologDeclList, I think it wins. So maybe the left-recursive rules should be changed. E.g.: > > SCP: > -------------------------------------------------- > statEnv |- () =>stat statEnv > > PrologDecl1 = [PrologDecl]_PrologDecl > statEnv |- PrologDecl1 =>stat statEnv1 > statEnv1 |- PrologDeclList =>stat statEnv2 ; PrologDeclList1 > -------------------------------------------------- > statEnv |- PrologDecl ; PrologDeclList =>stat statEnv2; > PrologDecl1 ; PrologDeclList1 > > STA: > statEnvDefault |- PrologDeclList =>stat statEnv ; PrologDeclList1 > statEnv |- [QueryBody]_Expr : Type > -------------------------------------------------- > PrologDeclList QueryBody : Type > > DCP: > -------------------------------------------------- > dynEnv |- () =>dyn dynEnv > > dynEnv |- PrologDecl =>dyn dynEnv1 > dynEnv1 |- PrologDeclList =>dyn dynEnv2 > -------------------------------------------------- > dynEnv |- PrologDecl ; PrologDeclList =>dyn dynEnv2 > > DEv: > dynEnvDefault |- PrologDeclList1 =>dyn dynEnv > dynEnv |- [QueryBody]_Expr => Value > -------------------------------------------------- > PrologDeclList QueryBody => Value ________ % 133 Notation # [82 (Formal)] PrologDecl You forgot FunctionDecl! ________ % 134 Notation / normalization # [PrologDecl]_PrologDecl == PrologDecl Use subscripts to distinguish the two PrologDecls, otherwise it looks like the []_PrologDecl function is the identity function. ________ Notation / judgment-form 1 # PrologDeclList =>stat statEnv; PrologDeclList1 % 135 (1) The use of a meta-syntactic semicolon is probably a poor choice, especially when base-syntactic semicolons are nearby. How about a bolded word like "with"? % 136 (2) It isn't clear what the resulting PrologDeclList1 is for. % 137 (3) There isn't a corresponding judgment-form declared for =>dyn: PrologDeclList =>dyn dynEnv ________ % 138 Notation / judgment-form 3 # dynEnv |- PrologDecl =>stat dynEnv Change '=>stat' to '=>dyn'. ________ % 139 SCP / rule 2 # PrologDecl1 = [PrologDecl]_PrologDecl When you have a normalization-invocation in an inference rule, you should perhaps make the judgment look more like the "longhand" judgment shown in 2.4.2 / Notation: > statEnv |- [PrologDecl]_PrologDecl == PrologDecl1 ________ % 140 SCP / rule 1 / conclusion DCP / rule 1 / conclusion # () =>stat statEnvDefault; () # () =>dyn dynEnvDefault These use '()' to denote a (syntactically) empty PrologDeclList. This is prehaps not a good idea, since there is possible confusion with '()' denoting a (semantically) empty sequence in the base language. In other rules, empty syntax is denoted by the empty string. See, e.g., 7.6.2 / Semantics / rule 1 / conclusion, where an an omitted ElementName in an 'ElementName? in context' judgment results in the judgment # statEnv |- in context global ... ________ % 141 SCP / rule 2 / premise 3 # statEnv1 |- PrologDecl1 =>stat statEnv2 ; PrologDecl1 Delete '; PrologDecl1'. When applied to a single PrologDecl, '=>stat' just produces a statEnv. ________ % 142 STA / rule 1 / premise 2 # statEnv |- [QueryBody]_Expr : Type Maybe split into > statEnv |- [QueryBody]_Expr == Expr2 > statEnv |- Expr2 : Type ________ % 143 DEv / rule 1 / premise 1 # PrologDeclList1 =>dyn dynEnv Presumably, the subscript 1 refers to the normalized prolog that =>stat "returned" during STA of the module. But as far as the notation is concerned, it just looks like PrologDeclList1 is "free". ________ % 144 DEv / rule 1 / premise 2. # dynEnv |- [QueryBody]_Expr => Value Maybe split into > statEnv |- [QueryBody]_Expr == Expr2 > dynEnv |- Expr2 => Value ------------------------------------------------------------------------ 5.2 Module Declaration % 145 Notation # URI =>module_statEnv statEnv # URI =>module_dynEnv dynEnv It seems to me that these mappings should be components of the static and dynamic environments, respectively. ________ % 146 SCP+DCP / rule 1 / premise 1 # (declare namespace NCName = String PrologDeclList) =>stat statEnv Delete the parens around the namespace decl, and insert a semicolon between the String and PrologDeclList: > declare namespace NCName = String ; PrologDeclList =>stat statEnv ________ % 147 SCP+DCP / rule 1 / premise 2 # module namespace NCName = String PrologDeclList Insert a semicolon again. But even, it's not a judgment ________ % 148 DCP / rule 1 / premise 1 # ... =>stat dynEnv Change '=>stat' to '=>dyn'. ------------------------------------------------------------------------ 5.4 Default Collation Declaration % 149 SCP / rule 1 / premise # statEnv1 = statEnv + collations( String) Change 'collations' to 'defaultCollation'. However, Section 3.1.1 tells us that statEnv.defaultCollation is a pair of functions, not a String. So first, look up the collation's URI in the static environment: > func-pair = statEnv.collations(String) > statEnv1 = statEnv + defaultCollation(func-pair) ________ % 150 DCP / rule 1 / conclusion # dynEnv |- default collation String =>dyn dynEnv Insert "declare" before "default". ------------------------------------------------------------------------ 5.7 Default Namespace Declaration % 151 SCP / rules 1, 2, 3 / conclusion # statEnv |- declare default element namespace = String =>stat statEnv1 Delete '=' after 'namespace'. ------------------------------------------------------------------------ 5.8 Schema Import % 152 Notation / judgment-form 1 # statEnv1 |- Definition* =>type statEnv2 The meta-syntactic '*' is used to denote a sequence of Definitions, but this overloads '*' unnecessarily. Instead, a new symbol 'Definitions' would be less confusion-prone. > [xx (Formal)] Definitions ::= Definition* (And propagate to F.1.3 Main mapping rules and F.2.1 Schema.) ________ % 153 SCP / rules 1,2,3 / premise 1 # ... schema String (at String)? ... Without subscripts, you're forcing the two String's to bind to the same object, which you don't want. Moreover, the schema location hint can be more involved than just "(at String)?". To take care of both of these problems, define > [xx (XQuery+Core)] ImportLocationHints ::= > (("at" StringLiteral) ("," StringLiteral)*)? use that in [149 (XQuery)] and [108 (Core)], and in the inference rules, change every occurrence of # (at String)? to > ImportLocationHints ________ % 154 SCP / rule 3: # default_elem_namespace( String (at String)?) Delete "(at String)?", as default_elem_namespace doesn't care about it. ________ % 155 SCP / rule 5 / conclusion # Definition1 Definition* =>type statEnv2 Prepend "statEnv |-". ------------------------------------------------------------------------ 5.9 Module Import % 156 SCP / rule 1 / premise 1 # String =>module_statEnv statEnv2 Change 'String' to 'String1', I think ________ % 157 SCP / rule 1 / premise 2 # statEnv3 = statEnv1(fs:local-variables(statEnv2, String1) # + fs:local-functions(statEnv2, String1)) This is vague, ad hoc syntax. The following is still ad hoc, but at least is more specific (re varType + funcDefn) and fits better with the syntax established by 2.1.4: > statEnv3 = statEnv1 + varType( fs:local-variables(a,b) ) > + funcDefn( fs:local-functions(a,b) ) ________ % 158 DCP / rule 1 / premise 1 # String =>module_dynEnv dynEnv2 Delete it. ________ % 159 DCP / rule 1 / premise 2 # dynEnv2 = dynEnv1 + varValue(expanded-QName => #IMPORTED(URI)) Add subscript 1 to 'expanded-QName'. ________ % 160 DCP / rule 1 / premise 3, conclusion # (expanded-QName2, Type2) ??? (expanded-QNamen, Typen) Put commas around ellipsis. ________ % 161 DCP / rule 2 / premise 1 # String =>module_dynEnv dynEnv2 Delete it. ________ % 162 DCP / rule 2 / premise 2 # dynEnv + funcDefn1(...) The subscript 1 is in the wrong place. Change to > dynEnv1 + funcDefn(...) ________ % 163 DCP / rule 2 / premise 2,3, conclusion # expanded-QName1(Type1,1, ..., Type1,n) # expanded-QName2(Type2,1, ..., Type2,n) # expanded-QNamek(Typek,1, ..., Typek,n) # expanded-QName1(Type1,1, ..., Type1,n) # expanded-QNamek(Typek,1, ..., Typek,n) Note that this appears to require that all functions imported from a module have the same number of arguments (n). Moreover, with all these subscripts and ellipses, the rule is hard to follow. To fix both of these problems, define a Formal symbol for function signatures: > [xx (Formal)] FuncSignature ::= > expanded-QName "(" ( Type ("," Type)* )? ")" Then you can say: > dynEnv2 = dynEnv1 + funcDefn( FuncSignature1 => #IMPORTED(URI) ) > dynEnv2 ; URI |- FuncSignature2 ??? FuncSignaturek > =>import_functions dynEnv3 > ------------------------------------------------ > dynEnv1 ; URI |- FuncSignature1 ??? FuncSignaturek > =>import_functions dynEnv3 ________ % 164 DCP / rule 2 / premise 3, conclusion Put commas around the (top-level) ellipsis. ________ % 165 DCP / rule 3 / premise 1 # String =>module_dynEnv dynEnv2 Change 'String' to 'String1', ________ % 166 DCP / rule 3 / premise 2,3 # dynEnv1 |- # dynEnv3 |- Change to > dynEnv1 ; String1 |- > dynEnv3 ; String1 |- to match the conclusion of rule 2. ________ % 167 DCP / rule 3 / conclusion # statEnv1 |- import module ... =>dyn statEnv4 Change each 'statEnv' to 'dynEnv'. ------------------------------------------------------------------------ 5.10 Namespace % 168 DCP / rule 1 / conclusion # declare namespace NCName =>dyn dynEnv Insert '= String' after 'NCName'. ------------------------------------------------------------------------ 5.11 Variable Declaration % 169 SCP / all rules / last premise # varType( Variable => Type ) Change '=>' to ':' if you want to follow 2.1.4. ________ % 170 DCP / all rules / conclusion # =>stat dynEnv Change '=>stat' to '=>dyn'. ------------------------------------------------------------------------ 5.12 Function Declaration % 171 Normalization + SCP + STA + DCP # define function QName should be > declare function QName ________ % 172 Normalization / rule 3 / LHS Add 'PrologDecl' subscript to right bracket. ________ % 173 SCP / para 1 # withtin Change to 'within'. ________ % 174 SCP / rule 1 / premise 2 + conclusion STA / rule 1 / conclusion STA / rule 2 / conclusion DCP / rule 1 / premise 4 + conclusion DCP / rule 2 / conclusion # [SequenceType1]sequencetype, ??? [SequenceTypen]sequencetype Put comma after ellipsis. ________ % 175 SCP / rule 1 / premise 2 # funcType(expanded-QName => ( [SequenceType1]sequencetype, ??? funcType is supposed to map an expanded-QName to a set of FuncDecls, but this maps it to a sequence of Types. ________ % 176 SCP / rule 1 / premise 3 # statEnv2 = statEnv + funcType1(expanded-QName) Seems to be a leftover. Delete it. In the conclusion, change 'statEnv2' to 'statEnv1'. ________ % 177 SCP / rules 1 / conclusion Prepend 'statEnv |-'. ________ % 178 STA / rule 1 / premise 1 # ... varType( VarRef : T; ... The domain of statEnv.varType is exapnded-QName, not VarRef, so: > VarRef = $ VarName > VarName of var expands to expanded-QName > ... varType( expanded-QName : T; ... ________ % 179 STA / rule 1+2 / conclusion # statEnv |- define function QName ... This doesn't appear to be a judgment. ________ % 180 DCP / rule 1 / premise 4 + conclusion # dynEnv' This is the only place where a prime is appended to an environment name. For greater consistency, use a subscript '1' instead. ________ % 181 DCP / rule 1 / premise 4 # funcDefn(expanded-QName => ... ) The domain of dynEnv.funcDefn is not just an expanded-QName, but a whole FuncSignature (expanded-QName and sequence of (parameter) Types). ________ % 182 DCP / rule 2 / conclusion # Variable1 as SequenceType1 # Variablen as SequenceTypen Change 'Variable' to 'VarRef'. ------------------------------------------------------------------------ ------------------------------------------------------------------------ 6.1.3 The fs:convert-operand function % 183 STA / rule 3,4,5 / premise 2 # statEnv |- Expr1 <: Type1 Change '<:' to ':'. ------------------------------------------------------------------------ 6.2.1 The fn:abs, fn:ceiling, fn:floor, fn:round, and fn:round-half-to-even functions % 184 STA / rule 1 / premise 3 # convert_untypedAtomic(....) can be promoted to Type1 Maybe change to > Type2 = convert_untypedAtomic(....) > statEnv |- Type2 can be promoted to Type1 ________ % 185 STA / rule 1 / premise 4 # xs:integer xs:decimal Insert comma after 'xs:integer'. ------------------------------------------------------------------------ 6.2.2 The fn:collection and fn:doc functions % 186 STA / rule 2,5 / premise 1 # statEnv |- statEnv.map(String) not defined Change 'not defined' to 'undefined' for consistency. Or change occurrences of 'undefined' to 'not defined'. ________ % 187 STA / rule 2,3 / conclusion # statEnv |- fn:collection(Expr) : node * 'node *' does not appear to be a valid Type. ________ % 188 STA / rule 3,6 # statEnv |- not(Expr = String) This is an attempt to express "Expr is not a literal string". However, note that Expr = String doesn't mean 'Expr' is a literal string but rather 'Expr' and 'String' are instantiated to the same object Because 'String' has no other reference in the rule, the inference engine is free to instantiate it to any object. In particular, it can *always* instantiate it to something different from 'Expr', causing the premise to hold, and thus the conclusion to hold (even when it shouldn't). I don't think you've defined the notation that would express this correctly. ________ % 189 SAT / rule 4 / premises 1,2 # statEnv |- statEnv.docType(String) = Type # statEnv |- statEnv.docType(String) = Type The two premises are the same. Delete one of them. ------------------------------------------------------------------------ 6.2.3 The fn:data function % 190 Notation / judgement-form 1 # statEnv |- data on Type1 : Type2 Put the colon in bold. ________ % 191 STA / rule 8 / premise 1 STA / rule 9 / premise 1,2 STA / rule 11 / premise 1 # statEnv |- ... type lookup (of type TypeName) The parens are ungrammatical. Note that 7.1.9 / Sem / rule 2 / conclusion E.1.1 / Sem / rule 2 / conclusion don't have them. ________ % 192 STA / rule 11 / premise 3 # define type TypeName Derivation? Mixed { Type1? } Change 'Mixed' to just 'mixed'. ------------------------------------------------------------------------ 6.2.5 The fn:error function % 193 STA / rule 1 / premise 1 # statEnv |- Expr : item ? "item?" does not appear to be a valid Type. % 194 Anyway, if fn:error() always has the 'none' type, why does the rule need a premise? ------------------------------------------------------------------------ 6.2.6 The fn:min, fn:max, fn:avg, and fn:sum functions % 195 Sem / rule 1,2,3 / premise 3 # Type1 can be promoted to T Prepend 'statEnv |-'. ------------------------------------------------------------------------ 6.2.7 The fn:remove function % 196 STA / rule 1 / conclusion # fn:remove(Expr,Expr1) : : prime(Type) ? quantifier(Type) Change ': :' to just ':'. ------------------------------------------------------------------------ 6.2.8 The fn:reverse function % 197 STA / rule 1 / conclusion # fn:reverse(Expr) : : prime(Type) ? quantifier(Type) Change ': :' to just ':'. ------------------------------------------------------------------------ 6.2.10 The op:union, op:intersect, and op:except operators % 198 STA / rule 2 / conclusion # prime(Type1, Type2); ? quantifier(Type1,Type2); ? ? Delete two semicolons. ------------------------------------------------------------------------ ------------------------------------------------------------------------ 7.1.3 Element and attribute name lookup (Dynamic) % 199 2nd Sem / rule 1 / premise 1 3rd Sem / rule 1,2 / premise 1 # ... statEnv.attrDecl(AttributeName) ... The domain of statEnv.attrDecl is expanded-QName, so change to: > statEnv |- AttributeName of attr expands to expanded-QName > ... statEnv.attrDecl(expanded-QName) .. ------------------------------------------------------------------------ 7.1.4 Element and attribute type lookup (Static) % 200 1st Sem / rule 2 / conclusion # statEnv |- element ElementName type lookup Nillable? xdt:untyped Insert 'of type' before xdt ________ % 201 2nd Sem / rule 1,2 / premise 1 # ... statEnv.attrDecl(AttributeName) ... The domain of statEnv.attrDecl is expanded-QName, so change to: > statEnv |- AttributeName of attr expands to expanded-QName > ... statEnv.attrDecl(expanded-QName) .. ________ % 202 2nd Sem / rule 2 / conclusion # statEnv |- attribute AttributeName type lookup xdt:untypedAtomic Insert 'of type' before xdt ------------------------------------------------------------------------ 7.1.5 Extension % 203 Sem / rule 1 / premise 1,2 # Type1 = AttributeAll1 , ElementContent1 What does it mean? 'AttributeAll' doesn't match any symbol name, and ElementContent isn't in the Formal language. Is 'ElementContent' supposed to be 'ElementContentType'? And similarly in 7.1.6 / Sem / rule 1 / premise 1. ------------------------------------------------------------------------ 7.1.6 Mixed Content % 204 Sem / rule 1 / conclusion # ( ElementContent & text* | xdt:anyAtomicType *) This relies on the relative precedence of type-operators '&' and '|', which has not been defined, and probably shouldn't be. Just use parens. ------------------------------------------------------------------------ 7.1.7 Type adjustment % 205 Sem / rule 1 / premise 3 # statEnv |- Type3 & processing-instruction* & comment* is Type4 What kind of judgment is this? ------------------------------------------------------------------------ 7.1.9 Type Expansion % 206 Notation / judgment-form 1 # statEnv |- Nillable? TypeReference expands to Type Given the use of this judgment in 7.2.3.1.2, it would be better to change 'Nillable? TypeReference' to 'TypeSpecifier'. ------------------------------------------------------------------------ 7.2.2.1 Static semantics of axes % 207 Sem / rule 8 / premise 2 Sem / rule 17 / premise 2 # Nillable? TypeReference expands to ... Prepend 'statEnv |-'. ________ % 208 Sem / rule 8 / premise 3, 4 # Type1 has-node-content Type1' Prepend 'statEnv |-'. ________ % 209 Sem / rule 16 / conclusion # processing-instructions* Delete final 's'. ________ % 210 Sem / rule 17 / premise 3, 4 # Type1 has-attribute-content Type1' Prepend 'statEnv |-'. ________ % 211 Sem / rule 23 / conclusion # document { Type } Italicize 'Type'. ------------------------------------------------------------------------ 7.2.2.2 Dynamic semantics of axes % 212 Sem / rules 3-10 # axis Axis self:: of NodeValue # axis Axis child:: of element ... # axis Axis attribute:: of ElementName ... # etc In each case, delete "Axis" before the actual axis name. ________ % 213 Sem / rule 5 / conclusion # dynEnv |- axis Axis attribute:: of ElementName ... Insert 'element' before 'ElementName'. ________ % 214 Sem / rule 11 # In all the other cases, the axis application results in an empty # sequence. # dynEnv |- axis Axis of NodeValue => () otherwise. The premises are unformalized. ------------------------------------------------------------------------ 7.2.3.1.1 (Static semantics of) Name Tests % 215 rule 13 / conclusion rule 26 / conclusion # prefix:local Change to italicized 'Prefix:LocalPart'. ________ % 216 rule 22 / premise 1 # fn:namespace-uri-from-QName(QName1) Change 'QName1' to 'expanded-QName1', and add > QName1 of attr expands to expanded-QName1 ------------------------------------------------------------------------ 7.2.3.1.2 (Static semantics of) Kind Tests % 217 throughout / many rules / conclusion # dynEnv |- Change 'dynEnv' to 'statEnv' ________ % 218 It would be nice if the division-headers of this section ('Document kind test', 'Element kind test', etc.) stood out more than the big bold 'Semantics' headers. ------------------------------------------ (Static semantics of) Document kind test % 219 Sem / rule 3 / premise 2 # (Type1 <: DocumentType or DocumentType <: Type1) Put 'or' in bold, since it's meta. ________ % 220 Sem / rule 3,4 / conclusion # document-node (Type) This is not a valid Type. Change to > document { Type } ------------------------------------------ (Static semantics of) Element kind test % 221 The "Semantics" header should be either one or two paras earlier. ________ % 222 Sem / rule 3 / conclusion Sem / rule 4 / premise 1 # element * TypeSpecifier This is not a valid Type. (Wildcards are allowed in XQuery Tests, not in Formal Types.) Delete the '*'. ________ % 223 Sem / rule 5 / premise 1, 2, 3, conclusion # ElementNameOrWildcard TypeSpecifier This is being used as if it's a Type, but it isn't. Change all to > element ElementName? TypeSpecifier ------------------------------------------ (Static semantics of) Attribute kind test % 224 The "Semantics" header should be either one or two paras earlier. ________ % 225 Sem / rule 3 / conclusion Sem / rule 4 / premise 1 # attribute * TypeSpecifier Change to: > attribute TypeReference and propagate. ________ % 226 Sem / rule 5 / premise 1, 2, 3, conclusion # AttribNameOrWildcard TypeSpecifier Change to: > attribute AttributeName? TypeReference and propagate. ------------------------------------------ (Static semantics of) Processing instruction, comment, and text kind tests. % 227 What, no "Semantics" header? ________ % 228 rule 4 / conclusion # test text() of with PrincipalNodeKind text Move the 'of': > test text() with PrincipalNodeKind of text ________ % 229 rule 6 # If none of the above rules apply, then the node test returns the empty # sequence and the following rule applies: # statEnv |- test node() with PrincipalNodeKind of NodeType : empty The premises are unformalized. ------------------------------------------------------------------------ 7.2.3.2.1 (Dynamic semantics of) Name Tests % 230 Sem / all rules / premise 1 # fn:node-kind( NodeValue ) = PrincipalNodeKind Italicize 'PrincipalNodeKind'. ________ % 231 Sem / rule 3 / premise 3 # fn:namespace-uri-from-QName( QName ) Change 'QName' to 'expanded-QName', and add > QName of attr expands to expanded-QName ________ % 232 Sem / rule 3 / conclusion # test prefix:* with PrincipalNodeKind of NodeValue Change 'prefix' to italicized 'Prefix'. ________ % 233 Sem / rule 4 / premise 3, conclusion # local Change 'local' to italicized 'LocalPart'. ------------------------------------------------------------------------ 7.2.3.2.2 (Dynamic semantics of) Kind Tests Processing instruction, comment, and text kind tests. % 234 Sem / rule 2 / premise 3, 4 # String Italicize 'String'. ________ % 235 Sem / rule 9 # If none of the above rules applies then the node test returns the # empty sequence, and the following dynamic rule is applied: # dynEnv |- test node() with PrincipalNodeKind of NodeValue => () The premises are unformalized. ------------------------------------------------------------------------ 7.2.4 Attribute filtering % 236 Sem / rules 1,2 / premise 1 # dynEnv |- Value1 of attribute:: => Value2 What kind of judgment is this? ________ % 237 Sem / rules 1,2 / premise 2 # dynEnv |- Value2 of "attribute", QName => ... Again, what kind of judgment is this? ------------------------------------------------------------------------ 7.3.1 Matches % 238 Sem / rule 1 / conclusion # AtomicValue of type AtomicTypeName Change 'AtomicValue' to 'AtomicValueContent'. ________ % 239 Sem / rule 2,3,4 / conclusion # String Italicize 'String'. ________ % 240 Sem / rule 8 / conclusion # attribute AttributeName of type TypeName { Value } Change '{ Value }' to '{ SimpleValue }'. ________ % 241 Sem / rule 15 / conclusion # statEnv |- empty matches Type* 'empty' is not a Value. Do you mean '()'? ------------------------------------------------------------------------ 7.3.2 Subtype and Type equality % 242 Note / para 1 # values which are not available at static type checking type. Change second 'type' to 'time'? ------------------------------------------------------------------------ 7.5.1 Type promotion % 243 1st Notation / judgment-form 1 # Type1 can be promoted to Type2 Prepend 'statEnv |-'. ________ % 244 1st Sem / rule 8 / premise 2 # prime(Type2) can be promoted to prime(Type2') Prepend 'statEnv |-'. ________ % 245 2nd Notation / judgment-form 2 # Value1 against Type2 promotes to Value2 Prepend 'statEnv |-' ________ % 246 2nd Semantics / rule 1 / premise 1, conclusion Prepend 'statEnv |-' ________ % 247 2nd Semantics / rule 2 / premise 3 # statEnv |- Type1 != Type2 Is statEnv needed for this judgment? ________ % 248 2nd Semantics / rule 2 / premise 4 # cast as Type2 (Value1) => Value2 Change to > statEnv |- (Value1) cast as Type2 => Value2 ------------------------------------------------------------------------ 7.6.2 Elements in validation context % 249 Sem / rule 1 / premise 3,4 Sem / rule 3 / premise 2 Sem / rule 6 / premise 3 # statEnv |- statEnv.elemDecl(expanded-QName) => define ElementType statEnv,elemDecl maps an expanded-QName to a Definition, but 'define ElementType' is not a valid Definition. Change it to 'define element ElementName Substitution? Nillable? TypeReference' and then construct ElementType out of those parts? ________ % 250 Sem / rule 2 / premise 1 Sem / rule 6 / premise 2 # element of TypeName Insert 'type' before 'TypeName'. ________ % 251 Sem / rule 2 / premise 2 # statEnv |- test element() with "element" of Type1 : Type2 Put 'with' in bold. ________ % 252 Sem / rule 2 / conclusion Sem / rule 6 / conclusion Sem / rule 7 / conclusion Sem / rule 8 / premise 2 + conclusion Sem / rule 9 / premise 2 + conclusion # in context type(TypeName) # in context ElementName2 # in context (SchemaGlobalContext "/" ... "/" SchemaContextStepN) # in context (SchemaGlobalContext "/" ... "/" SchemaContextStepN) "/" ElementName2 # in context SchemaContextStep # in context SchemaContextStep "/" ElementName2 These assume a syntax for ValidationContext that does not match the EBNF. Also, the slashes should not be in quotes. Similar problems in 7.6.3. ________ % 253 Sem / rule 3, 6, 7, 8, 9 # ValidationMode = "strict" or "lax" It would be better to say > ( ValidationMode = "strict" ) or ( ValidationMode = "lax" ) or > ValidationMode in { "strict", "lax" } At very least, 'or' should be in bold, since it's meta. Similar problems in 7.6.3. ________ % 254 Sem / rule 6 / premise 3 Sem / rule 7 / premise 5 Sem / rule 8 / premise 4 Sem / rule 9 / permise 4 # test ElementName with "element" of Type An ElementName is not a valid NodeTest. Also, put 'with' in bold. ------------------------------------------------------------------------ 7.6.3 Attributes in validation context % 255 Sem / rule 1 / premise 1,2 Sem / rule 3,4 / premise 1 # ... statEnv.attrDecl(AttributeName) ... The domain of statEnv.attrDecl is expanded-QName, so change to: > statEnv |- AttributeName of attr expands to expanded-QName > ... statEnv.attrDecl(expanded-QName) .. ________ % 256 Sem / rule 1 / premises 1,3 Sem / rule 3 / premise 1 # statEnv |- statEnv.attrDecl(AttributeName) => define AttributeType statEnv,attrDecl maps an expanded-QName to a Definition, but 'define AttributeType' is not a valid Definition. Change it to 'define attribute AttributeName TypeReference' and then construct AttributeType out of those parts? ________ % 257 Sem / rule 2 / premise 1 Sem / rule 6 / premise 2 # statEnv |- axis attribute:: of element of TypeName : Type1 Insert 'type' before 'TypeName'. ________ % 258 Sem / rule 5 / conclusion # resolves to element AttributeName Change 'element' to 'attribute'? ________ % 259 Sem / rule 6 / premise 3 Sem / rule 7 / premise 5 Sem / rule 8 / premise 5 Sem / rule 9 / premise 5 # test AttributeName An AttributeName is not a valid NodeTest. Maybe you want just QName. ________ % 260 Sem / rule 7 # statEnv |- statEnv.elemDecl(expanded-QName2) => define ElementType2 'define ElementType' is not a valid Definition. Change it to 'define element ElementName Substitution? Nillable? TypeReference' and then construct ElementType out of those parts? ------------------------------------------------------------------------ ------------------------------------------------------------------------ A.1 Core BNF % 261 Named Terminals # [18 (Core)] ElementContentChar ::= Char - [{}<&] - [{}<&] # [19 (Core)] QuotAttContentChar ::= Char - ["{}<&] - ["{}<&] # [20 (Core)] AposAttContentChar ::= Char - ['{}<&] - ['{}<&] Eliminate repetition (as in 4.7.1) ------------------------------------------------------------------------ ------------------------------------------------------------------------ E.1.1 Type resolution % 262 Notation / judgment-form 1 # statEnv |- (TypeReference | TypeDerivation) resolves to ... The '|' is meta. It would be better to declare the judgment-form twice, once for TypeReference and once for TypeDerivation. ------------------------------------------------------------------------ E.1.3.1 Simply erases % 263 Sem / rule 2 / premise 1,2 # statEnv |- SimpleValue1 simply erases to String1 SimpleValue1 != () Each is structured as a single premise, but presuambly should be two. ________ % 264 Sem / rule 3 / conclusion # AtomicValue of type AtomicTypeName Change 'AtomicValue' to 'AtomicValueContent' ------------------------------------------------------------------------ E.1.4.1 Simply annotate % 265 Notation # statEnv |- simply annotate as SimpleType ( SimpleValue ) => ... SimpleValue is in the EBNF but not SimpleType. ________ % 266 Sem / rule 2 / premise 1 # statEnv |- (...) fails Change to: > not( statEnv |- ... ) ------------------------------------------------------------------------ E.1.4.3 Annotate % 267 Sem / rule 1 / conclusion # annotate as () (()) => () Change the first '()' (the Type) to 'empty'. ________ % 268 Sem / rule 10,11,12 / last premise # nil-annotate as Type Nillable? Change to: > nil-annotate as Nillable? Type ________ % 269 Sem / rule 11 / premise 1 # Value filter @xsi:type => TypeName The 'filter' judgment "yields" a SimpleValue, but a TypeName is not a SimpleValue. ________ % 270 Sem / rule 11 / premise 2 # statEnv |- XsiTypeReference = of type TypeName Is statEnv needed for this judgment? ________ % 271 Sem / rule 15 / premise 1 # String as xs:anySimpleType Syntactically, what is the 'as xs:anySimpleType'? XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX -Michael Dyck
XQuery 1.0 and XPath 2.0 Formal Semantics W3C Working Draft 20 February 2004 I think the normalization rules for some and every are incorrrect: the call of the function fn:boolean is missing in the satisfies clause. I would write the normalization rule like this: [some VarRef1 in Expr1, ..., VarRefn in Exprn satisfies Expr]Expr == some VarRef1 in [Expr1]Expr satisfies some VarRef2 in [Expr2]Expr satisfies ... some VarRefn in [Exprn]Expr satisfies fn:boolean([Expr]Expr) Same for every. Minor typo: the two last 'satisfies' keyword are mispelled: satist fies(note the t before f) Best regards, Lionel
Section 3.1.1 Technical The static context should allow $fs:dot and friends to be predefined by an implementation with an implementation-provided static type in the outermost static variable declaration context.
Section 3.4.4 Technical Why does normalization of [document-node(ElementTest)]sequencetype include text in the result? This seems wrong since text should be part of the original type, shouldn't it? Also, you should not have the node types written with ().
Section 3.4.4 Technical " [processing-instruction()]sequencetype == processing-instruction ? ": Why ? ?
Section 3.4.1 Editorial/Technical Why is xdt:untypedAtomic not part of the definition of xs:anySimpleType. Please explain. Also, why is xs:anySimpleType not defined as xdt:anyAtomicType*?
Section 3.1.2 Technical Please replace "It is a static error to define a variable in the "fs" namespace." with "Since there is no namespace URI associated to the fs prefix, users cannot refer to such variables" Note that a user should be allowed to define a prefix called fs with any namespace he/she chooses. The point of not associating a namespace with the definitional prefixes is that there will be no need to check for a clash or disallow them.
Section 3.4.1 Editorial/Technical Could "( element? & text? & comment? & processing-instruction? )* " be written as the simpler "( element | text | comment | processing-instruction )* "?
MS-FS-LC1-037 Section 3.1.1 Editorial Replace "expaned " with "expanded " MS-FS-LC1-038 Section 3.1.1 Editorial "in-scope type definitions": Do we need to change this name as we did for "static in-scope namespaces"? [Note this comment has been addressed at the F2F and is submitted for completeness reasons.] MS-FS-LC1-040 Section 3.1.1 Editorial typeDefn, attrDecl, elemDecl: Mention that they are containing the imported schema components. MS-FS-LC1-041 Section 3.1.1 Editorial Default collation should be a member of the collation environment. MS-FS-LC1-042 Section 3.1.1 Editorial Replace "corresopnds " with "corresponds " MS-FS-LC1-043 Section 3.1.1 Editorial Please rename " fs:get_ns_from_items" to " fs:get_static_ns_from_items" to avoid confusion with dynamic in-scope namespaces MS-FS-LC1-046 Section 3.1.2 Editorial $fs:dot can be referred to by the user using the XPath expression ".". Please add. MS-FS-LC1-049 Section 3.4.1 Editorial There are still references to xdt:untypedAny. Should be replaced with xdt:untyped. MS-FS-LC1-050 Section 3.4.1 Editorial "derived derived " -> "derived " MS-FS-LC1-051 Section 3.4.1 Editorial The definition of fs:numerics seems broken. Also, do we really need to make it a type or can we just do the explosion into all the possible types? MS-FS-LC1-052 Section 3.4.3 Editorial "SequenceTypes can be used in [XPath/XQuery] to refer to a type imported from a schema ": Obviously it can refer to other types such as comment or element(a, b) that are not imported from a schema! MS-FS-LC1-054 Section 3.4.4 Editorial Also show NCName rule (not only string) for pi or do it in mapping to the Core syntax!
Section 3.1.2 Technical Why should the function body be part of the dynamic context. This seems to imply that I can change the function definition at runtime or based on an input value. I understand that we do not need the body of a function during compilation of a query, but I would assume that you do not have dynamic semantics with respect to function resolution. Maybe we need a special linking environment to contain this information?
Section 3.1.1 Technical Why can't the default function namespace be the empty namespace? Call it out either way.
Section 3.1.1 Editorial/Technical Are the namespace and collation environments already base URI adjusted? Please call out either way. Note that the term URI means an absolute URI which seems to indicate that base URIs have been applied.
Section 2.3.4 Editorial/Technical Why is <xsd:attribute name="country" type="xsd:NMTOKEN" fixed="US"/> mapped to an optional attribute? The instance always will have this attribute with the fixed value.
Section 2.3.4 Editorial/Technical " define type Section mixed { (element h1 of type xsd:string | element p of type xsd:string | element div of type Section)* } ": The Type grammar production does not allow "(", ")". Needs to be fixed in the Type grammar production.
Section 2.3.4 Editorial/Technical "A type declaration with simple content derived by restriction define type SKU restricts xsd:string { xsd:string } ": How does this work? If SKU is complex, how can it restrict from an atomic type? If it is a restriction from an atomic type, then the {xs:string} should not be there.
Section 2.3.2 Editorial/Technical "A name alone corresponds to a reference to a global element or attribute declaration. ": This is confusing. Why should this be used as a schema lookup? Shouldn't this be part of the schema import and inference results and denote something along the line of element a == element a of type xs:anyType?! Also affects the example and others: The following is a reference to a global attribute declaration attribute sizes Especially with the resolution of the ISSD lookup semantics, we think that the static type system should use explicit types and use another syntax in the static type system for references such as ref a/ref-attr a...
Section 2.3.4 Editorial/Technical "When the type derivation is omitted, the type derives by restriction from xs:anyType, as in:": Doesn't it derive from xdt:anyAtomicType? since it is an atomic type?
Section 2.3.1 Editorial/Technical Representation of content models: You are missing sequences (,).
Section 2.3.3 Technical Please provide the precedence rules for the ItemType grammar. Especially since no parens are allowed. For example, element a, element b | element b, element a can be interpreted in different ways.
Section 2.2 Editorial/Technical Please mention namespace nodes as an XPath 2.0 specific node.
Section 2.3.1 Editorial/Technical "For the purpose of static typing, the [XPath/XQuery] type system only describes minOccurs, maxOccurs combinations that correspond to the DTD operators +, *, and ?. ": Also add that one looks at minLength/maxLength for list types.
MS-FS-LC1-003 Section 2.1.1 Editorial Introduce the notion and purpose of XQuery Core before talking about its syntactic notation. MS-FS-LC1-004 Section 2.1.1 Editorial Please replace "language's semantics" with "languages' semantics" (there are two!) MS-FS-LC1-005 Section 2.1.2 Editorial "Expr raises Error": Add note that bold names refer to other judgments. In this case it is an auxiliary judgment. MS-FS-LC1-006 Section 2.1.3 Editorial Final Note is more confusing than helpful. It is not an algorithm since the rules are descriptive. Please remove. MS-FS-LC1-007 Section 2.1.4 Editorial Using "env" for environment group is confusing. MS-FS-LC1-008 Section 2.1.4 Editorial The scoping of some of the environments (variables, namespaces) is not understandable from the single sentence "Updating the environment captures the scope of a symbol ". Please improve or give better example. MS-FS-LC1-009 Section 2.1.5 Editorial Composition of several inference rules should be explained. MS-FS-LC1-010 Section 2.2 Editorial Please do not use the term "value" as a synonym for "item" or "sequence of items" (see similar comments on other documents). Thus rename the section of 2.2 to "XML items" and perform other such alignments throughout the document. MS-FS-LC1-012 Section 2.2 Editorial Please replace "Elements have a type annotation and contain a value" with "Elements have a type annotation and contain a sequence of items" MS-FS-LC1-013 Section 2.2 Editorial Replace "Text nodes always contain one string value of type xdt:untypedAtomic, therefore the corresponding type annotation is omitted." with "Text nodes always contain one string value of type xdt:untypedAtomic, therefore the corresponding type annotation is omitted in the formal notation of a text node." MS-FS-LC1-014 Section 2.2.1 Editorial Replace "Notably sequences cannot be nested." with "Notably sequences are automatically flattened." Since you can write nested sequences syntactically: they are just flattened. MS-FS-LC1-015 Section 2.2.2 Editorial Replace "true as xsd:boolean " with "true as xs:boolean " MS-FS-LC1-019 Section 2.3.2 Editorial Replace "Generic node types (e.g., node()), " with "Generic node types such as used in the SequenceType production (e.g., node()), " MS-FS-LC1-020 Section 2.3.2 Editorial Replace "The following is a type for a nillable element of type string" with "The following is a type for a nillable element of type string with name size" MS-FS-LC1-022 Section 2.3.3 Editorial Replace "with lower bound 0 or 1, and upper bound 1." with "with minOccurs 0 or 1, and maxOccurs 1." MS-FS-LC1-023 Section 2.3.3 Editorial Replace "The "&" operator builds the "interleaved product" of two types. For example, (element a & element b) = element a, element b | element b, element a " with "The "&" operator builds the "interleaved product" of two types. For example, (element a & element b) which is equivalent to element a, element b | element b, element a " MS-FS-LC1-025 Section 2.3.4 Editorial "element street of type xsd:string*": Explain that this is sequence of element with name street! People may bind * to xsd:string. Also, please use xs:string and not xsd:string. MS-FS-LC1-029 Section 2.4.1 Editorial "In XQuery, static the input context may be defined by the processing environment and by declarations in the Query Prolog ": Fix the sentence. MS-FS-LC1-030 Section 2.4.1 Editorial "Evaluation works by bottom-up application of evaluation rules over expressions, starting with evaluation of literals and variables.": From a query processing point of view, the expressions (such as path expressions) are actually evaluated top-down. Please explain based on an example and call out that the bottom-up application actually still may lead to a top-down evaluation of an expression such as /a/b/c[@d=42]. MS-FS-LC1-031 Section 2.4.1 Editorial/Conformance "Statically typed implementations are required to find and report type errors during static analysis, as specified in this document. ": This should be qualified as subject to implementations inferring more precise types. Also, some people read it as that the error messages are normatively given in the specification. Please write this clearer. MS-FS-LC1-032 Section 2.4.2 Editorial Please call out that some of the parts of the syntax is hotlinked (since it is not easily visible on a printed page or even on a browser). MS-FS-LC1-033 Section 2.4.2 Editorial "FWLR" -> "FLWOR" MS-FS-LC1-034 Section 2.5.1 Editorial "xdt: for XML Schema components and built-in types.": Actually the XQuery/XPath built-in types. Please fix. MS-FS-LC1-035 Section 2.5.2 Editorial "fn:distinct-nodes(node*) as node*": Has been cut. Please use a function that still exists. Also please use the F&O formatting for generic types.
Section 1.1 Normative and informative Sections Technical Make mapping of XSD into type system normative as far as specified. Otherwise we specify normative static semantics on top of non-normative basics.
MS-FS-LC1-001 Section 1 Introduction Editorial In section starting with "[XPath/XQuery] is a typed language. ": Make a better distinction between static type inference (inferring the static type) and static type checking for discovering errors.
There are a number of places in the Formal Semantics spec where it chooses a static type that is more general than the most specific type that is deducible. While we understand that an implementation is free to extend static typing to produce more specific types than the Formal Semantics spec says [1], we think it is important for the spec to choose the most specific type possible. Examples of places in the Formal Semantics where a more-specific type is desirable: ---------------------------------------------------- 1. SECTION 4.8.2 for expression 431: for expression type Under static type analysis, when a type declaration is present, the static environment should be extended to typing VarRef1 with type Type1, NOT type0. ---------------------------------------------------- 2. SECTION 4.8.3, let expression 432: let expression type bug The let expression variable has its declared type, instead of its actual type, entered into the static environment. Under static type analysis, when a type declaration is present, the static environment should be extended to typing VarRef1 with type Type1, NOT type0. ---------------------------------------------------- 3. SECTION 5.12, Function Declaration 454: function return type vs declared return type Example: declare function foo() as xdt:anyAtomicType {return 3;} foo() + 4 When doing static type analysis on foo() +4, should foo()'s static type be xdt:anyAtomicType or xs:integer ? According to the current spec, foo()'s static type is xdt:anyAtomicType. Then foo() +4 raises static type error. foo()'s static type should be xs:integer so that foo() +4 does NOT raise static type error. ---------------------------------------------------- 4. SECTION 6.2.8, fn:reverse function 442: explain why factored type is used here bug/editorial It may not be obvious why the static Type analysis for fn:reverse() function actually returns the factored type of the function's input sequence. For example, consider: fn:reverse((1, 'abc')). The input sequence type is (xs:integer, xs:string). After applying fn:reverse(), its most precise type should be (xs:string, xs:integer). If we compute the factored type, its type is (xs:string|xs:integer)+ , which is NOT as precise as (xs:string, xs:integer). Suggest: either return the most precise type (preferred solution), or add some text to explain why a factored type is used here. ---------------------------------------------------- [1] From the Formal Semantics spec: 3.6.7 Static Typing Extensions For some expressions, the static typing rules defined in the Formal Semantics are not very precise (see, for instance, the type inference rules for the ancestor axes — parent, ancestor, and ancestor-or-self— and for the function fn:root function. Some implementations may wish to support more precise static typing rules. A conforming implementation may provide a static typing extensionXQ, which is a type inference rule that infers a more precise static type than that inferred by the type inference rules in the Formal Semantics. Given an expression Expr, the type of Expr given by the extension must be a subtype of the type of Expr given by the Formal Semantics. "
These are Oracle's Formal Semantics Last Call comments, editorial. By "bugs" we mean mistakes in the text. "bugs" differ from "editorial" in that "bugs" significantly change the meaning of the document. Each comment has a header, with a number, the section, section title, an internal-to-Oracle comment number, and a 1-line summary. ---------------------------------------------------- B1. SECTION F9.3, Sequence Group 429: Sequence Vs Choice Group bug Immediately below schema mapping section, "Choice groups" should be "Sequence groups". ---------------------------------------------------- B2. SECTION 7.2.2.1, Static Semantics of axes 443: axis:child:: of document {Type} should include text * bug The inference rule for child axis of document node type should include text nodes as well. statEnv |- axis child:: of document {Type} : Type & processing-instruction *& comment* & text* Note text* is missing here. ---------------------------------------------------- B3. SECTION 7.2.3.2, Dynamic semantics of node tests 449: bug in the example conclusion bug For the 1st example, element bar:c of type xs:int {5} should be element foo:d of type xs:int {5} since we test for foo:* ---------------------------------------------------- B4. SECTION 3.5.3, Errors and Optimization 452: add 'NOT' in the last sentence of the section bug The last sentence of 3.5.3 says "In the example above, a static type error would be raised because a path expression may be applied to an atomic value" It should be "In the example above, a static type error would be raised because a path expression may NOT be applied to an atomic value" ---------------------------------------------------- B5. SECTION 3.1.2, Dynamic Context 462: dynEnv.varValue can also map an expanded variable name to #EXTERNAL bug In addition to Value or #IMPORTED(URI), an expanded variable name can also be mapped to #EXTERNAL. ---------------------------------------------------- B6. SECTION 3.4.4, Sequence Type Matching bug 453: normalization of document-node(ElementTest) There should be NO () after processing-instruction, comment, text types when defining normalization of document-node(ElementTest) because XQuery formal semantic type has no () for processing-instruction, comment, text types. ---------------------------------------------------- B7. SECTION 4.7.1, Direct Element Constructor 404: Normalization rule for Direct element constructor bug The normalization rule for a Direct element constructor distinguishes between the constructor having one element-content unit from the one having more than one element-content unit as illustrated in 4.7.1 section. The contructor containing one element-content unit preserves the typeinfo. So <date>{xs:date("2003-03-18")}</date> == element date {xs:date("2003-03-18")} This rule appears to contradict the XQuery 1.0 language spec section 3.7.1.5, type of a constructed element. In XQuery 1.0, there is no distinction between a construct having one element-content unit vs the one having more than one element-content unit. If we plan to implement Michael Kay's suggestion (documented as an editorial note in section 4.7.1), then the XQuery 1.0 spec needs to be changed to accommodate this. ---------------------------------------------------- B8. SECTION 7.6.3, Atributes in validation context 466: inference rule for the case of no attribute name present bug The inference rule for the case of no attribute name present is not right. The rule is stated as: statEnv |- axis attribute:: of element of TypeName: Type1 ------------------------------------------------------------ statEnv |- in context type(TypeName) with mode ValidationMode resolves to prime(Type2) The conclusion should refer to Type1, NOT Type2. ----------------------------------------------------
These are Oracle's Formal Semantics Last Call comments, editorial. By "editorial" we mean typos, plus suggestions on markup and wording to make the spec more readable. Each comment has a header, with a number, the section, section title, an internal-to-Oracle comment number, and a 1-line summary. ---------------------------------------------------- E1. SECTION F10: Particles 430: Typo editorial "Particles can be either and element reference ..." "and" should be "an" ---------------------------------------------------- E2. SECTION 4.4: Arithmetic Expressions, Core Grammar 433: Typo editorial "There are no Core grammar rules for value comparisons ..." Should be: "There are no Core grammar rules for arithmetic expressions ..." ---------------------------------------------------- E4. SECTION 4.12.4 Castable, Normalization 437: Castable normalization rule is specified twice (cut-paste error ?) editorial The "normalization of castable" expr rule is listed twice. ---------------------------------------------------- E5. SECTION 7.2.2.1, Static Semantics of axes 446: Suggest subsections under 7.2.2.1 editorial Please subsection 7.2.2.1 based on the axes access section (child axes, parent axes, attribute axes etc.) for readability. ---------------------------------------------------- E6. SECTION 7.2.2.1, Static Semantics of axes 444: possibly missing words 'type of' editorial "The static type of the attribute axis is similar to the static the child axis." Should be ? "The static type of the attribute axis is similar to the static [type of] the child axis." ---------------------------------------------------- E7. SECTION 2.1.3, Notations for inference rules 448: inference rules need clearer markup editorial The inference rules are written as a collection of premises and a conclusion, written respectively above and below a dividing line. Having seen these rules in different fonts, browsers, print-outs, it is clear that some more markup is needed to make it easier to read the rules. Suggest: draw a box around the entire rule and/or make some other markup around the entire rule, such as background shading. When there are multiple inference rules listed together, it is very hard for the reader to mentally draw the boundary around each inference rule. This is especially true for inference rules without premises. When there are many inference rules, some of which have no premises and some of which have premises, listed in a cluster under a section, it is hard for reader to separate the inference rules. See especially 7.2.3.1.1, 7.2.3.1.2, 7.2.3.2.2 ---------------------------------------------------- E8. SECTION 7.2.3.1.2, kind tests 450: possible mis-wording in 7.2.3.1.2, 3rd paragraph editorial "After normalization of the kind test an XQuery type, the expression's type is compared to the normalized XQuery type." Should be ? "After normalization of the kind test [as] an XQuery type, the expression's type is compared to the normalized XQuery type." ---------------------------------------------------- E9. SECTION 3.4.1, Predefined Types 458: xdt:untyped definition editorial The definition of xdt:untyped includes xdt:untypedAny. Presumably this was overlooked when changing xdt:untypedAny to xdt:untyped. ---------------------------------------------------- E10. SECTION 6.1.4, The fs:convert-simple-operand function 465: reference to convert_untypedAtomic editorial fs:convert-simple-operand function makes a reference to a function convert_untypedAtomic. Please make a reference to 6.2.6 where convert_untypedAtomic is defined. convert_untypedAtomic is also used in 6.2.1, with no reference to a definition. ---------------------------------------------------- E11. SECTION 3.6.7, Static Typing Extensions 464: There is no definition of '<:' in 3.6.7 editorial Suggest: add a reference to the definition of '<:' in 7.3.2. ---------------------------------------------------- E12. SECTION 4.1.4, Context Item Expression 455: static type analysis missing for context item expression editorial In the introduction section, it states that the context item may be either a node or an atomic value. However, it does NOT explcitly state that this as an inference rule in a 'static type analysis' rule. ---------------------------------------------------- E13. SECTION 6.2.2, The fn:collection and fn:doc function 439: The first premise of the first inference rule for fn:doc() is done twice editorial StatEnv |- statEnv.docType(string) = Type premise for fn:doc() first inference rule is listed twice ---------------------------------------------------- E14. SECTION 7.2.3.2, Dynamic semantics of node tests 469: Singular used when plural required editorial In the second paragraph under Semantics, the phrase "are similar to those for axis" should read "are similar to those for axes". ---------------------------------------------------- E15. SECTION 4.7.1, Direct Element Constructors 467: Two typos editorial Under Normalization, the paragraph beginning "So to preserve useful type information" includes the phrase "constructor's that contain"; the apostrophe between the "r" and "s" is incorrect, because the constructor being discussed does not posess "that contain"...it's merely a plural form of "constructor". In the same paragraph, the last sentence reads "Here is the normalization of the first and fourth examples above:" There are two things wrong with this sentence. First, it's unclear whether "first" and "fourth" are counting in reverse document order ;^) or in document order starting at the subheading "Normalization". More importantly, the shaded text that follows that sentence makes it clear that the examples are not the "first and fourth", but either the "second and fourth" (if in reverse document order) or the "first and third" (if in document order from the subheading). ---------------------------------------------------- E16. SECTION 4.7.3.6, computed comment constructors 436: computed processing-instruction editorial Under the normalization section, the first 3 words "Computed processing-instruction should be "Computed comment" ---------------------------------------------------- E17. SECTION 4, Expression 456: static type analysis for expressions with empty type clarification It is a static type error for most (but not all) expressions to have the empty type. Is '3+()' a static type error ? We expect NO, because + is normalized into fs:plus() (6.1.1), which can return empty type. Does 'local namespace declaration' defined in 4.7.4 raise a static type error, as the static type analysis yields empty type ? ---------------------------------------------------- E18. SECTION 3.4.1, predefined types 457: definition of fs:numeric editorial The definition of fs:numeric does not appear to be right. The usage of '&' and ';' and usage of _ do not seem to be right. It should be: define type fs:numeric restricts xs:anyAtomicType { xs:decimal | xs:float | xs:double} ---------------------------------------------------- E19. SECTION 2.3.3, Content models 461: '&' operator and XML SChema All editorial The definition in Formal Semantics of '&' operator is, (element a & element b) = element a, element b | element b , element a The text says "The interleaved product represents all groups in XML Schema. But "all groups in XML Schema" would result in: (element a & element b) = element a, element b | element b , element a | element a | element b | empty Suggest changing this text" "The interleaved product represents all groups in XML Schema. All groups in XML Schema are restricted to apply only on global or local element declarations with lower bound 0 or 1, and upper bound 1." to e.g. "The interleaved product represents all groups in XML Schema, restricted to apply only on global or local element declarations with lower bound 0 or 1, and upper bound 1." ---------------------------------------------------- E20. SECTION 7.2.3.2.2, kind tests 451: The conclusion of the inference rule for comment() test is incomplete editorial When the Formal Semantics document is printed (using Netscape), the inference rule for comment nodes is printed as: not(fn:node-kind(NodeValue) = "comment") ----------------------------------------------------- () The () conclusion should be replaced as dynEnv|- test comment() with PrincipalNodeKind of NodeValue => () When the Formal Semantics document is displayed directly in a browser (including Netscape), the conclusion displays as expected. ---------------------------------------------------- E21. SECTION 6.2.7, 6.2.8, fn:remove and fn:reverse function 441: 'factored type' not defined editorial There is no definition of 'factored type'. Suggest defining it in 7.4 where prime type and its computation is defined, and then reference this definition wherever 'factored type' is used. ---------------------------------------------------- E22. SECTION 5.11 - variable declaration 434: no 'static type analysis' section editorial There is no 'static type analysis' section for Variable declaration. ---------------------------------------------------- E23. SECTION 6.2.6, The fn:min, fn:max, fn:avg, and fn:sum functions 468: Incomplete list of types for fn:mix and fn:max editorial Under the subheading "Semantics", the paragraph starting "Instead of writing a separate judgement", the second sentence deals with fn:min and fn:max. That sentence has a list of data types that incorrectly omits the types xs:date, xs:time, and xs:dateTime. As evidenced by F&O section 15.4.3, fifth paragraph, sentence beginning "If date/time values do not have a timezone...", F&O properly handles fn:max and fn:min applied to those three types. Please add these three types to the list in the second sentence. (Do not add it to sentences dealing with fn:avg and fn:sum, of course.) ---------------------------------------------------- E24. SECTION 2.3.2, Item types 460: element content nodes editorial Section 2.3.2 says: "We distinguish between document nodes, attribute nodes, and nodes that can occur in element content (elements, comments, processing instructions, and text nodes), as we need to refer to element content nodes later in the formal semantics." The spec refers to "element content type" elsewhere, but not "element content NODES". ----------------------------------------------------
Hi, a question dealing with the function fs:convert-operand as described in <> . When having statEnv <> .xpath1.0_compatibility <> = false, type($actual) = String and type($expected) = Integer no conversion is done, right? Considering a general comparison of a string and an integer value. According to the formal semantics of the general comparison, convert-operand would be called for both values but no conversion would take place actually. So I end up with a comparison of a string and an integer that is not defined (no overloaded comparison function exists taken these two types). That would force me to throw a XP0004 or XP0006 error due top the incompatible types, right? Thanks & Cheers Daniel
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 6.2.9 The last inference rule for fn:subsequence indicates that the types of the second and third arguments must be xs:integer. In fact, from F&O Section 15.1.3, they must be of type xs:double. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 6.2.7 The inference rule for fn:remove doesn't seem correct. For example, for fn:remove(1,1), the rule yields type xs:integer. The result type should not simply use the quantifier of the type of the first argument, as the operation may remove an item from the sequence. If quantifier(Type) is "1" or "?", the inferred type of the result should be prime(Type)?; if quantifier(type) is "+" or "*", the inferred type of the result should be prime(Type)*. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 6.2.6 The paragraph between the two inference rules for fn:sum indicates, "The second form of fn:sum takes one argument, with an implicit second argument of the integer value 0. In this case, the result type is the union of target type T and xs:integer." However, F&O section 15.3.5 states "If the converted sequence is empty, then the single-argument form of the function returns the xs:double value 0.0e0." The inference rule here needs to be made consistent with the description in F&O. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 6.2.6 The paragraph before the first inference rule states, "When the function variable F is fn:min or fn:max, the target type T must be one of xs:decimal, xs:float, xs:double, xdt:yearMonthDuration, or xdt:dayTimeDuration." However, according to F&O section 15.3.3 and 15.3.4, these functions also accept arguments of type xs:date, xs:time and xs:dateTime. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 4.4 The normalization rule for the unary arithmetic operators is problematic for values of type xs:float and xs:double. If the operand of unary minus is positive zero, the result produced using the usual IEEE.738 rules for arithmetic ought to be negative zero, but the result of the normalized operation 0.0-(+0.0) will be positive zero. Similarly, if the operand of unary plus is negative zero, the result ought to be negative zero, but the result of the normalized operation 0.0+(-0.0) will be positive zero. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 3.1.2 The penultimate paragraph refers to the "fs" namespace, and indicates that it is a static error to define a variable in that namespace. However, section 2.5.1 indicates that the "fs:" prefix is a notational device, and that there is no namespace that corresponds to it. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 2.4.1 The second paragraph before the last numbered list states, "Notice that the separation of logical processing into phases is not meant to imply that implementations must separate the static analysis phase from the dynamic evaluation phase; processors may choose to perform all phases simultaneously at evaluation-time and may even mix the phases in their internal implementations." This sentence should be further clarified. If the static typing feature is in effect, and an error was detected by that subphase, the dynamic evaluation phase must not occur. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Hello, The following is a comment from IBM on the Last Call working draft of Formal Semantics. Section 2.1.3 Some inference rules are written as if the order of the premises is significant, using terms like "first", "second", "then" (see last paragraph of section 2.1.5, for example). If the order is signficant, that should be stated here. Otherwise, those inferences should not be written as if the order was significant. Thanks, Henry (on behalf of IBM) ------------------------------------------------------------------ Henry Zongaro Xalan development IBM SWS Toronto Lab T/L 969-6044; Phone +1 905 413-6044 mailto:
Both the Formal Semantics and the internal XQuery specification seem to allow empty text nodes, but this conflicts with the Data Model: 6.7 Text Nodes 6.7.1 Overview Text nodes must satisfy the following constraint: 1. A text node must not contain the empty string as its content. The formal semantics uses empty text nodes so it can suppress spaces between adjacent enclosed expressions: 4.7.1 Direct Element Constructors Normalization [ElementContent1 ..., ElementContentn]ElementContent-unit, n > 1 == fs:item-sequence-to-node-sequence([ ElementContent1 ]ElementContent , text { "" }, ..., text { "" }, [ ElementContentn]ElementContent 4.7.1.1 Attributes Normalization [ AttributeValueContent1 ..., AttributeValueContentn]AttributeContent-unit, n > 1 == fs:item-sequence-to-untypedAtomic( [AttributeValueContent1]]AttributeContent , text { "" }, ..., text {""}, [ AttributeValueContentn]AttributeContent Note also that the rule for Dynamic Evaluation of Text Node Constructors does not check for an empty string. Only the static typing consider this by returning 'text?'. Also, the informal XQuery specification has a problem here: 3.7.3.4 Text Node Constructors 2. If the result of atomization is an empty sequence, no text node is constructed. ... However, it says nothing about a content expression that consists of a single empty string. I suggest removing the above sentence, and modifying the 3rd rule: 3. The individual strings resulting from the previous step are merged into a single string by concatenating them with a single space character between each pair. If the resulting string is the empty string, no text node is constructed (and the expressions returns an empty sequence). Otherwise, the resulting string becomes the content of the constructed text node. Alternatively, change the data model to allow empty text nodes. I don't see any particular reason to prohibit them, even if they're not in the XML infoset. Just replace the sentence "In addition, document and element nodes impose the constraint that two consecutive text nodes can never occur as adjacent siblings" by adding "nor can any of their text node children have the empty string as the content". My recommendation: 1. Change the Data Model to allow empty text nodes. 2. Change the Text Node Constructor to allow empty string content. 3. Change element and ocument constructor normalization so that they remove empty text nodes *and* combine adjacent text nodes. -- --Per Bothner per@bothner.com
This is a request for the rationale as to why the quantifiers for "()" and "none" changed between Aug 2002 and May 2003. In Aug 2002: quantifier(()) = 0 quantifier(none) = 0 In May 2003, this changed to: quantifier(()) = ? quantifier(none) = 1 Why? The current version seems rather odd. Why should quantifier(none) be 1? - Paul BEA Systems, Inc.
The normalization of FLWOR clauses seems wrong. Specifically, the 'for' normalization in 4.8.1 following the sentence: Therefore, a ForClause is normalized to nested for expressions: appears to be incorrect. Consider: for $i in 0 to 9 for $j in 0 to 9 stable order by $j return 10*$i+j This yields the tuple sequence: (i=0,j=0), (i=0, j=1), (i=0, j=2) ... so the sorted result should be: 0, 10, 20, ..., 1, 11, 21, ... The "normalized" expression is: for $i in 0 to 9 (for $j in 0 to 9 stable order by $j return 10*$i+j) This performs 10 independents sorts, none of which change the order, so the result is as if there was no order by clause: 0, 1, 2, ..., 10, 11, 12, ... -- --Per Bothner per@bothner.com
MS-FS-LC1-058 Section 4.1.3 Editorial "It is a static error for any expression other than () to have the empty type (see [4 Expressions].)": Make this statement less absolute: "Often it is a static error for any expression to have the empty type. See [4 Expressions] for the detailed rules." MS-FS-LC1-059 Section 4.1.5 Editorial "xdt:anyAtomic" -> "xdt:anyAtomicType" MS-FS-LC1-061 Section 4.1.5 Editorial Instead of listing prototypical values, just explain what it is being used for, MS-FS-LC1-063 Section 4.1.5 Editorial Please clarify when dispatch based on provided union type is needed. Most function dispatches are based on arity and not type and thus would not lead to a successful application of this rule. MS-FS-LC1-066 General Editorial Please provide op: functions with links to their definition in the F&O spec. MS-FS-LC1-067 Section 4.2.1/4.3.2 Editorial It would be better to combine the rules into one section. MS-FS-LC1-069 Section 4.2.1 Editorial The remainder of the static semantics of axis and node test is given in section 7. But there is no link visible that takes one there and it is not clear in this section how the semantics play out. Either move parts up or add references. MS-FS-LC1-105 Section 4.3.3 Editorial Please link to section 6.2.10 where the op:union et al are defined instead to 6. MS-FS-LC1-112 General Editorial/Technical Please also refer to the section where the dynamic semantics of the functions is specified. Not only the function invocation! MS-FS-LC1-115 Section 4.7.1 Editorial "The next example contains six element-content units:": depends on the XQuery boundary whitespace handling rules since you have boundary whitespace in your query. MS-FS-LC1-117 Section 4.7.1 Editorial The section numbering needs to be better. Elements do not have their own subsections but attributes do. Others are in separate 4.7.2. MS-FS-LC1-124 Section 4.7.3.4 Editorial "The static semantics checks that the argument expression has type xs:string." This is guaranteed by the normalization. So why do we need this condition? MS-FS-LC1-128 Section 4.8 Editorial There are several places (including the title) where we refer to FLWR instead of FLWOR. Please fix. MS-FS-LC1-131 Section 4.12.2 Editorial Replace " an optional VarRef, which is bound the value of the input expression" with " an optional VarRef, which is bound to the value of the input expression"
Appendix B.2 Technical The table implies static types but the semantic described is the dynamic semantics. This needs to be rectified (for example, what if the static type of A is xs:integer? ? What is the result of () eq () (static error if static typing? () dynamically.).
MS-FS-LC1-109 Appendix B.2 Editorial Please replace "Gregorian" with "Australian" :-) MS-FS-LC1-111 Appendix B.2 Editorial fs:minus: Decimal -> xs:decimal
Section 6.2.10 Editorial Some spurious ; in judgment for op:intersection
Appendix B.2 Technical fs:is-same-node: Here you indicate static types. use this for the other ops above as well and provide static and dynamic semantics. Also fix node to be node().
Section 4.2.2 Technical Dynamic dispatch of positional predicate is problematic for performing implementations. See also comments MS-XQ-LC1-065, MS-FS-LC1-114.
Section 4.3.1 Technical Do we allow expr1 to expr2 where either expr1 or expr2 have a static type of atomic? ? If so, we either need to extend the op:to signature or make it clear that this is allowed during normalization.
Section 4.7.2 Technical CDATA should not be treated as a constructor. The XQuery parser should take care of it before it gets to the F.S. level.
Section 4.7.1 Technical The whole business of distinguishing element content to sometimes preserve content type is incompatible with the dynamic semantics of the construction. With the three current validation modes on construction, we cannot infer statically some preserved type of the content. Please remove this complexity from the spec. Note: Even with preserve mode, we cannot preserve atomic type information. This will also simplify the static typing of construction and make the section easier to understand.
Section 4.3.2 Technical In the case of a literal numeric, shouldn't we have also have a special normalization rule for last()
Section 4.6. Technical As mentioned in MS-FS-LC1-068, we should not use the full power of fn:boolean() since we need to be able to statically dispatch on predicates.
Section 4.7.2 Technical The construction of comments and Pis uses the attribute content normalization that will perform entitization and escaping. This should not occur when constructing comments and Pis. Instead certain characters sequences (- -- etc) need to be treated specially in the context of comment constructions.
Sections 4.7.3.1/2, 4.13 - We will not review these sections due to the changes with respect to validation and construction. We expect them to be submitted separately for a review once the changes have been made.
Section 4.7.3.3 Technical The document node constructor should not erase type information on its content. It should keep that information (always).
Section 6.1.6 Technical fs:item-sequence-to-node-sequence(): items_to_nodes() should collapse atomictype*/+ to text and text*/+ to text.
Section 4.7.3.5 Technical Normalization is using two things not available in XQuery: A union sequence type (just call this out), and casting from string to QName (please fix). Since we raise an error if the QName is not an NCName, we should instead use NCName (which happens to be a subtype of xs:string). This would simplify the normalization and still give us type safety.
Section 4.8.4 Technical The static type for order by seems wrong: Assume that element person can contain multiple phone elements of type xs:int. Then the following expression should be a static error: for $p in /person order by $p/phone return $p Since there is more than one phone per person. Also we need rules to deal with type promotion of numeric, untyped and other types.
Section 4.12.4 Editorial/Technical Replace "[Expr castable as AtomicType]Expr == let $v as xdt:anyAtomicType? := fn:data([ Expr ]Expr) return $v castable as AtomicType? " with "[Expr castable as AtomicType ?]Expr == let $v as xdt:anyAtomicType? := fn:data([ Expr ]Expr) return $v castable as AtomicType? "
Section 4.12.5 Technical Constructor functions now cast to T?, thus we request the following normalization: [AtomicType(Expr)]Expr == [(Expr) cast as AtomicType? ]Expr
Section 4.7.4 Editorial/Technical Since a namespace declaration only accepts string literals, the normalization and static semantics judgment seem like overkill. There is no need for the casting to untyped and then string and there is no need to check for the input type (since the parser would have not allowed anything else to go through).
Section 4.8.3 Editorial/Technical Please add a sentence what happens if a variable with the name already exists or add a reference to the variable name and scoping rules.
Section 4.7.3.4 Technical "The type is zero-or-one, because no text node is constructed if the argument of the text node constructor is the empty string.": Now the empty text node is allowed. Please align with that decision.
Section 4.12.3/4 Technical The current normalization of cast as/castable seems to raise a static error if I have an expression E cast as T and E infers to be of static type ET?. This means that most applications of cast as T will lead to static errors. Shouldn't this be a dynamic error?
Section 4.1.5 Editorial/Technical "SequenceType <: xs:anySimpleType" -> "SequenceType <: xdt:anyAtomicType*" (no named union types or list types can be sequence types!)
Section 4.1.5 Technical "if the expected type is a union of atomic types then this check is performed separately for each possibility": Remove. The expected type cannot be a union of atomic types. Or did you mean the inferred type?
General Technical The formal semantics raises both static type errors and dynamic type errors not differentiating that under static typing, no dynamic type errors should occur. This needs to be made explicit. With static typing on, all type errors need to be detected statically (conservative static typing!).
Section 4.1.5 Technical What happens if I have an inferred type of a union of atomic (xs:int | xs:double) and I find a function expecting xs:double. The rule doing promotion does not apply, the union rule also does not apply it seems. Please clarify. Also, is xs:integer? treated as an atomic type or a union of xs:integer | empty() ?
Section 4.1.1 Editorial/Technical Mention that literal overflows are raised during parsing.
MS-FS-LC1-070 Sections 7.2.2.1/7.2.3.1 Editorial Add more whitespace before the inferences statEnv |- axis Axis of none : none statEnv |- axis Axis of empty : empty MS-FS-LC1-075 Section 7.1.4 Editorial Sometimes the type lookup results in just a type name, sometimes it returns "of type Typename". Please be consistent. MS-FS-LC1-077 Section 7.1.10 Editorial Can you add a more complex example that shows restrictions and derivation? MS-FS-LC1-080 Section 7.1.7 Editorial "if the complex type is mixed, interleaves the type with a sequence of text nodes and xdt:anyAtomicType.": Note that the atomic type is or'ed and not part of the interleave adjustment. MS-FS-LC1-081 Section 7.1.9 Editorial/Technical "statEnv |- Type2 is Type1 extended with union interpretation of TypeName statEnv |- Mixed? Type1 adjusts to Type2 ------------------------------------------------------------------------ -------- statEnv |- of type TypeName expands to Type2 " -> Are the number mixed up? MS-FS-LC1-084 Section 7.1.6 Editorial Please add example. MS-FS-LC1-095 Section 7.2.2.1 Editorial Please remove the "improved" version for ancestor axis unless we fix the type inference for the parent axis! MS-FS-LC1-096 Section 7.2.3.1.1 Editorial "statEnv |- QName1 of elem/type expands to expanded-QName statEnv |- QName2 of elem/type expands to expanded-QName": Add subscripts to expanded-QName and add an equality condition of the two expanded Qnames (same for attributes) MS-FS-LC1-097 Section 7.2.3.1.1 Editorial Please add more whitespace between inference rules. The current spacing is unreadable. MS-FS-LC1-098 Section 7.2.3.1.1 Editorial Replace "statEnv |- test * with "element" of element prefix:local TypeSpecifier? : element prefix:local TypeSpecifier?" With "statEnv |- test * with "element" of element QName TypeSpecifier? : element QName TypeSpecifier?" Not every QName has a prefix! (same holds for attributes) MS-FS-LC1-099 Section 7.2.3.1.1 Editorial How do we deal with testing an element name foo against element() ? I would assume that the inferred type is element(foo)? and not element(foo). Same for a against a|b. The result should be a? and not a or raise an error. Same issues with *:b test a:*: should be a:b? and not a:b. Please clarify the use of ? for syntactic purposes and as Occurrence indicator MS-FS-LC1-100 Section 7.2.3.1.1 Editorial With the adoption of element(name) being the same as the name name test, can we simplify the specification by making them map to the same rules? MS-FS-LC1-101 Section 7.2.3.1.2 Editorial "Document kind test" etc: What should be the editorial status of these words? Title? Sentence? MS-FS-LC1-102 Section 7.2.3.1.2 Editorial What should the following inferred type be: Inferred: document(element(A), Kindtest: document(element(*,T)). That seems to be document(element(a,T)?). However, I think it should be document(element(a,T))? MS-FS-LC1-103 Section 7.2.3.1.2 Comment We have not reviewed Element and Attribute kind tests since they will be changed due to the change in SequenceType semantics. MS-FS-LC1-108 Section 7.4 Editorial The quantifier composition | and . (dot) are the same. Just use one of them.
Section 7.4 Technical Prime(empty) = none: How can we get none as the prime type? Isn't that leading to errors since none reflects the type of an error? Why not = empty? For example, you say: prime(element a | empty) = element a But isn't this element a | none? And doesn't none propagate (so that we propagate errors?)
Section 7.2.3.1.2 Technical " ------------------------------------------------------------------------ -------- statEnv |- test node() with PrincipalNodeKind of NodeType : NodeType If none of the above rules apply, then the node test returns the empty sequence and the following rule applies: statEnv |- test node() with PrincipalNodeKind of NodeType : empty ": Remove the judgment. This is confusing and is in contradiction to the rule before the sentence. As fallback, it also does not cover any of the other kind tests!
Section 7.2.2.1 Technical " ------------------------------------------------------------------------ -------- statEnv |- axis ancestor:: of NodeType : element* Note that this rule will always result in the type (element | document)* ": Seems to contradict each other. Please fix the judgment.
Section 7.2.2.1 Technical Replace "statEnv |- axis descendant:: of Type1 : Type2 ------------------------------------------------------------------------ -------- statEnv |- axis descendant-or-self:: of Type1 : (prime(Type1) | prime(Type2))* " with "statEnv |- axis descendant:: of Type1 : Type2 ------------------------------------------------------------------------ -------- statEnv |- axis descendant-or-self:: of Type1 : Type1 | Type2 " Do the same for ancestor-or-self.
Section 7.2.2.1 Editorial/Technical "statEnv |- ElementType type lookup Nillable? TypeReference Type = (Type1, Type2) statEnv |- Type1 <: attribute * statEnv |- Type2 <: ElementContentType * | xdt:anyAtomicType * ------------------------------------------------------------------------ -------- statEnv |- Type has-attribute-content Type1 " -> Why the type lookup?
Section 7.2.2.1 Technical has-attribute-content: Is the result type an interleave of all attributes or a union?
Sections 7.1.7/7.1.8 Technical The typed BuiltInAttributes should not be added if the content type is untyped, since the untyped content could contain such a named attribute that is containing a different value.
Section 7.1.8 Technical "fs:anyURIlist" -> make it an anonymous type since there is no such named type in XML Schema.
Section 7.1.6 Editorial/Technical Since we now use the union expansion, do we still need to add "| xdt:anyAtomicType"? Since we know will get the more precise subtypes anyway...
Section 7.1.5/7.1.7 Technical "Type2 extended by (processing-instruction? & comment?)*": Extended by uses "," for adding element content. This clearly is incorrect for adding PI and comment interleaves since they can appear in lots of places. For example, assume that Type2 is ((a|b), c )& d. Then the above would yield ((a|b), c )& d, (processing-instruction? & comment?)* Which is incorrect. It should yield: ((a|b) & (processing-instruction? & comment?)*, c & (processing-instruction? & comment?)*) & (d & (processing-instruction? & comment?)*)
Section 7.1.10 Technical The expanded type union should preserve whether the subtypes are mixed or not so the later adjustment will add the text nodes.
Section 7.1.6 Technical " ElementContent & text* " does not match: If the Element content is a, b, then (a,b) & text* does not match (a, text, b) even though mixed content allows that. Please make it explicit or use a new mix operator.
Section 7.1.10 Technical "statEnv.typeDefn(expanded-QName) => define type TypeNameR,1 restricts TypeName0 Mixed? { TypeR,1? }": There are many rules that look-up different type definitions using the same expanded-QName. This looks like a bug.
Section 7.1.7 Editorial/Technical "statEnv |- Type1 mixes to Type2 statEnv |- Type2 extended by BuiltInAttributes is Type3 statEnv |- Type3 & processing-instruction* & comment* is Type4 ": What is the meaning of the last is? Is that Type3 extended by pi and comments? Also see comment on extended by...
Section 7.1.4 Technical Replace "statEnv |- ElementName of elem/type expands to expanded-QName statEnv.elemDecl(expanded-QName) undefined ------------------------------------------------------------------------ -------- statEnv |- element ElementName type lookup Nillable? xdt:untyped " with "statEnv |- ElementName of elem/type expands to expanded-QName statEnv.elemDecl(expanded-QName) undefined ------------------------------------------------------------------------ -------- statEnv |- element ElementName type lookup T" where T is determined by the context (was the containing element of type xdt:untyped or xs:anyType?). Depending on resolution of preserve mode on data model, this comment also applies to attribute lookup.
Section 7.2.2.1 Technical Can we improve the following rule: Type = Type1, Type2 statEnv |- Type1 <: attribute * statEnv |- Type2 <: xdt:anyAtomicType + ------------------------------------------------------------------------ -------- statEnv |- Type has-node-content text ? to take list types (+ needs to be *) and string types into account?
Section 7.2.2.1 Technical Why is it ElementContentType + and not ElementContentType * in judgment has-node-content?
Section 7.2.2.1 Technical PI's and comments can occur before, after and inbetween the elements given by the Type of the document. Thus the following rule: ------------------------------------------------------------------------ -------- statEnv |- axis child:: of document { Type } : Type & processing-instructions* & comment* should be: ------------------------------------------------------------------------ -------- statEnv |- axis child:: of document { Type } : (pi? & cmt?)* , interspersepicmt(Type), (processing-instructions? & comment?) Or introduce a new symbol to denote the interspersing semantics instead of misusing &.
Hi, the latest XQuery Formal Semantics defines the fs:convert-operand() function in Section 6.1.3 [1]. In a nutshell, fs:convert-operand() casts its first argument to the type of a given sencond argument, if it had been a subtype of xdt:untypedAtomic before. Otherwise the first argument is returned unchanged. The type of fs:convert-operand(), however, is defined as fs:convert-operand($actual as item *, $expected as xdt:anyAtomicType) as xdt:anyAtomicType ? . Note that it allows an arbitrarily long sequence of items as its first argument. The return value, however, is a sequence of at most length one. The specifications only consider the case where $actual has a length no longer than one. So the return value for $actual being a longer sequence remains undefined. fs:convert-operand() could easily be fixed by restricting $actual to an optional item (item?). This, however, would make queries such as XMark 11 [2] illegal: for $p in fn:doc("auction.xml")/site/people/person return let $l := for $i in document("auction.xml")/site/open_auctions/open_auction/initial where $p/profile/@income > (5000 * $i/text()) return $i return element items { attribute name { $p/name/text() } text { count ($l) } } Note the `5000 * $i/text()'. $i/text() evaluates to node*. The Formal Semantics rule for Arithmetics [3] applies fn:data(), returning an xdt:untypedAtomic* on the non-validated document. If the first argument of fs:convert-operand() were restricted to item? it could not be applied to `$i/text()', making the above query illegal. Regards Jens Teubner [1] [2] [3] -- Jens Teubner University of Konstanz, Department of Computer and Information Science D-78457 Konstanz, Germany Tel: +49 7531 88-4379 Fax: +49 7531 88-3577 Statistics show that most people are in the majority, while a few are in the minority. -- Nitin Borwankar