Re: TRUE and FALSE values in the relational lattice

On Jun 21, 3:14 am, Jan Hidders <hidd..._at_gmail.com> wrote:
> On 19 jun, 22:32, Marshall <marshall.spi..._at_gmail.com> wrote:
>
> > I am thinking about formalizing the lattice logic. That would
> > involve a formal statement of the axioms and the rules of
> > inference. We would then want a soundness proof, and
> > a proof of consistency. We would also want to understand
> > how complete such a logic would be, and how strong it
> > was relative to FOL. And how decidable. My hope is
> > that it is decidable even if that means it is weaker than
> > FOL. We also have to think about what else besides
> > & and | we're putting in to it. Clearly 00 is a strong
> > candidate. I'm currently thinking that the negation
> > operator I defined a week or two ago is *not* a good idea.
> > The scary one is division/group by.
>
> I would assume the following operations: (in yet another notation)
> - E * E : natural join
> - E + E : generalized union
> - {()} : the relation with empty header and a single empty tuple
> - [A,B,..D] : the empty relation with header {A, B, ..., D} (possibly
> the empty set)
> - A=B : the equality relation with header {A, B}
> - A=c : the relation with header {A} and tuple (A:c)
> - R : a relation with name R (and known header)
>
> That would be roughly equivalent with unions of conjunctive queries,
> for which equivalence is known to be decidable.

Hmm. But without generalized distributivity, we can't always reduce an expression to conjunctive normal form nor disjunctive normal form. We might have a conjunction of a disjunction of a conjunction that we can't reduce. Doesn't that mean we can't always decide equivalence? Mightn't there be two irreducible expressions that are always equal but we can't prove it?

> Adding the set difference or division
> would make it relationally complete (so, FOL)
> and make this undecidable.

I would be interested to have the axioms for division especially. (Have you seen the stuff Vadim's written on the relationship between division and group-by?) Earlier I was playing around with complement, but it introduces infinities into what can otherwise be a completely finite system.

> Actually, a (sound and complete) axiomatization would be a small but
> publishable result. It doesn't seem that impossible either. You could
> start with showing that you have enough rules to bring the thing into
> some union normal form, and then show that you also have enough rules
> to show a homomorfisme over the conjuncts. Quite interesting indeed.
> Anyone interested in thinking about a paper on that?

Yes.

These are the papers I've found that come closest to this sort of thing:

http://citeseer.ist.psu.edu/437168.html

http://consequently.org/writing/gndl/

As an aside, I wrote a modest expression simplifier, that took advantage of all the lattice axioms. I want to add inference rules to it and make it in to a theorem prover. Perhaps just one rule is sufficient? With lattice order as implication, a rule that takes A & (A=>B) into A & (A => B) & B, perhaps?

This is also motivating my interest in division--what are its axioms?

Going further, I am working on a system for allowing join to work with functions, and include aggregators, generators, and many-to-many functions, and to build a programming language capable of executing all of this. (Aggregators are applied with division.)

Marshall Received on Thu Jun 21 2007 - 16:12:48 CEST