Quantified expressions: no support for restriction predicates

[phil.clayton@lineone.net]

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