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

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


simeon@us.ibm.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |ASSIGNED




------- Additional Comments From simeon@us.ibm.com  2005-07-20 18:45 -------
The semantics is really neither both of those universal/existential alternative
that you provide. This is much more of a conditional inference. The way to read
it is:

Here is the inference rule:

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

It essentially means:

IF
  statEnv |- Expr1 : Type1
AND
  statEnv |- Expr2 : Type2
THEN
  statEnv |- Expr1, Expr2 : Type 1, Type2

The important point here is that *all* of the preconditions must hold for the
conclusion to hold.

In a few cases, we use the following notation (1 <= i <= k). We have a separate
 comment from Michael Dyck I believe which recommends not to use that notation
which is confusing. A better way to write those cases is as follows:

dynEnv |- Expr1 => false
dynEnv |- Expr2 => false
--------------------------------------
dynEnv |- Expr1 and Expr2 => false

which is what is intended in the rest of the spec. This clearly illustrate
that the 1 <= i <= k notation is not only confusing but leads to bugs. Since in
the case here its just the wrong semantics. What is intended is the two
following rules:

dynEnv |- Expr1 => false
--------------------------------------
dynEnv |- Expr1 and Expr2 => false

dynEnv |- Expr2 => false
--------------------------------------
dynEnv |- Expr1 and Expr2 => false

Which is how the semantic should be written for those cases.

- Jerome

Received on Wednesday, 20 July 2005 18:45:36 UTC