Re: completeness of the relational lattice

On 30 jun, 04:54, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:

> 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