Re: completeness of the relational lattice

Marshall schreef:
> On Jun 22, 2:06 am, Jan Hidders <hidd..._at_gmail.com> wrote:
> > Hello Vadim, Marshall and others,
> >
> > The discussion seems to warrant it's own thread, so here goes.
> >
> > There seems to be some disagreement on what algebra we are studying.
> > So let's discuss this first. It is important this get's fixed, because
> > otherwise any time I spent on proving things might be lost. I think
> > it's also important that we settle on notation, because I noticed I
> > was getting confused. Since it's bascially Vadim's idea I'll try to
> > stick to his notation as much as possible.
>
> Okay.
>
> (Over in sci.math, they mostly use ^ v for conjunction/disjunction
> instead of /\ \/. Once I got over my horror of seeing a letter
> used as an operator in mostly worked for me. Do we care?)

I care about fixing a notation. Which one is of minor importance for me. Of course I like mine the best. :-)

> Oh, we haven't mentioned precedence. I propose \/ and /\
> have the same precedence, so that when we write
> the dual of an expression, we will never have to add
> any parentheses.

Agreed.

> > So the syntax of the algebra is as follows: (E is the non-terminal for
> > algebra expressions)
> > - R : a relation name
> > - E /\ E : the natural join
> > - E \/ E : the inner union
> > - 00 : the empty relation with empty header
> > - 01 : the relation with the empty tuple and empty header
> > - 10 : the empty relation with the set of all attributes as header
> > - 11 : the relation with all tuples over all attributes
> > - [x] : the empty relation over header {x} with x a single attribute
> > - 'x=y' : the binary equality relation with header {x,y} and the
> > restriction that x<>y
>
> I believe we might be able to get along without the last three.
> (11, [x], and `x=y`.) And if we do need to talk about attributes,
> I think we need to be talking about sets of attributes. (So x
> above would be a set.)
>
> I didn't see (relational) = mentioned in there. Is that just assumed?
> We need either relational equality or the relational comparator.

Because this is the syntax for the algebra. So the expressions defined are queries, not propositions. The propositions will all be of the form e1 = e2 where e1 and e2 are expresssions in the algebra but sometimes with variables instead of relations.

> Also I don't see division in there yet. We were talking about
> including that, weren't we?

Yes. I strongly suggest to postpone adding division and difference until we have a completeness result without them. I'm fairly certain they will make our task impossible, so I first want to try without them.

> > I don't like having 10 and 11 because it clearly steps outside the
> > relational model and first order logic, but I see no direct reasons to
> > remove them.
>
> 10 seems required, because without it, the lattice is neither
> bounded nor complete, whereas with it it is both.

Well, as I said, I accept them, so I'm not going to argue against them. But if we run into trouble because of them during the completeness proof, I reserve the right to say "See! I told you!". :-)

> > There was some doubt on the presence of [x] but I don't
> > see how we can otherwise define projection.
>
> Any expression of the form
>
> E \/ [x]
>
> can be rewritten as
>
> E \/ (X /\ 00)
>
> where X is any relation with the same header as [x].

?? Either you can express it or you cannot. Either you can give me an expression equivalent to [x] or you cannot. An expression that is only equivalent under certain circumstances is not good enough. It means your expressive power in terms of queries that you can express drops below that of the unions of conjunctive queries (UCQ). If the database consists of just R(a,b) then how can I project on {a}, or on {c,d}?

What your argument does show however is that reasoning over projections is going to be similar to reasoning over relations for which we know certain equations hold. So the equations we need for [x] can probably be readily derived from that. There is probably not really something fundamentally new here and the soundness of the extra rules can be easily proved using the usual laws. But proving that can only be done by allowing the construct and proceeding with the proof.

> > Also I don't see how we can avoid mentioning attributes
> > since we already have 'x=y' where the are already mentioned.
>
> Will go looking for where we use that and respond there.

You need to be able to express simple equality selections which are in UCQ. Also here you need to show that you can come up with an expression that is always equivalent. I don't think you can without introducing another construct. In fact, it is not hard to proof that there are queries you cannot express without 'x=y' and [x] since you can only express only projections (and not even all of them) of the natural join of all relations in the database, which is a very weak class indeed.

> > So can we agree on this algebra and notation?
>
> Sure, modulo the questions above.

Great! Progress! :-)

• Jan Hidders