SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/lattice

Lattices: Partial orders with infimum and supremum

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

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

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
 

Emacs suffix

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

- Introduction

- Semilattice

- Basic declaration

- Order structure

- Infimum

- Dual semilattice

- Lattice

- Complete lattice

- Distributive lattice

- Emacs suffix


ip-location