Boolean lattices

Introduction

This article is dedicated to boolean lattices. A boolean lattice is another
name for a boolean algebra.

A boolean lattice is an algebraic structure with two binary operators “*” and
“+” which represent “and” and “or”, a unary operator “-” which represents
negation. The binary operators are commutative, associative and
distributive. Furthermore there are the constants “0” and “1” which represent
“False” and “True”. “0” is neutral for “+” and “1” is neutral for “*”. In
addition to that we have the axioms “a*(-a)=0” and “a+(-a)=1” for all “a”.

I.e. a boolean lattice is a distributive lattice with some additional
operations, some additional axioms and some lost axioms (e.g. the absorption
laws are not axioms in a boolean lattice).

The fact that in a boolean lattice some of the inherited axioms loose their
axiom status requires some attention.

Inheriting axioms

Abstract modules can have axioms and abstract operations. Axioms are
assertions which do not have a proof. They are assumptions. From the axioms
some other assertions can be derived. I.e. we have the following logic within
an abstract module “m1”.

  m1_axioms => m1_assertions

If we design a module “m2” which inherits “m1” we can decide which of the
axioms we keep and which of them we abandon. I.e. we split the axioms

  m1_axioms = kept_axioms + lost_axioms

Furthermore we can give “m2” some new axioms, i.e. we get

  m2_axioms = kept_axioms + new_axioms

The axioms of “m2” are not sufficient to prove the derived assertions of
“m1” because some axioms of “m1” lost their axiom status. In order to use the
asssertions of “m1” the module “m2” has to provide a proof for all abandoned
axioms based on its own axioms.

  m2_axioms  => lost_axioms

These proofs must be done without the use of the derived assertions of
“m1”. Otherwise we introduce circular reasoning. As soon as the abandoned
axioms are proved within “m2” the full power of the derived assertions of the
module “m1” is available within the module “m2”.

The base class DISTRIBUTIVE_LATTICE

A boolean lattice inherits from a distributive lattice. A distributive lattice
is based in the following operations and axioms

  deferred class
      DISTRIBUTIVE_LATTICE
  end

  feature     -- Operations
      * (a,b: CURRENT): CURRENT
         deferred end

      + (a,b: CURRENT): CURRENT
          deferred end

      = (a,b: CURRENT): BOOLEAN
          deferred end

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

      >= (a,b: CURRENT): BOOLEAN
          ensure Result = (a+b=b) end

      -- ... "<", ">" defined in the usual manner (not important for the
      -- following)
  end

  feature      -- Axioms
      all(a,b,c:CURRENT)
          deferred ensure
              -- strong equality
              a=b => a~b

              -- commutative
              a*b = b*a
              a+b = b+a

              -- associative
              a*b*c = a*(b*c)
              a+b+c = a+(b+c)

              -- absorption
              a = a*(a+b)
              a = a+(a*b)

              -- distributive
              a*(b+c) = a*b+a*c
              a+(b*c) = (a+b)*(a+c)
          end
  end

With this operations and axioms a couple of assertions have already been
proved.

  feature      -- Proved assertions
      all(a,b,c:CURRENT)
          ensure
              a=a
              (a=b) = (b=a)
              a=b => b=c => a=c

              a*a = a
              a+a = a

              a*b <= a
              a*b <= b
              c<=a => c<=b => c<=a*b

              a <= a+b
              b <= a+b
              a<=c => b<=c => a+b<=c

              a<=a
              a<=b => b<=a => a=b
              a<=b => b<=c => a<=c

              a<=b = b>=a
          end
  end

For a descendant of “distributive_lattice” it is not important how the proofs
have been done.

The derived class BOOLEAN_LATTICE

The module “boolean_lattice” has the following basic definitions in addition to
the already inherited ones.

  deferred class
      BOOLEAN_LATTICE
  inherit
      DISTRIBUTIVE_LATTICE
  end

  feature    -- Additional operations and axioms
      0: CURRENT
              -- The bottom element.
          deferred end

      1: CURRENT
              -- The top element.
          deferred end

      - (a:CURRENT): CURRENT
              -- The complement (negation) of `a'.
          deferred end

      all(a,b:CURRENT)
          deferred ensure
              neutral_0: a+0 = a
              neutral_1: a*1 = a

              compl_0:   a*(-a) = 0
              compl_1:   a+(-a) = 1
          end
  end

A compiler analyzing the module “boolean_lattice” discovers that the module
does not have any effective assertion which states strong equality,
commutativity, associativity and distributivity. Therefore it concludes that
these laws are kept as axioms. Because the class BOOLEAN_LATTICE is an
abstract class it is allowed to have axioms

Furthermore the compiler discovers that the absorption laws are stated as
effective assertions within the module (see next chapter). From this fact it
concludes that it has to prove the absorption laws without using any inherited
derived assertions.

Idempotence and absorption

In a boolean lattice it is possible to prove the idempotence laws of the join
and meet operation based on the distributivity and the neutrality axioms.

  feature   -- Idempotence
      all(a:CURRENT)
          check
              c1: a*a + a*(-a)   = a*a  -- compl_0, neutral_0
              c2: (a+a)*(a+(-a)) = a+a  -- compl_1, neutral_1
          ensure
              idem_1: a = a*a           -- c1, distr, compl_1
              idem_2: a = a+a           -- c2, distr, compl_0
          end
  end

Having the idempotence laws available it is possible to prove some facts about
“0” and “1”.

  feature   -- Properties of "0" and "1"
      all(a:CURRENT)
          check
              c1: a*0 = a*(a*(-a))        -- compl_0
              c2: a+1 = a+(a+(-a))        -- compl_1
          ensure
              bottom:  a*0 = 0            -- c1, assoc, idem, compl_0
              top:     a+1 = 1            -- c2, assoc, idem, compl_1

              max_1: a<=1                 -- def "<=", neutral_1
              min_0: 0<=a                 -- def "<=", bottom
          end
  end
  feature   -- Top and bottom are complements
      all
          check
              c1: -0 = (-0) * (0 + (-0))             -- neutral_1, compl_1
              c2: -1    = (-1) + 1*(-1)              -- neutral_0, compl_0
          ensure
              bot_compl: -0 = 1      -- c1, distr, idem, compl_0, compl_1
              top_compl: -1 = 0      -- c2, distr, idem, compl_1, compl_0
          end
  end

With the help of the idempotence laws and the assertions “a*0=0” and “a+1=1”
it is possible to prove the absorption laws.

  feature   -- Absorption
      all(a,b:CURRENT)
          check
              c1: a*(a+b) = a*1+a*b          -- distr, idem, neutral_1
              c2: a+a*b   =(a+0)*(a+b)       -- distr, idem, neutral_0
          ensure
              absorb_1: a*(a+b) = a          -- c1, distr, top, neutral_1
              absorb_2: a+a*b   = a          -- c2, distr, bottom, neutral_0
          end
  end

Since the absorptions laws are proved based on the inherited axioms and the
new axioms, all proved assertions inherited from the module
“distributed_lattice” can be used from now on without the danger of creating
circular proofs.

Involution

In a boolean algebra the inversion law “-(-a)=a” is valid. Since the inversion
law is an equality, it can be proved by using the law of antisymmetry of the
order relation.

  feature    -- Involution
      all(a:CURRENT)
          check
              c1: a = a*((-a)+(-(-a)))   -- neutral_1, compl_1
              c2: a <= -(-a)       -- c1, dist, compl_0, neutral_1, def "<="

              c3: a = a + (-a)*(-(-a))   -- neutral_0, compl_0
              c4: a >= -(-a)       -- c3, dist, compl_1, neutral_0, def ">="
          ensure
              -(-a) = a                  -- antisymm, c2,c4
          end
  end

Order reversal

Negation inverts the order, i.e. “a<=b” is equivalent to “-b <= -a”. The order
reversal law is similar to the contrapositive law of boolean values. Since the
order reversal law is a boolean equivalence, it can be proved by proving the
forward and backward direction.

We use an additional lemma to prove the forward an backward direction. Since
the auxiliary lemma is not interesting to the user we put it into a private
feature block.

  feature{NONE}    -- Lemma for order reversal
      reversal_lemma:
      all(a,b:CURRENT)
         require
             a<=b
         check
             c1:   a = a*b

             c2:  -b = (-b)*(-a) + (-b)*a   -- neutral_1, compl_1, dist

             c3:  (-b)*a = (-b)*(a*b)       -- c1
             c4:  (-b)*a = 0                -- c3, com, assoc, compl_0, bottom

             c5:  -b = (-b)*(-a)            -- c2, c4, neutral_0
         ensure
             -b <= -a                       -- c5
         end
  end

With this lemma it is easy to prove the order reversal law.

  feature     -- Order reversal
      all(a,b:CURRENT)
          check
              c1: (-b <= -a) => (-(-a) <= -(-b)) -- reversal_lemma
          ensure
              (a<=b) = (-b <= -a)     -- fwd: reversal_lemma, bwd: c1,inversion
          end
  end

De Morgan’s laws

The laws of de Morgan

     -(a*b) = (-a)+(-b)
     -(a+b) = (-a)*(-b)

are equality laws. They can be proved with the help of the antisymmetry law of
the corresponding order relation. We factor out the needed inequality laws and
put them into a private feature block.

  feature{NONE}    -- Lemmas for de Morgan
      lemma_1: all(a,b:CURRENT)
          check
              c1: a <= a+b          -- inherited
              c2: b <= a+b          -- inherited
              c3: -(a+b) <= -a      -- c1, order reversal
              c4: -(a+b) <= -b      -- c2, order reversal
          ensure
              -(a+b) <= (-a)*(-b)   -- c3, c4, meet is infimum
          end

      lemma_2: all(a,b:CURRENT)
          check
              c1: a*b <= a          -- inherited
              c2: a*b <= b          -- inherited
              c3: -a <= -(a*b)      -- c1, order reversal
              c4: -b <= -(a*b)      -- c2, order reversal
          ensure
              (-a)+(-b) <= -(a*b)   -- c3, c4, join is supremum
          end
  end

With the help of the lemmas the proof of De Morgan’s laws is straighforward.

  feature    -- De Morgan
      all(a,b:CURRENT)
          check
              c1: -((-a)+(-b)) <= a*b   -- lemma_1, involution
              c2: -(a*b) <= (-a)+(-b)   -- c1, order reversal

              c3: a+b <= -((-a)*(-b))   -- lemma_2, involution
              c4: (-a)*(-b) <= -(a+b)   -- c3, order reversal
          ensure
              -(a*b) = (-a)+(-b)        -- c2, lemma_2, antisymm
              -(a+b) = (-a)*(-b)        -- c4, lemma_1, antisymm
          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: