previous up next
Go up to 4.7 Arithmetic Notions
Go forward to 4.7.2 Arithmetic Quantifiers
RISC-Linz logo

4.7.1 Minimum and Maximum

Definition 54 (Minimum and Maximum Quantifier) If x is a variable and F is a formula, then the following are terms with bound variable x:
minx F;
maxx F.
The value of the first term is the smallest value of x such that F holds; the value of the second term is the largest such value, i.e.,
minx F := such x: F /\  (forall y: F[x <- y] => x <= y);
maxx F := such x: F /\  (forall y: F[x <- y] => x >= y).

Usually the variable x is dropped and has to be deduced from the context.

We can use this notion to define corresponding functions on sets as follows.

Definition 55 (Minimum and Maximum Functions) 
min(S) := minx x in S;
max(S) := maxx x in S;

Please note that the definition of "min" and "max" depends on the choice of the predicate <= . Furthermore, minimum and maximum are not necessarily defined.


Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next