This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
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"
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
(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".)
It might help if you (a) rewrote 1 <= i <= k as i in { 1, ..., k } (since that ties into existing syntax whose semantics readers might be more comfortable with), and (b) put the premise on a separate line (so it looked less like an annotation on the preceding premise).
Michael, Thanks for the additional feedback. Still from all this discussion, it seems to me that we would be better off by avoiding the 1 <= i <= n notation entirely. For the universally quantified ones, we can use ellipsis which is used for other places. For the existentially quantified ones we can use several rules, or i in { 1,..., n} as you suggest. I believe that would cover all the cases. Did I miss anything? - Jerome
(In reply to comment #4) > > Still from all this discussion, it seems to me that we would > be better off by avoiding the 1 <= i <= n notation entirely. Yup, you're probably right. > I believe that would cover all the cases. Did I miss anything? If we're ignoring the "for all 1 <= j <= m" case of 4.1.5 (which is covered by Bug 1584 and Bug 1693), then no, I don't think you missed anything. But note that I'm not the original poster.
The WG will deal with this editorially.
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.
Implemented the proposed editorial suggestions to improve the notation section. More specifically, fixed the notation section, and the rest of the specification to use the following conventions: * 1 <= i <= n is replaced by i in {1,...,n} and always put on a different line. * ellispes are now always meant to deal with cases from 1 to n, and never bottom out to the vanishing case. Added explicit inference rules when needed in the spec to deal with the vanishing case. Documented that convention in the notation section. - Jerome