This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.

Bug 1728 - [FS] stronger inference is possible in 7.2.13 "fn:subsequence"
Summary: [FS] stronger inference is possible in 7.2.13 "fn:subsequence"
Status: CLOSED FIXED
Alias: None
Product: XPath / XQuery / XSLT
Classification: Unclassified
Component: Formal Semantics 1.0 (show other bugs)
Version: Last Call drafts
Hardware: PC Windows 2000
: P2 major
Target Milestone: ---
Assignee: Jerome Simeon
QA Contact: Mailing list for public feedback on specs from XSL and XML Query WGs
URL:
Whiteboard:
Keywords:
: 1968 2303 (view as bug list)
Depends on:
Blocks:
 
Reported: 2005-07-18 21:47 UTC by Fred Zemke
Modified: 2006-04-22 02:34 UTC (History)
2 users (show)

See Also:


Attachments

Description Fred Zemke 2005-07-18 21:47:53 UTC
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.
Comment 1 Jerome Simeon 2005-07-19 18:26:29 UTC
Reverted to 'major' for simpler handling.
- Jerome
Comment 2 Michael Rys 2005-07-20 00:52:32 UTC
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.
Comment 3 Michael Rys 2005-07-20 21:41:24 UTC
*** Bug 1766 has been marked as a duplicate of this bug. ***
Comment 4 Michael Dyck 2005-07-20 22:19:47 UTC
[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.
Comment 5 Michael Rys 2005-07-20 22:24:05 UTC
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.
Comment 6 Michael Dyck 2005-07-20 22:55:24 UTC
(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].
Comment 7 Jerome Simeon 2005-07-21 21:57:07 UTC
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
Comment 8 Jim Melton 2005-07-26 16:36:36 UTC
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.
Comment 9 Jerome Simeon 2005-09-06 15:49:23 UTC
*** Bug 1968 has been marked as a duplicate of this bug. ***
Comment 10 Jerome Simeon 2005-09-28 10:18:13 UTC
*** Bug 2303 has been marked as a duplicate of this bug. ***
Comment 11 Michael Dyck 2006-04-22 02:34:18 UTC
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?