From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,802ee425bbc3eba3,start X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Received: by 10.68.213.106 with SMTP id nr10mr7485109pbc.2.1335486655162; Thu, 26 Apr 2012 17:30:55 -0700 (PDT) Path: r9ni102461pbh.0!nntp.google.com!news1.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail From: phil.clayton@lineone.net Newsgroups: comp.lang.ada Subject: Quantified expressions: no support for restriction predicates Date: Thu, 26 Apr 2012 17:29:07 -0700 (PDT) Organization: http://groups.google.com Message-ID: <22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8> NNTP-Posting-Host: 2.24.14.246 Mime-Version: 1.0 X-Trace: posting.google.com 1335486655 3938 127.0.0.1 (27 Apr 2012 00:30:55 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 27 Apr 2012 00:30:55 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=2.24.14.246; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Date: 2012-04-26T17:29:07-07:00 List-Id: I read the discussion in AI-0176 a while ago and could not see any consider= ation given to supporting 'restriction predicates' in quantified expression= s. It is not uncommon for logic notations used in computer science/formal = methods to allow a predicate following a vertical bar to restrict the value= s over which the bound variable is quantified, e.g. =E2=88=80 X : T | Even(X) =E2=88=99 P(X) -- P(X) is true for all even X = in T =E2=88=83 X : T | Odd(X) =E2=88=99 Q(X) -- Q(X) is true for any odd X i= n T For example, see [1, 2, 3] (references at the bottom). (Note that in [2], = ':' is used instead of '=E2=88=99'. Furthermore, there exist texts where '= |' is used for '=E2=88=99' above, however the particular choice of symbols = is not relevant to my point - the point is that some notations allow a pred= icate that restricts the elements being quantified!) The above predicates = are equivalent to the following predicates, respectively, that do not use t= he restriction notation: =E2=88=80 X : T =E2=88=99 Even(X) =E2=87=92 P(X) =E2=88=83 X : T =E2=88=99 Odd(X) =E2=88=A7 Q(X) Notice that in the case of for all, the logical effect of the restriction i= s an implication and, in the case of exists, the effect is conjunction. Th= is is why the restriction notation is particularly useful: it avoids the ne= ed to think about the required logical effect after the spot '=E2=88=99' of= the quantification. Furthermore, using the restriction notation makes it simpler to work with q= uantification terms. For example, to negate a quantified expression, the u= sual rule can be used (move the negation inside the quantifier and swap the= quantifier) without having to worry about the restriction, e.g. =C2=AC (=E2=88=80 X : T | Even(X) =E2=88=99 P(X)) =E2=89=A1 =E2=88=83 X= : T | Even(X) =E2=88=99 =C2=AC P(X) I can see the lack of restriction predicates being a potential 'gotcha' whe= n writing/transforming pre/postconditions, e.g. incorrectly converting not (for all X in T =3D> if Odd(X) then P(X)) into (for some X in T =3D> if Odd(X) then not P(X)) which should have been (for some X in T =3D> not (if Odd(X) then P(X))) which would hopefully be correctly simplified to (for some X in T =3D> Odd(X) and also not P(X)) Conceptually the restriction predicate is a restriction on the discrete_sub= type_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, someth= ing like (for some X in T with Odd(X) =3D> not P(X)) (for some X in T with Odd(T) =3D> not P(X)) (for some X in T with Predicate =3D> Odd(T) =3D> not P(X)) I haven't followed all the developments in the areas of predicates. Perhap= s 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