Re: struggling proving lattice identity

mikharakiri_nospaum_at_yahoo.com
Date: 02/23/05 

Date: 23 Feb 2005 11:36:24 -0800

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]
2. c\/a = a
  [given]
3. ((a/\b)\/c)\/a = a
  [1\/2, associativity, commutativity, idempotence]
4. (a/\b)\/b = b
  [absorption]
5. (a/\b)\/(b\/c) = b\/c
  [4\/c, associativity)
6. c\/(b\/c) = b\/c
  [absorption]
7. ((a/\b)\/c)\/(b\/c) = b\/c
  [5\/6]
8. (a/\b)\/c = ((a/\b)\/c)/\a
  [3/\((a/\b)\/c) absorption]
9. (a/\b)\/c = ((a/\b)\/c)/\(b\/c)
  [7/\((a/\b)\/c) absorption]
10. (a/\b)\/c = ((a/\b)\/c)/\a/\(b\/c)
  [8/\9]

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.

BTW, is there a computer algebra system supporting lattice operations?

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:

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)

Rewritten in terms of the relational lattice operators
http://arxiv.org/abs/cs.DB/0501053
the previous identity is

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)

where p(x,y) <= empty(x,y,z). The problem is that the relational
lattice is not modular...