[Bug 3664] Definition of type promotion complex and inconsistent

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