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
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
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
We can convert the above example of a partial order into a semilattice by adding
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, ...
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.
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.
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”
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
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
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
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
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
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