|
{ids.P|E} |
Set comprehension |
|
{E|P} |
Set comprehension (short form) |
ids is a comma-separated list of one ore more identifiers whose type must be inferable by the predicate . The predicate
and
can contain references to the identifiers ids.
The set comprehension contains all values of
for the values of
where
is true.
is a short form for
where
denotes the list of free identifiers occurring in
(see Section 3.3.1.3)).
With and
:
The following set comprehensions contain all the first 10 squares numbers:
|
{} |
Empty set |
|
{exprs} |
Set extension |
is a comma-separated list of one or more expressions of the same type.
The empty set contains no elements. The set extension
is the set that contains exactly the elements
.
, where
is an arbitrary type.
with
|
<: |
subset |
|
/<: |
not a subset |
|
<<: |
strict subset |
|
/<<: |
not a strict subset |
checks if
is a subset of
, i.e. if all elements of
occur in
.
checks if
is a subset of
and
does not equal
.
and
are the respective negated variants.
is a predicate with
,
for each operator
of
,
,
,
.
for each operator
of
,
,
,
.
|
\/ |
Union |
|
/\ |
Intersection |
|
\ |
Set subtraction |
The union denotes the set that contains all elements that are in
or
. The intersection
denotes the set that contains all elements that are in both
and
. The set subtraction or set difference
denotes all elements that are in
but not in
.
with
and
for each operator
of
,
,
for each operator
of
,
,
|
POW |
Power set |
|
POW1 |
Set of non-empty subsets |
denotes the set of all subsets of the set
.
denotes the set of all non-empty subsets of the set
.
and
with
.
|
finite |
Finite set |
|
card |
Cardinality of a finite set |
is a predicate that states that
is a finite set.
denotes the cardinality of
. The cardinality is only defined for finite sets.
is a predicate and
with
, i.e.
must be a set.
|
partition |
Partitions of a set |
is a predicate that states that the sets
constitute a partition of
. The union of all elements of a partition is
and all elements are disjoint.
is equivalent to
and
to
.
is a predicate with
and
for
|
union |
Generalized union |
|
inter |
Generalized intersection |
is the union of all elements of
.
is the intersection of all elements of
. The intersection is only defined for non-empty
.
and
with
.
|
UNION |
Quantified union |
|
INTER |
Quantified intersection |
is the union of all values of
for valuations of the identifiers
that fulfill the predicate
. The types of
must be inferable by
.
Analogously is the intersection of all values of
for valuations of the identifiers
that fulfill the predicate
.
Like set comprehensions (3.3.4.1), the quantified union and intersection have a short form where the free variables of the expression are quantified implicitly: and
.
With and
being a predicate: