Lattices — Partial order with supremum and infimum

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
Advertisements
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: