(Msg. 61) Posted: Fri Jun 29, 2007 7:00 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 29, 1:40 pm, Jan Hidders wrote:
> On 29 jun, 18:20, Vadim Tropashko wrote:
>
> > On Jun 28, 3:41 pm, Jan Hidders wrote:
>
> > > > > I invite you to challenge me to show that it can prove an equation
> > > > > that holds. Of course you should also check if all these equations can
> > > > > be derived by you.
>
> > One more challenge:
>
> > <xy> + S + Q = <xy> + S
>
> > where S * [] = [z], and Q header is unconstrained. (I don't see axioms
> > about the lattice bottom element:-)
>
> Sorry. The rules axiomatize the algebra for relations with finite
> headers. When I redid parts of the completeness proof with the
> corrected distribution rule new axioms for W kept on popping up, so I
> decided to do the proof first without W. Once it's completely done I
> might try to put it back in.

I'm OK with no W. Yet the identity in question

<xy> + S + Q = <xy> + S

doesn't involve any of 11,10,1E, so why do we need wide relations in
order to prove it? The bottom element 01 is the essence of the
problem, not wide relations:

<xy> + 00 = 01

I'm stuck on this identity, because when trying to prove it it seems
to me that the only axioms needed are the ones that don't include join
operations -- and this is a very limited list.

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

On 29 jun, 18:20, Vadim Tropashko wrote:
> On Jun 28, 3:41 pm, Jan Hidders wrote:
>
> > > > I invite you to challenge me to show that it can prove an equation
> > > > that holds. Of course you should also check if all these equations can
> > > > be derived by you.
>
> One more challenge:
>
> <xy> + S + Q = <xy> + S
>
> where S * [] = [z], and Q header is unconstrained. (I don't see axioms
> about the lattice bottom element:-)

Sorry. The rules axiomatize the algebra for relations with finite
headers. When I redid parts of the completeness proof with the
corrected distribution rule new axioms for W kept on popping up, so I
decided to do the proof first without W. Once it's completely done I
might try to put it back in.

Of course, you might also try to proof this yourself. The tactic would
be to show that there are enough axioms to rewrite any expression to
either an expression r without W or to the form r * W where r contains
no W. If you can show this then completeness of the algebra with W
follows from the completeness of the current algebra.

(Msg. 63) Posted: Fri Jun 29, 2007 11:54 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 29, 6:29 pm, Jan Hidders wrote:
> On 29 jun, 22:40, Jan Hidders wrote:
> > Sorry. The rules axiomatize the algebra for relations with finite
> > headers. When I redid parts of the completeness proof with the
> > corrected distribution rule new axioms for W kept on popping up, so I
> > decided to do the proof first without W. Once it's completely done I
> > might try to put it back in.
>
> I had a brief look and perhaps it's not so bad. It seems only the
> following rules are required for the introduction of W:
>
> (32a) W + [] = <>
> (32b) W + [x] = <x> with x a single attribute
> (55) W * <x> = W with x a single attribute
> (56) W + (r * s) = (W + r) * (W + s)

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

On 30 jun, 00:00, Vadim Tropashko wrote:
> On Jun 29, 1:40 pm, Jan Hidders wrote:
>
>
>
> > On 29 jun, 18:20, Vadim Tropashko wrote:
>
> > > On Jun 28, 3:41 pm, Jan Hidders wrote:
>
> > > > > > I invite you to challenge me to show that it can prove an equation
> > > > > > that holds. Of course you should also check if all these equations can
> > > > > > be derived by you.
>
> > > One more challenge:
>
> > > <xy> + S + Q = <xy> + S
>
> > > where S * [] = [z], and Q header is unconstrained. (I don't see axioms
> > > about the lattice bottom element:-)
>
> > Sorry. The rules axiomatize the algebra for relations with finite
> > headers. [...]
>
> I'm OK with no W.

Ok. I misunderstood "unconstrained". You mean it is an arbitrary
header.

It seems I forgot a rule (it turns out I needed it in a part of
the proof I had no worked out yet)
This rule is of course:

(62) r + <> = <>

And then it is easy:

<xy> + S + Q
(20) = <xy> + S + (S * []) + Q
(22) = <xy> + S + [z] + Q
(26) = <> + S + Q
(62) = <>
(62) = <> + S
(26) = <xy> + S + [z]
(22) = <xy> + S + (S * [])
(20) = <xy> + S

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

On 29 jun, 22:40, Jan Hidders wrote:
> On 29 jun, 18:20, Vadim Tropashko wrote:
>
> > On Jun 28, 3:41 pm, Jan Hidders wrote:
>
> > > > > I invite you to challenge me to show that it can prove an equation
> > > > > that holds. Of course you should also check if all these equations can
> > > > > be derived by you.
>
> > One more challenge:
>
> > <xy> + S + Q = <xy> + S
>
> > where S * [] = [z], and Q header is unconstrained. (I don't see axioms
> > about the lattice bottom element:-)
>
> Sorry. The rules axiomatize the algebra for relations with finite
> headers. When I redid parts of the completeness proof with the
> corrected distribution rule new axioms for W kept on popping up, so I
> decided to do the proof first without W. Once it's completely done I
> might try to put it back in.

I had a brief look and perhaps it's not so bad. It seems only the
following rules are required for the introduction of W:

(32a) W + [] = <>
(32b) W + [x] = <x> with x a single attribute
(55) W * <x> = W with x a single attribute
(56) W + (r * s) = (W + r) * (W + s)

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

On 30 jun, 04:54, Vadim Tropashko wrote:
> On Jun 29, 6:29 pm, Jan Hidders wrote:
>
>
> > (32a) W + [] = <>
> > (32b) W + [x] = <x> with x a single attribute
> > (55) W * <x> = W with x a single attribute
> > (56) W + (r * s) = (W + r) * (W + s)
>
> Challenge:
>
> ((W*P)+(W*Q))*W*R = (W*P*R)+(W*Q*R)
>
> It could be proved if we know that A(W*P) = A(W*Q)= A(W*R)=A(W), or
> equivalently W*P*[]=W*Q*[]=W*R*[]=W*[] but how do we derive these?

So we need to prove W * R * [] = W * []. I'm assuming A(R) = {a,b}.

W * R * []
--> (22) W * [a,b]
--> (11) W * [a] * [b]
--> (29) W * <a> * [] * <b> * []
--> (1) (2) (3) W * <a> * <b> * []
--> (55) W * <a> * []
--> (55) W * []

If we allow R to have infinite width we need to add an extra rule:

R * [] = W * [] if A(R) contains all attributes

Note that altough the system is complete on concrete equations it is
not complete on equation schemas. The schema W * r * [] = W * []
holds, and for any concrete r we can derive it, but the general
equation schema cannot be derived by rewriting alone.

An intriguing question is to which extent the system is complete as an
inference system where we allow concrete equations to be added to the
axiom set. That would correspond to reasoning under the knowledge of
database constraints. As you know we could express full FOL that way,
so a completeness result would be truly spectacular. But I have
currently no idea how to solve that question, and still need to finish
the proof for UCQ.

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