# Re: completeness of the relational lattice

Date: Thu, 28 Jun 2007 18:09:39 -0000

Message-ID: <1183054179.943491.198060_at_n60g2000hse.googlegroups.com>

On 28 jun, 17:52, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:

> On Jun 28, 2:30 am, Jan Hidders <hidd..._at_gmail.com> wrote:

*>
**>
**>
**> > On 28 jun, 03:18, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
**>
**> > > On Jun 27, 4:23 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
**>
**> > > > On 27 jun, 23:55, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
**>
**> > > > > On Jun 27, 2:17 pm, "Brian Selzer" <b..._at_selzer-software.com> wrote:
**>
**> > > > > > "Vadim Tropashko" <vadimtro_inva..._at_yahoo.com> wrote in message
**>
**> > > > > >news:1182964456.876858.28340_at_g37g2000prf.googlegroups.com...
**>
**> > > > > > > On Jun 26, 7:03 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
**> > > > > > >> I suspect that the condition
**> > > > > > >> for r + (s * t) = (r + s) * (r + t)
**> > > > > > >> should be A(r) * A(s) = A(r) * A(t) = A(s) * A(t).
**> > > > > > >> So if two have an attribute, the third must also have it.
**>
**> > > > > > > This is more powerful condition than in the "First steps..." paper.
**> > > > > > > Indeed, the correct criteria is:
**>
**> > > > > > > A(x,t) \/ (B(y,t) /\ C(z,t)) = (A(x,t) \/ B(y,t)) /\ (A(x,t) \/
**> > > > > > > C(z,t))
**>
**> > > > > > > The proof is by writing down both sides in the set notation. Assuming
**> > > > > > > general relation headers A(x,u,w,t), B(y,u,v,t), C(z,w,v,t) the left
**> > > > > > > hand side works out to be
**>
**> > > > > > > exists xyzv : A \/ (B /\ C)
**>
**> > > > > > > The right hand side evaluates to
**>
**> > > > > > > exists zy : (exists xwv: A \/ B) /\ (exists xuv: A \/ C)
**>
**> > > > > > > In predicate logic we have
**>
**> > > > > > > exists x: (P /\ Q) <-> exists x: P /\ exists x: Q
**>
**> > > > > > While it is true that
**>
**> > > > > > exists x: (P \/ Q) implies exists x: P \/ exists x: Q
**> > > > > > and
**> > > > > > exists x: P \/ exists x: Q implies exists x: (P \/ Q),
**>
**> > > > > > isn't it true that
**>
**> > > > > > exists x: (P /\ Q) implies exists x: P /\ exists x: Q
**> > > > > > but
**> > > > > > exists x: P /\ exists x: Q does not imply exists x: (P /\ Q)?
**>
**> > > > > > Consequently,
**>
**> > > > > > exists x: (P /\ Q) is not equivalent to exists x: P /\ exists x: Q
**>
**> > > > > That's right, I was looking tohttp://en.wikipedia.org/wiki/First-order_logic#Identities
**> > > > > before posting, but apparently didn't notice this subtlety. So I don't
**> > > > > see how we can justify attribute x in the distributivity law and fail
**> > > > > to find a counter example either...
**>
**> > > > I think what you missed is rules like "P or ( Exists x : Q(x) ) <=>
**> > > > Exists x : ( P and Q(x) )" where P has no free occurrence of x.
**>
**> > > > So you start with:
**>
**> > > > A(x, t) \/ (B(y, t) /\ C(z, t) which is formally:
**>
**> > > > { (t) | (Exists x : A(x, t)) \/
**> > > > (Exists y, z : B(y, t) /\ C(z, t)) }
**>
**> > > > = /* pull y and z quantifiers to the front */
**>
**> > > > { (t) | Exists y, z :
**> > > > (Exists x : A(x, t)) \/ (B(y, t) /\ C(z, t)) }
**>
**> > > > = /* distribution */
**>
**> > > > { (t) | Exists y, z :
**> > > > ((Exists x : A(x, t)) \/ B(y, t)) /\
**> > > > (Exists x : A(x, t)) \/ C(z, t))) }
**>
**> > > > = /* push y and z quantifiers back to their variables */
**>
**> > > > { (t) | ((Exists x : A(x, t)) \/ (Exists y : B(y, t))) /\
**> > > > (Exists x : A(x, t)) \/ (Exists z : C(z, t)))) }
**>
**> > > > which is indeed the representation of
**>
**> > > > (A(x,t) \/ B(y,t)) /\ (A(x,t) \/ C(z,t))
**>
**> > > Right. If the rule
**> > > exists x: (P /\ Q) --> exists x: P /\ exists x: Q
**> > > don't allow to pull x to the outermost level, it could be leveraged to
**> > > push the x back in front of A\/B and A\/C.
**>
**> > I'm not sure what you mean here. The rule I used for pushing is the
**> > same as the one I used for pulling, but applied in reverse.
**>
**> At the "distribution" step:
**>
**> { (t) | Exists y, z :
**> (Exists x : A(x, t)) \/ (B(y, t) /\ C(z, t)) }
**>
**> = /* distribution */
**>
**> { (t) | Exists y, z :
**> ((Exists x : A(x, t)) \/ B(y, t)) /\
**> (Exists x : A(x, t)) \/ C(z, t))) }
**>
**> you applied one more rule
**> exists x: (P /\ Q) --> exists x: P /\ exists x: Q
**> after distributivity.
*

?? After distributivity I apply once more "P or ( Exists x : Q(x) ) <=> Exists x : ( P and Q(x) )". I can do this because each variable appears only on one side of the "and".

Anyway, I've made a little progress with checking my proof, but I could not avoid adding new axioms. I also noticed that dealing with W / 10 / 11 now caused agaiin a lot of extra axioms, so for now I'm leaving them out again. The current list of axioms (and that I conjecture to be complete) is as follows:

We consider the following algebra:

E ::= R | E * E | E + E | [H] | <H>.

- R : a relation with name R (and known header) - E * E : natural join - E + E : generalized union - [H] : the empty relation with header H (possibly empty) - <H> : the equality relation { (x, ..., x) | x in Domain } overheader H

The * and + will also be used as intersection and union on headers. Headers are finite sets of attributes.

We define a function A that computes the header of the result:

- A(R) = H where H is the header of R - A(r * s) = A(r) + A(s) - A(r + s) = A(r) * A(s) - A([H]) = H - A(<H>) = H

Standard equalities:

(1) r * r = r (2) r * s = s * r (3) r * (s * t) = (r * s) * t (4) r + r = r

(5) r + s = s + r

(6) r + (s + t) = (r + s) + t

Absorption:

(20) r + (r * s) = r

(21) r * (r + s) = r

Special constants:

(7) r * <> = r

Distribution:

(8) r * (s + t) = (r * s) + (r * t) if A(r) * A(s) <= A(t)
and A(r) * A(t) <= A(s)

(9) r + (s * t) = (r + s) * (r + t) if A(s) * A(t) = A(s) *
A(r) = A(t) * A(r)

Special distribution:

(53) [H] + (r * s) = ([H] + r) * ([H] + s) if A(r) * A(s) <= H

Headers:

(10) R = R + [H] if H is the headerof R

(11) [H] * [S] = [H + S] (12) [H] + [S] = [H * S] (22) R * [] = [H] if H is the headerof R

Equations:

(27) <H> * <S> = <H + S> if H * S nonempty (28) R * <x> = R if x a single attribute in header H

Headers and Equations:

(26) <H> + [S] = <H * S> (29) [H] * <S> = [H + S] (31) ((r * <S>) + [H]) * <S> = ((r * <S>) + [H + S]) * <S> ifS * H nonempty

- Jan Hidders