Re: completeness of the relational lattice

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.

Your suggestion might work, but you would have to first formalize what your inference mechanism is before we can start thinking about it. Right now my formalism is quite simple. It derives r = s iff it can rewrite r to s with the given axioms. Yours would probably be much more complicated than that. Can you give a formal definition of yours?

> 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

Yes, but again this means that you extend your inference mechanism, namely with first order logic inference. Again, this requires that you first define this formally, and even then I would still be inclined to come up with a proof for the simpeler inference mechanisme first. Note that once you have that, you can probably from that derive proofs for more complicated inference mechanisms.

> > (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?

By the way, I may also some other good news. I looked briefly at the problem of the infinitely wide relations, and it seems that is not so difficult to solve. The reason is that any expression r that returns an infinitely wide result can be rewritten to r' * W where W is my version of 11, (W as in "wide" and omega) with r' an expression without W. Since for such expressions s' * W and r' * W it holds that they are equivalent iff s' and r' are equivalent, this means that we can reduce this problem to deciding equivalence for the finitely wide expressions. I actually only needed one extra axiom for this:

(32) W + [x] = <x> with x a single attribute

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