[Bug 1612] New: what is the quantification of unbound variables?

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

           Summary: what is the quantification of unbound variables?
           Product: XPath / XQuery / XSLT
           Version: Last Call drafts
          Platform: PC
        OS/Version: Windows 2000
            Status: NEW
          Severity: normal
          Priority: P2
         Component: Formal Semantics
        AssignedTo: simeon@us.ibm.com
        ReportedBy: fred.zemke@oracle.com
         QAContact: public-qt-comments@w3.org


2.1.5 Putting it together
You have not stated what is the quantification (universal or
existential) for your free variables (Expr1, Type1, etc.) in
your inferences.  Looking at your first example

statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
------------------------
statEnv |- Expr1, Expr2 : Type 1, Type2

it seems that you mean implicit universal quantification for
any variable appearing below the line, like this:

(for all Expr1, Expr2, Type1 and Type2)
[
  statEnv |- Expr1 : Type1
  statEnv |- Expr2 : Type2
  ------------------------
  statEnv |- Expr1, Expr2 : Type 1, Type2
]

Turning to variables that appear only above the line, 
consider the first inference in 4.6 "Logical expressions"
under "dynamic evaluation":

dynEnv |- Expri => false  1 <= i <= 2
--------------------------------------
dynEnv |- Expr1 and Expr2 => false

Here you must mean implicit existential quantification for i,
so that this is implicitly:

(for all Exp1, Expr2) 
[
  (there exists i, 1 <= i <= 2)
  [
    dynEnv |- Expr1 => false
  ]
  ---------------------------
  dynEnv |- Expr1 and Expr2 => false
]

These conventions should be stated explicitly, especially 
since the implicit quantification for variables below the 
line and above the line are different.

It might also be helpful to adopt the convention that 
quantifiers above the line are always shown explicitly,
because sometimes you use existential and sometimes you
use universal above the line.  I personally do not regard
"1 <= i <= 2" as indicative of existential quantification,
and would prefer to see "there exists i, 1 <= i <= 2"
or "for some i, 1 <= i <= 2"

Received on Friday, 15 July 2005 00:10:39 UTC