Re: Quantified expressions: no support for restriction predicates

[phil.clayton@lineone.net]

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