Version 1.3 of ai12s/ai12-0158-1.txt

Unformatted version of ai12s/ai12-0158-1.txt version 1.3
Other versions for file ai12s/ai12-0158-1.txt

!standard 4.5.8(1/3)          15-03-26 AI05-0158-1/02
!standard 4.5.8(6/3)
!standard 4.5.8(8/3)
!standard 4.5.8(9/3)
!class binding interpretation 15-03-23
!status Corrigendum 2015 15-03-26
!status ARG Approved 8-0-2 15-03-26
!status work item 15-03-23
!status received 15-02-28
!priority Low
!difficulty Easy
!qualifier Clarification
!subject Definition of quantified expressions
!summary
Reword the semantics of quantified expressions to reduce confusion.
!question
What is the value of a quantified expression if the array has zero elements? Is it always True? (Yes, for All.) Always False? (Yes, for Some.)
The RM says: "if the quantifier is all, the expression is True if the evaluation of the predicate yields True for each value of the loop parameter. It is False otherwise." It is definitely not clear to me, but this wording seems to lean toward being treated as False.
!recommendation
(See Summary.)
!wording
Add before 4.5.8(1/3): [before "Syntax", that is as introductory text]
Quantified expressions provide a way to write universally and existentially quantified predicates over containers and arrays.
Replace 4.5.8(6/3) with:
For the evaluation of a quantified_expression, the loop_parameter_specification or iterator_specification is first elaborated. The evaluation of a quantified_expression then evaluates the predicate for the values of the loop parameter in the order specified by the loop_parameter_specification (see 5.5) or iterator_specification (see 5.5.2).
4.5.8(7/3) [not modified, provided for context]
The value of the quantified_expression is determined as follows:
Replace 4.5.8(8/3) with:
* If the quantifier is all, the expression is False if the evaluation of any
predicate yields False; evaluation of the quantified_expression stops at that point. Otherwise (every predicate has been evaluated and yielded True), the expression is True. Any exception raised by evaluation of the predicate is propagated.
Replace 4.5.8(9/3) with:
* If the quantifier is some, the expression is True if the evaluation of any
predicate yields True; evaluation of the quantified_expression stops at that point. Otherwise (every predicate has been evaluated and yielded False), the expression is False. Any exception raised by evaluation of the predicate is propagated.
!discussion
AARM 4.5.8(8.a/3) gives the intended answer (True) for quantifier all. How this supposed ramification is derived is not crystal clear.
The ramifications follow from the standard mathematical meaning of the forall and exists set operators. However, that may not be obvious to readers with less formal mathematics knowledge. We don't want Ada to only be understandable to a handful of elite people.
An additional issue was raised during the discussion of wording alternatives for this bullet: the wording makes it sound like all of the predicates are evaluated before the answer is determined. It then follows with a sentence that effectively says to forget that, actually it is short-circuited. It would be better to tell the truth in the first place.
Thus, we adopt wording which says what the operations do without any attempt to make them appear to be similar to some set operation. That sort of thing is best done in the introduction, rather than trying to bend the dynamic semantics to serve that purpose. We add an introductory paragraph to serve this purpose.
!corrigendum 4.5.8(1/3)
Insert before the paragraph:
quantified_expression ::= for quantifier loop_parameter_specification => predicate | for quantifier iterator_specification => predicate
the new paragraph:
Quantified expressions provide a way to write universally and existentially quantified predicates over containers and arrays.
!corrigendum 4.5.8(6/3)
Replace the paragraph:
For the evaluation of a quantified_expression, the loop_parameter_specification or iterator_specification is first elaborated. The evaluation of a quantified_expression then evaluates the predicate for each value of the loop parameter. These values are examined in the order specified by the loop_parameter_specification (see 5.5) or iterator_specification (see 5.5.2).
by:
For the evaluation of a quantified_expression, the loop_parameter_specification or iterator_specification is first elaborated. The evaluation of a quantified_expression then evaluates the predicate for the values of the loop parameter in the order specified by the loop_parameter_specification (see 5.5) or iterator_specification (see 5.5.2).
!corrigendum 4.5.8(8/3)
Replace the paragraph:
by:
!corrigendum 4.5.8(9/3)
Replace the paragraph:
by:
!ASIS
No ASIS effect.
!ACATS test
This rule does not change the meaning of any quantified expression (since the intent is specified in AARM notes, so no additional tests are needed.
!appendix

From: Brad Moore
Sent: Saturday, February 28, 2015  7:48 PM

I ran across an issue when converting Ada 2005 code into Ada 2012.

What is the value of a quantified expression if the array has zero elements?  Is
it always true? Always false?

It was particularly unclear to me if the quantifier is "all".

For "some", it seemed obvious to me that the value should be always false, since
one is checking for existence of some property in an array. However, when I
mentioned this to Randy, he thought it should return True for both the "some"
case and the "all" case, since their originally intended use is in assertions,
for which True means OK. He thought that nothing should be always be OK. But he
also added that it might depend on the usage.

The RM says; "if the quantifier is all, the expression is True if the evaluation
of the predicate yields True for each value of the loop parameter. It is False
otherwise."  Its definitely not clear to me, but this wording seems to lean
toward being treated as  false.

The case I ran into was an entry guard that had a quantified expression checking
to see if the elements in a variant array component whose length was dependent
on a discriminant all had the same value.

          when (for all I in Gate'Range => Gate (I) = True)

Here I want the guard to pass if all elements are true, but also if there are no
elements. This suggests that returning True is the correct choice.

However, I also note that this is confusing code to the reader, because he will
likely be scratching is head just as I was.

It would be clearer to write something like;

          when (Gate'Length = 0 or else
                for all I in Gate'Range => Gate (I) = True)

So ideally, it would be nice if the first version of the guard above could be
discouraged from use somehow, but that may be too hard to do, or too much of a
corner case to worry about.

In any case, I think the RM should be more clear about what value to expect when
evaluating such expressions.

****************************************************************

From: Ed Schonberg
Sent: Saturday, February 28, 2015  8:19PM

The convention in set theory is that a universally quantified expression over an
empty set is always true. So it is true that all the elements of the empty set
are green. You can devise a consistent set of axioms for set theory that takes
the opposite view, but this is one is the most intuitive,  This is also the
current implementation in GNAT (not that this is a proof of anything).

Itís consistent with the identity which obviously holds for non-empty sets:
     (some X in S => (P (X))  = not (all X in S => not P (X))

****************************************************************

From: Robert Dewar
Sent: Saturday, February 28, 2015  8:23 PM

> For "some", it seemed obvious to me that the value should be always
> false, since one is checking for existence of some property in an
> array. However, when I mentioned this to Randy, he thought it should
> return True for both the "some" case and the "all" case, since their
> originally intended use is in assertions, for which True means OK.
> He thought that nothing should be always be OK. But he also added that
> it might depend on the usage.

If seems OBVIOUS to me that some should be false for the null set and all should
be true for the null set. That's the convention in mathematics for a long time!

> The RM says; "if the quantifier is all, the expression is True if the
> evaluation of the predicate yields True for each value of the loop
> parameter. It is False otherwise."  Its definitely not clear to me,
> but this wording seems to lean toward being treated as  false.

It IS True for each value of the loop, or think of it this way, it is true for
ALL of them.

> The case I ran into was an entry guard that had a quantified
> expression checking to see if the elements in a variant array
> component whose length was dependent on a discriminant all had the same value.
>
>            when (for all I in Gate'Range => Gate (I) = True)
>
> Here I want the guard to pass if all elements are true, but also if
> there are no elements. This suggests that returning True is the
> correct choice.

Yes, of course it is

> However, I also note that this is confusing code to the reader,
> because he will likely be scratching is head just as I was.
>
> It would be clearer to write something like;
>
>            when (Gate'Length = 0 or else
>                  for all I in Gate'Range => Gate (I) = True)
>
> So ideally, it would be nice if the first version of the guard above
> could be discouraged from use somehow, but that may be too hard to do,
> or too much of a corner case to worry about.
>
> In any case, I think the RM should be more clear about what value to
> expect when evaluating such expressions.

Sure, but I am AMAZED that anyone would question the obvious mathematical
intepretation. Anything else would be perverse.

****************************************************************

From: Robert Dewar
Sent: Saturday, February 28, 2015  8:27 PM

> The convention in set theory is that a universally quantified
> expression over an empty set is always true. So it is true that all
> the elements of the empty set are green.

I agree with this

> You can devise a consistent
> set of axioms for set theory that takes the opposite view, but this is
> one is the most intuitive,

I do not agree with the idea that this is more intuitive, I think it is
completely non-intuitive, but Dodgson lost this argument ages ago, and it is now
well established that universal predicates over the null set are True.

> This is also the current
> implementation in GNAT (not that this is a proof of anything). Itís
> consistent with the identity which obviously holds for non-empty
> sets: (some X in S => (P (X))  = not (all X in S => not P (X))

It's the only conceivable implementation. The difficulty in reading the RM comes
in my mind from the fact that it is not intuitive. If I ask someone who has no
children "Are all your children over 18?", they do not answer yes. So indieed,
clarification in the RM is appropriate here.

****************************************************************

From: Tucker Taft
Sent: Sunday, March  1, 2015  8:40 AM

> I ran across an issue when converting Ada 2005 code into Ada 2012.
>
> What is the value of a quantified expression if the array has zero
> elements?  Is it always true? Always false?
>
> It was particularly unclear to me if the quantifier is "all".
> ...
> In any case, I think the RM should be more clear about what value to
> expect when evaluating such expressions.

The AARM includes notes that address these questions.
See AARM 4.5.8(8.a/3, 9.a/3).  I think these were aimed at compiler writers who
might not be that familiar with the rules of formal logic (unfortunately!).

As Robert points out, this isn't always intuitive, but the rules of logic have
been very clear on the rules for a long time in this area, and Ada isn't about
to reverse that!

See the Wikipedia entry on "vacuous truth" for a longer discussion of this
issue:

    http://en.wikipedia.org/wiki/Vacuous_truth

I suppose we could add a user note, if we felt it important enough.

****************************************************************

From: Robert Dewar
Sent: Sunday, March  1, 2015  9:07 AM

If it confused Brad, that by definition means that it is important enough to add
a note, I don't like the "each" wording for the universal quantifier, "all"
wording would be better.

****************************************************************

From: Brad Moore
Sent: Sunday, March  1, 2015  9:36 AM

Although the world of mathematics has sorted this out long ago, it wasn't all
that clear that Ada is following a mathematical model for the syntax. Its great
that it does, but I think users will be tripping over this, as it is
non-intuitive, so a user note would be helpful. In fact I think it might be nice
if the compiler generated a warning when a universal quantifier is applied to an
array that could potentially could have zero length.

****************************************************************

From: Bob Duff
Sent: Sunday, March  1, 2015  9:39 AM

> If it confused Brad, that by definition means that it is important
> enough to add a note, I don't like the "each" wording for the
> universal quantifier, "all" wording would be better.

Perhaps, but I think that's really the job of textbook authors.

****************************************************************

From: Robert Dewar
Sent: Sunday, March  1, 2015  5:29 PM

> In fact I think it might be nice if the compiler generated a warning
> when a universal quantifier is applied to an array that could
> potentially could have zero length.

I don't like that suggestion at all, I think it would generate tons of annoying
and confusing false positives. Applying universal quantifiers to null sets
happens ALL the time, and is completely normal and standard, not an appropriate
subject for a warning IMO.

****************************************************************

From: Robert Dewar
Sent: Sunday, March  1, 2015  5:30 PM

> Perhaps, but I think that's really the job of textbook authors.

Well talking about "each" of the elements of a null set is not standard
mathematical terminology, and IMO is peculiar, so given we choose to use this
peculiar terminology, I see no harm in an explanatory note.

****************************************************************

From: Jeff Cousins
Sent: Monday, March  2, 2015  4:26 AM

> If it confused Brad, that by definition means that it is important enough to
> add a note, I don't like the "each" wording for the universal quantifier,
> "all" wording would be better.

I can remember this coming up during the original ARG discussion of AI05-0176,
and I think half the people at the meeting were surprised (even if they might
not admit it now!), so I would join in with recommending a user note.  "All"
might be better too if it could be wrapped up in the same change.

****************************************************************

From: John Barnes
Sent: Monday, March  2, 2015 10:55 AM

In old Spark

For All over an empty array ==> true
There Exists (that is for some) over an empty array ==> false

So that's consistent.

****************************************************************

From: Robert Dewar
Sent: Tuesday, March  3, 2015  7:34 AM

Regarding universal quantifiers and the null set. There is a picture going
around on face book of the oval office, with the caption

"A group picture of all the Republican Presidentss who have
  reduced the deficit in the last 50 years."

The picture is of an empty office

****************************************************************

From: Randy Brukardt
Sent: Tuesday, March 17, 2015  9:46 PM

> > If it confused Brad, that by definition means that it is important
> > enough to add a note, I don't like the "each"
> > wording for the universal quantifier, "all" wording would be better.
>
> I can remember this coming up during the original ARG discussion of
> AI05-0176, and I think half the people at the meeting were surprised
> (even if they might not admit it now!), so I would join in with
> recommending a user note.
> "All" might be better too if it could be wrapped up in the same
> change.

I just took a look at this to see how to proceed.

I certainly agree that we ought to do something, but I don't think a note fixes
anything. Looking at the wording that we have:

* If the quantifier is all, the expression is True if the evaluation of the
  predicate yields True for each value of the loop parameter. It is False
  otherwise.

   Ramification: The expression is True if the domain contains no values.

* If the quantifier is some, the expression is True if the evaluation of the
  predicate yields True for some value of the loop parameter. It is False
  otherwise.

   Ramification: The expression is False if the domain contains no values.

The only way I can derive those "Ramifications" is to apply the Dewar rule,
because the wording is essentially identical, but somehow we're supposed to come
up with a different result for them.

Specifically, the second wording is crystal-clear: the expression is only true
if "some value" of the loop parameter yields True. If there are no values of the
loop parameter, then we clearly fall into the otherwise.

If we then look at the first wording in the same way, we're going to get the
same result: the expression is only True if "each value" yields True. Again, if
there are no values, we're going to fall into the otherwise -- there are no
values that return True, so how possibly could the wording apply?

I don't think that trivial wording change could possibly change that. I'd prefer
the wording had used "every" rather than "each", but that changes nothing in the
null case. The suggestion to use "all" doesn't work at all, as it would require
changing the sentence to a plural form -- and then the entire point of using the
same form for both is lost, in which case we should simply say what we mean and
be done with it.

Thus I suggest changing the first wording to (4.5.8(8/3)):

If the quantifier is all, the expression is True if the evaluation of the
predicate yields True for {every}[each] value of the loop parameter {or if there
are no values of the loop parameter}. It is False otherwise.

I don't think we need a similar change to 4.5.8(9/3), but we could consider
making that clear too:

If the quantifier is some, the expression is True if the evaluation of the
predicate yields True for some value of the loop parameter. It is False
otherwise {(including when there are no values of the loop parameter)}.

We then don't need a note nor the AARM Ramifications.

My thinking here is that we've already argued this twice or more (presuming
Jeff's memory is accurate, but it probably is based on the AARM ramifications;
someone wanted the meaning clarified). It's better to say outright what we mean
so that it's not necessary to have this discussion again.

Thoughts? Improvements?

****************************************************************

From: Ed Schonberg
Sent: Tuesday, March 17, 2015  9:54 PM

> I certainly agree that we ought to do something, but I don't think a
> note fixes anything. Looking at the wording that we have:
>
> * If the quantifier is all, the expression is True if the evaluation
> of the predicate yields True for each value of the loop parameter. It
> is False otherwise.
>
>  Ramification: The expression is True if the domain contains no values.

The ramification would be more obvious if you use the converse:

    if the quantifier is all, the expression is False if the evaluation of the
    predicate yields False for any value of the loop parameter. Is it True
    otherwise.

The ramification then falls out. It doesnít in the original.

****************************************************************

From: Randy Brukardt
Sent: Tuesday, March 17, 2015  10:17 PM

> The ramification would be more obvious if you use the converse:
>
>     if the quantifier is all, the expression is False if the
>     evaluation of the predicate
>     yields False for any value of the loop parameter. Is it True otherwise.
--------------------------------------------------------^^^^^---------------^
Looks like a question mark is missing here. Freudian slip! :-)

> The ramification then falls out. It doesn't in the original.

Seriously, this is better than my long-winded version. We'd still want the
ramifications, but at least one can read the wording and reason to arrive at the
correct result. It also melds better with the rest of the paragraph (the part
about being allowed to stop early).

I'll write it up this way unless some else has an even better idea.

****************************************************************

From: Ben Brosgol
Sent: Tuesday, March 17, 2015  10:45 PM

> The ramification would be more obvious if you use the converse:
>
>      if the quantifier is all, the expression is False if the evaluation of
>      the predicate yields False for any value of the loop parameter. Is it
>      True otherwise.

I don't like "for any value of the loop parameter" since "any" is ambiguous and
could be interpreted to mean "all" :-)  How about

<<
   if the quantifier is all, the expression is False if the evaluation of the
   predicate yields False for some value of the loop parameter. It is True
   otherwise.
 >>

****************************************************************

From: Jean-Pierre Rosen
Sent: Wednesday, March 18, 2015  12:50 AM

> If the quantifier is all, the expression is True if the evaluation of
> the predicate yields True for {every}[each] value of the loop
> parameter {or if there are no values of the loop parameter}. It is False
> otherwise.
>
> If the quantifier is some, the expression is True if the evaluation of
> the predicate yields True for some value of the loop parameter. It is
> False otherwise {(including when there are no values of the loop parameter)}.

Looks good, and will not leave any room for argument.

****************************************************************

From: Tucker Taft
Sent: Wednesday, March 18, 2015  2:50 AM

> <<
>    if the quantifier is all, the expression is False if the evaluation
>    of the predicate yields False for some value of the loop parameter.
>    It is True otherwise.
>  >>

I find it confusing to use "some" when we are defining "all."  How about "at
least one"? I.e.:

    if the quantifier is ALL, the expression is False if the evaluation of the
    predicate yields False for at least one value of the loop parameter. It is
    True otherwise.

****************************************************************

From: Jeff Cousins
Sent: Wednesday, March 18, 2015   2:52 AM

> I don't like "for any value of the loop parameter" since "any" is
> ambiguous and could be interpreted to mean "all" :-)  How about

Any seems clear enough to me; my dictionary says one out of many.

****************************************************************

From: Robert Dewar
Sent: Wednesday, March 18, 2015  7:38 AM

> I certainly agree that we ought to do something, but I don't think a
> note fixes anything. Looking at the wording that we have:
>
> * If the quantifier is all, the expression is True if the evaluation
> of the predicate yields True for each value of the loop parameter. It
> is False otherwise.
>
>     Ramification: The expression is True if the domain contains no values.
>
> * If the quantifier is some, the expression is True if the evaluation
> of the predicate yields True for some value of the loop parameter. It
> is False otherwise.
>
>     Ramification: The expression is False if the domain contains no values.
>
> The only way I can derive those "Ramifications" is to apply the Dewar
> rule, because the wording is essentially identical, but somehow we're
> supposed to come up with a different result for them.

Well I guess some people are really confused by standard mathematics!
No, the wording is NOT "essentially identical", one says each and one says some.
HUGE difference. To me the wording is totally clear without the stated
ramifications, which I would rather call notes, but obviously it confuses some
people, so let's add the notes

> If we then look at the first wording in the same way, we're going to
> get the same result: the expression is only True if "each value"
> yields True. Again, if there are no values, we're going to fall into
> the otherwise -- there are no values that return True, so how possibly could
> the wording apply?

I really can't spend time giving an elementary math lesson here, but each of no
values is a very well defined concept, and I would have thought that the wording
of the first case was crystal clear, especially since we know ab initio that the
universal quantifier is true over the null set (any other intepretation would be
bizarre nonsense).

> I don't think that trivial wording change could possibly change that.
> I'd prefer the wording had used "every" rather than "each", but that
> changes nothing in the null case. The suggestion to use "all" doesn't
> work at all, as it would require changing the sentence to a plural
> form -- and then the entire point of using the same form for both is
> lost, in which case we should simply say what we mean and be done with it.

I agree, no point in changing the wording, if you are going to misinterpret it
anyway, then others may do so to, so a note is the appropriate approach.

> Thus I suggest changing the first wording to (4.5.8(8/3)):
>
> If the quantifier is all, the expression is True if the evaluation of
> the predicate yields True for {every}[each] value of the loop
> parameter {or if there are no values of the loop parameter}. It is False
> otherwise.

I object to the "or if there are no values ...", it is redundant nonsense.
Instead add a note for the unenlightened.

> I don't think we need a similar change to 4.5.8(9/3), but we could
> consider making that clear too:

> My thinking here is that we've already argued this twice or more
> (presuming Jeff's memory is accurate, but it probably is based on the
> AARM ramifications; someone wanted the meaning clarified). It's better
> to say outright what we mean so that it's not necessary to have this
> discussion again.

I don't think adding redundant junk is the answer, I think it just confuses! It
has anyone reasonable wondering "well, yes, of course, so why are they saying
that?"

The wording as is is fine. I don't need the notes, but apparently some do!

****************************************************************

From: Robert Dewar
Sent: Wednesday, March 18, 2015  7:40 AM

> Seriously, this is better than my long-winded version. We'd still want
> the ramifications, but at least one can read the wording and reason to
> arrive at the correct result. It also melds better with the rest of
> the paragraph (the part about being allowed to stop early).

MUCH better than the long-winded version (which is just misguided I think). I am
cool with Ed's change, I don't think it changes anything, but if it makes some
non-mathematicians happier, why not? I still would not state the notes as
ramifications, they are too obvious IMO to be elevated to this level, keep them
as notes.

****************************************************************

From: Erhard Ploedereder
Sent: Wednesday, March 18, 2015  7:40 AM

I really do not see a problem with the wording at all. The way to derive these
ramifications is to appeal to standard logic. I don't think we need a statements
that Ada applies standard logic to its boolean operations and to the description
of Ada semantics. If not so, we also need to explain why 2**0 = 1, because after
all, how do you derive this from the Ada manual? (And it is surprising to some!)

****************************************************************

From: Robert Dewar
Sent: Wednesday, March 18, 2015  7:42 AM

>      if the quantifier is ALL, the expression is False if the evaluation of
>      the predicate yields False for at least one value of the loop parameter.
>      It is True otherwise.

That's also OK, a bit odd, but equivalent to the original, so certainly
acceptable.

****************************************************************

From: Erhard Ploedereder
Sent: Wednesday, March 18, 2015  7:53 AM

I agree with Robert. Odd, but it also points to the connection between "all not"
and "not some", which may be useful as well.

****************************************************************

From: Steve Baird
Sent: Wednesday, March 18, 2015  11:19 AM

> How about "at least one"?

I don't like this because quantified expressions are defined to be
short-circuiting (i.e., their evaluation loop exits as soon as the result has
been determined).

To me, "at least one" suggests the opposite - it suggests that two or more such
evaluations might be possible.

> I find it confusing to use "some" when we are defining "all."
An argument in favor of the original wording.

I generally agree with Robert that there isn't really any problem worth fixing
with the current wording, but if folks really find it confusing I would focus on
the contradiction between
    The evaluation of a quantified_expression then evaluates the
    predicate for each value of the loop parameter.
(which incorrectly states that short-circuiting is not performed) and the two
      Evaluation of the quantified_expression stops when  ...
rules (which correctly state that short-circuiting is performed).

Contrast this with the more precise wording for for-loops:
   Otherwise, the sequence_of_statements is executed once for each value
   of the discrete subtype defined by the discrete_subtype_definition
   that satisfies the predicate of the subtype (or until the loop is
   left as a consequence of a transfer of control).

****************************************************************

From: Robert Dewar
Sent: Wednesday, March 18, 2015  12:21 PM

>> How about "at least one"?
>
> I don't like this because quantified expressions are defined to be
> short-circuiting (i.e., their evaluation loop exits as soon as the
> result has been determined).
>
> To me, "at least one" suggests the opposite - it suggests that two or
> more such evaluations might be possible.

good point, let's leave the original wording here and not even bother with a
note. If someone asks, there will be plenty of people who can tell them the
answer (well known for over a hundred years (*))

>> I find it confusing to use "some" when we are defining "all."
> An argument in favor of the original wording.

(*) There was a big argument over the meaning of predicates on the null set in
the eighteenth century with Dodgson (Alice) being a main proponent of predicates
being false on the null set, but he lost, and ever since then, it is taken as
revealed obvious truth that all predicates are true on the null set.

****************************************************************

From: Robert Dewar
Sent: Wednesday, March 18, 2015  1:17 PM

> Any seems clear enough to me; my dictionary says one out of many.

So far no suggested rewording is clearly  superior to the original, which is IMO
perfectly clear, let's just leave it as is.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, March 18, 2015  2:42 PM

> > Any seems clear enough to me; my dictionary says one out of many.
>
> So far no suggested rewording is clearly  superior to the original,
> which is IMO perfectly clear, let's just leave it as is.

I strongly disagree, for a number of reasons.

(1)
> Well I guess some people are really confused by standard mathematics!

Not at all. This (the meaning of "each") is not part of the basic mathematics
that we all agree are included in the standard (i.e. basic arithmetic, boolean
logic). It comes for a corner of set theory that few have a reason to recall.
(Surely if I ever knew it, I've forgetten it. I of course know about the various
Greek set operators, but I couldn't tell you what any of them do on the empty
set.) That's illustrated by the fact that Brad and I both are completely
confused by this wording. We're not writing this solely for a handful of elites,
we're trying to write it to be understandable by all reasonably experienced Ada
programmers. And even if some of the supposed elites are confused, we have a
problem.

Besides, a couple of weeks ago, you said:

> Well talking about "each" of the elements of a null set is not
> standard mathematical terminology, and IMO is peculiar, ...

I'll go with RKBD-1. :-)

and you also said:

> The difficulty in reading the RM comes in my mind from the fact that
> it is not intuitive.
> If I ask someone who has no children "Are all your children over 18?",
> they do not answer yes.

And the same surely is true for "each". I view "each" as a noise word, meaning
"individual", used when a word is necessary, but usually left out. The usual use
that one sees in daily life is on prices. "Oranges, $0.15 each". If you see a
price on oranges of $0.15, you will automatically think "$0.15 each". And what's
the price of zero oranges?

One figures that out by multiplying. (0*0.15=0.00). 0*True doesn't make any
sense, so to the casual reader, the wording doesn't make sense in the null case.

(2) Leaning on "standard mathematics" here is circular -- we're trying to define
    the result here without requiring the reader to know advanced set theory,
    yet we have wording that clearly requires that to get the right answer. We
    could have saved a lot of time by not using any wording at all and telling
    readers that they're supposed to know what it does!

(3) I would have preferred "every" to "each". But even then, the wording is
    backwards. It makes much more sense for the wording to be written so that
    the "otherwise" is the default result (especially as that is how it would be
    implemented, particularly given the short circuit described in the next
    sentence). Thus, Ed's version is far preferable. We can argue about the word
    to use, I lean toward "some" simply because if it is good enough for the
    latter version, it's good enough for the first version. (I think both should
    use the same words, it's exactly the same semantics with True/False
    inverted.)

(4) I tend to agree with Steve's contention that it is weird that we first
    define this without a short circuit and then say that it is possible. OTOH,
    it is weird that we're requiring short circuiting here. Usually, for
    expressions, we allow but don't mandate short circuiting. But presuming that
    we do want to mandate short circuiting, then we should simply have defined
    the evaluation that way.

So, something like the following (replacing the entire bullet) would be better,
IMHO:

If the quantifier is all, the expression is False if the evaluation of any
predicate yields False; evaluation of the quantified_expression stops at that
point. Otherwise (all of the predicates have been evaluated and yielded True),
the expression is True. Any exception raised by evaluation of the predicate is
propagated.

That's actually shorter than the original (and it would be a lot shorter without
the parenthetical remark, which is optional), and leaves no doubt as to what is
happening. Similarly for the second bullet:

If the quantifier is some, the expression is True if the evaluation of any
predicate yields True; evaluation of the quantified_expression stops at that
point. Otherwise (all of the predicates have been evaluated and yielded False),
the expression is False. Any exception raised by evaluation of the predicate is
propagated.

I think these are clearly superior because they don't appear to lie about
short-circuiting, they correspond directly to an implementation, and don't
require knowledge of Dodgson beyond Alice in Wonderland. :-)

****************************************************************

Questions? Ask the ACAA Technical Agent