|
To test whether some enumerated set is empty or not, one may use
the IsEmpty function. However, to use IsEmpty, the set
has to be created in full first. The existential quantifier
exists enables one to do the test and abort the construction
of the set as soon as an element is found; moreover, the element
found will be assigned to a variable.
Likewise, forall enables one to abort the construction of
the set as soon as an element not satisfying a certain
property is encountered.
Note that exists(t){ e(x) : x in E | P(x) }
is not designed to
return true if an element of the set of values e(x) satisfies P, but rather
if there is an x∈E satisfying P(x) (in which case e(x) is
assigned to t).
For the notation used here, see the beginning of this chapter.
exists(t1, ..., tr){ e(x) :x in E | P(x) }
Given an enumerated structure E and a Boolean expression P(x),
the Boolean value true is returned if E
contains at least one element x for which P(x) is true.
If P(x) is not true for any element x of E, then the
Boolean value false is returned.
Moreover, if P(x) is found to be true for the element y, say, of E, then
in the first form of the exists expression, variable t will be assigned
the value of the expression e(y).
If P(x) is never true for an element of E,
t will be left unassigned.
In the second form, where r variables t1, ..., tr are given,
the result e(y) should be a tuple of length r; each variable
will then be assigned to the corresponding component of the tuple. Similarly,
all the variables will be left unassigned if P(x) is never true.
The clause (t) may be omitted entirely.
The expression P may be omitted if it is always true.
exists(t1, ..., tr){ e(x1, ..., xk) :x1 in E1, ..., xk in Ek | P }
Given enumerated structures E1, ..., Ek, and a Boolean expression
P(x1, ..., xk), the Boolean value true is returned
if there is an element <y1, ..., yk> in the
Cartesian product E1 x ... x Ek, such that
P(y1, ..., yk) is true.
If P(x1, ..., xk) is not true for any element
(y1, ..., yk) of E1 x ... x Ek,
then the Boolean value false is returned.
Moreover, if P(x1, ..., xk) is found to be true for the element
<y1, ..., yk> of
E1 x ... x Ek, then
in the first form of the exists expression, the variable t will
be assigned the value of the expression e(y1, ..., yk).
If P(x1, ..., xk) is never true for an element
of E1 x ... x Ek, then the variable t will
be left unassigned.
In the second form, where r variables t1, ..., tr are given,
the result e(y1, ..., yk) should be a tuple of length r; each variable
will then be assigned to the corresponding component of the tuple. Similarly,
all the variables will be left unassigned if P(x1, ..., xk) is
never true.
The clause (t) may be omitted entirely.
The expression P may be omitted if it is always true.
If successive structures Ei and Ei + 1 are identical, then
the abbreviation xi, xi + 1 in Ei may be used.
As a variation on an earlier example, we check whether or not
some integers can be written as sums of cubes (less than 10 3 in
absolute value):
> exists(t){ <x, y> : x, y in [ t^3 : t in [-10..10] ] | x + y eq 218 };
true
> t;
<-125, 343>
> exists(t){ <x, y> : x, y in [ t^3 : t in [1..10] ] | x + y eq 218 };
false
> t;
>> t;
^
User error: Identifier 't' has not been declared
forall(t1, ..., tr){ e(x) :x in E | P(x) }
Given an enumerated structure E and a Boolean expression P(x),
the Boolean value true is returned if P(x)
is true for every element x of E.
If P(x) is not true for at least one element x of E,
then the Boolean value false is returned.
Moreover, if P(x) is found to be false for the element y, say, of E, then
in the first form of the exists expression, variable t will be assigned
the value of the expression e(y).
If P(x) is true for every element of E,
t will be left unassigned.
In the second form, where r variables t1, ..., tr are given,
the result e(y) should be a tuple of length r; each variable
will then be assigned to the corresponding component of the tuple. Similarly,
all the variables will be left unassigned if P(x) is always true.
The clause (t) may be omitted entirely.
The expression P may be omitted if it is always true.
forall(t1, ..., tr){ e(x1, ..., xk) :x1 in E1, ..., xk in Ek | P }
Given sets E1, ..., Ek, and a Boolean expression
P(x1, ..., xk), the Boolean value true is returned
if P(x1, ..., xk) is true for every element
(x1, ..., xk) in the Cartesian product
E1 x ... x Ek.
If P(x1, ..., xk) fails to be true for some element
(y1, ..., yk) of E1 x ... x Ek,
then the Boolean value false is returned.
Moreover, if P(x1, ..., xk) is false for the element
<y1, ..., yk> of
E1 x ... x Ek, then
in the first form of the exists expression, the variable t will
be assigned the value of the expression e(y1, ..., yk).
If P(x1, ..., xk) is true for every element
of E1 x ... x Ek, then the variable t will
be left unassigned.
In the second form, where r variables t1, ..., tr are given,
the result e(y1, ..., yk) should be a tuple of length r; each variable
will then be assigned to the corresponding component of the tuple. Similarly,
all the variables will be left unassigned if P(x1, ..., xk) is
never true.
The clause (t) may be omitted entirely.
The expression P may be omitted if it is always true.
If successive structures Ei and Ei + 1 are identical, then
the abbreviation xi, xi + 1 in Ei may be used.
This example shows that forall and exists may be nested.
It is well known that every prime that is 1 modulo 4 can be written
as the sum of two squares, but not every integer m congruent to 1 modulo 4 can.
In this example we explore for small m whether perhaps m plus or minus ε
(with |ε|leq1) is always a sum of
squares.
> forall(u){ m : m in [5..1000 by 4] |
> exists{ <x, y, z> : x, y in [0..30], z in [-1, 0, 1] |
> x^2+y^2+z eq m } };
false
> u;
77
[Next][Prev] [Right] [Left] [Up] [Index] [Root]
|