Re: completeness of the relational lattice

On Jun 22, 9:42 am, Jan Hidders <hidd..._at_gmail.com> wrote:
> Marshall schreef:
>
> I care about fixing a notation. Which one is of minor importance for
> me. Of course I like mine the best. :-)

Of course. I think "forall x: x says 'I like mine the best'" must be a theorem for some branch of mathematics or other. :-)

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

Well, hrm, humm. So that would mean no nesting of equalities? Does that mean there is no value to an expression like:

  A ^ (A=B) ^ B = A

I don't see how we'll be able to, say, combine various premises into a big conjunction unless we can nest equalities.

(To my logic-outsider's eyes (and programmer's sensibilities) all the various distinctions between queries, propositions, equalities, theorems, hypotheses, premises, lemmas, and conclusions seem entirely artificial and unnecessary. I see only expressions, some of which are axioms. Is there some important theoretic distinction that I'm missing? An axiom is an expression that evaluates to true (or 01) by definition. A theorem is an expression that evaluates to 01 under a specific set of axioms. A contradiction is an expression that evaluates to false. Any other expression is just an expression.)

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

Yes, got it. I'm signed up with that.

> > > 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!". :-)

I strongly support you having this right!

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

Hmmm, I think you're not quite getting where I'm coming from.

In simplified terms, you're proposing that we allow the construction of relations with a specific set of attributes and a specific body (namely: empty.) I'm proposing that we only allow the construction of relations with a specific set of attributes. Hence my proposal introduces fewer concepts, therefore it is simpler, and we should by default choose the simplest alternative that gets us what we need.

In fact, I've not yet found a case (in the *logic*) that we need even to be able to specify a given header. It is entirely sufficient merely to say (for example)

A(x,y)
B(y,z)

And know that x, y, and z are sets of attributes. I have not found a need to specify anything more than that. (Not that this is nothing; there is some unification going on with the sets-of-attributes names. "y" in A represents the same set of attributes as the "y" in B.)

I have some stuff I'm working on that works like this. Maybe I can finish it and clean it up and post it.

Now, again, if there is something we need for the completeness proof that we can't get with the above, then I must needs accommodate.

Also, please feel free to continue in whatever means suit you, and allow me the opportunity to see if I can't rewrite what you produce using only the constructs I describe. Is that an acceptable proposal?

In fact, let me take this opportunity to check in. Is the process so far acceptable to you? I honestly believe we share the same goal despite distinctly different backgrounds, and I think some amount of jockeying over terminology, notation, and process is inevitable. Further, if you'd like me to suspend any particular tack, please just ask. I'm happy to oblige for the opportunity to see where you go. I am a neophyte and an autodidact, and I entirely acknowledge your superior credentials in this area. My stuff can always come later.

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

Okay.

> > > 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! :-)

Hoera!

Marshall Received on Fri Jun 22 2007 - 20:36:22 CEST