Re: completeness of the relational lattice

On Jun 25, 12:56 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
> > > (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.

So you have axiom schemas, instead of a single axiom system? I don't challenge this approach, but think that a single axiom system is workable as well (see below).

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

OK, I have relation variables, 5 constants 00, 01, 10, 11, 1E, and two binary operations \/, /\, and the inequlity Y <= X abbreviation for X / \ Y = X. Axioms:

1-8. Lattice axioms
9. Spight criteria:
(R/\00) \/ (S/\00) <= Q/\00 and (R/\00) \/ (Q/\00) <= S/\00 implies (R /\ S) \/ (R /\ Q) = R /\ (S \/ Q)
10. (R/\00) \/ (Q/\00) <= R/\00 implies (R /\ S) /\ (R \/ Q) = R \/ (S /\ Q)

11. 01 <= R <= 10
12. R = (00 /\ R) \/ (11 /\ R)
13. Universal equality relation 1E axioms.

Do you imply that I can't reduce both sides of the expression R = S to the Union Normal Form in this system?

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

[b,c,e] = B /\ C /\ E /\ 00

<a,b,c> = 1E \/ (B /\ C /\ E /\ 00)

where 1E is the universal equality relation. Once again your brakets are clever abbreviations, but they are not fundamental.

> > 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.

?? When we write R /\ 00, there is no x and y mentioned anywhere.

> > > 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.

OK, if this is a critical showstopper, then I would have to introduce single attribute relations, conveniently designated with small letters r,s,t etc. Your rule #28, for example becomes

28. x /\ 00 <= R /\ 00 implies
R /\ ((x /\ 00) \/ 1E) = R

The (informal) implication is there in both systems yours and mine, there is no way around it.

> 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) <> = {()}

This is a theorem, not axiom.

<> = 00 \/ 1E = 01 = {()}

It follows from the 1E being non empty. 1E is not empty because if it is empty then for non empty R the left side of

R /\ ((x /\ 00) \/ 1E) = R

evaluates to empty relation.

Oh, yeah, the empty relation is formalized as follows

R \/ 00 = 00 iff R empty
R \/ 00 = 01 iff R nonempty

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

OK, I see that you slightly modified the equality axiom. Can you please derive

(((R(x,y) * <yz>) + [xz]) * <yz>) + [xy] = R(x,y)

in your system? Received on Tue Jun 26 2007 - 00:29:13 CEST