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
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
1 2 3 4 5 | 6
5 is reachable from
1 via the chain
2 are in the same equivalence class of the first partition set, then,
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
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.
x->y between the two arbitrary relations
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
Our critical observation is that the partition lattice and relational lattice are connected via semi-lattice homomorphism. Specifically:
r#(x ^ y) = (r#x) ^ (r#y).
is meet homomorphism (^H). The dual assertion
r#(x v y) = (r#x) v (r#y).
which would have elevated it to full lattice homomorphism, is not valid.
These meet homomorphism allows to prove Armstrong axioms:
x < y -> r#x < r#y.
r#x < r#y -> r#(x^z) < r#(y^z).
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 ^ y = x.
We need to prove partition inequality which, likewise, can be rewritten as equality in lattice terms:
r#x ^ r#y = r#x.
This is accomplished in just two steps:
r#x ^ r#y = (^H) r#(x ^ y) = (given) r#x
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) ;