[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Accumulation quantifier support?
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.
email@example.com or firstname.lastname@example.org