# Re: completeness of the relational lattice

From: Jan Hidders <hidders_at_gmail.com>
Date: Sat, 30 Jun 2007 10:34:34 -0000

```> On Jun 29, 6:29 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
>
>
> > (32a)  W + [] = <>
> > (32b)  W + [x] = <x>             with x a single attribute
> > (55)   W * <x> = W               with x a single attribute
> > (56)   W + (r * s) = (W + r) * (W + s)
>
> Challenge:
>
> ((W*P)+(W*Q))*W*R = (W*P*R)+(W*Q*R)
>
> It could be proved if we know that A(W*P) = A(W*Q)= A(W*R)=A(W), or
> equivalently W*P*[]=W*Q*[]=W*R*[]=W*[] but  how do we derive these?

```

So we need to prove W * R * [] = W * []. I'm assuming A(R) = {a,b}.

W * R * []
--> (22) W * [a,b]
--> (11) W * [a] * [b]
--> (29) W * <a> * [] * <b> * []
--> (1) (2) (3) W * <a> * <b> * []
--> (55) W * <a> * []
--> (55) W * []

If we allow R to have infinite width we need to add an extra rule:

R * [] = W * [] if A(R) contains all attributes

Note that altough the system is complete on concrete equations it is not complete on equation schemas. The schema W * r * [] = W * [] holds, and for any concrete r we can derive it, but the general equation schema cannot be derived by rewriting alone.

An intriguing question is to which extent the system is complete as an inference system where we allow concrete equations to be added to the axiom set. That would correspond to reasoning under the knowledge of database constraints. As you know we could express full FOL that way, so a completeness result would be truly spectacular. But I have currently no idea how to solve that question, and still need to finish the proof for UCQ.

• Jan Hidders
Received on Sat Jun 30 2007 - 12:34:34 CEST

Original text of this message