complement in relational bi-lattice

From: <>
Date: Tue, 29 Jul 2008 14:24:57 -0700 (PDT)
Message-ID: <>

To establish a context for this message a reader is referred to
and old thread
  1. INTRODUCTION Classic Relational Algebra employs six basic operations: projection, restriction, join, union, difference, and renaming. Relational Lattice [1,2] represents them in a compact system of two mathematically attractive binary operations: natural join and inner union. In [1] we argued why the ◄OR► operation, which is a part of D&D A New Relational Algebra (named appropriately as A [3]), didn't fit into any lattice model, let alone a stronger system like Boolean Algebra. In [2] we gave the ◄OR► axiomatic definition in lattice terms, and derived most of its properties algebraically. In this paper we would like to reverse our stance, and restore the ◄OR► in all its glory as a part of larger system.

We keep a very succinct algebraic notation, and operate exclusively with relation variables and constants. In rare cases, where we appeal to reader's intuition and give the definition in standard set notation, the relation symbols would be amended with the list of attributes. In the following definition section the R(x,y) and S(y,z) are two relations named R and S with the headers consisting of the sets of attributes {x, y} and {y, z}, correspondingly. Here are definitions for basic operations in set theoretic notation:

i. natural join (denoted with lattice meet operation symbol ∧)

R ∧ S ≝ {(x,y,z) | (x,y) in R /\ (y,z) in S }

ii. inner union (denoted with lattice join operation symbol ∨)

R ∨ S ≝ {(y) | exists x (x,y) in R /\ exists z (y,z)S }

It has been demonstrated that these operations satisfy lattice axioms, hence the notation switched from using join symbol ) from classic relational theory to lattice meet ∧. Also in [1] we invented a new symbol for inner union, but later in [2] have switched to lattice join ∨. We continue to employ Prover9 [4] as our primary theorem prover tool. Consequently, we'll use symbols ^ (caret) for natural join, and v (letter v) for inner union.

2. DATE&DARWEN ◄OR► Operation and its dual The ◄OR► operation can be defined either in set notation

R ◄OR► S ≝ {(x,y,z) | (x,y) in R /\ z in Z or x in X and (y,z) in S }

or, alternatively, in the relational lattice terms

R ◄OR► S ≝ (R ^ (S v R11)) v (S ^ (R v R11)).

where R11 is the universal relation [1,2]. We found it convenient to switch the notation to the plus symbol + in order to continue leveraging Prover9 facilities. Then, we proved + associativity and distributivity of natural join ∧ over the +

Q + (R + S) = (Q + R) + S.
Q ^ (R + S) = (Q ^ R) + (Q ^ S).

in the relational lattice system. These theorems can be proved within set theory framework as well, of course. Unlike set theory framework, however, relational lattice provided an axiom system for proving these facts algebraically by means of automatic theorem prover. To round up this development let's call the + operation as outer union.

Let introduce a new operation * -- inner join, which is dual to the outer union. In set notation

R * S ≝ {(y) | exist x (x,y) in R /\ exists z (y,z) in S }

while in the relational lattice terms

R * S ≝ (R v ( S ^ R00)) ^ ( S v ( R ^ R00)).

This was the last occurrence where set notation was used. From now on we switch to lower letters relation names and write x and y instead of R and S.

The following theorem, which claims absorption property for outer union and inner join, proved to be critical for further development

x + (x * y) = x.

Like in our previous work [2] we extract assertions and goal from Prover9 generated proof, so that reader can reproduce it at will. Please refer to Appendix A for the details.

These results establish that inner join and outer union operations form another lattice structure. The next natural question is what are the top and bottom elements in the newly defined lattice? Here are two more theorems

x * R00 = R00.
x * R11 = x.

(Appendix B). Then, of course

x + R00 = x.
x + R11 = R11.

In other words, the R00 and R11 elements in the inner join/natural union lattice play the roles of the R01 and R10 and vice versa. These new results force the reevaluation of the entire relational lattice axiom system.

Here is the new axiom system:

x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.
x v y = y v x.
(x v y) v z = x v (y v z).
x v (x ^ y) = x.

x + x = x. %added because (x * y) * z = x * (y * z) is invalid x * y = y * x.
x * (x + y) = x.

x + x = x. %since x + (x * y) = x is invalid x + y = y + x.
(x + y) + z = x + (y + z).

 x ^ R10 = R10.
 x v R01 = R01.
 x * R00 = R00.
 x + R11 = R11.

%theorem: x = (x ^ R00) v (x ^ R11). %FDI
%theorem: x = (x + R01) * (x + R10).

x * y = (x v (y ^ R00)) ^ (y v (x ^ R00)).
%x + y = (x ^ (y v R11)) v (y ^ (x v R11)). %theorem:
%x * y = (x ^ y) v ((x v y) ^ R00). %theorem:

x ^ y = (x + (y * R10)) * (y + (x * R10)).
%x v y = (x * (y + R01)) + (y * (x + R01)). %theorem:

x ^ (y + z) = (x ^ y) + (x ^ z).
x + (y ^ z) = (x + y) ^ (x + z).
%invalid x * (y v z) = (x * y) v (x * z).
%invalid x v (y * z) = (x v y) * (x v z).

3. COMPLEMENT Complement is a unary operation which we denote with symbol ' in order to stay within Prover9 syntax. Here are the defining axioms:

x' ^ x = x ^ R00.
x' v x = x v R11.

Two theorems, which again can be automatically deducted in Prover9:

(x')' = x.
x' + y' = (x ^ y)'.

1.SPIGHT, M., TROPASHKO, V. 2006. First Steps in Relational Lattice.
2.SPIGHT, M., TROPASHKO, V. 2008. Relational Lattice Axioms.
3.DATE, C.J., DARWEN, H. 2000. Foundation for Future Database Systems: The Third Manifesto. Addison-Wesley. (The algebra A description is located in the appendix A, which is available online at 4.MCCUNE, W. Prover9 and Mace4. 5.GINSBERG, M. 1990. Bilattices and Modal Operators. Theoretical Aspects of Reasoning about Knowledge: Proceedings of the Third Conference. Received on Tue Jul 29 2008 - 23:24:57 CEST

Original text of this message