A relation that distinguishes one tuple, from the other is binary. It is an equivalence relation. Equivalence relation (in general) correspond to a sets of equivalence classes or, in other words, partitions of a set. There is more than one equivalence relation that can be defined upon a single relation X: one can consider equivalence classes of tuples projected to a single attribute (or set of attributes). This construction is proved to be useful for formalization of functional dependency.
We start with a well known fact that partitions form a lattice. Lattice meet operation is partition intersection. In example of partitions of the set {1,2,3}:
1 | 2 3
^
1 2 | 3
=
1 | 2 | 3
Lattice join definition is a little more involved, so that partitions are the equivalence classes of element reachable via transitive closure. In example of partitions of the set {1,2,3,4,5,6}:
1 2 | 3 4 | 5 | 6
v
1 | 2 3 | 4 5 | 6
=
1 2 3 4 5 | 6
Here 5 is reachable from 1 via the chain 1->2->3->4->5: both 1 and 2 are in the same equivalence class of the first partition set, then, 2 and 3 are in the same equivalence class of the second partition set, and so on.
How partitions can be applied to dependency theory? Consider the following relation
X=[p q r] 0 a 0 0 a 1 1 c 0 1 c 1 2 a 0 ;
This relation is written in QBQL notation.
Relation partitioning is a binary operation x#y between the two relations x and y. It partitions tuples from the left hand side relation x based on the values of attributes from the right hand side relation y. Therefore the result doesn’t depend on the content of y, which may assumed to be empty. In the above example we have
X#R00 = <0,a,0> <0,a,1> <1,c,0> <1,c,1> <2,a,0>;
X#[p] = <0,a,0> <0,a,1> | <1,c,0> <1,c,1> | <2,a,0>;
X#[q] = <0,a,0> <0,a,1> <2,a,0> | <1,c,0> <1,c,1>;
X#[r] = <0,a,0> <1,c,0> <2,a,0> | <0,a,1> <1,c,1>;
X#[p q]= <0,a,0> <0,a,1> | <1,c,0> <1,c,1> | <2,a,0>;
X#[q r]= <0,a,0> <2,a,0> | <0,a,1> | <1,c,0> | <1,c,1>;
X#[r p]= <0,a,0> | <0,a,1> | <1,c,0> | <1,c,1> | <2,a,0>;
X#R10 = <0,a,0> | <0,a,1> | <1,c,0> | <1,c,1> | <2,a,0>;
which is the actual output of the QBQL program:
X=[p q r] 0 a 0 0 a 1 1 c 0 1 c 1 2 a 0 ; X#R00; X#[p]; X#[q]; X#[r]; X#[p q]; X#[q r]; X#[r p]; X#R10;
Here is the partitions lattice diagram:
Lattice, in general, defines order relation via the following equivalences
x < y <-> x v y = y.
x < y <-> x ^ y = x.
Informally, the element y is greater than x when it is reachable from node x and positioned higher in lattice diagram. The higher in the lattice order we ascend, the coarser partition granularity becomes.
Functional dependency x->y between the two arbitrary relations x and y respective to the host relation r is defined as a constraint:
r#x < r#y.
Informally, the partitioning of the relation r defined by tuple values projected into the set of attributes of the relation x has finer granularity than its partitioning induced by the attributes of y.
Our critical observation is that the partition lattice and relational lattice are connected via lattice homomorphism. Specifically:
r#(x ^ y) = (r#x) ^ (r#y).
is meet homomorphism (^H), and
r#(x v y) = (r#x) v (r#y).
is join homomorphism (vH).
These two properties allow to prove Armstrong axioms:
- Reflexivity:
x < y -> r#x < r#y. - Augmentation:
r#x < r#y -> r#(x^z) < r#(y^z). - Transitivity:
r#x < r#y & r#y < r#z -> r#x < r#z.
Reflexivity proof starts with rewriting the inequality condition of the implication in terms of lattice meet, join and equality:
x v y = y.
We need to prove partition inequality which, likewise, can be rewritten as equality in lattice terms:
r#x v r#y = r#y.
This is accomplished in just two steps:
r#x v r#y = (vH) r#(x v y) = (given) r#y
Augmentation proof follows the similar venue. Transitivity is the easiest of all: it is transitivity of partition lattice order.
Formal Concept Analysis
Another way to formalize functional dependencies is converting database relation into a boolean matrix. The matrix columns retain their attribute structure, while rows correspond to differences between the tuples. In our running example, the relation
X=[p q r] 0 a 0 -- t1 0 a 1 -- t2 1 c 0 -- t3 1 c 1 -- t4 2 a 0 -- t5 ;
is converted into
X=[p q r] = = != --(t1,t2) != != = --(t1,t3) != != != --(t1,t4) != = = --(t1,t5) != != != --(t2,t3) != != = --(t2,t4) != = != --(t2,t5) = = != --(t3,t4) != != = --(t3,t5) != != != --(t4,t5) ;
Here the first row <=,=,!=> is the difference between <0,a,0> and <0,a,1>. We can eliminate duplicate rows in the matrix, or just feed it into Concept Explorer program as it is:
and then, generate FCA lattice
The lattice is isomorphic to lattice of partitions, which leads to conclusion that partitions are formal concepts.
