The Eiffel Compiler / Interpreter (tecomp)

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

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 an 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" and "b".

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

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

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