Re: Relational Lattice, what is it good for?

Mikito Harakiri wrote:
> Marshall Spight wrote:
> > Sets of attributes are given with lower case letters, according
> > to which relations these attributes appear in. Thus, (ab) is the
> > set of attributes that are common to A and B. This set may be empty.
> > The letters of the name are normalized to be in alphabetical order.
>
> This is fine, as long as (ab) is the set of attributes. Below, however,
> you use it in tuple set notation.

Yes. I guess what I am saying is ab is the set of attributes, and (ab) is a tuple with (only) those attributes from the set ab.

> > Definitions
> > The Inner Union, A || B is:
> >
> > { (ab) | (ab) in A or (ab) in B }
>
> I understand this as abbreviation of
>
> { (ab) | (ab) in pi_a_b A or (ab) in pi_a_b B }

If I may correct this last line a bit:

{ (ab) | (ab) in pi_ab A or (ab) in pi_ab B }

The name "ab" is atomic, so I'm uncomfortable with putting the underscore between the a and the b.

Let me try to be more precise. "(ab) in A" means that (ab) is a a tuple whose set-of-attributes equals the set ab, and furthermore, this tuple is constraint to be in the set that is the projection of the relation A over the set-of-attributes ab.

> Alternatively, you have to use existential qualifier, as Jon written in
> the old exchange.

I only vaguely recall this exchange, and I seem to remember that I didn't understand it at the time.

> > 4) = { (a,ab,ac,abc,bc) |
> > ( (a,ab,ac,abc) in A and (ab,bc,abc) in B )
> > or
> > ( (a,ab,ac,abc) in A and (ac,bc,abc) in C )
> > }
> >
> > 5) = { (a,ab,ac,abc,bc) |
> > (a,ab,ac,abc) in A and
> > ((ab,bc,abc) in B or (ac,bc,abc) in C) }
>
> This step is not obvious. Again, careful manipulation would involve
> projection.

I don't understand the problem. This step relies only on the distributivity of the boolean algebra; note that the operands of the boolean operators ("and", "or") in the expressions are syntactically unchanged between steps 4 and 5. I assumed I could rely on boolean distributivity; was that an unjustified assumption?

> > Suggestions, comments, and particularly
> > corrections/refutations/confirmations
> > welcome.
>
> You aren't reading Imre Lakatos, by any chance?

No. Should I be?

> Anyhow, that's an
> outstanding effort (by this group standards) that has a chance to be
> repaired.

My current crazy idea is to learn Coq and see if it can't help me with these sorts of questions. It is called a "proof assistant" isn't it? I could use an assistant right about now. And probably a personal trainer as well.

> A similar manipulation for dual law (with jon and union swapped)
> reveals a that it has to meet the same criteria.

I think so. I have spent significantly less time looking at this one. But we would expect the results to be the same because of the duality.

> Although I seem to
> have (a pathological?) counterexample.
>
> Let
>
> `1` := {x=1}
> `2b` := {x=2, y=b}
>
> 00,01,10, and 11 are defined as before. Then
>
> 00 || (`1` && `2b`) = 00
> (00 || `1`) && (00 || `2b`) = 01 && 01 = 01

Very interesting.

I really haven't finished my examination of the situation, and I don't think I've drawn the right conclusion yet from step six. I think I begin to perceive why this counterexample does what it does.

More work to do. My book on Coq just showed up from Amazon yesterday. We'll see if it can help.

Marshall Received on Sat Feb 18 2006 - 06:33:15 CET