# Re: completeness of the relational lattice

Date: Thu, 28 Jun 2007 12:47:29 -0700

Message-ID: <1183060049.173769.85940_at_e16g2000pri.googlegroups.com>

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