# Mathematical sets

Sets abound in mathematics. If a mathematician wants to treat a collection of

objects which satisfy a certain property as an entity, he defines a set.

Sets are a very powerful tool in specifications. In order to obtain good

readability we introduce a set like notation.

# Set expressions

The expression

{1,2,3}

is the set of the three numbers “1”, “2” and “3”. But in general the elements

of a set are expressed by a boolean expression. The expression

{x:NATURAL: x.is_even}

is the set of all natural numbers which are even. This is the basic notation

for mathematical sets in our programming language.

{x:T: bexp} -- set of all x which satisfy the boolean expression `bexp'

The variable “x” is a bound variable. Its name is not relevant and can be

changed arbitrarily, i.e. we have

{x:T: bexp} = {y:T: bexp[x:=y]} -- "y" must not occur free in `bexp' -- bexp[x:=y]: all free occurrences of `x' within `bexp' substituted by `y'

In many cases the type T of the bound variable can be inferred from the

context. In these case the expression

{x: bexp}

is sufficient to describe the set.

The notation “{a,b,…}” is just a shorthand.

-- shorthand {a,b,...} = {x:T: x~a or x~b or ...}

If we have a set we can ask whether an element belongs to the set

a in {x:T: bexp} -- Does `a' belong to the set "{x:T: bexp}"?

For this boolean expression the following equivalence is evident

a in {x:T: bexp} = bexp[x:=a] -- bexp[x:=a]: all free occurrences of `x' within `bexp' substituted by `a'

The set of all elements of a certain type is

{x:T: True}

and the empty set is

{x:T: False}

We can build the union (“+”) and the intersection (“*”) of sets and the

complement (“-“) of sets with the following notations

{x:T: e1} + {x:T: e2} = {x:T: e1 or e2} -- set union {x:T: e1} * {x:T: e2} = {x:T: e1 and e2} -- set intersection -{x:T: e} = {x:T: not e} -- set complement

The relation “<=” is the subset relation with the following notation

{x:T: e1} <= {x:T: e2} -- Is the first set contained in the second? -- The "<=" operator is defined as ({x:T: e1} <= {x:T: e2}) = (all(x:T) e1 => e2) -- ^ boolean implication -- ^ boolean equality -- ^ subset relation

Two sets are equal if they contain the same elements

({x:T: e1} = {x:T: e2}) = (all(x:T) e1 = e2) -- ^ boolean equality -- ^ boolean equality -- ^ set equality

Clearly for sets defined with arbitrary boolean expressions the subset

operator “<=” and the set equality operator “=” are not decidable in

general. Therefore they must be represented by ghost functions.

# Predicates: The type of sets

The set expression “{x:T: bexp}” has the type PREDICATE[T]. Since predicates

are used frequently there is the shorthand T? for PREDICATE[T].

## Basic functions

The type PREDICATE[T] is a builin type with the following basic definitions

-- module: "predicate" immutable class PREDICATE[G] end feature -- Basic functions in (e:G, p:G?): BOOLEAN -- Is the element `e' contained in the set `p'? note built_in end <= (a,b:G?): ghost BOOLEAN -- Is `a' a subset of `b'? ensure Result = all(x:G) x in a => x in b end = (a,b:G?): ghost BOOLEAN -- Do the sets `a' and `b' have the same elements? ensure Result = (a<=b and b<=a) end * (a,b:G?): G? -- The intersection of the sets `a' and `b'. ensure Result = {x: x in a and x in b} end + (a,b:G?): G? -- The union of the sets `a' and `b'. ensure Result = {x: x in a or x in b} end - (a:G?): G? -- The complement of the set `a'. ensure Result = {x: not (x in a)} end 0: G? -- The empty set ensure Result = {x: False} end 1: G? -- The universal set ensure Result = {x: True} end end

## Subset and equality relation

The subset relation is reflexive and antisymmetric

feature all(a,b:G?) ensure reflexive: a<=a -- def "<=" antisymmetric: a<=b => b<=a => a=b -- def "<=", "=" end -- Note: - Implication "=>" is right associative -- - "p=>q=>r" is equivalent to "p and q => r" end

The transitivity of the subset relation can be verified with the following

detailed proof.

feature transitive: all(a,b,c:G?) require r1: a<=b r2: b<=c check c1: all(x:G) require r3: x in a check c2: x in b -- r3, r1, def "<=" ensure x in c -- c2, r2, def "<=" end ensure a<=c -- c1, def "<=" end end

The reflexivity, symmetry and transitivity of the equality relation is an

immediate consequence of the definition and the corresponding properties of the

subset relation.

feature all(a,b,c:G?) ensure reflexive: a=a symmetric: a=b => b=a transitive: a=b => b=c => a=c end end

## Intersection and union

The intersection of two sets “a*b” is contained in both sets, therefore it has

to be a subset of both sets. If we build the intersection of a set “b” with

one of its subsets “a” then the intersection must be equal to the subset. The

fact that “a<=b” is equivalent to “a=a*b” is evident. Here is a pedantic proof

of this fact.

all(a,b:G?) check c1: require r1: a<=b check c2: all(x) x in a => x in b -- r1, def "<=" c3: all(x) require r2: x in a ensure x in a and x in b -- r2, c2 end c4: all(x) require r3: x in a and x in b check ensure x in a -- r3 end ensure a=a*b -- c3, c4, def "=" end c5: require r4: a=a*b check c6: all(x) x in a => x in a*b -- r4, def "=" c7: all(x) x in a => x in b require r5: x in a check c8: x in a*b -- r5, c6 c9: x in a and x in b -- c8, def "*" ensure x in b -- c9 end ensure a<=b end ensure a<=b = (a=a*b) -- c1, c5 end

Note that this proof just requires the expansion of function definitions and

the application of some very simple laws of logic. Therefore the proof engine

can do this proof automatically.

With a similar technique it can be shown that the commutative, associative and

absorption laws for “*” and “+” are valid. The reader is encouraged to do the

detailed proofs. Here just the assertions are stated with a hint on how to

construct the proof.

all(a,b:G?) ensure com_1: a*b = b*a -- def "=", "*" com_2: a+b = b+a -- def "=", "+" assoc_1: a*b*c = a*(b*c) -- def "=", "*" assoc_2: a+b+c = a+(b+c) -- def "=", "+" absorb_1: a = a*(a+b) -- def "=", "*", "+" absorb_2: a = a+(a*b) -- def "=", "*", "+" dist_1: a*(b+c) = a*b+a*c -- def "=", "*", "+" dist_2: a+(b*c) = (a+b)*(a+c) -- def "=", "*", "+" end

## The empty and the universal set

The empty set is the neutral element of set union and the universal set is the

neutral element for set intersection. The intersection of a set with its

complement yields the empty set and the union of a set with its complement

yields the universal set. This is expressed in the following assertions:

all(a:G?) ensure -- proof: expansion of function definitions and elementary laws -- of logic neutral_0: a+0 = a neutral_1: a*1 = a compl_0: a*(-a) = 0 compl_1: a+(-a) = 1 end

## Predicates are boolean lattices

In the last chapters some elementary laws have been shown which are satisfied

by predicates. Exactly these laws are the axioms of a boolean lattice (see

article about boolean lattices). From this we can conclude that predicates are

boolean lattices, i.e. the class PREDICATE can inherit from BOOLEAN_LATTICE

and inherit all the additional properties of a boolean lattice (e.g. order

reversal, de Morgan’s laws, double negation).

immutable class PREDICATE inherit ghost BOOLEAN_LATTICE redefine <= end end

Two remarks are important:

– The class PREDICATE must inherit BOOLEAN_LATTICE as a ghost parent. This is

necessary because PREDICATE defines the relations “<=” and “=” as ghost

functions. In the BOOLEAN_LATTICE these relations are defined as normal

relations. By inheriting the parent as “ghost” the descendant has the

freedom to define the functions as ghost functions or normal functions.

– The class BOOLEAN_LATTICE has a definition of “<=”. The class PREDICATE

overrides this definition. This has to be indicated in the inheritance

clause. The definition of “<=” from BOOLEAN_LATTICE becomes a proof

obligation within the class PREDICATE. In the previous chapters the

equivalence of “a<=b” and “a=a*b” have been proved.

# Set of sets

We can build set of sets i.e. expressions of type T??.

## Some examples

The set “ss1” defined as

ss1 = {s:NATURAL?: all(n,m:NATURAL) n in s => m in s => n+m in s}

describes the set of all set of natural numbers which are closed with respect

to addition. Some examples of sets which belong to the specified set of sets:

s0 = {} s1 = {0,2,4,...} -- Warning: Ellipsis ... is not part of the s2 = {0,3,6,...} -- programming language s3 = {0,2,3,4,6,8,9,10,12,14,15,...} s4 = {2,3,4,6,8,9,10,12,14,15,...} s5 = {2,3,4,6,8,9,10,11,12,14,15,...} -- s4 plus multiples of "11" ... sn = {0,1,2,3,...} s0 in ss1, s1 in ss1, ...

If we have a set of sets like “ss1” we can ask the questions “What is the

intersection of all sets of “ss1?”. Note that “ss1” contains an infinite number

of sets, therefore such a function cannot be obtained by combining the

intersection operator “*”. From the above definition it is clear that the

empty set is the intersection of all sets of “ss1”.

In order to make the question a little bit more interesting we construct

another set of sets

ss2 = {s:NATURAL?: 2 in s and 3 in s}

and ask the question “What is the intersection of all sets contained in

“ss1*ss2 (i.e. the set of sets which satisfy both conditions)?”. The set

“ss1*ss2” has the two members “s3” and “s4” and a lot of supersets of these

two sets. The intersection of all these sets is “s4”.

From this example one might conclude that the intersection of a set of sets is

always a member of the set of sets. But this is not true. For a simple

counterexample consider the set of sets

ss3 = {s:NATURAL?: 2 in s or 3 in s}

and build the intersection of all sets in “ss1*ss3”. The set “ss1*ss3” has the

following members

{0,2,4,...} {2,4,6,...} {0,3,6,...} {3,6,9,...} -- and many supersets of these sets

The intersection of all these sets is the empty set which is not contained in

“ss1*ss3” because it fails the specification to contain either “2” or “3”.

## Infimum and supremum

We can define a function “infimum” to return the intersection of a set of sets

and a function “supremum” to return the union of a set of sets.

feature infimum(pp:G??): ghost G? -- The intersection of all sets contained -- in the set of sets `pp'. ensure Result = {x: all(p) p in pp => x in p} end supremum(pp:G??): ghost G? -- The union of all sets contained -- in the set of sets `pp'. ensure Result = {x: some(p) p in pp and x in p} end end

The set “pp.infimum” contains only the elements which are contained in all

sets in “pp”, i.e. “pp.infimum” is the intersection of all sets in “pp”. The

set “pp.supremum” contains only elements which are contained in at least one

set of “pp”, i.e. “pp.supremum” is the union of all sets in “pp”.

But is “pp.infimum” really an infimum and “pp.supremum” supremum? This

question is nontrivial because the notions “infimum” and “supremum” are

defined independently of “intersection” and “union”.

Let us recall the definition of an infimum. The infimum of a set “pp” (here

set of sets) is the maximum of the lower set of “pp”. The lower set of “pp” is

the set of all sets which are subsets of all sets in “pp”

pp.low_set = {p: all(q) q in pp => p<=q}

In order to prove that “pp.infimum” is an infimum we have to prove

all(pp:G??) ensure contained: all(p) p in pp => pp.infimum<=p maximum: all(q) (all(p) p in pp => q<=p) => q<=pp.infimum end

A detailed proof of “contained”:

contained: all(pp:G??, p:G?) require r1: p in pp check c1: all(x:G?) require r2: all(r) r in pp => x in r ensure x in p -- r1, r2 end c2: {x: all(r) r in pp => x in r} <= p -- def "<=", c1 ensure pp.infimum<=p -- c2, def "infimum" end

A detailed proof of “maximum”:

all(pp:G??, q:G?) require r1: all(p) p in pp => q<=p check c1: all(x:G, r:G?) require r2: x in q r3: r in pp check c2: all(p) p in pp => x in p -- r2, r1 ensure x in r -- r3, c2 end c3: q <= {x: all(r) r in pp => x in r} -- c1 ensure q<=pp.infimum -- c3, def "infimum" end

The proof that “pp.supremum” is the minimum of “pp.up_set” is a similar

excercise.

The infimum of the empty set is the universal set and the supremum of the

empty set is the empty set. I.e. we have

{p:G?: False}.infimum = 1 {p:G?: False}.supremum = 0

These claims are proved by simple expansion of the definitions of “infimum” and

supremum” and elementary laws of logic.

## Predicates as complete lattices

A complete lattice is a lattice where each set of elements has an infimum and

a supremum. In the previous chapter we have defined the two functions

“infimum” and “supremum” and have shown that the return value of these

functions satisfies the specification of an “infimum” and a “supremum”

respectively. Therefore the class PREDICATE can inherit not only from the

class BOOLEAN_LATTICE but also from the class “COMPLETE_LATTICE” because it

satisfies the axioms of both. I.e. we can define the class PREDICATE as

immutable class PREDICATE[G] inherit ghost BOOLEAN_LATTICE redefine <= end ghost COMPLETE_LATTICE redefine <= 0 1 end end

The class PREDICATE overrides the definitions of “<=”, “0” and “1” of its

parent COMPLETE_LATTICE because it has its own definition of these

functions. But we have demostrated that the class PREDICATE satisfies the

definitions of these inherited functions.

With this declaration all assertions of the module “boolean_lattice” and

“complete_lattice” are inherited as valid assertions.