Re: completeness of the relational lattice

On 28 jun, 21:47, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
> On Jun 28, 11:09 am, Jan Hidders <hidd..._at_gmail.com> wrote:
>
>
>
> > 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.
>
> Here we go.
>
> Challenge #1:
> R * [x] = R * [] if x is in header R

        R * [x] =
(29) R * <x> * [] =
(28) R * []

> Challenge #2:
> [] * R * ( ([]*Q) + ([]*S) ) = [] * (R*Q + R*S)

I'm going to assume the following headers (becaues my axiomatization assumes this is known, and needs it to be complete): R(a,d,e,g) Q(b,d,f,g) S(c,e,f,g)

        [] * R * ( ([]*Q) + ([]*S) ) =

(22)  [adeg]  * ( [bdfg] + [cefg] ) =
(12)  [adeg]  * [fg] =
(11)  [adefg]
(12)  [abdefg] + [acdefg]
(11)  [adeg]*[bdfg] + [adeg]*[cefg]
(22)  []*R*[]*Q + []*R*[]*S
(1)  []*R*Q + []*R*S
(8)  [] * (R*Q + R*S)

Yes, I know that using the concrete attributes somehow seems a bit like cheating and too low level, but adding extra machinery to abstractly reason over headers seems unnecessary to me.

• Jan Hidders