Re: struggling proving lattice identity

From: William Elliot (marsh_at_privacy.net)
Date: 02/24/05 

Date: Wed, 23 Feb 2005 19:23:44 -0800

On Wed, 23 Feb 2005 mikharakiri_nospaum@yahoo.com wrote:

> William Elliot wrote:
>> c <= a ==> a/\b \/ c <= a /\ b\/c
>> a/\b <= a
>> c <= a
>> a/\b \/ c <= a
>>
>> a/\b <= b <= b\/c
>> c <= b\/c
>> a/\b \/ c <= b\/c
>>
>> a/\b \/ c <= a /\ b\/c
>
> Thank you, William! It was easy to translate your proof leveraging
> order relation into the proof with equalities:
>
> 1. (a/\b)\/a = a
> [absorption]
...
> 10. (a/\b)\/c = ((a/\b)\/c)/\a/\(b\/c)
> [8/\9]
>
Yicks, you like doing it the hard way.

For long expressions, use some spaces for easier readability.
((a/\b)\/c) /\ a /\ (b\/c)

> There is no way for me finding such a proof directly! Unless there is a
> proof at least twice as short, I'm tempted to conclude that inequality
> is higher level relation in the lattice theory than the equality.
>
It is not.
<= is directly defined from lattice operations + and * by
a <= b when a = ab = a/\b

Then show a <= b iff a\/b = a + b = b.
Next is to show that ab and a+b are glb and lub of a,b
for the defined order <=.

Alternatively, define <= for a set L and insist that
every a,b in L has a glb and lub in L.

Show glb and lub are unique so that one can
then define ab = glb a,b, a + b = lub a,b
and proceed to demonstrate the lattice axioms for
the constructed + and *.

> BTW, is there a computer algebra system supporting lattice operations?
>
Yes, the human brain.

> As you mentioned the modular property, let me go on a little bit about
> applications. The modular property is essentially the commutativity of
> projection and selection operation in the relational algebra:
>
Huh? Is that incomprehensible for
         a <= c ==> (a + b)c = a + bc ?

> sigma_p(x,y) pi_x,y,z A(w,x,y,z) =
> = pi_x,y,z sigma_p(x,y) A(w,x,y,z)
>
I have no idea what you're talking about.

> Rewritten in terms of the relational lattice operators
> http://arxiv.org/abs/cs.DB/0501053
> the previous identity is
>
As pdf files with much math don't up clearly, I've little interest in
downloading and procuring a transcription.

> empty(x,y,z) union ( A(w,x,y,z) join p(x,y) ) =
> = ( empty(x,y,z) union ( A(w,x,y,z) ) join p(x,y)
>
Translation?

> where p(x,y) <= empty(x,y,z). The problem is that the relational
> lattice is not modular...
>
Computer buffs are prone to mess things up making the simple complicated.