The Eiffel Compiler / Interpreter (tecomp)

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.

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

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

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.

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

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

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

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