From: <bugzilla@wiggum.w3.org>

Date: Sun, 17 Jul 2005 22:17:21 +0000

To: public-qt-comments@w3.org

Cc:

Message-Id: <E1DuHRp-00049J-Ev@wiggum.w3.org>

Date: Sun, 17 Jul 2005 22:17:21 +0000

To: public-qt-comments@w3.org

Cc:

Message-Id: <E1DuHRp-00049J-Ev@wiggum.w3.org>

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

*
This archive was generated by hypermail 2.3.1
: Wednesday, 7 January 2015 15:45:25 UTC
*