Re: completeness of the relational lattice

On Jun 22, 2:53 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
> 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.

Ok, developing attribute agnostic methods is a separate goal that I can put aside for a while.

> Maybe a compromise is possible. As you and Marshall already noted it
> holds that
>
> [H] = R /\ 01

typo: [H] = R /\ 00

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

Agreed, the issue if the [] is requitred is not essential. Again this notation is handy (see below).

Could we work out an example in order to make comfortable with your method? Assume R(x,y) and consider the following two expressions:

(`x=y`) \/ R \/ ( ((R /\ `y=z`) \/ [x,z]) /\ ((R /\ `x=z`) \/ [z,y]) )

and

( (`x=y`) \/ (R /\ `y=z`) ) /\ ( (`x=y`) \/ (R /\ `x=z`) )

Are they equivalent or not?

One of the methods you suggested is some kind of distributivity axiom (in pure equational form). This issue is still hanging, right?

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

OK

> Deal? :-)

No cliche phrases, please:-) Received on Sat Jun 23 2007 - 00:24:36 CEST