Re: Relational lattice

Vadim Tropashko wrote:
> Jan Hidders wrote:
>

>> Mikito Harakiri wrote:
>> 
>>> http://arxiv.org/abs/cs.DB/0501053
>> 
>> Very interesting link. But you not only have to admit them as 
>> intermediate results, you need them in your base language in order
>> to express certain queries. Strictly speaking the language consists
>> of the two operators plus an (infinite?) set of these infinite
>> relations. I'm not sure if that simplifies much.
>> 
>> Strictly speaking Vadim doesn't really prove that because he only shows 
>> that he can simulate the manipulation of binary relations, which is
>> strictly weaker than full first order logic. But it could be that
>> his proof can be generalized for the n-ary case, I haven't checked
>> that.

That would be fine if all your definitions and proofs were easily generalizable for the n-ary case. For most of them this is true, but I have severe doubts over the simulation of the set difference. So the conclusion is that you did not proof what you claim in the article, i.e., that your operators are relationally complete.

At first sight I would say you can express exactly all unions of conjunctive queries with negation. That's not relationally complete, but still quite a large class of queries and having a nice algebra for that could be very interesting.

> It is indeed hard to tell if this development has any practical
> applications yet. The main goal is to make all algebraic
> manipulations formal. Consider, for example, the following identity
> in the standard RA:
>
> sigma_R(x,y) pi(x,y,z) A(w,x,y,z) = = pi(x,y,z) sigma_R(x,y)
> A(w,x,y,z)
>
> where R(x,y) just an arbitrary predicate for selection operator (it
> doesn't have to be binary).
>
> This rule is folklore, so it's hard to find a reference which would
> contain a proof.

Of course. The proof is trivial. You can simply prove it from the set-theoretic definitions. You have a problem with that just because it is not an algebraic proof?

> [...] Without
> distributivity law it's even unclear if there is a normal form for
> lattice expressions.

It's very unlikely that such a normal form with reasonable properties exists because the equality of relational algebra is undecidable.

> It is fair to conclude that a lot remains yet to undestand.

Let's start with understanding with (1) what it is that you actually claim (i.e. formulating a formal theorem) and (2) coming up with an actual proof for that claim, and then we can see were it goes from there. Getting the math right is a "conditio sine qua non" here.

• Jan Hidders