Quantified expressions: no support for restriction predicates

Quantified expressions: no support for restriction predicates

[phil.clayton]

I read the discussion in AI-0176 a while ago and could not see any consideration given to supporting 'restriction predicates' in quantified expressions.  It is not uncommon for logic notations used in computer science/formal methods to allow a predicate following a vertical bar to restrict the values over which the bound variable is quantified, e.g.

  ∀ X : T | Even(X) ∙ P(X)  -- P(X) is true for all even X in T

  ∃ X : T | Odd(X) ∙ Q(X)   -- Q(X) is true for any odd X in T

For example, see [1, 2, 3] (references at the bottom).  (Note that in [2], ':' is used instead of '∙'.  Furthermore, there exist texts where '|' is used for '∙' above, however the particular choice of symbols is not relevant to my point - the point is that some notations allow a predicate that restricts the elements being quantified!)  The above predicates are equivalent to the following predicates, respectively, that do not use the restriction notation:

  ∀ X : T ∙ Even(X) ⇒ P(X)

  ∃ X : T ∙ Odd(X) ∧ Q(X)

Notice that in the case of for all, the logical effect of the restriction is an implication and, in the case of exists, the effect is conjunction.  This is why the restriction notation is particularly useful: it avoids the need to think about the required logical effect after the spot '∙' of the quantification.

Furthermore, using the restriction notation makes it simpler to work with quantification terms.  For example, to negate a quantified expression, the usual rule can be used (move the negation inside the quantifier and swap the quantifier) without having to worry about the restriction, e.g.

  ¬ (∀ X : T | Even(X) ∙ P(X))  ≡  ∃ X : T | Even(X) ∙ ¬ P(X)

I can see the lack of restriction predicates being a potential 'gotcha' when writing/transforming pre/postconditions, e.g. incorrectly converting

  not (for all X in T => if Odd(X) then P(X))

into

  (for some X in T => if Odd(X) then not P(X))

which should have been

  (for some X in T => not (if Odd(X) then P(X)))

which would hopefully be correctly simplified to

  (for some X in T => Odd(X) and also not P(X))

Conceptually the restriction predicate is a restriction on the discrete_subtype_definition T.  Given that a discrete_subtype_definition can (I think) denote a subtype that a static predicate applies to, it would, perhaps, be nice if there was some corresponding way to apply a predicate to a discrete_subtype_definition in a loop_parameter_specification.  For example, something like

  (for some X in T with Odd(X) => not P(X))
  (for some X in T with Odd(T) => not P(X))
  (for some X in T with Predicate => Odd(T) => not P(X))

I haven't followed all the developments in the areas of predicates.  Perhaps there are good reasons not to have such restriction predicates.  Anyway, just thought I would raise the idea as they seem useful.

Phil



References

  1. Programming from Specifications
     Carroll Morgan
     http://www.cs.ox.ac.uk/publications/books/PfS/PfS.ps.gz
     Note laws in section A.2, p.262
       A.54
       A.55

  2. A Logical Approach to Discrete Math, Gries & Schneider
     See the following copy of the laws from the book:
     http://www.cslab.pepperdine.edu/warford/math221/221-Equations.pdf
     Note laws
       9.2
       9.19
       9.18(b)
       9.18(c)

  3. The Z Notation: a reference manual
     Mike Spivey
     http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf
     Note laws on p.70

Re: Quantified expressions: no support for restriction predicates

[Randy Brukardt]

<phil.clayton@lineone.net> wrote in message 
news:22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8...
...
>I can see the lack of restriction predicates being a potential 'gotcha' 
>when writing/transforming
> pre/postconditions, e.g. incorrectly converting
>
>  not (for all X in T => if Odd(X) then P(X))
>
>into
>
>  (for some X in T => if Odd(X) then not P(X))

This is not a problem, since both of these are illegal. :-) Conditional 
expressions always have to be directly enclosed in parens, and that isn't 
done here. (There are special cases to allow the omission of those parens 
when they are already *directly* there, but in only those cases, like P(if 
Odd(X) then not P(X)); but not P(Param => if Odd(X) then not P(X));.)

Has nothing to do with your point, though.

...
>I haven't followed all the developments in the areas of predicates. 
>Perhaps there are good reasons
> not to have such restriction predicates.  Anyway, just thought I would 
> raise the idea as they seem useful.

We decided to leave all of the contract expressions as code easily 
understandable by any novice Ada programmer (or middle-aged Ada programmer 
who has forgotten most of the advanced mathematics he once knew - like, say, 
me :-).

Conditional expressions and quantified expressions themselves were both a 
bit controversial for this reason. We added conditional expressions mainly 
so that implications and the like could be specified without having to write 
a separate function (which of course would defy compile-time analysis as the 
body wouldn't be present). We rejected the idea of an "implies" operator 
because a lot of people are confused by what it means -- the equivalent 
conditional expression is much clearer, especially at 2 am!

Quantified expressions are hard enough to understand as it is. I don't think 
complicating them further would be helpful, especially for the programmer 
that only saw them rarely (which is likely to be most Ada programmers).

                                         Randy. 

Re: Quantified expressions: no support for restriction predicates

[phil.clayton]

On Saturday, April 28, 2012 12:43:51 AM UTC+1, Randy Brukardt wrote:
> wrote in message 
> news:22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8...
> ...
> >I can see the lack of restriction predicates being a potential 'gotcha' 
> >when writing/transforming
> > pre/postconditions, e.g. incorrectly converting
> >
> >  not (for all X in T => if Odd(X) then P(X))
> >
> >into
> >
> >  (for some X in T => if Odd(X) then not P(X))
> 
> This is not a problem, since both of these are illegal. :-) Conditional 
> expressions always have to be directly enclosed in parens, and that isn't 
> done here. (There are special cases to allow the omission of those parens 
> when they are already *directly* there, but in only those cases, like P(if 
> Odd(X) then not P(X)); but not P(Param => if Odd(X) then not P(X));.)
> 
> Has nothing to do with your point, though.

Drat.  I knew about the parentheses.  (Personally, I would have liked parentheses to be required only when there is a syntactic ambiguity.  I suppose that is so often, you may as well have them all the time.)


> ...
> >I haven't followed all the developments in the areas of predicates. 
> >Perhaps there are good reasons
> > not to have such restriction predicates.  Anyway, just thought I would 
> > raise the idea as they seem useful.
> 
> We decided to leave all of the contract expressions as code easily 
> understandable by any novice Ada programmer (or middle-aged Ada programmer 
> who has forgotten most of the advanced mathematics he once knew - like, say, 
> me :-).
> 
> Conditional expressions and quantified expressions themselves were both a 
> bit controversial for this reason. We added conditional expressions mainly 
> so that implications and the like could be specified without having to write 
> a separate function (which of course would defy compile-time analysis as the 
> body wouldn't be present). We rejected the idea of an "implies" operator 
> because a lot of people are confused by what it means -- the equivalent 
> conditional expression is much clearer, especially at 2 am!

I think "if P then Q", i.e. implicit "else true", is a really neat way to provide implies.  It will be much more widely understood than an implies operator and makes clear when Q is evaluated.


> Quantified expressions are hard enough to understand as it is. I don't think 
> complicating them further would be helpful, especially for the programmer 
> that only saw them rarely (which is likely to be most Ada programmers).

Honestly, my motivation was to help those who were a little rusty on their maths/logic!  May be I wrote one to many ∀s :)

My thinking is that having a predicate to restrict the elements that one is quantifying over (just like a subtype predicate restricts the elements of a subtype) would avoid the need to work out the equivalent logical expression, which differs depending on the quantifier - a likely source of error.  So, while more syntax would be needed, this should actually simplify quantification concepts.

It's all a bit late in the day anyway but I feel better now I've said that!

Phil

Re: Quantified expressions: no support for restriction predicates

[Robert A Duff]

phil.clayton@lineone.net writes:

> Drat.  I knew about the parentheses.  (Personally, I would have liked
> parentheses to be required only when there is a syntactic ambiguity.
> I suppose that is so often, you may as well have them all the time.)

Note that you don't need "extra" parentheses.
You can say "F(for all ...)" instead of "F((for all ...))".

> I think "if P then Q", i.e. implicit "else true", is a really neat way
> to provide implies.

Me, too.  I argued strongly for adding an "implies" operator,
but I discovered that a lot of folks are confused by it,
yet find (if P then Q) crystal clear.  So I changed my mind.

> Honestly, my motivation was to help those who were a little rusty on
> their maths/logic!

Sure.

> My thinking is that having a predicate to restrict the elements that
> one is quantifying over (just like a subtype predicate restricts the
> elements of a subtype) would avoid the need to work out the equivalent
> logical expression, which differs depending on the quantifier - a
> likely source of error.  So, while more syntax would be needed, this
> should actually simplify quantification concepts.

Well, if you are willing to give a name to the subtype, you
can put a Static_Predicate or Dynamic_Predicate aspect on it.
Does that help?

- Bob

Re: Quantified expressions: no support for restriction predicates

[phil.clayton]

On Sunday, April 29, 2012 3:03:50 PM UTC+1, Robert A Duff wrote:
> phil.c...@lineone.net writes:
> 
> > Drat.  I knew about the parentheses.  (Personally, I would have liked
> > parentheses to be required only when there is a syntactic ambiguity.
> > I suppose that is so often, you may as well have them all the time.)
> 
> Note that you don't need "extra" parentheses.
> You can say "F(for all ...)" instead of "F((for all ...))".

I also knew that but didn't choose my words very well :)


> > My thinking is that having a predicate to restrict the elements that
> > one is quantifying over (just like a subtype predicate restricts the
> > elements of a subtype) would avoid the need to work out the equivalent
> > logical expression, which differs depending on the quantifier - a
> > likely source of error.  So, while more syntax would be needed, this
> > should actually simplify quantification concepts.
> 
> Well, if you are willing to give a name to the subtype, you
> can put a Static_Predicate or Dynamic_Predicate aspect on it.
> Does that help?

Is that actually possible for a Dynamic_Predicate?  Section 3.2.4 Subtype Predicates, para 27/3 says:

  The discrete_subtype_definition of a loop_parameter_specification
  shall not denote ... or any subtype to which Dynamic_Predicate
  specifications apply.

Phil

Re: Quantified expressions: no support for restriction predicates

[Robert A Duff]

phil.clayton@lineone.net writes:

> Is that actually possible for a Dynamic_Predicate?  Section 3.2.4 Subtype Predicates, para 27/3 says:
>
>   The discrete_subtype_definition of a loop_parameter_specification
>   shall not denote ... or any subtype to which Dynamic_Predicate
>   specifications apply.

Yeah, I think you're right.  The idea is that we didn't want hidden
inefficiencies.

    type T is new Integer with
        Dynamic_Predicate => T mod 10_000 = 0;
    for X in T loop -- Illegal!

If that were legal, it would probably be grossly inefficient.

- Bob

Re: Quantified expressions: no support for restriction predicates

[Adam Beneschan]

On Saturday, April 28, 2012 4:30:00 AM UTC-7, phil.c...@lineone.net wrote:
> 
> Drat.  I knew about the parentheses.  (Personally, I would have liked parentheses to be required only when there is a syntactic ambiguity.  I suppose that is so often, you may as well have them all the time.)

I have a vague memory of seeing code like this in a textbook, a long time ago.  I think it was in some version of Algol:

   if if if if A then B else C then D else E then F else G then
      ...

Although this isn't syntactically ambiguous, it is definitely migraine-inducing.  Based on this, I'm glad they decided to require the parentheses.  Although code like this shouldn't be written, at least a reader would have a fighting chance of understanding something like

   if (if (if (if A then B else C) then D else E) then F else G) then

                          -- Adam

Re: Quantified expressions: no support for restriction predicates

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wcc7gwywcuh.fsf@shell01.TheWorld.com...
> phil.clayton@lineone.net writes:
>
>> Is that actually possible for a Dynamic_Predicate?  Section 3.2.4 Subtype 
>> Predicates, para 27/3 says:
>>
>>   The discrete_subtype_definition of a loop_parameter_specification
>>   shall not denote ... or any subtype to which Dynamic_Predicate
>>   specifications apply.
>
> Yeah, I think you're right.  The idea is that we didn't want hidden
> inefficiencies.
>
>    type T is new Integer with
>        Dynamic_Predicate => T mod 10_000 = 0;
>    for X in T loop -- Illegal!
>
> If that were legal, it would probably be grossly inefficient.

Especially if Integer is a 64-bit type in this implementation. :-) My 
examples of this problem always used Long_Integer for this reason:

    type T is new Long_Integer with
        Dynamic_Predicate => T mod 2**30 = 0;
    for X in T loop -- Illegal!

                                        Randy.

Re: Quantified expressions: no support for restriction predicates

[phil.clayton]

On Monday, April 30, 2012 4:57:11 PM UTC+1, Adam Beneschan wrote:
> On Saturday, April 28, 2012 4:30:00 AM UTC-7, phil.c...@lineone.net wrote:
> > 
> > Drat.  I knew about the parentheses.  (Personally, I would have liked parentheses to be required only when there is a syntactic ambiguity.  I suppose that is so often, you may as well have them all the time.)
> 
> I have a vague memory of seeing code like this in a textbook, a long time ago.  I think it was in some version of Algol:
> 
>    if if if if A then B else C then D else E then F else G then
>       ...
> 
> Although this isn't syntactically ambiguous, it is definitely migraine-inducing.  Based on this, I'm glad they decided to require the parentheses.  Although code like this shouldn't be written, at least a reader would have a fighting chance of understanding something like
> 
>    if (if (if (if A then B else C) then D else E) then F else G) then

I would prefer to be allowed to indent without parentheses as follows:

  if
    if
      if
        if A then B else C
      then D
      else E
    then F
    else G
  then
    ...

I've probably been influenced by writing a lot of SML, which has conditional expressions of the form

  if C then A else B

(there are no statements, being a functional programming language) and the lack of parentheses has not been an issue.  Clearly Ada must force parentheses in some places to avoid the dangling-else ambiguity (because "else B" is optional when A and B are boolean).

The case I have in mind where I would like to omit parentheses is

  X + if C then A else B

However, I would argue that parentheses should be required in

  (if C then A else B) + X

to avoid the syntactic ambiguity.  Such behaviour can probably be achieved in a grammar (by distinguishing 'right-most' expressions and allowing conditional/quantified expressions in these positions to omit parentheses) but would require additional expressions hierarchies in the grammar.  That's a bit complicated so I think the current approach is the most practical one.

I note that reducing parentheses in future maintains compatibility with all existing code :)

Phil

Re: Quantified expressions: no support for restriction predicates

[phil.clayton]

On Sunday, April 29, 2012 8:35:18 PM UTC+1, Robert A Duff wrote:
> phil.c...@lineone.net writes:
> 
> > Is that actually possible for a Dynamic_Predicate?  Section 3.2.4 Subtype Predicates, para 27/3 says:
> >
> >   The discrete_subtype_definition of a loop_parameter_specification
> >   shall not denote ... or any subtype to which Dynamic_Predicate
> >   specifications apply.
> 
> Yeah, I think you're right.  The idea is that we didn't want hidden
> inefficiencies.
> 
>     type T is new Integer with
>         Dynamic_Predicate => T mod 10_000 = 0;
>     for X in T loop -- Illegal!
> 
> If that were legal, it would probably be grossly inefficient.

Right, this is the key point.  Writing pre- and postconditions where many elements are quantified over but immediately ignored due to a 'restriction predicate' is not good style, given these conditions are to be evaluated.  It would be preferable to quantify over just the elements that satisfy the restriction predicate in the first place.

For a subtype with a static predicate, presumably there is no efficiency issue because the restrictions placed on a static predicate enable the compiler to generate code that skips the elements not satisfying the predicate.

For static analysis, one would not worry about efficiency of evaluation and restriction predicates are common-place.  

Phil