# Re: completeness of the relational lattice

From: Jan Hidders <hidders_at_gmail.com>
Date: Mon, 25 Jun 2007 20:56:45 -0000

On 25 jun, 20:04, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
> On Jun 25, 5:34 am, Jan Hidders <hidd..._at_gmail.com> wrote:
>
>
>
> > Hello Marshall and Vadim,
>
> > The axioms for equality axioms looked a bit ugly, so I wondered if
> > that could be improved. I think we can if we introduce in analogy to
> > [H] the operation <H> which denotes the relation with header H that
> > contains all tuples of the form (x,x,..,x).
>
> > The syntax:
>
> > E ::= R | E * E | E + E | {()} | [H] | <H>
>
> > If we adapt the equations we get:
>
> > 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
>
> > (7) r * {()} = r
> > (13) {()} = {()} + []
>
> > Special distribution equalities:
>
> > (8) r * (s + t) = (r * s) + (r * t)
> > if A(r) * A(s) <= A(t) or A(r) * A(t) <= A(s)
> > (9) r + (s * t) = (r + s) * (r + t)
> > if A(s) * A(t) <= A(r)
>
> > Absorption:
>
> > (20) r + (r * s) = r
> > (21) r * (r + s) = r
>
> > Empty relations:
>
> > (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
>
> You have informal "H is the header of R" in many places. Why don't we
> use this axiom as a definition of [H]? Then, we just substitute [H]
> with R * [].

Well, I would not say it is informal. It has a precise meaning since we can assume that we know the database schema, and given that schema you can see which axioms are generated by the axiom schemas.

> Also given that we agreed not to introduce operator precedence, the RL
> expressions contain a lot of parenthesis. Therefore, introducing
> constants which include brackets is not the best choice.

They are sets, so I need to put something around them. :-) Seriously, I don't see what else I could do. Note that in a real expression there would be things like <a,b,c> and [b,c,e]. How do you want me to write that without brackets?

> The [] brakets are very convenient when we want to specify relation
> arguments explicitly, e.g [x,y]. In the algebraic context relation
> header is just R * 00

.. under the assumption that the header of R is {x,y}, and such assumptions we cannot use in our inference mechanism. Again, we could move to such an inference mechanism but we would have to formalize it.

> > Equalities
>
> > (27) <H> * <S> = <H + S>
> > (28) R * <x> = R
> > if x in header H (NOTE x is a single attribute)
>
> I don't see why it is an equality axiom. The <x> is unary relation
> which is domain x.

Yes, it corresponds to the equation x=x, but the grouping of the axioms is just to give it some structure.

> And also you have informal note. Once again you can express the
> condition that the relation R is a single attribute relation as
>
> 00 <= X <= R /\ 00 implies X = 00 or X = R /\ 00

> > (30) <> = {()}
>
> > Miscellaneous
>
> > (26) <H> + [S] = <H * S>
> > (29) [H] * <S> = [H + S]
> > (31) ((r * <S>) + [H]) * <S> = ((r * <S>) + [H'])
> > if S * H nonempty and H + S = H'
>
> You have to specify that headers of <S> and r overlap on no more than
> a single attribute -- and I don't see this condition here.

Why do you think that condition is necessary?

With things seeming to go relatively well I also became a bit more interested in the next step. Could we for example also axiomatize complement (and thereby the whole of first order logic)?

I came up with a few axioms, but have no idea if they are complete:

(34) ~R + R = W + [H] if H header of R
(35) ~R * R = [H] if H header of R

```(36) ~(r * s) = (~r * (W + [A(s)])) + (~s * (W + [A(s)]))
(37) ~(r + s) = (~r + [A(s)]) * (~s + [A(r)])
(38) ~[H] = W + [H]
(39) ~< > = []
(40) ~<x> = [x]
(41) ~<H + S> = (~<H> * (W + [H + S])) + (~<S> * (W + [H + S])
(51) ~W = W * []

```

These axioms seem complete in the sense that the only possible interpretatoin is the complement operator, but that doesn't prove that as inference rules they are complete.

• Jan Hidders
Received on Mon Jun 25 2007 - 22:56:45 CEST

Original text of this message