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

*To*: Bill McUmber <bill@spi.org>*Subject*: Re: Accumulation quantifier support?*From*: Bruno Dutertre <bruno@dcs.qmw.ac.uk>*Date*: Tue, 30 Sep 1997 19:31:42 +0100*CC*: pvs-help@csl.sri.com*References*: <199709301528.LAA02017@q.spi.org>*Sender*: bruno@dcs.qmw.ac.uk

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

**References**:**Accumulation quantifier support?***From:*Bill McUmber <bill@spi.org>

- Prev by Date:
**Accumulation quantifier support?** - Next by Date:
**Re: WITH and dependent types** - Prev by thread:
**Accumulation quantifier support?** - Next by thread:
**WITH and dependent types** - Index(es):