Re: Relational lattice completeness

Jan Hidders wrote:
> 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?
>
> Often it is shown that you can use the rewrite rules to rewrite the
> expression to some normal form and then it is shown that for this
> normal form it holds that expressions are sementically equivalent iff
> they are syntactically equivalent. I'll give the example for the
> boolean case you presented.
>
> You need to show that if you have two equivalent expressions you can
> rewrite one to the other. What is often a good idea for showing
> equivalence is to rewrite them to some normal form. For the disjunctive
> normal form you need:
>
> (1) (v1 || v2) && v3 == (v1 && v3) || (v2 && v3)
> (1') v1 && (v2 || v3) == (v1 && v2) || (v1 && v3)
>
> Note that this is enough to get you into DNF, which means here an
> expresssion of the following syntax:
>
> E1 ::= E2 | E1 || E1
> E2 ::= V | E2 && E2
>
> We have the usual idempotency, commutativity and associativity rules:
>
> (2) (v1 || v1) == v1
> (3) (v1 && v1) == v1
> (4) (v1 || v2) == (v2 || v1)
> (5) (v1 && v2) == (v2 && v1)
> (6) (v1 || v2) || v3 == v1 || (v2 || v3)
> (7) (v1 && v2) && v3 == v1 && (v2 && v3)
>
> Which essentially means that we can view the expression as a set of
> sets of variables, e.g., (v1 || (v2 && v3)) || ((v2 && v4) && v5) can
> be thought of as { {v1}, {v2, v3}, {v2, v4, v5} }. I will call this a
> set representation of a DNF expression.
>
> 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

Oops. That should of course read:

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

• Jan Hidders