Re: Relational lattice completeness

Marshall Spight wrote:

>
> So, how would one go about proving that any boolean expression
> with the grammar
>
> E ::= V
>       | E && E
>       | E || E
>
> could be transformed into any equivalent expression, using only
> some fixed set of transformations. (That is the basic idea,
> right?) What is the smallest set of transformations necessary?

Note that we can now also drop rule (1') because it follows from (1),
(4) and (5).

If we add the following rule

(8) (v1 && v2) || v2 == v1 && v2

then we can always rewrite to a DNF such that it holds for its set version {C1, ..., Cn} that there are no Ci and Cj such that Ci is a subset of Cj. I will call set-representations with that property subset-free.

We now set out to show that if two expressions e1 and e2 are rewritten to DNF expressions with subset-free set-representions s1 and s2, respectively, and e1 and e2 are semantically equivalent then s1 = s2. We proof this by contradiction:

We begin with assuming that two expressions e1 and e2 are rewritten to DNF expressions with subset-free set-representations s1 and s2, respectively, and e1 and e2 are semantically equivalent. Let us now also assume that s1 <> s2. Let s1 = {B1, ..., Bn} and s2 = {C1, ..., Cm}. Now there is some Bi that is not a superset of any of C1, ..., Cm or there is a Cj that is not a superset of any of B1, ..., Bn. Note that this is true because s1 and s2 are different, finite and subset-free. (Proof of that is left to the reader as an exercise.) Let us assume that such a Bi exists. (The case for Cj is symmetric.) Let M(Bi) be the model that assigns all variables in Bi to TRUE and all other variables to FALSE. Then clearly M(B_i) is a model for which e1 evaluates to TRUE, but e2 evaluates to FALSE, since none of C1, ..., Cm is a subset of Bi. It follows that e1 and e2 are semantically different, which contradicts the assumption that e1 and e2 are semantically equivalent.

So we know that if two expressions e1 and e2 are semantically equivalent then there is a a subset-free set-representation s' such that both e1 and e2 can be rewritten to e1' and e2' with s' as their set-version. Clearly since e1' and e2' have the same set-representation they can be rewritten to each other, and so we can rewrite e1 to e1' to e2' to e2.

QED So the conclusion is that the set of rules (1), ..., (8) are indeed complete in the sense that we talked about. Note that the dual of (1), i.e.,

   (v1 && v2) || v3 == (v1 || v3) && (v2 || v3)

is missing but that indeed we can prove it from the other rules by algebraic rewriting. That's also left to the reader as an exercise. :-)

Hope this helps,

• Jan Hidders