1728 2005-07-18 21:47:53 +0000 [FS] stronger inference is possible in 7.2.13 "fn:subsequence" 2006-04-22 02:34:18 +0000 1 1 1 Unclassified XPath / XQuery / XSLT Formal Semantics 1.0 Last Call drafts PC Windows 2000 CLOSED FIXED P2 major --- 1 fred.zemke simeon jens.teubner jmdyck public-qt-comments oldest_to_newest 4840 0 fred.zemke 2005-07-18 21:47:53 +0000 7.2.13 fn:subsequence When the third argument is 1 and the Expr's quantifier is *, one can conclude that the length of the result is 0 or 1, ie, the quantifier is ?, without even knowing the second argument. Thus the third and fourth inferences under "static analysis" can be combined into a single and more powerful rule, to wit statEnv |- Expr1 : Type quantifier (Type) in {*} ------------------------ statEnv |- fn:subsequence (Expr1, Expr2, 1) : prime(Type)? However, I note that the first sentence of the section says that the section only applies when the second argument is 1 or fs:last, so perhaps it was decided to deliberately forgo this opportunity. 4916 1 simeon 2005-07-19 18:26:29 +0000 Reverted to 'major' for simpler handling. - Jerome 4967 2 mrys 2005-07-20 00:52:32 +0000 The joint XQuery/XSLT face-to-face meeting resolves this bug in the following way: Bug 1728 is resolved by generalizing the 3rd inference rule of 7.2.13 to work with fn:subsequence(expression, numeric literal, 1) and not generalize to arbitrary expressions. Note that while your proposed rule is a generalization, we decided to not require static typing implementations to implement this rule, since it means that one of the main use cases, when people write Expr[1] to reduce the cardinality would have to be extended to also reduce cardinality in the much less likely case of Expr[1+6 div 6]. Note that implementations are allowed to use your more general rule, but we did not feel that the use cases make it useful to require it. If you disagree with the resolution, please reopen the bug with your objection, otherwise please indicate your acceptance by closing the bug. 5035 3 mrys 2005-07-20 21:41:24 +0000 *** Bug 1766 has been marked as a duplicate of this bug. *** 5042 4 jmdyck 2005-07-20 22:19:47 +0000 [Coming in from Bug 1766...] (In reply to comment #2) > static typing implementations ... would have to be extended to also > reduce cardinality in the much less likely case of Expr[1+6 div 6]. Expr[1+6 div 6] doesn't entail a call to fn:subsequence, so how is it relevant to STA of fn:subsequence? And I don't understand why static typing implementations would have to be 'extended'. It seems to me that going from having to ask "Is the 2nd arg a 1 or $fs:last?" to "Is the 2nd arg an expr?" (Duh!) is a simplification, not an extension. 5044 5 mrys 2005-07-20 22:24:05 +0000 Personal response: The normalization of [] predicates is mapped to fn:subsequence. The desire to allow people to get static type reductions in Expr[numeric-literal] was the main driving scenario to have these static rules. If we widen the rules on fn:subsequence, it thus also affects [] expressions. 5047 6 jmdyck 2005-07-20 22:55:24 +0000 (In reply to comment #5) > > The normalization of [] predicates is mapped to fn:subsequence. Not always. In particular, not for Expr[1+6 div 6]. > The desire to > allow people to get static type reductions in Expr[numeric-literal] was the > main driving scenario to have these static rules. If we widen the rules on > fn:subsequence, it thus also affects [] expressions. Calls to fn:subsequence() resulting from normalization of predicates have a second arg that is either a NumericLiteral, $fs:last, or $fs:position. Given that you've just agreed to generalize fn:subsequence rule 3 to NumericLiteral, the only further effect (on STA for predicates) of simplifying the STA for fn:subsequence() in the suggested way would be to handle $fs:position, and my guess is that you actually *want* cardinality reduction in a case like ancestor::node()[2]. 5109 7 simeon 2005-07-21 21:57:07 +0000 Yes you are right. I got a closer look at where fn:subsequence is used in normalization of predicates and we have at least three specific changes to make it consistent: (1) Add a specific static typing rules for $fs:position, in [Section 7.2.13 The fn:subsequence function], as follows: statEnv |- Expr : Type quantifier(Type) in { * } ------------------------------------------------------------ statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type) ? (2) Add a normalization rule for PrimaryExpr[last()] in [Section 4.3.2 Filter Expressions]. I think this has just been overlooked. [| PrimaryExpr PredicateList [ last() ] |]Expr == let $fs:sequence := [PrimaryExpr PredicateList]Expr return fn:subsequence($fs:sequence,last(),1) (3) Remove the second inference rule in [Section 7.2.13 The fn:subsequence function]: statEnv |- Expr : Type quantifier(Type) in { 1, + } --------------------------------------------------------- statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type) I believe this rule will not be type safe, when the normalization result from something else than a predicate. For instance: $x//a/fn:subsequence(1,last(),1) NOTE: this last problem is subtle and somewhat worrying. We may want to reconsider the use of fn:subsequence for predicates, and instead use a fs:subsequence function which will be introduced only for the normalization of predicates (with will be dynamically equivalent to fn:subsequence, but with the more precise typing rules), and use the simpler more general rule consistently for fn:subsequence. - Jerome 5232 8 jim.melton 2005-07-26 16:36:36 +0000 This is the formal response from the XML Query WG and the XSL WG. We particularly request that both the original commenter (Fred Zemke) and the additional contributer (Michael Dyck) to consider this response. We have agreed to make the changes suggested in Additional Comment #7 and believe that the changes resolve the comment entirely. Please let us know if you agree with this resolution of your issue, by adding a comment to the issue record and changing the Status of the issue to Closed. Or, if you do not agree with this resolution, please add a comment explaining why. If you wish to appeal the WG's decision to the Director, then also change the Status of the record to Reopened. If you wish to record your dissent, but do not wish to appeal the decision to the Director, then change the Status of the record to Closed. If we do not hear from you in the next two weeks, we will assume you agree with the WG decision. 5725 9 simeon 2005-09-06 15:49:23 +0000 *** Bug 1968 has been marked as a duplicate of this bug. *** 6514 10 simeon 2005-09-28 10:18:13 +0000 *** Bug 2303 has been marked as a duplicate of this bug. *** 9404 11 jmdyck 2006-04-22 02:34:18 +0000 So, if an XQuery processor implements STA, is it required to apply the STA rules of 7.2.13 on fn:subsequence calls that *don't* arise from normalization of predicates?