# Re: TRUE and FALSE values in the relational lattice

Date: Thu, 21 Jun 2007 14:12:48 -0000

Message-ID: <1182435168.322277.180170_at_z28g2000prd.googlegroups.com>

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