[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Accumulation quantifier support?

Bill McUmber wrote:
> What sort of support exists and how would one go about writing so-called
> accumulation quantifiers such as found in Gries/Schneider book, Chap 8
> (as well as elsewhere). In general, terms like (*i: R(i): P(i)) where
> the operator * is applied to each P(i) over the range specified by R(i).
> The operator for FORALL is conjunction, EXISTS, disjunction, etc. The
> primary one needed is the 'Count of' (Gries 'N' operator):
> (Ni: R(i): P(i)) gives the count of P(i) true in the range. In the
> static case, this can be written as a rather large disjunction but in
> the variable case I don't think it can.
> Thanx much.
> Bill McUmber
> bill@spi.org or mcumber@cps.msu.edu

These generalised quantifiers can be considered as functions
with two arguments P and R of type [T -> bool]. 

It's not clear how the operator N should behave when there is an 
infinite number of P(i) true but if you can restrict yourself to 
finite ranges, you can use card from the finite set library.
For example,

   R: VAR finite_set[T]
   P: VAR [T -> bool]

   N(R, P): nat = card({ i:T | R(i) and P(i)})

or N(R, P): nat = card({ i:(R) | P(i)}).

If you want a syntax closer to quantification you can define
N as a function with a single argument P: [T -> bool] (where 
T is a type parameter); then you can write an expression like 

  (N! (i: nat): i < 5)

which is an abbreviation for N(lambda (i: nat): i < 5). If you want 
a predicate R to speciy the range, you can use subtyping:

  (N! (i: (R)): P(i))  or  (N! (i:nat | R(i)) : P(i)).

This syntax can be used directly with card.

In the general case, you probably have to define accumulation
quantifiers by induction on finite sets.

Bruno Dutertre