Oracle FAQ Your Portal to the Oracle Knowledge Grid
HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US
 

Home -> Community -> Usenet -> comp.databases.theory -> Re: completeness of the relational lattice

Re: completeness of the relational lattice

From: Jan Hidders <hidders_at_gmail.com>
Date: Fri, 22 Jun 2007 19:42:41 -0000
Message-ID: <1182541361.660010.123300@o11g2000prd.googlegroups.com>


On 22 jun, 20:36, Marshall <marshall.spi..._at_gmail.com> wrote:
> On Jun 22, 9:42 am, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > Marshall schreef:
>
> > 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.

What do you man by premises? Arbitrary conjuctions of conditions is no problem if you can express UCQ, and with my suggested additions you can. By the way, you can prove that such an operator would indeed add expressive power (so more than UCQ) but it's not clear to me how much. So that makes me a little nervous, so again I would say, let's first axiomatize the algebra without this operation.

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

No.

> An axiom is an expression that evaluates to true (or 01)
> by definition.

Hmm, I would say it is a constraint you know always holds for the database. But that's actually saying thing.

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

Sure. Nothing wrong with looking at it that way.

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

That is entirely possible.

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

Let me see if I understand. So you propose a constructm, say [X] with X a set of attributes, with the semantics that it returns an arbitrary relation with header S. That makes your algebra non-deterministic! Do you realize how much problems non-determinism are going to introduce in the proofs?

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

It's not so much needed for the completeness proof, but rather it is required for the result to be interesting and publishable. There is no point in coming up with a complete axiomatization for some weird fragment of the relational algebra that nobody is interested in. The UCQ fragment is really the minimum.

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

Of course.

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

It always is. This is also the case in my daytime research. :-)

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

Ok. That's of course very helpful. I hope I can convince Vadim to come along as well.

> > > > So can we agree on this algebra and notation?
>
> > > Sure, modulo the questions above.
>
> > Great! Progress! :-)
>
> Hoera!

Nice! :-)

Received on Fri Jun 22 2007 - 14:42:41 CDT

Original text of this message

HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US