(Msg. 16) Posted: Fri Jun 22, 2007 9:39 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: comp>databases>theory (more info?)

On Jun 22, 5:27 pm, Marshall wrote:
> > Sure x,y,z have to belong to the same domain, while "a" and "b" may be
> > from a different domain. This is again an informal definition that is
> > supposed to drive the intuition.
> Hmm. I don't get that. Also, is there any significance to the fact
> that x=y and a=b are enclosed in different kinds of quotes?

No, the quote around a was suposed to distinguis it from article:-) I
should have put quoyes around x,y,z, but being lazy.

What I meant is that Equality relation looks like this:

x y z a b
----------
1 1 1 i i
1 1 1 j j
2 2 2 i i
2 2 2 j j
3 3 3 i i
3 3 3 j j

where x,y,z are from domain integers, and a and b from the domain of
"i" and "j" letters.

> Let me just say that I think that domains are pure distraction,
> best ignored.

No wonder you don't accept element 11. Because 11 \/ R produces a
cartesian product of domains. If R /\ 00 is atomic, then 11 \/ R is an
individual domain.

(Msg. 17) Posted: Fri Jun 22, 2007 9:53 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 22, 5:38 pm, Jan Hidders wrote:
> On 23 jun, 01:05, Vadim Tropashko wrote:
> > A(R \/ B) = A(R) intersect A(B)
> > Note that function A is not a homomorhism, that is the dual identity
> > A(R /\ B) = A(R) union A(B)
> > doesn't hold.
>
> Really? It doesn't? Can you give a counterexample?

Oops, you are right. In my notation it corresponds to

00 /\ (R /\ B) = (00 /\ R) /\ (00 /\ B)

I confused it with the identity

00 \/ (R /\ B) = (00 \/ R) /\ (00 \/ B)

which doesn't hold.

So function A is a true lattice homomorphism to boolean algebra of
header sets.

> > BTW, if you have finction A, then we probably don't need element 00,
> > right? (The element A(01) is just an empty set in the boolean algebra
> > of headers, not the lattice element 00)
>
> Not sure what you are asking. A is not really part of the algebra, but
> only used in describing the rules, so A(01) is not an expression in
> the algebra.

I cleared my confusion. What would be the result of join betwwen empty
relation R and empty relation S with disjoint attributes? 00, of
course.

(Msg. 18) Posted: Fri Jun 22, 2007 10:20 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 22 jun, 19:36, Vadim Tropashko wrote:
> On Jun 22, 3:08 am, Jan Hidders wrote:
>
> > > > We cannot distribute in general, but we have a specific distribution rule:
>
> > > > (1) r /\ ((s \/ [H]) \/ (t\/[H])) = r /\ (s \/ [H]) \/ r*(t \/ [H])
>
> > > Which is BTW a very limited case embraced by Spight criteria.
>
> > Indeed. But it is a simple equation, no premises.
>
> Your premise is that H is a set of attributes which is a subset of
> attributes of relations s and t

No, any set of attributes H will do.

> > > BTW, why don't we define square brackets [R] as an unary operator,
> > > expressed in my notation as
>
> > > [R] = R /\ 00
>
> > What is R? In [R] it is a set of attributes. So a set of attributes is
> > a valid expression in your syntax? I'm not sure what that means.

Sorry, I missed your point there. The problem with [R] is that is
doesn't allow me to define a projection for an arbitrary set of
attributes.

> > Could
> > you give a complete definition of your syntax just like I did?
>
> - R : a relation name
> - Expr /\ Expr : the natural join
> - Expr \/ Expr : 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
> - E : the "universal" equlity relation

And extended with [R] I assume. Can you prove that you can express all
queries in UCQ?

> Once again, I'm not convinced about syntax until I see a convincing
> set of axioms.

We have to start somewhere. Otherwise I'm afraid we are not going to
get anywhere. Even an ugly axiomatization is better then no
axiomatization at all.

(Msg. 19) Posted: Fri Jun 22, 2007 10:24 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 22 jun, 19:14, Vadim Tropashko wrote:
> On Jun 22, 9:42 am, Jan Hidders wrote:
>
>
>
> > Marshall schreef:
> > > 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}?
>
> You cannot. [...]

Indeed. So can we agree on my addition for the time being?

(Msg. 20) Posted: Fri Jun 22, 2007 10:27 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 22, 11:20 am, Jan Hidders wrote:
>
> We have to start somewhere. Otherwise I'm afraid we are not going to
> get anywhere. Even an ugly axiomatization is better then no
> axiomatization at all.

That's a good point. Why don't we move forward with what Jan
has in the OP? There is certainly nothing objectionable in it.
And if it isn't minimal, we can come back later and simplify it.

(Msg. 21) Posted: Fri Jun 22, 2007 10:36 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 22, 9:42 am, Jan Hidders 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!

(Msg. 22) Posted: Fri Jun 22, 2007 11:42 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 22 jun, 20:36, Marshall wrote:
> On Jun 22, 9:42 am, Jan Hidders 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!

(Msg. 23) Posted: Fri Jun 22, 2007 11:59 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 22, 12:42 pm, Jan Hidders wrote:
> On 22 jun, 20:36, Marshall wrote:

[lots of agreement snipped]

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

Ack, no!

> That makes your algebra non-deterministic!

No no no! Abort, abort!

> Do you realize how much problems non-determinism are going
> to introduce in the proofs?

Being someone who has written a lot of concurrent code,
I am on a first name basis with nondeterminism. This is not
to say that we are friendly with each other; merely that we
are well acquainted. No, I am extremely sensitive to issues
of nondeterminism, and nothing in the algebra ought to be
nondeterministic. In my programming language, I am careful
to ensure this is so, and in fact have carefully charted all
the possible holes where nondeterminism may leak in.
A modest amount of *controlled* nondeterminism in
multithreaded code and around I/O is acceptable; in
the core algebra, no no no.

(Msg. 24) Posted: Sat Jun 23, 2007 1:28 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 22 jun, 22:14, Vadim Tropashko wrote:
> On Jun 22, 12:59 pm, Marshall wrote:
>
>
>
> > On Jun 22, 12:42 pm, Jan Hidders wrote:
>
> > > On 22 jun, 20:36, Marshall wrote:
>
> > [lots of agreement snipped]
>
> > > > 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.
>
> > Ack, no!
>
> May I suggest that there is no concept of relation construction other
> than specifying it in terms of other relations via primary lattice
> operations?

If you can achieve the expressive power of UCQ that way, I'm all for
it, but I doubt that you can. And if you cannot then any completeness
result will become much less interesting and probably not publishable
in a target that would be interesting for me. I'd really like to put
time in this, because I think it is very nice. However I also have
other urgent things to do for my daytime job, so if I think there is
no real chance of a publishable result then I cannot justify putting
much time in this.

Maybe a compromise is possible. As you and Marshall already noted it
holds that

[H] = R /\ 01

for all relations R with header H. This means several things. First it
means that if you have a complete axiomatization for the algebra
without [H] you will automatically get a complete axiomatization for
the algebra with [H] if you add this rule. The procedure for proving
e_1 = e_2 would be to convert all the occurrences of [H_i] to R_i /\
01 with R_i the header H_i, obtaining e'_1 = e'_2, then prove the
equivalence. It also works the other way around. If we find a complete
axiomatization for the algebra with [H] and need a certain rule
involving [H] then the counterpart with [H] replaced should be
derivable in the axiomatization without [H]. So it is actually
unlikely that there are fundamental different difficulties in proving
the completeness of with or without [H].

So we could do the following. I start from the algebra with [H] and
you start from the algebra without [H] and we both try to prove
completeness. You tell me the rules that you think you need (because I
will need those anyway) and I will tell you the rules I think I need
in addition for [H] (because you will need to check if you have the
corresponding rule with [H] replaced).

(Msg. 25) Posted: Sat Jun 23, 2007 1:28 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 22 jun, 21:11, Vadim Tropashko wrote:
> On Jun 22, 11:20 am, Jan Hidders wrote:
>
>
>
> > On 22 jun, 19:36, Vadim Tropashko wrote:
>
> > > On Jun 22, 3:08 am, Jan Hidders wrote:
>
> > > > > > We cannot distribute in general, but we have a specific distribution rule:
>
> > > > > > (1) r /\ ((s \/ [H]) \/ (t\/[H])) = r /\ (s \/ [H]) \/ r*(t \/ [H])
>
> > > > > Which is BTW a very limited case embraced by Spight criteria.
>
> > > > Indeed. But it is a simple equation, no premises.
>
> > > Your premise is that H is a set of attributes which is a subset of
> > > attributes of relations s and t
>
> > No, any set of attributes H will do.
>
> Counterexample:
>
> r(x,y) = {(1,7),(1,4),(2,4),(2,7)}
> s(x) = {2}
> t(y) = {7}
> H = {x,y}
>
> s \/ [H] = {2}
> t \/ [H] = {7}
> ((s \/ [H]) \/ (t\/[H])) = 01
> r /\ ((s \/ [H]) \/ (t\/[H])) = *** {(1,7),(1,4),(2,4),(2,7)} ***
> r /\ (s \/ [H]) = {(2,4),(2,7)}
> r /\ (t \/ [H]) = {(1,7),(2,7)}
> r /\ (s \/ [H]) \/ r*(t \/ [H]) = *** {(1,7),(2,4),(2,7)} ***

[.. multiple expletives deleted ..] You are right!! I'd missed that.
That seemed a serious threat to the proof technique I had in mind. But
I think it is not fatal.

> AFIR you explicitly mentioned that H is a set of attributes which is
> intersection of that of s and t -- and that's a premise.

Yes, that is how I wanted to construct that H and I think I can, but
I'm annoyed by this premise. I wanted all my rules to be without
premises. But I don't seem to be able to avoid it. Anyway, with
premises I can probably simplify using Marshall's rule. Assuming I
have a function A(e) that gives the header of the result of e:

r /\ (s \/ t) = (r /\ s) \/ (r /\ t) if (A(r) * (A(s)) - A(t) is
empty and (A(r) * A(t)) - A(s) is empty

Clearly the function A can be defined for the algebra, including [H]
and 'x=y'.

(Msg. 26) Posted: Sat Jun 23, 2007 4:27 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Just some quick comments:

On Jun 22, 11:29 am, Vadim Tropashko
wrote:
>
> Before giving the equality axiom let describe informally what the
> constant E is. We join all possible equality relations in the system,
> so that we have something like this
>
> E = `x=y` /\ `y=z` /\ ... /\ 'a=b' /\ ...

How interesting! That would have made some of the stuff I was
working on a few weeks ago a lot easier. However, not having
it meant I had to come up with an entirely different approach that
I think has some merit, namely the "free relation variable with
fixed header."

> Sure x,y,z have to belong to the same domain, while "a" and "b" may be
> from a different domain. This is again an informal definition that is
> supposed to drive the intuition.

Hmm. I don't get that. Also, is there any significance to the fact
that x=y and a=b are enclosed in different kinds of quotes?

Let me just say that I think that domains are pure distraction,
best ignored. The algebra needn't have domains; they complicate
without adding benefit. Domains make more sense as a kind of
constraint.

(Msg. 27) Posted: Sat Jun 23, 2007 4:38 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 23 jun, 01:05, Vadim Tropashko wrote:
> On Jun 22, 3:31 pm, Jan Hidders wrote:
>
> > I can probably simplify using Marshall's rule. Assuming I
> > have a function A(e) that gives the header of the result of e:
>
> > r /\ (s \/ t) = (r /\ s) \/ (r /\ t) if (A(r) * (A(s)) - A(t) is
> > empty and (A(r) * A(t)) - A(s) is empty
>
> OK, to summarize we have 2-sorted algebra:
> 1. Relations (which is lattice)
> 2. Relation headers (which is standard BA)
> The function A maps relations to headers, and enjoys the following
> rule
> A(R \/ B) = A(R) intersect A(B)
> Note that function A is not a homomorhism, that is the dual identity
> A(R /\ B) = A(R) union A(B)
> doesn't hold.

Really? It doesn't? Can you give a counterexample?

> Please also note, that in my notation the algebra is not many sorted.

Duly noted.

> BTW, if you have finction A, then we probably don't need element 00,
> right? (The element A(01) is just an empty set in the boolean algebra
> of headers, not the lattice element 00)

Not sure what you are asking. A is not really part of the algebra, but
only used in describing the rules, so A(01) is not an expression in
the algebra.

(Msg. 28) Posted: Sat Jun 23, 2007 5:53 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 23 jun, 02:53, Vadim Tropashko wrote:
>
>
> I cleared my confusion. What would be the result of join betwwen empty
> relation R and empty relation S with disjoint attributes? 00, of
> course.

Sure? I would describe that as [H1] /\ [H2] wich is equivalent to [H3]
where H3 is the union of H1 and H2, wich would not be empty.

Btw. let me give a rough sketch of what my plan of attack is going to
be. It takes very big steps and ignores important technical issues,
but it should give you an idea of what my ideas are. The proof is
going to proceed in several stages with several normal forms. The
syntax I'll start from is:

E ::= R | E /\ E | E \/ E | 11 | [H] | 'x=y'

I allow H to be empty, so I omitted 00 = [], 01 = 11 \/ [] and 10 =
11 /\ []

The first stage will be a normalization to a "union normal form" that
I already talked about. This normal form means that the expression is
in a form r_1 \/ ... \/ r_n with the r_i such that the contain no \/
except in the form s \/ [H]. I will refer to these r_i's as the
disjuncts.

Conjecture: we have enough rewrite rules to achieve this normal form.

Some of the disjuncts will be conjunctive queries (CQ) and some will
not. There are three reasons why some are not in CQ: (1) the result
may be always empty, (2) the result is (infinitely) wide and (3) the
result is (infinitely) long.

Conjecture: if a disjunct always returns an empty result it can be
rewritten to []

That would take care disjuntionts with problem (1). For the other two
problems I conjecture the following:

Conjecture: if a disjunct returns a wide or long result it can be
rewritten to r /\ W or r /\ W /\ 11 where r is a query in CQ and W a
conjunction of 'x=y's such that x and y are not in A(r).

If this holds then we can probably split the problem in showing
completeness for queries in CQ and for special queries such as W.

Conjecture: the rewrite rules are complete for boolean combinations of
'x=y's

So we can the concentrate on expressions that represent normal CQ's.
We can think of those queries as expressed by Horn clauses or:

In fact you might read that as a shorthand for our algebra where for
example
- S(a=x, b=y) denotes (S /\ 'a=x' /\ 'b=y') \/ [x,y]
- { (c=x d=y) | r } denotes (r /\ 'c=x' /\ 'd=y') \/ [c,d]

Conjecture: all disjuncts in CQ can be written in this form

For completeness we need to show that if two such queries subsume each
other we can perform absorption. This is enough because for CQ's it
holds that disjunctions of CQ's between which there is no subsumption
that they are equivalent iff it describes the same set of CQ's. So
what is needed for this? We need to be able to rename the variables,
e.g., in the above example we should be able to replace x, y, z with
u, v an w, for example. Of course this is only possible because these
are projected out afterwards.

Conjecture: the variables can be renamed with the rewriting rules.

Probably this requires that we have or can derive a rule like:

r /\ [H] = (r /\ 'x=y') \/ [H] where x and y not in H, and x in
A(r) and y not in A(r)

We should also be able to make two variables the same:

These would allow us to generate from a disjunct versions with renamed
variables and versions where more variables are required to be equal,
which are exactly all queries that are subsumed. So if another
disjunct is subsumed we can do the reverse, i.e., have absorption.

Until sofar. I hope this made some sense. If have to move to other
work now, so I might be less present in the coming days.

(Msg. 29) Posted: Sat Jun 23, 2007 7:11 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 23, 6:53 am, Jan Hidders wrote:
> Btw. let me give a rough sketch of what my plan of attack is going to
> be. It takes very big steps and ignores important technical issues,
> but it should give you an idea of what my ideas are. The proof is
> going to proceed in several stages with several normal forms. The
> syntax I'll start from is:
>
> E ::= R | E /\ E | E \/ E | 11 | [H] | 'x=y'
>
> I allow H to be empty, so I omitted 00 = [], 01 = 11 \/ [] and 10 =
> 11 /\ []
>
> The first stage will be a normalization to a "union normal form" that
> I already talked about. This normal form means that the expression is
> in a form r_1 \/ ... \/ r_n with the r_i such that the contain no \/
> except in the form s \/ [H]. I will refer to these r_i's as the
> disjuncts.

Let see if I can follow this. Say we have an expression from my other
post:

> Conjecture: we have enough rewrite rules to achieve this normal form.

While the above example can be worked out to demonstrate that both
expressions are equivalent, it fairly easy to cook up the example
which can't be reduced to union normal form:

Let R(u,w), S(u), Q(w), T(V), P(u,v), then we can't apply
distributivity to simplify

( (R /\ (S \/ Q)) \/ T ) /\ P

> Some of the disjuncts will be conjunctive queries (CQ) and some will
> not. There are three reasons why some are not in CQ: (1) the result
> may be always empty, (2) the result is (infinitely) wide and (3) the
> result is (infinitely) long.

I don't follow this, the example maybe helpful. I can't resist a
feeling that those appears to be merely some special cases.

> Conjecture: if a disjunct always returns an empty result it can be
> rewritten to []

In the example above

( (R /\ (S \/ Q)) \/ T ) /\ P

suppose the join of P with the rest of the expression is empty. How do
we collapse it to []?

> That would take care disjuntionts with problem (1). For the other two
> problems I conjecture the following:
>
> Conjecture: if a disjunct returns a wide or long result it can be
> rewritten to r /\ W or r /\ W /\ 11 where r is a query in CQ and W a
> conjunction of 'x=y's such that x and y are not in A(r).
>
> If this holds then we can probably split the problem in showing
> completeness for queries in CQ and for special queries such as W.
>
> Conjecture: the rewrite rules are complete for boolean combinations of
> 'x=y's
>
> So we can the concentrate on expressions that represent normal CQ's.
> We can think of those queries as expressed by Horn clauses or:
>
> { (c=x d=y) | R(a=x, b=x) /\ S(a=x, b=y) /\ T(a=y, b=z) }
>
> In fact you might read that as a shorthand for our algebra where for
> example
> - S(a=x, b=y) denotes (S /\ 'a=x' /\ 'b=y') \/ [x,y]
> - { (c=x d=y) | r } denotes (r /\ 'c=x' /\ 'd=y') \/ [c,d]

I'm totally confused here because I don't see any distinction between
the 2: the right sides are identical modulo variable names.

> Conjecture: all disjuncts in CQ can be written in this form
>
> For completeness we need to show that if two such queries subsume each
> other we can perform absorption. This is enough because for CQ's it
> holds that disjunctions of CQ's between which there is no subsumption
> that they are equivalent iff it describes the same set of CQ's. So
> what is needed for this? We need to be able to rename the variables,
> e.g., in the above example we should be able to replace x, y, z with
> u, v an w, for example. Of course this is only possible because these
> are projected out afterwards.
>
> Conjecture: the variables can be renamed with the rewriting rules.
>
> Probably this requires that we have or can derive a rule like:
>
> r /\ [H] = (r /\ 'x=y') \/ [H] where x and y not in H, and x in
> A(r) and y not in A(r)
>
> We should also be able to make two variables the same:
>
> r /\ [H] = ((r /\ 'x=y') \/ r) \/ [H]

There must be a typo here, because (r /\ 'x=y') \/ r evaluates to r by
absorption. Then r /\ [H] can't be equal to r \/ [H].

> Also needed is a rule to merge two queries:
>
> { (c=x d=y) | r1 } \/ { (c=x d=y) | r2 } = { (c=x d=y) | r1 \/
> r2 }
>
> These would allow us to generate from a disjunct versions with renamed
> variables and versions where more variables are required to be equal,
> which are exactly all queries that are subsumed. So if another
> disjunct is subsumed we can do the reverse, i.e., have absorption.
>
> Until sofar. I hope this made some sense. If have to move to other
> work now, so I might be less present in the coming days.
>
> -- Jan Hidders >> Stay informed about: completeness of the relational lattice

(Msg. 30) Posted: Mon Jun 25, 2007 3:32 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 24 jun, 00:11, Vadim Tropashko wrote:
> On Jun 23, 6:53 am, Jan Hidders wrote:
>
>
>
> > Btw. let me give a rough sketch of what my plan of attack is going to
> > be. It takes very big steps and ignores important technical issues,
> > but it should give you an idea of what my ideas are. The proof is
> > going to proceed in several stages with several normal forms. The
> > syntax I'll start from is:
>
> > E ::= R | E /\ E | E \/ E | 11 | [H] | 'x=y'
>
> > I allow H to be empty, so I omitted 00 = [], 01 = 11 \/ [] and 10 =
> > 11 /\ []
>
> > The first stage will be a normalization to a "union normal form" that
> > I already talked about. This normal form means that the expression is
> > in a form r_1 \/ ... \/ r_n with the r_i such that the contain no \/
> > except in the form s \/ [H]. I will refer to these r_i's as the
> > disjuncts.
>
> Let see if I can follow this. Say we have an expression from my other
> post:
>
> (`x=y`) \/ R \/ ( ((R /\ `y=z`) \/ [x,z]) /\ ((R /\ `x=z`) \/ [z,y]) )
>
> It is in union normal form, right? And
>
> ( (`x=z`) \/ ( (R /\ `y=z`) \/ [x,z] ) /\ ( (`z=y`) \/ ( (R /\ `x=z`)
> \/ [z,y]) )
>
> is not?

Correct.

> > Conjecture: we have enough rewrite rules to achieve this normal form.
>
> While the above example can be worked out to demonstrate that both
> expressions are equivalent, it fairly easy to cook up the example
> which can't be reduced to union normal form:
>
> Let R(u,w), S(u), Q(w), T(V), P(u,v), then we can't apply
> distributivity to simplify
>
> ( (R /\ (S \/ Q)) \/ T ) /\ P

This is solved by the extra rules for [H]. These allow me to make the
attributes of an expression explicit by rewriting it to r \/ [H] where
H contains all attributes of r. That means that in the above you can
rewrite S \/ Q to (S \/ [H1]) \/ (Q \/ [H2]) which in turn can be
rewritten to (S \/ [H1*H2]) \/ (Q \/ [H1*H2]). By then distribtivity
will apply.

> > Some of the disjuncts will be conjunctive queries (CQ) and some will
> > not. There are three reasons why some are not in CQ: (1) the result
> > may be always empty, (2) the result is (infinitely) wide and (3) the
> > result is (infinitely) long.
>
> I don't follow this, the example maybe helpful. I can't resist a
> feeling that those appears to be merely some special cases.

True, but for the moment I had to leave out the infinitely wide
relations, because I didn't see immediately how to deal with them. I
might try again later.

> > Conjecture: if a disjunct always returns an empty result it can be
> > rewritten to []

This is actually trivially false. What it should have said is that
every expression r that returns always an empty result can be
rewritten to [A(r)] where A is the function that give the attribute
set of the result.

> In the example above
>
> ( (R /\ (S \/ Q)) \/ T ) /\ P
>
> suppose the join of P with the rest of the expression is empty. How do
> we collapse it to []?

With the extra rules for [] that I haven't told you about yet.

Maybe at this point I should simply show you the rules that I think
are necessary. I'm not completely sure they are really complete,
because I haven't finished the proof completely yet, but I suspect it
is close.

While working on the proof I changed the fragment a little, and
removed the infinitely wide relations because they were hard to deal
with. I also reverted to my old notation for the natural join and
inner join. My apologies for that.

We consider the following algebra:

E ::= R | E * E | E + E | {()} | [H] | 'x=y'

Where:
- R : a relation with name R (and known header)
- E * E : natural join
- E + E : generalized union
- {()} : the relation with empty header and a single empty tuple
- [H] : the empty relation with header H (possibly empty)
- 'x=y' : the relation { (x=a, y=b) | a in D, b in D, a=b }

The * and + will also be used as intersection and union on sets of
attributes.

We define a function A that computes the header of the result:
- A(R) = H where H is the header of R
- A(r * s) = A(r) + A(s)
- A(r + s) = A(r) * A(s)
- A({()}) = {}
- A([H]) = H
- A('x=y') = {x,y}

Standard equalities:

(1) r * r = r
(2) r * s = s * r
(3) r * (s * t) = (r * s) * t

(4) r + r = r
(5) r + s = s + r
(6) r + (s + t) = (r + s) + t

(7) r * {()} = r
(13) {()} = {()} + []

Special distribution equalities:

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

(14) 'x=y' = 'x=y' + [x,y]
(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

Equalities

(15) 'x=y' = 'x=y' * 'x=x'
(16) 'x=y' = 'x=y' * 'y=x'
(17) 'x=y' * 'y=z' = 'x=y' * 'y=z' * 'x=z'
(18a) R * 'x=x' = R if x in header R

Miscellaneous

(18b) [] * 'x=y' = [x,y]
(18c) 'x=y' + [H] = 'x=x' if x in H and y not in H
(19) 'x=y' + [] = {()}
(24) ((r * 'x=y') + [H]) * 'x=y' = ((r * 'x=y') + [H + {y}]) if x
in H

That's it. Apologies for the weird numbering, it reflects the order in
which I needed them in the proof.

Relational Lattice, what is it good for? - Let's begin with an anonymous review of the earlier iteration of the paper ("Dualities among Relational Algebra Operators"): <review> While the paper does have an intriguing premise, it is inappropriate for inclusion in a refereed academ...

Relational lattice completeness - Mikito Harakiri wrote: > Jan Hidders wrote: > > I'm asking the question for a specific model, not in general as you > > did. For example, boolean algebra for boolean value *is* complete. > > According to Matt all that I have to do to...

Complement in Relational Lattice - RL complement is well-defined. It is roughly the complement of the rows and the complement of the columns. 1. !A has all the columns that aren't in A In other words: A \/ !A \/ 10 = 00 Equivalently: A \/ !A >= 00 2a. If A is nonempt...

TRUE and FALSE values in the relational lattice - Given a relation R(x,y) with domains x={0,1,2}, y={'a','b'} we know from classic predicate theory that the expression R(x=0, y='a') evaluates to true or false. Here is how we establish this siumple fact in the relational lattice. First, lets substitut...

Proof of Completeness of Algebraic Properties of Relationa.. - The Relational Lattice algebra ("RL") consists of two generic operations on relations: natural join, written "&&", and inner union, written "||". It has been shown that the RL operations possess the followi...

All times are: Pacific Time (US & Canada) Goto page Previous1, 2, 3, 4, 5

Page 2 of 5

You can post new topics in this forum You can reply to topics in this forum You can edit your posts in this forum You can delete your posts in this forum You can vote in polls in this forum