[Bug 1693] New: [FS] lack of quantification and double subscripting is seriously wrong

http://www.w3.org/Bugs/Public/show_bug.cgi?id=1693

           Summary: [FS] lack of quantification and double subscripting is
                    seriously wrong
           Product: XPath / XQuery / XSLT
           Version: Last Call drafts
          Platform: PC
        OS/Version: Windows 2000
            Status: NEW
          Severity: major
          Priority: P2
         Component: Formal Semantics
        AssignedTo: simeon@us.ibm.com
        ReportedBy: fred.zemke@oracle.com
         QAContact: public-qt-comments@w3.org


4.1.5 Function calls
Under "dynamic errors", the second error condition considered is
when some argument cannot be promoted to the type of its formal
parameter in any eligible signature.  The prose description
is "If, for all possible function signatures, the evaluation
of some actual argument yields a value that cannot be
promoted to the corresponding formal type of the parameter, 
the function call raises a type error."

The logical structure of this sentence is:

 If (for all possible function signatures FS)
      (there exists an actual argument AA)
        (AA can not be promoted to the formal type of the 
         corresponding parameter of FS)
 then raise a type error.

I agree with this rule.  However, I think that the formalization of
it is incorrect.  I think your formal inference expresses the 
following (incorrect) rule:

 If (there exists an actual argument AA)
      (for all possible function signatures FS) 
        (AA can not be promoted to the formal type of the 
         corresponding parameter of FS)
 then raise a type error.

For example, the incorrect rule just given cannot detect the 
type error in fs:eq ($a, $b) when $a is an xs:double and $b
is an xs:boolean.  According to appendix B.2 "Mapping of 
overloaded internal functions",
there is a signature of fs:eq for which the first argument is
acceptable, and there is a different signature of fs:eq for which
the second argument is acceptable, but there is no signature for
which both arguments are acceptable. 

It is very hard to be sure what the inference means
because your inferences do not have explicit quantification
(a major no-no in my book).  Let me explain why I think the 
inference as stated expresses the incorrect rule rather than
the correct one.

In the first premise, expanded-QName is a free variable which 
must have existential quantification.  Similarly for m and 
FuncDecl1 through FuncDeclm in the second premise.

The third premise admirably ends with
"for all 1 <= j <= m", though "for all j, 1 <= j <= m" would 
be better (m is not actually a free variable; it is bound by 
being the number of function declarations in the preceding premise,
so you cannot mean "for all j, m, 1 <= j <= m").  

However, the third premise also has variables n, Type1, ... Typen,
and Type,
which all need quantification.  n is just the arity of the 
function, which is essentially bound by the conclusion of the 
inference.  This leaves Type1 through Typen, plus Type, to quantify.
My working hypothesis is that variables introduced in the premises
have existential quantification by default.  Then the next issue
is whether this quantification occurs before or after the 
"for all j, 1 <= j <= m".  If we read it

  (there exists Type1, ... Typen, Type) 
    (for all j, 1 <= j <= m)
      FuncDecln = define function expanded-QName(Type1, ... Typen)
                                 as Type

this won't work because it is saying that every FuncDecl has the
same list of parameter types.  Thus it must be

  (for all j, 1 <= j <= m)
    (there exists Type1, ... Typen, Type)
      FuncDecln = define function expanded-QName(Type1, ... Typen)
                                 as Type

Probably the rule would be better stated using double subscripts 
on the Type's.

In the next premise, "dynEnv |- Expri => Valuei",
the subscript i is a free variable.  I think you mean 
existential quantification on i, that is, "if there exists an 
i such that yada-yada, then raise typeError".   However, the 
last premise ends with the cryptic "1 <= i <= n".  You
don't state whether this is existential or universal quantification.
The earlier line with "for all 1 <= j <= m" suggests that you
simply forgot to include "for all" on this one, but on the other
hand, the preceding premise seems to require existential 
quantification of i.  So perhaps your convention is that you 
write universal quantification explicitly but omit the existential
quantifiers.  And indeed the logic of the situation for
this premise also inclines toward existential quantification:
you only need one i such that Valuei does not promote in order
to have a type error.
Seen in this light, the last two premises are linked, and the 
value of i must be the same in both.  

For that matter, the Type1, ... Typen introduced in the third
premise must have the same values in the last premise.

In addition, it seems clear
that the Valuei' in the final premise has existential quantification.

The conclusion I come to is
that the last three premises are interpreted as:

  (for all j, 1 <= j <= m)
    (there exists FuncDeclj, Type1, ... Typen, Type)
      [
        FuncDeclj = define function expanded-QName(Type1, ... Typen)
                                 as Type
      and
        (there exists i, 1 <= i <= n)
          (there exists Valuei, Valuei')
            [
              dynEnv |- Expri => Valuei
            and
              statEnv |- not (Valuei against Typei 
                              promotes to Valuei')
            ]
       ]

Thus the rules seem to say: there exists a single function 
declaration FuncDeclj and a single argument number i such that
the i-th argument does not promote the the i-th parameter type.
And of course this is not good enough.

Received on Sunday, 17 July 2005 22:17:24 UTC