W3C home > Mailing lists > Public > public-qt-comments@w3.org > July 2005

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

From: <bugzilla@wiggum.w3.org>
Date: Wed, 20 Jul 2005 18:45:30 +0000
To: public-qt-comments@w3.org
Cc:
Message-Id: <E1DvJZS-0001ml-GE@wiggum.w3.org>

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

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