- From: <bugzilla@wiggum.w3.org>
- Date: Thu, 07 Sep 2006 07:47:55 +0000
- To: public-qt-comments@w3.org
- CC:

http://www.w3.org/Bugs/Public/show_bug.cgi?id=3664 Summary: Definition of type promotion complex and inconsistent Product: XPath / XQuery / XSLT Version: Candidate Recommendation Platform: All OS/Version: All Status: NEW Severity: normal Priority: P2 Component: Formal Semantics AssignedTo: simeon@us.ibm.com ReportedBy: jens.teubner@in.tum.de QAContact: public-qt-comments@w3.org 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.

Received on Thursday, 7 September 2006 07:48:03 UTC