Re: completeness of the relational lattice

From: Jan Hidders <>
Date: Fri, 22 Jun 2007 21:53:01 -0000
Message-ID: <>

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

Deal? :-)

  • Jan Hidders
Received on Fri Jun 22 2007 - 23:53:01 CEST

Original text of this message