Re: More on lists and sets

Jan Hidders wrote:
> Mikito Harakiri wrote:
> > Less chatty version:
> > http://arxiv.org/ftp/cs/papers/0603/0603044.pdf
>
> Mikito, do you know if Vadim's axiomatization is complete? I mean, are
> two queries equivalent iff the algebraic identities allow me to rewrite
> one to the other? Or might there still be algebraic identities missing?

Axiomatization of relational algebra -- that was the question you asked on c.d.t back in 2001?

Relational lattice theory is not complete. Many parts still remain informal -- Spight distributivity criteria among them. It could be written formally, but this expression

(A /\ C /\ 00) \/ (B /\ C /\ 00) \/ (A /\ B /\ 00) = (B /\ 00) \/ (C /\ 00)
==>
A /\ (B \/ C) == (A /\ B) \/ (A /\ C)

doesn't look like a satisfying axiom.

If we just write all what is known so far there would be too many axioms.

1. 8 Lattice axioms. This set can be reduced -- see any standard source on lattice theory (even wikipedia would do).
2. Decomposition: A = (00 /\ A) \/ (11 \/ A)
3. Homomorphisms into boolean algebras: X -> X /\ 00 X -> X \/ 00 X -> X /\ 11 X -> X \/ 11 This informal condition can be rewritten into a set of formal axioms, e.g. restrictive cases of distributivity A/\11 /\ ( (B/\11) \/ (C/\11) ) == (A /\ B /\ 11) \/ (A /\ C /\ 11)
4. More restrictive cases of distributivty, that doesn't seem to follow from the above 00 /\ (A \/ B) = (00 /\ A) \/ (00 /\ B) 11 \/ (A /\ B) = (11 \/ A) /\ (11 \/ B)