Oracle FAQ Your Portal to the Oracle Knowledge Grid
HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US
 

Home -> Community -> Usenet -> comp.databases.theory -> Re: completeness of the relational lattice

Re: completeness of the relational lattice

From: Jan Hidders <hidders_at_gmail.com>
Date: Thu, 28 Jun 2007 18:09:39 -0000
Message-ID: <1183054179.943491.198060@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>.

Where:

- 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 } over
header 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 header
of R
(11)   [H] * [S] = [H + S]
(12)   [H] + [S] = [H * S]
(22)   R * [] = [H]                                if H is the header
of 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>       if
S * H nonempty

I invite you to challenge me to show that it can prove an equation that holds. Of course you should also check if all these equations can be derived by you.

Received on Thu Jun 28 2007 - 13:09:39 CDT

Original text of this message

HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US