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

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





------- Additional Comments From jmdyck@ibiblio.org  2005-07-20 20:04 -------
(In reply to comment #1)
> 
> 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.

Nope, not me. In Bug 1763, I recommended eliminating the uses in 7.2.10, not
because it was confusing, but because it didn't convey the intended semantics.
(And in Bug 1584, I talked about the problems surrounding "for all 1 <= j <= m"
 , but that's a different notation with a different intent.)

> 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.

No, it isn't. Except for the cases noted above, each occurrence of 1 <= i <= k
is just a judgment that must be made to hold like all the other premises; it is
not some kind of annotation saying that other premises should be duplicated in
the way you indicate. Thus, the rule in question can be interpreted:

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

i.e., if either of the two Exprs yields false, then the and-expr yields false.

This is the intended semantics for i <= i <= k for rules in:
  4.1.5 / DErr / rule 1
  4.6   / (DEv|DErr)
  4.8.2 / DErr
  4.11  / (DEv|DErr)
(Note that the accompanying prose tends to use words like "any", "either", or
"some", rather than "all" or "every".)

Received on Wednesday, 20 July 2005 20:04:46 UTC