This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
Section 8.5.1 of the XQuery Formal Semantics contains the judgment prime(t1) can be promoted to prime(t1') prime(t2) can be promoted to prime(t2') --------------------------------------------- (t1 | t2) can be promoted to (t1' | t2') This rule seems unnecessarily complex. The rule t1 can be promoted to t t2 can be promoted to t ----------------------------------------------------- (t1 | t2) can be promoted to t contains the same definition (together with the remaining rules in 8.5.1). Note that in the original inference rule, t1' could be the same type as t2', which is why I replaced it with t in "my" rule. If promotability holds for prime types, it also holds for the original types (hence, my replacement of prime types with their original types). The same (original) definition is also *inconsistent* with a second rule in 8.5.1: prime(t1) can be promoted to prime(t2) quant(t1) <= quant(t2) ----------------------------------------------------------------- t1 can be promoted to t2 Now if I replace t1 with (t1 | t1) and t2 with (t2 | t2) (which are the same types), and use the definition at the beginning of my report, I can "circumvent" the restriction on quantifiers.
I've looked at these rules again, and I believe Jens is correct. The last two rules in 8.5.1 are inconsistent and unnecessary complex. The rule that Jens suggest is both simpler and covers the intended semantics. I would recommend to accept the bug and replace the last two inference rules in 8.5.1 by the rule Jens suggests. - Jerome
Jens, The XSLT and XML Query Working Groups have looked at your comment and decided to accept your suggested changes. Best regards, - Jerome On behalf of the XSLT and XML Query WGs