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

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





------- Additional Comments From fred.zemke@oracle.com  2005-07-25 20:47 -------
Regarding this thread, I think that my suggestion that inferences
are patterns representing all possible substitutions for the 
variables would handle my concern, and simultaneously convey
the correct part of additional comment #1.  

Regarding the 
use of "1 <= i <= n", I think the proposal in additional 
comment #3, to write this on a separate line to avoid the 
appearance of a quantifier, is a good one and should be 
accepted.  I am personally indifferent whether it is expressed
as 1 <= i <= n or i in {1, ..., n}, since, as a mathematician,
I regard "for all i in {1, ..., n}" as just a much a 
quantifier as "for all i, 1 <= i <= n".  The important thing is
to get the judgment on its own line.  

It would also help if section 2 somewhere explicitly considered 
this notation.  Using my convention that every inference is a 
pattern,  the inference

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

is a pattern for inferences such as

  dynEnv |- ($a = $b) => false
  1 <= 1 <= 2
  ------------------------------------------
  dynEnv |- ($a = $b) and ($c = $d) => false

and

  dynEnv |- ($c = $d) => false
  1 <= 2 <= 2
  ------------------------------------------
  dynEnv |- ($a = $b) and ($c = $d) => false

Regarding the proposal that ellipses be used instead of universal
quantification in inferences, I find this acceptable with two
provisos:

a) document it.  Jim relayed to me that someone thought this
was already well understood, but what does it cost you to 
write a paragraph about a convention?

b) you must examine every premise with universal quantification
and decide whether the vanishing case is permitted (ie,
the upper bound is 0 and there are no cases at all), or 
alternatively the minimum for the upper bound is 1.  See 
my comment #1737 about the inference in 8.1.10 "Union type of
derived types".  After much inferencing on my own part, I concluded
that the ellipsis 1 ... n is permitted to vanish (n = 0)
whereas the ellipsis 1 ... m is not permitted to vanish
(m > 0).  So it seems that there is something to explain 
about ellipses after all!

My suggestion is that every ellipsis should come with an 
additional judgment, either of the form n >= 0 or n > 0,
on a separate line, and section 2 should explain this convention
with an example.

Received on Monday, 25 July 2005 20:47:57 UTC