The Eiffel Compiler / Interpreter (tecomp)

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.

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.

The set expression "{x:T: bexp}" has the type PREDICATE[T]. Since predicates are used frequently there is the shorthand T? for PREDICATE[T].

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

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

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 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

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.

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

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".

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.

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.

Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: