Re: completeness of the relational lattice

On Jun 22, 9:42 am, Jan Hidders <hidd...@xxxxxxxxx> 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

.

Relevant Pages

  • Re: completeness of the relational lattice
    ... are queries, not propositions. ... The propositions will all be of the ... expressive power (so more than UCQ) but it's not clear to me how much. ... construction of relations with a specific set of attributes ...
    (comp.databases.theory)
  • Re: In the empty domain:
    ... What may be going on--both in empty domains ... Aristotelian and mediaeval logic did not quantify ... holds in standard modern logic, which is therefore just as much ...
    (sci.logic)
  • Re: A implies I
    ... propositions as true only when their subject terms exist (or, ... interpretation of syllogistic logic roughly 70 years ago. ... tradition according to which the ancients were unaware of empty terms." ... A and O are contradictories. ...
    (sci.logic)
  • Re: A implies I
    ... propositions as true only when their subject terms exist (or, ... interpretation of syllogistic logic roughly 70 years ago. ... tradition according to which the ancients were unaware of empty terms." ... A and O are contradictories. ...
    (sci.logic)
Loading