Math Notes – Quantifying Set Operators
The set union operator and the set
intersection operator may be used in quantified expressions in a way similar to
quantifying either the logical conjunction operator or the logical disjunction
operator. The theorems and techniques
are well established. The references
below provide more information on quantifying basic set operators.
Set-based program state concepts (for
example, Set-based analysis of if-statements) may
refer to a collection or set of related program state spaces. Each set in the collection may be denoted by
a subscript or index. Thus, a set of
state spaces may be denoted as
{i|k£i£n: B[i]}
The theorems on this page are proved using
the notation shown above, because the notation is also used in the analysis of
programming methods.
(Èi|k£i£n:B[i]).
(Çi|k£i£n:B[i]).
The meaning of a quantified expression over the
union operator is
(Èi|k£i£n:B[i]) = B[k] È B[k+1] È ¼ È B[n].
A quantified expression over the intersection
operator has a similar interpretation with the intersection operator in place
of the union operator.
Sometimes the
range expression is false, indicating an empty range. A quantified expression with an empty or false range has the
value the identity element. For
set-unions, the identity element is the null set. For set-intersections, the identity element is the universal
set. Thus:
The union and
intersection operators are symmetric and idempotent, so splitting off a term
and splitting a range are both valid operations.
DeMorgan’s law
for two sets generalizes to a quantified expression.
DeMorgan’s law also applies to following
theorem. The left half of the expression is the union of solutions to an
if-statement under certain constraints.
The expression may be simplified by dropping out the set negations.
Theorem 2: (Èj|k£j£n:(Çi|k£i£j-1:~B[i])ÇB[j]) =
(Èj|k£j£n:B[j])
References:
Fejer, Peter and Simovici, Dan A., 1991, Mathematical
Foundations of Computer Science, New York, NY: Springer-Verlag
Gries, David and Schneider,
Fred B., 1993, A Logical Approach to Discrete Math, New York, NY:
Springer-Verlag