Quantified Expressions: "some"

Quantified Expressions: "some"

[Georg Bauhaus]

AI05-0176 explains two new expressions,

  (for all X in domain | P (X))

and

  (for some X in domain | P (X))

Thus, "all" gets a new meaning and "some" is all new,
with a special, context dependent role of the word "some",
IIUC.

Will it still be English when this, in order to re-use a word
already reserved by Ada, uses the word "when" in place of the
new "some"?

  (for when X in domain | P (X))

"When" is not the same as the mathematically correct (MC?)
wording. Perhaps unusual. But if programming in Ada is not the
same as writing mathematics, maybe "when" just emphasizes the
presence of a computing apparatus as an added benefit?

Re: Quantified Expressions: "some"

[AdaMagica]

On 17 Nov., 01:03, Georg Bauhaus <rm-host.bauh...@maps.futureapps.de>
wrote:
>   (for all  X in domain | P (X))
>   (for some X in domain | P (X))
These are the Ada expressions for the mathematical "all" and
"existence" quantifiers and read quite naturally.

Draft 10 of RM 2010 defines some as a new reserved word.

>   (for when X in domain | P (X))

This is silly English, and when I try to make sense of it, I arrive at
the all quantifier. So I think, just for avoiding a new reserved word,
this is a very bad proposal.

Re: Quantified Expressions: "some"

[Niklas Holsti]

AdaMagica wrote:
> On 17 Nov., 01:03, Georg Bauhaus <rm-host.bauh...@maps.futureapps.de>
> wrote:
>>   (for all  X in domain | P (X))
>>   (for some X in domain | P (X))
> These are the Ada expressions for the mathematical "all" and
> "existence" quantifiers and read quite naturally.
> 
> Draft 10 of RM 2010 defines some as a new reserved word.
> 
>>   (for when X in domain | P (X))
> 
> This is silly English, and when I try to make sense of it, I arrive at
> the all quantifier. So I think, just for avoiding a new reserved word,
> this is a very bad proposal.

Among the existing keywords, "select" has nearly, but not quite, the 
right meaning:

    (for select X in domain | P (X))

But it would be better as "selected", and if a new word must be 
reserved, I agree that "some" is best. Although it is yet another nice, 
short, expressive word that will then be forbidden us for use as an 
identifier.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Quantified Expressions: "some"

[Dmitry A. Kazakov]

On Tue, 16 Nov 2010 22:31:50 -0800 (PST), AdaMagica wrote:

> On 17 Nov., 01:03, Georg Bauhaus <rm-host.bauh...@maps.futureapps.de>
> wrote:
>> � (for all  X in domain | P (X))
>> � (for some X in domain | P (X))
> These are the Ada expressions for the mathematical "all" and
> "existence" quantifiers and read quite naturally.
> 
> Draft 10 of RM 2010 defines some as a new reserved word.
> 
>> � (for when X in domain | P (X))
> 
> This is silly English, and when I try to make sense of it, I arrive at
> the all quantifier. So I think, just for avoiding a new reserved word,
> this is a very bad proposal.

It is also a silly Ada policy to make words reserved where the syntax does
not require that. Many Ada reserved words need not and should not be
reserved.

"for some" looks awful, why not "exists" or U+2203, since we are Unicode
now? (:-))

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Quantified Expressions: "some"

[stefan-lucks]

On Wed, 17 Nov 2010, Georg Bauhaus wrote:

> AI05-0176 explains two new expressions,
> 
>  (for all X in domain | P (X))
> 
> and
> 
>  (for some X in domain | P (X))

As a keyword-reuising alternative for "for some", Geor proposed

>  (for when X in domain | P (X))

This is really ill-readable, IMHO. As others in this thread have pointed
out, this may be read as "all", actually.

If you really really really wanted to avoid "some", use Mathematics:

    P holds for some X    <=>   not (not P holds for all X).

Thus, the expression

   (for some X in domain | P(X))

could be rephrased as

   (not (for all X in domain | not P(X)))

without any need for the word "some".

But honestly, I prefer to write "some" over using "not" twice.

Stefan


-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Quantified Expressions: "some"

[(see below)]

On 17/11/2010 10:46, in article 1t7pvrh3i022d.8t9yqjonagar$.dlg@40tude.net,
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:

> On Tue, 16 Nov 2010 22:31:50 -0800 (PST), AdaMagica wrote:
> 
>> On 17 Nov., 01:03, Georg Bauhaus <rm-host.bauh...@maps.futureapps.de>
>> wrote:
>>> � (for all  X in domain | P (X))
>>> � (for some X in domain | P (X))
... 
> "for some" looks awful, why not "exists" or U+2203, since we are Unicode
> now? (:-))

Why? It reads as perfectly idiomatic English and is standard mathematical
phrasing.

-- 
Bill Findlay
with blueyonder.co.uk;
<surname><forename>

Re: Quantified Expressions: "some"

[Peter C. Chapin]

On 2010-11-17 03:25, Niklas Holsti wrote:

> Among the existing keywords, "select" has nearly, but not quite, the
> right meaning:
> 
>    (for select X in domain | P (X))
> 
> But it would be better as "selected", and if a new word must be
> reserved, I agree that "some" is best. Although it is yet another nice,
> short, expressive word that will then be forbidden us for use as an
> identifier.

I think it's nice that Ada has reserved a number of short, expressive
words. Once reserved they are easy to reuse elsewhere when the language
is extended. I could imagine some future feature wanting to use 'some'
for some other purpose.

(or is that "wanting to use 'some' for when other purpose?") :)

Peter

Re: Quantified Expressions: "some"

[Dmitry A. Kazakov]

On Wed, 17 Nov 2010 12:05:14 +0000, (see below) wrote:

> On 17/11/2010 10:46, in article 1t7pvrh3i022d.8t9yqjonagar$.dlg@40tude.net,
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> 
>> On Tue, 16 Nov 2010 22:31:50 -0800 (PST), AdaMagica wrote:
>> 
>>> On 17 Nov., 01:03, Georg Bauhaus <rm-host.bauh...@maps.futureapps.de>
>>> wrote:
>>>> � (for all  X in domain | P (X))
>>>> � (for some X in domain | P (X))
> ... 
>> "for some" looks awful, why not "exists" or U+2203, since we are Unicode
>> now? (:-))
> 
> Why? It reads as perfectly idiomatic English and is standard mathematical
> phrasing.

I never saw "for some" quantification.

BTW, it also looks inconsistent with Ada. The proposal uses | in the
meaning "condition". But Ada's meaning for | was "union." The word Ada used
for "condition" was "when."

I have no idea what the proposal would do with:

   ( for all X in 1 | 3..5 | F'Range | P(X) )

One could use a simpler notation for convolutions/set measures than the
above, and, in any case, without introduction of a free variable (e.g. X).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Quantified Expressions: "some"

[Georg Bauhaus]

On 17.11.10 13:29, Peter C. Chapin wrote:

> (or is that "wanting to use 'some' for when other purpose?") :)

No, just wanting to use "some" for when there is a need to do so. ;-)

Seriously,  referring to AI 139,

   while some X of Container loop
     ...

might convey lazy evaluation, or goal directed evaluation, Icon style.

Alternatives:

  while exists X of Container loop
  while select X of Container loop

Is the first "exists" equivalent to "some" in this case, too?
Just as readable and clear?

Re: Quantified Expressions: "some"

[Georg Bauhaus]

On 17.11.10 14:38, Dmitry A. Kazakov wrote:

> I have no idea what the proposal would do with:
> 
>    ( for all X in 1 | 3..5 | F'Range | P(X) )

I think it will refer to that extended membership test which
adds a pair of parens:

 ( for all X in (1 | 3..5 | F'Range) | P(X) )

Re: Quantified Expressions: "some"

[Dmitry A. Kazakov]

On Wed, 17 Nov 2010 15:16:34 +0100, Georg Bauhaus wrote:

> On 17.11.10 14:38, Dmitry A. Kazakov wrote:
> 
>> I have no idea what the proposal would do with:
>> 
>>    ( for all X in 1 | 3..5 | F'Range | P(X) )
> 
> I think it will refer to that extended membership test which
> adds a pair of parens:
> 
>  ( for all X in (1 | 3..5 | F'Range) | P(X) )

Awful.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Quantified Expressions: "some"

[J-P. Rosen]

Le 17/11/2010 15:20, Dmitry A. Kazakov a �crit :
> On Wed, 17 Nov 2010 15:16:34 +0100, Georg Bauhaus wrote:
> 
>> On 17.11.10 14:38, Dmitry A. Kazakov wrote:
>>
>>> I have no idea what the proposal would do with:
>>>
>>>    ( for all X in 1 | 3..5 | F'Range | P(X) )
>>
>> I think it will refer to that extended membership test which
>> adds a pair of parens:
>>
>>  ( for all X in (1 | 3..5 | F'Range) | P(X) )
> 
> Awful.
> 
Actually, It's been decided recently to change "|" to "=>", so it will read:
( for all X in 1 | 3..5 | F'Range => P(X) )

(General note: for everything related to Ada-2012, bear in mind that it
is work-in-progress, and that things do change. This AI (AI05-0176) is
at version 17!)
-- 
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Adalog a d�m�nag� / Adalog has moved:
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00

Re: Quantified Expressions: "some"

[Dmitry A. Kazakov]

On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:

> Le 17/11/2010 15:20, Dmitry A. Kazakov a �crit :
>> On Wed, 17 Nov 2010 15:16:34 +0100, Georg Bauhaus wrote:
>> 
>>> On 17.11.10 14:38, Dmitry A. Kazakov wrote:
>>>
>>>> I have no idea what the proposal would do with:
>>>>
>>>>    ( for all X in 1 | 3..5 | F'Range | P(X) )
>>>
>>> I think it will refer to that extended membership test which
>>> adds a pair of parens:
>>>
>>>  ( for all X in (1 | 3..5 | F'Range) | P(X) )
>> 
>> Awful.
>> 
> Actually, It's been decided recently to change "|" to "=>", so it will read:
> ( for all X in 1 | 3..5 | F'Range => P(X) )

Not much better: "=>" means "implies." P is neither implied nor selected.
Actually it is antecedent, on the left side. IF kind of X, such that P(X)
AND X in the set, THEN something [ ELSE something ].

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Quantified Expressions: "some"

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:puezn7v9naom.1nrc5rh8wzm7p.dlg@40tude.net...
> On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:
...
>> Actually, It's been decided recently to change "|" to "=>", so it will 
>> read:
>> ( for all X in 1 | 3..5 | F'Range => P(X) )
>
> Not much better: "=>" means "implies." P is neither implied nor selected.
> Actually it is antecedent, on the left side. IF kind of X, such that P(X)
> AND X in the set, THEN something [ ELSE something ].

"=>" is what SPARK uses.

I personally agreed with you and voted for neither. But I was the only one.

                            Randy.

Re: Quantified Expressions: "some"

[Dmitry A. Kazakov]

On Wed, 17 Nov 2010 19:12:53 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:puezn7v9naom.1nrc5rh8wzm7p.dlg@40tude.net...
>> On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:
> ...
>>> Actually, It's been decided recently to change "|" to "=>", so it will 
>>> read:
>>> ( for all X in 1 | 3..5 | F'Range => P(X) )
>>
>> Not much better: "=>" means "implies." P is neither implied nor selected.
>> Actually it is antecedent, on the left side. IF kind of X, such that P(X)
>> AND X in the set, THEN something [ ELSE something ].
> 
> "=>" is what SPARK uses.
> 
> I personally agreed with you and voted for neither.

At least they could use "when" instead of "=>".

> But I was the only one.

I'd prefer a set-measure notation:

   P'Min (1 | 3..5 | F'Range)  -- or  P'Inf
   P'Max (1 | 3..5 | F'Range)  -- or  P'Sup

Of course first-class functions with operations on them and sets were more
suitable for this stuff, i.e. "apply f to S, then measure the result with
m:

   Min (P (1 | 3..5 | F'Range))

But it is difficult to do.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Quantified Expressions: "some"

[AdaMagica]

On 18 Nov., 09:47, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 17 Nov 2010 19:12:53 -0600, Randy Brukardt wrote:
> > "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de> wrote in message
> >news:puezn7v9naom.1nrc5rh8wzm7p.dlg@40tude.net...
> >> On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:
> > ...
> >>> Actually, It's been decided recently to change "|" to "=>", so it will
> >>> read:
> >>> ( for all X in 1 | 3..5 | F'Range => P(X) )
>
> >> Not much better: "=>" means "implies." P is neither implied nor selected.
> >> Actually it is antecedent, on the left side. IF kind of X, such that P(X)
> >> AND X in the set, THEN something [ ELSE something ].
>
> > "=>" is what SPARK uses.
>
> > I personally agreed with you and voted for neither.
>
> At least they could use "when" instead of "=>".

( for all X in 1 | 3..5 | F'Range when P(X) ) ?????

That's nonsense, it's the other way round (compare exit L when ...
case X is when ...). If we are dreaming up syntax:

Use a colon or double colon:

( for all X in 1 | 3..5 | F'Range :: P(X) )

Re: Quantified Expressions: "some"

[Dmitry A. Kazakov]

On Thu, 18 Nov 2010 01:48:07 -0800 (PST), AdaMagica wrote:

> On 18 Nov., 09:47, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Wed, 17 Nov 2010 19:12:53 -0600, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de> wrote in message
>>>news:puezn7v9naom.1nrc5rh8wzm7p.dlg@40tude.net...
>>>> On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:
>>> ...
>>>>> Actually, It's been decided recently to change "|" to "=>", so it will
>>>>> read:
>>>>> ( for all X in 1 | 3..5 | F'Range => P(X) )
>>
>>>> Not much better: "=>" means "implies." P is neither implied nor selected.
>>>> Actually it is antecedent, on the left side. IF kind of X, such that P(X)
>>>> AND X in the set, THEN something [ ELSE something ].
>>
>>> "=>" is what SPARK uses.
>>
>>> I personally agreed with you and voted for neither.
>>
>> At least they could use "when" instead of "=>".
> 
> ( for all X in 1 | 3..5 | F'Range when P(X) ) ?????
> 
> That's nonsense, it's the other way round (compare exit L when ...
> case X is when ...).

   exit when for all X in 1 | 3..5 | F'Range when P(X);

does not look bad, except that "for" is misplaced. Should be

   exit when all X in 1 | 3..5 | F'Range when P(X);

> If we are dreaming up syntax:
> 
> Use a colon or double colon:
> 
> ( for all X in 1 | 3..5 | F'Range :: P(X) )

Colon is usually used as <set> : <function> => <set>. It should be kind of:

   1 | 3..5 | F'Range : P => (others => True)

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Quantified Expressions: "some"

[AdaMagica]

>    exit when for all X in 1 | 3..5 | F'Range when P(X);
>    exit when all X in 1 | 3..5 | F'Range when P(X);
>    1 | 3..5 | F'Range : P => (others => True)

I can't help, but I cannot make sense of these statements.

Re: Quantified Expressions: "some"

[Niklas Holsti]

AdaMagica wrote:
> On 18 Nov., 09:47, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Wed, 17 Nov 2010 19:12:53 -0600, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de> wrote in message
>>> news:puezn7v9naom.1nrc5rh8wzm7p.dlg@40tude.net...
>>>> On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:
>>> ...
>>>>> Actually, It's been decided recently to change "|" to "=>", so it will
>>>>> read:
>>>>> ( for all X in 1 | 3..5 | F'Range => P(X) )

> Use a colon or double colon:
> 
> ( for all X in 1 | 3..5 | F'Range :: P(X) )

I like that. The double-colon is visually more apparent than '|' and 
there is no risk of confusion with the earlier and other meanings of 
"=>". A single colon could also work, if we don't want to add new lexemes.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Quantified Expressions: "some"

[Georg Bauhaus]

On 18.11.10 14:24, Niklas Holsti wrote:

>> Use a colon or double colon:
>>
>> ( for all X in 1 | 3..5 | F'Range :: P(X) )
> 
> I like that. The double-colon is visually more apparent than '|' and there is
> no risk of confusion with the earlier and other meanings of "=>". A single
> colon could also work, if we don't want to add new lexemes.
> 

Ad double colon, ::, adds to confusion if you work cross-language.

Re: Quantified Expressions: "some"

[Peter C. Chapin]

On 2010-11-18 08:24, Niklas Holsti wrote:

>> Use a colon or double colon:
>>
>> ( for all X in 1 | 3..5 | F'Range :: P(X) )
> 
> I like that. The double-colon is visually more apparent than '|' and
> there is no risk of confusion with the earlier and other meanings of
> "=>". A single colon could also work, if we don't want to add new lexemes.

I spent some time this morning reading the email discussions associated
with AI05-0176 here

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0176-1.txt?rev=1.17

The ARG has clearly (and not surprisingly) already considered many
issues. I'd encourage anyone interested in this subject to review the
extensive discussion before speculating on alternative syntax, etc.

For example on February 24, 2010 Edmond Schonberg says,

"Slight preference for colon in this context, but that would conflict
with the new iterator syntax, where we could say:

    for all X : T of C : P (X)

which is definitely confusing.  So right arrow may be the obvious choice."

I don't know if the "new iterator syntax" is still valid but I can
certainly see how the ':' might be a less than ideal choice in the
example above.

John Barnes outlines his objection to the vertical bar in a message
dated September 15, 2010. Two of his objections would also apply to ':'
as well ("too weak a symbol" and "=> is better because SPARK uses the
same symbol for the same purpose.")

Peter

Re: Quantified Expressions: "some"

[Georg Bauhaus]

On 18.11.10 18:58, Peter C. Chapin wrote:

> John Barnes outlines his objection to the vertical bar in a message
> dated September 15, 2010. Two of his objections would also apply to ':'
> as well ("too weak a symbol" and "=> is better because SPARK uses the
> same symbol for the same purpose.")

More fun with arrows.  The AI started from the usual Such That (|) notation:

  (for all I in A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I)))


With "=>" replacing "|", this becomes

  (for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I)))

Slightly reformatted:

  (for all I in A'First .. T'Pred(A'Last)
      => A (I) <=
      A (T'Succ (I)))


This is nothing new, just venerable pointy syntax. There has always been,
for example, Boolean'Array (1 => 3 <= N).

But! The expression structure seems rather more likely now,
as it will appear frequently in Post aspects, one example being upper
bounds on a parameter.  The sequence of characters "=> X <=" is
a bit odd, because on the one hand, the "arrows" are so
close together, and symmetrical, but on the other hand, the readers
must doubly distinguish between them to understand the program;
doing so, they must be alert and

(a) know that "=>" is just an arrow for associations(*), and

(b) know that its very mirror, "<=" is defined at a very different
linguistic level, that of relational operators.

This *is* confusing (and is an opportunity for condescension of
Him Who Knows Ada Well), even though this piece of obfuscation is old,
if rarely used in the past.

I guess, then, one Would recommend a pair of parentheses:

  (for all I in A'First .. T'Pred(A'Last) => (A (I) <= A (T'Succ (I))))

OK.  However, by the same token, the pair could be used for "in (3 | 4)"
and Such That could stay as "|".

__
(*) better not to have written any Prolog recently...

Re: Quantified Expressions: "some"

[Georg Bauhaus]

On 19.11.10 18:48, Georg Bauhaus wrote:

> This is nothing new, just venerable pointy syntax. There has always been,
> for example, Boolean'Array (1 => 3 <= N).

Boolean_Array'(1 => 3 <= N)

Re: Quantified Expressions: "some"

[Vinzent Hoefler]

Georg Bauhaus wrote:

> (a) know that "=>" is just an arrow for associations(*), and
>
> (b) know that its very mirror, "<=" is defined at a very different
> linguistic level, that of relational operators.
>
> This *is* confusing (and is an opportunity for condescension of
> Him Who Knows Ada Well), even though this piece of obfuscation is old,
> if rarely used in the past.

It's even more confusing if you know Ada's little sister VHDL, where the
"<=" actually is a signal assignment:

           .-- 8< --
          |      if (Reset = '1') then
here ==> |         Rnd_Out <= (others => '0');
          |      elsif Rising_Edge (Clock) then
           `-- 8< --

Or, if you already think that's funny, then take a look at a case
statement:

-- 8< --
    case Input_Select is
       when "00"   => Output <= In (0);
       [...]
       when others => Output <= 'Z';
    end case;
-- 8< --


Vinzent.

-- 
Mail address temporary, use domain to filter.

Re: Quantified Expressions: "some"

[Andre]

On 11/19/2010 21:03, Vinzent Hoefler wrote:
> Georg Bauhaus wrote:
>
>> (a) know that "=>" is just an arrow for associations(*), and
>>
>> (b) know that its very mirror, "<=" is defined at a very different
>> linguistic level, that of relational operators.
>>
>> This *is* confusing (and is an opportunity for condescension of
>> Him Who Knows Ada Well), even though this piece of obfuscation is old,
>> if rarely used in the past.
>
> It's even more confusing if you know Ada's little sister VHDL, where the
> "<=" actually is a signal assignment:
>
> .-- 8< --
> | if (Reset = '1') then
> here ==> | Rnd_Out <= (others => '0');
> | elsif Rising_Edge (Clock) then
> `-- 8< --
>
> Or, if you already think that's funny, then take a look at a case
> statement:
>
> -- 8< --
> case Input_Select is
> when "00" => Output <= In (0);
> [...]
> when others => Output <= 'Z';
> end case;
> -- 8< --
>
or when "00" => Rnd_Out <= (others => '0')