# Introduction

Types which satisfy the concept of a partial order (i.e. which are descendants

of the type PARTIAL_ORDER) have a binary relation “<=” which is reflexive,

transitive and antisymmetric, i.e. for every three objects “a”, “b”, and “c”

the following conditions are satisfied:

reflexive: a<=a transitive: a<=b => b=>c => a=>c antisymmetric: a<=b => b=>a => a=b

The order is partial because for any two objects “a” and “b” it is possible that

neither “a<=b” nor “b<=a” is valid (i.e. that “a” and “b” are unrelated). In a

total order either “a<=b” or “b<=a” is valid. The following is an example of a

partial order

Example of a partial order: a b c | | \ | | | \ | | | \ | | | \ | | | \ | | | \ | | d e \ / \ / \ / \ / \ / \ / f g order relation: f<=a, f<=d, f<=b, d<=b, g<=d, g<=b, g<=e, g<=c, e<=b, e<=c

In general it is possible that for each two elements “a” and “b” there is no

element which is less than both. (Remark: In the following “less than” always

means “less than or equal”). In the above example we have “f<=a” and “f<=b”,

i.e. for “a” and “b” there is an element which is less than both. But this is

not the case for “a” and “c” (and neither for “a” and “e” nor for “f” and

“g”).

A semilattice is a partial order with the special property that for each two

elements “a” and “b” there are always elements which are less than both

(i.e. less or equal). The binary operation “a*b” returns the maximum of these

elements. I.e. “a*b” is the infimum of the set which contains “a” and “b”.

In the literature the operation “*” is often called a “meet” operation because

“a*b” is an object where “a” and “b” meet following the order relation

downwards.

We can convert the above example of a partial order into a semilattice by adding

one element.

Example of a semilattice: a b c | | \ | | | \ | | | \ | | | \ | | | \ | | | \ | | d e \ / \ / \ / \ / \ / \ / f g \ / \ / \ / h meet operation: a*b=f, a*c=h, f*g=h, b*c=g, ...

# Semilattice

## Basic declaration

We get a semilattice with the following declaration.

deferred class SEMILATTICE inherit STRONG_EQUALITY -- Needed to substitute equals for equals PARTIAL_ORDER end feature -- deferred functions and properties * (a,b:CURRENT): CURRENT deferred end all(a,b,c:CURRENT) deferred ensure idempotent: a*a = a commutative: a*b = b*a associative: a*b*c = a*(b*c) end end

Many of the proofs of the properties of lattices require to substitute equals

for equals. Therefore it is necessary that SEMILATTICE inherits from

STRONG_EQUALITY. The type STRONG_EQUALITY has beside the usual equality axioms

(reflexivity, symmetry and transitivity of “=”) the additional axiom

a=b => a~b -- equality implies identity!

Having this axiom enables the verifier to substitute “equals” for “equals”

because all “equals” are identical i.e. indistiguishable.

## Order structure

The meet operation “*” of the semilattice is used to define the order relation

in the following way:

<= (a,b:CURRENT): BOOLEAN ensure Result = (a = a*b) end

It has to be shown that “<=” satisfies the axioms of a order relation.

all(a,b,c:CURRENT) ensure reflexivity: a<=a -- definition of "<=",idem antisymmetry: (a<=b) => (b<=a) => (a=b) -- definition of "<=",comm transitivity: (a<=b) => (b<=c) => (a<=c) -- proof see below end

Reflexivity and antisymmetry are immediate consequences of the definition of

“<=”. Transitivity can be proved by:

all(a,b,c:CURRENT) require r1: a<=b r2: b<=c check d1: a=a*b -- r1, definition of "<=" d2: b=b*c -- r2, definition of "<=" c1: a=a*(b*c) -- "d2" into "d1" c2: a=(a*b)*c -- associativity c3: a=a*c -- "d1" into "c2" ensure a<=c -- c3, definition of "<=" end

We have only two deferred functions (“=”, “*”) with the corresponding

axioms. The deferred functions of a partial order are defined in terms of “*”

and the deferred proofs of the partial order are done.

## Infimum

It is easy to see that “a*b” is less than both operands.

all(a,b:CURRENT) ensure a*b <= a -- def "<=", assoc, com, assoc, idem a*b <= b -- def "<=", assoc, idem end

Furthermore every element “c” for which “c<=a” and “c<=b” is valid, the

relation “c<=a*b” is valid as well.

all(a,b,c:CURRENT) ensure c<=a => c<=b => c<=a*b -- def "<=", assoc end

These assertions demonstrate that “a*b” is an infimum of the set containing “a”

and “b”.

# Dual semilattice

For every partial order there is a corresponding dual partial order where “<=”

is replaced by “>=” (and minimum by maximum, …). By reversing the order

relation we can define a corresponding dual of a semilattice. The dual of the

meet operation “*” is called a join operation “+”. In a join semilattice each

two objects “a” and “b” have a supremum “a+b”.

We can define a join semilattice based on a meet semilattice in the following

manner by just renaming the corresponding functions.

deferred class DUAL_SEMILATTICE inherit SEMILATTICE rename * as + <= as >= < as > >= as <= > as < low_set as up_set up_set as low_set is_minimum as is_maximum is_maximum as is_minimum is_minimal as is_maximal is_maximal as is_minimal is_infimum as is_supremum is_supremum as is_infimum end end

# Lattice

A lattice is obtained by merging a meet and a join semilattice.

deferred class LATTICE inherit SEMILATTICE undefine >= end DUAL_SEMILATTICE undefine <= end end

In the meet semilattice “a<=b” is defined as “a=a*b” and the definition of

“a>=b” as “b<=a” is inherited from the partial order. The join semilattice

(i.e. the dual of a semilattice) defines “a>=b” as “a=a+b” and inherits the

definition of “a<=b” from the partial order (note that in the dual all order

functions are reversed). In order to avoid double definitions we have to

undefine “>=” of the meet semilattice and “<=” of the join semilattice.

Remember that undefining functions in Modern Eiffel leads to the proof

obligation that the undefined definition can be proved as a normal assertion.

In a lattice we require the following axioms to be valid (i.e. proofs must be

supplied by effective descendants).

feature -- axioms all(a,b,c: CURRENT) deferred ensure commutative_1: a*b = b*a commutative_2: a+b = b+a associative_1: a*b*c = a*(b*c) associative_2: a+b+c = a+(b+c) absorption_1: a*(a+b) = a absorption_2: a+(a*b) = a end end

The idempotence laws “a=a*a” and “a=a+a” are no longer amongst the

axioms. This is no longer necessary because the idempotence laws are

consequences of the above axioms.

feature -- Idempotence all(a:CURRENT) check c1: a = a*(a+a*a) -- absorption_1 c2: a*(a+a*a) = a*a -- absorption_2 c3: a = a+a*(a+a) -- absorption_2 c4: a+a*(a+a) = a+a -- absorption_1 ensure a = a*a -- c1, c2 a = a+a -- c3, c4 end end

The join operation “+” and the meet operation “*” define a partial order. We

have to prove that both define the same order.

feature -- Consistency of order relation all(a,b:CURRENT) check c1: a=a*b => b=b+a -- commutative_1, absorption_2 c2: b=b+a => a=a*b -- commutative_2, absorption_1 ensure (a<=b) = (b>=a) -- def "<=", ">=", c1, c2 end end

# Complete lattice

In a lattice each two elements “a” and “b” have an infimum and a supremum. But

this does not imply that any set of elements have an infimum and a supremum,

because of the possibility of infinite sets.

A lattice is complete if all sets of elements have an infimum and a supremum.

deferred class COMPLETE_LATTICE inherit LATTICE end feature infimum(p:CURRENT?): CURRENT -- Infimum of the set described by the predicate `p'. deferred end supremum(p:CURRENT?): CURRENT -- Supremum of the set described by the predicate `p'. deferred end all(p:CURRENT?) deferred ensure ax_inf: p.infimum.is_infimum(p) ax_sup: p.supremum.is_supremum(p) end end

The two axioms require that an object returned by “infimum” is actually an

infimum and an object returned by “supremum” is actually a supremum

(for the definition of “is_infimum” and “is_supremum” see the article about

order structure).

Remember that an element is an infimum of a set “p” if it is contained in

“p.low_set” (i.e. in the set of elements which are lower than all elements in

p) and if it is the maximum of “p.low_set”. Therefore the axioms imply the

following consequences.

feature -- Consequences all(p:CURRENT?) ensure inf_1: p.infimum in p.low_set -- ax_inf, def "is_infimum" inf_2: p.infimum.is_maximum(p.low_set) -- ax_inf, def "is_infimum" sup_1: p.supremum in p.up_set -- ax_sup, def "is_supremum" sup_2: p.supremum.is_minimum(p.up_set) -- ax_sup, def "is_supremum end end

There is the predicate “False:CURRENT?” which describes the empty set of

lattice elements and the predicate “True:CURRENT?” which describes the set of

all lattice elements.

The set “(False:CURRENT?).low_set” is the set of elements which are lower than

all elements in “False:CURRENT?”. Since there are no elements in

“False:CURRENT?” all elements are lower than all elements in

“False:CURRENT?”. I.e. we have “(False:CURRENT?).low_set = True:CURRENT?”.

The set “False:CURRENT?” has an infimum. This infimum (in order to be an

infimum) is the maximum of “True:CURRENT?”, i.e. the maximum of all elements

of the lattice. This maximum is called “top”.

A bottom element can be defined with similar reasoning.

feature -- Top and bottom top: CURRENT deferred ensure Result = (False:CURRENT?).infimum end bottom: CURRENT deferred ensure Result = (False:CURRENT?).supremum end all(a:CURRENT) ensure e1: top.is_maximum(True:CURRENT?) -- def "top", inf_2 e2: a<=top -- e1, def "is_maximum" e3: bottom.is_minimum(True:CURRENT?) -- def "bottom", sup_2 e4: bottom<=a -- e3, def "is_minimum" e5: a=a*top -- e2, def "<=" e6: a+top=top -- e2, def ">=" e7: bottom = bottom*a -- e4, def "<=" e8: bottom+a = a -- e4, def ">=" end end

# Distributive lattice

A lattice is called distributive if the meet operation “*” distributes over

the join operation “+” and vice versa.

deferred class DISTRIBUTIVE_LATTICE inherit LATTICE end feature all(a,b,c:CURRENT) deferred ensure a+(b*c) = (a+b)*(a+c) a*(b+c) = (a*b)+(a*c) end end