Re: Relational lattice completeness

Jan Hidders wrote:
> Finally, trying to prove completeness is
> simply a good way of checking if there are no obvious algebraic
> identities still missing.

It seems a very interesting question. But I haven't been able to come up with an idea of how to approach it. I was thinking I'd try to understand
some simpler cases first. For example, one can construct every possible boolean function with only NAND (or NOR), but the only proof of this I'm aware of is simply one by demonstration. There are only 16 possible boolean functions, so it's quite to simply build them all with NAND and there's your proof.

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?

Any pointers to further reading appreciated; I'm completely uninformed on this topic.

Marshall Received on Sat Apr 15 2006 - 02:46:06 CEST