Re: completeness of the relational lattice

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

Challenge #2:
[] * R * ( ([]*Q) + ([]*S) ) = [] * (R*Q + R*S) Received on Thu Jun 28 2007 - 21:47:29 CEST