# Re: completeness of the relational lattice

From: Jan Hidders <hidders_at_gmail.com>
Date: Tue, 26 Jun 2007 00:53:52 -0700
Message-ID: <1182844432.160701.20510_at_p77g2000hsh.googlegroups.com>

On Jun 26, 12:29 am, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
> 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).

It's a schema anyway because you still have relation variables. Although I agree that I need two types of variables, or three if you count the singleton attributes, and you have one (or two if you have special ones for singleton sets, as you suggest later). On the other hand, I only have equations, and you need propositional formulas over equation.

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

You found those already?

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

I don't know, you've onlly given axioms and not the inference mechanism. Since they are propositional formulas I assume you want to use propositional calculus. If you add this you can no longer claim that you have a pure algebraic axiomatization, which makes the completeness claim less interesting. But is propositional calculus all you allow, or are you also allowing reasoning by rewriting? The latter can be captured in either your inference mechanism or by adding adding extra axioms (e.g. the rules "if R = R' and S = S' then R /\ S = R' /\ S'" and "if R = S and S= T then S = T" and ... ). There is the usual trade off between putting your inference in the axioms or in the inference mechanism. So how do you want do that? And yes, I want a full formal specification of that. You cannot write a paper on the completeness of some reasoning system and not specify formally its inference mechanism. Note by the way that this changes the notion of "complete" because it then not only means that you can derive all equations that hold, but in fact that you can derive all propositional formulas (including negations) over equations that hold. I have no idea how to prove that. Do you?

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

Ok. I think that would work. But also here you have to say how the inference deals with this. How does it know what and what not to match x with when it rewrites? This is solvable, but again it adds complexity to the inference mechanism.

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

Of course. But the difference is that I have fully formally specified what my system is (the axioms *and* the inference mechanism) and you have not. Moreover it seems that you want to push a lot of the complexity into the inference mechanism in order to keep you set of axioms simple. As I already said, that makes the completeness claim at the same time harder to prove, and less interesting.

> > > > (30) <> = {()}
>
> This is a theorem, not axiom.

Yes, in your inference mechanism, but not in mine. So I need it.

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

Sure. (I'm skipping rewrites involving shifting brackets):

``` (((R(x,y) * <yz>) + [xz]) * <yz>) + [xy]
= (((R(x,y) * <yz>) + [xz]) * <yz> * <yz>) + [xy]       (1)
= (((R(x,y) * <yz>) + [xyz]) * <yz>) + [xy]                (31)
= (R(x,y) * <yz> * <yz>) + ([xyz] * <yz>) + [xy]       (8)
= (R(x,y) * <yz>) + ([xyz] * <yz>) + [xy]                  (1)
= ((R(x,y) * <yz>) + [xyz] + [xy]                              (29)
= ((R(x,y) * <yz>) + [xy]                                         (12)
= (R(x,y) + [xy]) * (<yz> + [xy])                              (9)
= (R(x,y) + [xy]) * <y>                                           (26)
```
= R(x,y) * <y>
(10)
=
R(x,y)
(28)
• Jan Hidders
Received on Tue Jun 26 2007 - 09:53:52 CEST

Original text of this message