SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/boolean lattice

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
 

Emacs suffix

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

- Introduction

- Inheriting axioms

- The base class DISTRIBUTIVE_LATTICE

- The derived class BOOLEAN_LATTICE

- Idempotence and absorption

- Involution

- Order reversal

- De Morgan's laws

- Emacs suffix


ip-location