complement in relational bi-lattice
vadi...@gmail.com
http://arxiv.org/pdf/0807.3795
and old thread
http://groups.google.com/group/comp.databases.theory/browse_frm/thread/14f53564b7d121b5/85b9566325550e36?hl=en&lnk=st&q=#85b9566325550e36
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)'.
REFERENCES
1.SPIGHT, M., TROPASHKO, V. 2006. First Steps in Relational Lattice.
http://arxiv.org/pdf/cs.DB/0603044
2.SPIGHT, M., TROPASHKO, V. 2008. Relational Lattice Axioms.
http://arxiv.org/pdf/0807.3795
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
http://www.dcs.warwick.ac.uk/~hugh/TTM/APPXA.pdf)
4.MCCUNE, W. Prover9 and Mace4. http://www.cs.unm.edu/~mccune/mace4/
5.GINSBERG, M. 1990. Bilattices and Modal Operators. Theoretical
Aspects of Reasoning about Knowledge: Proceedings of the Third
Conference. http://citeseer.ist.psu.edu/47148.html