Lossless decomposition and normal forms

23 fully proved

Heath's theorem

TheoremHeath's theorem#✓fully proved

If the dependency R₁ ∩ R₂ → R₁ holds in a relation r over R₁ ∪ R₂, then r is the natural join of its projections onto R₁ and R₂.

theorem join_project_eq_of_holdsIn {R₁ R₂ : Finset A} {r : Finset (Tuple A D)}
    (hr : IsOver (R₁ ∪ R₂) r) (h : FD.HoldsIn ⟨R₁ ∩ R₂, R₁⟩ (↑r : Set (Tuple A D))) :
    join (project R₁ r) (project R₂ r) = r

Uses 9 · Used by 2

Statement usesFunctional dependency · A functional dependency holds in a relation · Relation over a schema · Tuple · Natural join · Projection of a relation

Proof usesTuple over a schema · Restriction of a tuple · Membership in a join

Used byThe BCNF decomposition is lossless · Lossless binary decompositions from derivable dependencies

DefinitionSatisfying a set of dependencies on a scheme#✓fully proved

A relation \(r\) satisfies a finite set \(F\) of functional dependencies on a set \(S\) of attributes when every dependency \(X \to Y\) with \(X, Y \subseteq S\) that is derivable from \(F\) by Armstrong's axioms holds in \(r\).

def SatisfiesOn (F : Finset (FD A)) (S : Finset A) (r : Finset (Tuple A D)) : Prop :=
  ∀ X ⊆ S, ∀ Y ⊆ S, Derives F ⟨X, Y⟩ → FD.HoldsIn ⟨X, Y⟩ (↑r : Set (Tuple A D))

Uses 4 · Used by 4

Statement usesDerivability with Armstrong's axioms · Functional dependency · A functional dependency holds in a relation · Tuple

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Lossless decomposition into two schemes · Lossless binary decompositions from derivable dependencies

DefinitionLossless decomposition into two schemes#✓fully proved

Let \(F\) be a finite set of functional dependencies, let \(R_1\) and \(R_2\) be finite sets of attributes, and let \(D\) be a type of values. The decomposition of \(R_1 \cup R_2\) into \(R_1\) and \(R_2\) is lossless for \(F\) with values in \(D\) when every relation \(r\) over \(R_1 \cup R_2\) with values in \(D\) that satisfies \(F\) on \(R_1 \cup R_2\) (every dependency \(X \to Y\) with \(X, Y \subseteq R_1 \cup R_2\) that is derivable from \(F\) by Armstrong's axioms holds in \(r\)) is the natural join of its projections: \(\pi_{R_1}(r) \bowtie \pi_{R_2}(r) = r\).

def LosslessJoin (F : Finset (FD A)) (R₁ R₂ : Finset A) : Prop :=
  ∀ r : Finset (Tuple A D), IsOver (R₁ ∪ R₂) r → SatisfiesOn F (R₁ ∪ R₂) r →
    join (project R₁ r) (project R₂ r) = r

Uses 6 · Used by 3

Statement usesFunctional dependency · Relation over a schema · Satisfying a set of dependencies on a scheme · Tuple · Natural join · Projection of a relation

Used byConverse of the lossless-join test for two schemes · Lossless binary decompositions · Lossless binary decompositions from derivable dependencies

TheoremLossless binary decompositions from derivable dependencies#✓fully proved

Let \(F\) be a finite set of functional dependencies and let \(R_1\), \(R_2\) be sets of attributes. If \(R_1 \cap R_2 \to R_1\) or \(R_1 \cap R_2 \to R_2\) is derivable from \(F\) by Armstrong's axioms, then for every value type \(D\) the decomposition of \(R_1 \cup R_2\) into \(R_1\) and \(R_2\) is lossless for \(F\) with values in \(D\).

theorem losslessJoin_of_derives {F : Finset (FD A)} {R₁ R₂ : Finset A}
    (h : Derives F ⟨R₁ ∩ R₂, R₁⟩ ∨ Derives F ⟨R₁ ∩ R₂, R₂⟩) : LosslessJoin D F R₁ R₂

Uses 11 · Used by 1

Statement usesDerivability with Armstrong's axioms · Functional dependency · Lossless decomposition into two schemes

Proof usesA functional dependency holds in a relation · Relation over a schema · Satisfying a set of dependencies on a scheme · Tuple · Natural join · Commutativity of the natural join · Heath's theorem · Projection of a relation

Used byLossless binary decompositions

TheoremConverse of the lossless-join test for two schemes#✓fully proved

Let \(F\) be a set of functional dependencies, let \(R_1\) and \(R_2\) be schemes whose union is the set of all attributes, and let \(D\) be a value type containing at least two distinct elements. If the decomposition of \(R_1 \cup R_2\) into \(R_1\) and \(R_2\) is lossless for \(F\) with values in \(D\), then \(F\) derives \(R_1 \cap R_2 \to R_1\) or \(R_1 \cap R_2 \to R_2\).

theorem derives_of_losslessJoin {F : Finset (FD A)} {R₁ R₂ : Finset A} {d₀ d₁ : D}
    (hd : d₀ ≠ d₁) (hR : R₁ ∪ R₂ = Finset.univ) (h : LosslessJoin D F R₁ R₂) :
    Derives F ⟨R₁ ∩ R₂, R₁⟩ ∨ Derives F ⟨R₁ ∩ R₂, R₂⟩

Uses 18 · Used by 1

Statement usesDerivability with Armstrong's axioms · Functional dependency · Lossless decomposition into two schemes

Proof usesArmstrong's axioms are sound · Relation over a schema · A relation satisfies a set of dependencies · Satisfying a set of dependencies on a scheme · Tuple · Tuple over a schema · Restriction of a tuple · Attribute closure · Iterated closure rounds · One round of the attribute-closure algorithm · The closure algorithm decides derivability · Natural join · Membership in a join · Projection of a relation · The attribute closure is closed under the dependencies

Used byLossless binary decompositions

TheoremLossless binary decompositions#✓fully proved

Let \(F\) be a finite set of functional dependencies, let \(R_1\) and \(R_2\) be sets of attributes whose union is the set of all attributes, and suppose that the value type \(D\) has two distinct elements. Then the decomposition into \(R_1\) and \(R_2\) is lossless for \(F\) with values in \(D\) if and only if \(R_1 \cap R_2 \to R_1\) or \(R_1 \cap R_2 \to R_2\) is derivable from \(F\) by Armstrong's axioms.

theorem losslessJoin_iff {F : Finset (FD A)} {R₁ R₂ : Finset A} {d₀ d₁ : D} (hd : d₀ ≠ d₁)
    (hR : R₁ ∪ R₂ = Finset.univ) :
    LosslessJoin D F R₁ R₂ ↔ Derives F ⟨R₁ ∩ R₂, R₁⟩ ∨ Derives F ⟨R₁ ∩ R₂, R₂⟩

Uses 5

Statement usesDerivability with Armstrong's axioms · Functional dependency · Lossless decomposition into two schemes

Proof usesConverse of the lossless-join test for two schemes · Lossless binary decompositions from derivable dependencies

Joins of projections

DefinitionUnit relation of the natural join#✓fully proved

The relation containing only the empty tuple, the unit of the natural join.

def joinUnit : Finset (Tuple A D) := {fun _ => none}

Uses 1 · Used by 3

Statement usesTuple

Used byThe BCNF decomposition is lossless · Join of the projections of a relation · Membership in a join of projections

DefinitionJoin of the projections of a relation#✓fully proved

For a relation \(r\) (a finite set of tuples) and a list of schemes \(S_1, \dots, S_n\), this is the natural join of the projections \(\pi_{S_1} r, \dots, \pi_{S_n} r\), computed as \(\pi_{S_1} r \bowtie (\pi_{S_2} r \bowtie (\cdots \bowtie (\pi_{S_n} r \bowtie U)))\), where \(U\) is the relation containing only the empty tuple; for the empty list it is \(U\).

def joinProjections (l : List (Finset A)) (r : Finset (Tuple A D)) : Finset (Tuple A D) :=
  l.foldr (fun S acc => join (project S r) acc) (joinUnit D)

Uses 4 · Used by 3

Statement usesTuple · Natural join · Unit relation of the natural join · Projection of a relation

Used byThe BCNF decomposition is lossless · Membership in a join of projections · Synthesis is lossless

DefinitionUnion of a list of schemes#✓fully proved

For a list \(S_1, \dots, S_n\) of schemes (finite sets of attributes), this is the union \(S_1 \cup \dots \cup S_n\); for the empty list it is the empty set.

def schemaUnion (l : List (Finset A)) : Finset A := l.foldr (· ∪ ·) ∅

Used by 2

Used byMembership in a join of projections · Synthesis is lossless

TheoremMembership in a join of projections#✓fully proved

Let \(r\) be a relation over a schema \(R\) and let \(S_1, \dots, S_n\) be a list of schemes, each contained in \(R\). A tuple \(t\) belongs to the natural join of the projections \(\pi_{S_1} r, \dots, \pi_{S_n} r\) if and only if \(t\) is a tuple over \(S_1 \cup \dots \cup S_n\) and, for every \(i\), the restriction of \(t\) to \(S_i\) belongs to \(\pi_{S_i} r\).

theorem mem_joinProjections {r : Finset (Tuple A D)} {R : Finset A} (hr : IsOver R r) :
    ∀ (l : List (Finset A)), (∀ S ∈ l, S ⊆ R) → ∀ {t : Tuple A D},
      t ∈ joinProjections l r ↔ t.IsOver (schemaUnion l) ∧ ∀ S ∈ l, t.restrict S ∈ project S r

Uses 12 · Used by 1

Statement usesRelation over a schema · Tuple · Tuple over a schema · Restriction of a tuple · Join of the projections of a relation · Projection of a relation · Union of a list of schemes

Proof usesCompatible tuples · Merge of two tuples · Natural join · Unit relation of the natural join · Membership in a join

Used bySynthesis is lossless

Boyce–Codd normal form

DefinitionBoyce–Codd normal form#✓fully proved

A scheme \(S\) is in Boyce–Codd normal form for a set \(F\) of functional dependencies when, for every dependency \(X \to Y\) derivable from \(F\) with \(X, Y \subseteq S\), either \(Y \subseteq X\) or \(F\) derives \(X \to S\) (that is, \(X\) is a superkey of \(S\)).

def IsBCNF (F : Finset (FD A)) (S : Finset A) : Prop :=
  ∀ X ⊆ S, ∀ Y ⊆ S, Derives F ⟨X, Y⟩ → Y ⊆ X ∨ Derives F ⟨X, S⟩

Uses 2 · Used by 1

Statement usesDerivability with Armstrong's axioms · Functional dependency

Used byThe BCNF decomposition produces BCNF schemes

DefinitionBCNF violations#✓fully proved

Let \(F\) be a set of functional dependencies and \(S\) a scheme, and write \(X^+\) for the attribute closure of a set \(X\) of attributes under \(F\). A set \(X \subseteq S\) violates BCNF in \(S\) when \(S \not\subseteq X^+\) and \(X^+ \cap S \not\subseteq X\), that is, when the closure \(X^+ \cap S\) of \(X\) within \(S\) is neither \(X\) nor \(S\).

def IsBCNFViolation (F : Finset (FD A)) (S X : Finset A) : Prop :=
  X ⊆ S ∧ ¬ S ⊆ attrClosure F X ∧ ¬ attrClosure F X ∩ S ⊆ X

Uses 2 · Used by 3

Statement usesFunctional dependency · Attribute closure

Used byBCNF decomposition with bounded depth · The BCNF decomposition is lossless · The BCNF decomposition produces BCNF schemes

DefinitionCandidate BCNF violations#✓fully proved

Given a list \(l\) of attributes and a set \(S\) of attributes, the candidate violations of BCNF in \(S\) are all subsets of the set of attributes that occur in \(l\) and lie in \(S\), listed once each. Duplicates in \(l\) are removed first, so there are \(2^k\) candidates when \(k\) distinct attributes of \(l\) lie in \(S\).

def bcnfCandidates (l : List A) (S : Finset A) : List (Finset A) :=
  ((l.filter (· ∈ S)).dedup.sublists).map List.toFinset

Used by 3

Used byBCNF decomposition with bounded depth · The BCNF decomposition is lossless · The BCNF decomposition produces BCNF schemes

DefinitionBCNF decomposition with bounded depth#✓fully proved

Let \(F\) be a set of functional dependencies, \(l\) a list of attributes, \(n\) a natural number and \(S\) a scheme. For \(n = 0\) the result is the list \([S]\). For \(n > 0\), the candidate violations of BCNF in \(S\) built from \(l\) are searched in order for the first \(X\) that violates BCNF in \(S\) for \(F\). If there is none, the result is \([S]\). Otherwise, with \(X^+\) the attribute closure of \(X\) under \(F\), the result is the decomposition of \(X^+ \cap S\) followed by the decomposition of \(S \setminus (X^+ \setminus X)\), both computed with depth bound \(n - 1\).

def bcnfDecompose (F : Finset (FD A)) (l : List A) : ℕ → Finset A → List (Finset A)
  | 0, S => [S]
  | n + 1, S =>
    match (bcnfCandidates l S).find? (fun X => decide (IsBCNFViolation F S X)) with
    | none => [S]
    | some X => bcnfDecompose F l n (attrClosure F X ∩ S) ++
        bcnfDecompose F l n (S \ (attrClosure F X \ X))

Uses 4 · Used by 3

Statement usesFunctional dependency · BCNF violations · Attribute closure · Candidate BCNF violations

Used byBCNF decomposition · The BCNF decomposition is lossless · The BCNF decomposition produces BCNF schemes

DefinitionBCNF decomposition#✓fully proved

Let \(F\) be a set of functional dependencies, \(l\) a list of attributes and \(S\) a scheme. The BCNF decomposition of \(S\) for \(F\) and \(l\) is the BCNF decomposition with bounded depth run on \(S\) with depth bound \(|S|\). At each step, if some candidate violation of BCNF in the current scheme \(T\) built from \(l\) violates BCNF in \(T\) for \(F\), the first such \(X\) is used: with \(X^+\) the attribute closure of \(X\) under \(F\), \(T\) is replaced by the decomposition of \(X^+ \cap T\) followed by the decomposition of \(T \setminus (X^+ \setminus X)\). Otherwise, or once the depth bound is reached, \(T\) is kept as it is.

def bcnfDecomposition (F : Finset (FD A)) (l : List A) (S : Finset A) : List (Finset A) :=
  bcnfDecompose F l S.card S

Uses 2 · Used by 2

Statement usesFunctional dependency · BCNF decomposition with bounded depth

Used byThe BCNF decomposition is lossless · The BCNF decomposition produces BCNF schemes

TheoremThe BCNF decomposition is lossless#✓fully proved

Let \(F\) be a set of functional dependencies, \(l\) a list of attributes and \(S\) a set of attributes, and let \(r\) be a relation over \(S\) that satisfies every dependency \(X \to Y\) derivable from \(F\) with \(X, Y \subseteq S\). Then \(r\) is the natural join of its projections onto the schemes of the BCNF decomposition of \(S\) for \(F\) and \(l\).

theorem bcnfDecomposition_lossless (F : Finset (FD A)) (l : List A) {S : Finset A}
    {r : Finset (Tuple A D)} (hr : IsOver S r) (hF : SatisfiesOn F S r) :
    joinProjections (bcnfDecomposition F l S) r = r

Uses 27

Statement usesFunctional dependency · Relation over a schema · Satisfying a set of dependencies on a scheme · Tuple · BCNF decomposition · Join of the projections of a relation

Proof usesDerivability with Armstrong's axioms · Decomposition rule · Union rule · A functional dependency holds in a relation · BCNF violations · Compatible tuples · Tuple over a schema · Merge of two tuples · Restriction of a tuple · Attribute closure · Candidate BCNF violations · BCNF decomposition with bounded depth · Iterated closure rounds · One round of the attribute-closure algorithm · Natural join · Unit relation of the natural join · Associativity of the natural join · Commutativity of the natural join · Heath's theorem · Projection of a relation · Cascade of projections onto a subset

TheoremThe BCNF decomposition produces BCNF schemes#✓fully proved

Let \(F\) be a set of functional dependencies and \(l\) a list containing every attribute. Then for every scheme \(S\), every scheme in the BCNF decomposition of \(S\) for \(F\) and \(l\) is in Boyce–Codd normal form for \(F\).

theorem isBCNF_of_mem_bcnfDecomposition (F : Finset (FD A)) {l : List A} (hl : ∀ a, a ∈ l)
    {S T : Finset A} (hT : T ∈ bcnfDecomposition F l S) : IsBCNF F T

Uses 13

Statement usesFunctional dependency · Boyce–Codd normal form · BCNF decomposition

Proof usesDerivability with Armstrong's axioms · Decomposition rule · Union rule · BCNF violations · Attribute closure · Candidate BCNF violations · BCNF decomposition with bounded depth · Iterated closure rounds · One round of the attribute-closure algorithm · The closure algorithm decides derivability

Synthesis

DefinitionEquivalent sets of functional dependencies#✓fully proved

Two sets \(F\) and \(G\) of functional dependencies are equivalent when \(F\) derives every dependency of \(G\) and \(G\) derives every dependency of \(F\).

def Equivalent (F G : Finset (FD A)) : Prop := (∀ g ∈ G, Derives F g) ∧ ∀ f ∈ F, Derives G f

Uses 2 · Used by 2

Statement usesDerivability with Armstrong's axioms · Functional dependency

Used bySynthesis is dependency-preserving · Synthesis is lossless

DefinitionProjection of the dependency closure onto a scheme#✓fully proved

For a finite set \(F\) of functional dependencies and a set \(S\) of attributes, this is the finite set of all dependencies \(X \to Y\) with \(X, Y \subseteq S\) that are derivable from \(F\) by Armstrong's axioms, that is, the projection onto \(S\) of the closure \(F^+\) of \(F\).

def projectFDs (F : Finset (FD A)) (S : Finset A) : Finset (FD A) :=
  ((S.powerset ×ˢ S.powerset).filter fun p => Derives F ⟨p.1, p.2⟩).image fun p => ⟨p.1, p.2⟩

Uses 4 · Used by 2

Statement usesDerivability with Armstrong's axioms · Functional dependency · Attribute closure · The closure algorithm decides derivability

Used byDependency-preserving decompositions · Synthesis is dependency-preserving

DefinitionDependency-preserving decompositions#✓fully proved

A list \(l\) of schemes is dependency-preserving for a set \(F\) of functional dependencies when every dependency of \(F\) is derivable from the union, over the schemes \(S\) of \(l\), of the sets of dependencies \(X \to Y\) derivable from \(F\) with \(X, Y \subseteq S\).

def DependencyPreserving (F : Finset (FD A)) (l : List (Finset A)) : Prop :=
  ∀ f ∈ F, Derives ((l.map (projectFDs F)).foldr (· ∪ ·) ∅) f

Uses 3 · Used by 1

Statement usesDerivability with Armstrong's axioms · Functional dependency · Projection of the dependency closure onto a scheme

Used bySynthesis is dependency-preserving

DefinitionSynthesis#✓fully proved

Given a list \(G\) of functional dependencies and a set of attributes \(K\), the synthesized decomposition is the list of schemes consisting of \(K\) followed by, for each dependency \(X \to Y\) of \(G\) in order, the scheme \(X \cup Y\).

def synthesize (G : List (FD A)) (K : Finset A) : List (Finset A) :=
  K :: G.map fun g => g.lhs ∪ g.rhs

Uses 1 · Used by 2

Statement usesFunctional dependency

Used bySynthesis is dependency-preserving · Synthesis is lossless

TheoremSynthesis is dependency-preserving#✓fully proved

Let \(F\) be a finite set of functional dependencies and \(G\) a list of functional dependencies equivalent to \(F\) (each derives every dependency of the other). Then for every set of attributes \(K\), the decomposition synthesized from \(G\) and \(K\), with one scheme \(X \cup Y\) for each dependency \(X \to Y\) of \(G\) together with the scheme \(K\), is dependency-preserving for \(F\).

theorem synthesize_dependencyPreserving {F : Finset (FD A)} {G : List (FD A)}
    (hG : Equivalent F G.toFinset) (K : Finset A) : DependencyPreserving F (synthesize G K)

Uses 8

Statement usesDependency-preserving decompositions · Equivalent sets of functional dependencies · Functional dependency · Synthesis

Proof usesDerivability with Armstrong's axioms · Attribute closure · The closure algorithm decides derivability · Projection of the dependency closure onto a scheme

TheoremSynthesis is lossless#✓fully proved

For a cover G of F and a superkey K of all attributes, every relation over all attributes satisfying F is the join of its projections onto the synthesized schemes.

theorem synthesize_lossless {F : Finset (FD A)} {G : List (FD A)} (hG : Equivalent F G.toFinset)
    {K : Finset A} (hK : IsSuperkey F K) {r : Finset (Tuple A D)} (hr : IsOver Finset.univ r)
    (hF : Satisfies (↑r : Set (Tuple A D)) F) :
    joinProjections (synthesize G K) r = r

Uses 22

Statement usesEquivalent sets of functional dependencies · Functional dependency · Relation over a schema · Superkey · A relation satisfies a set of dependencies · Tuple · Join of the projections of a relation · Synthesis

Proof usesDerivability with Armstrong's axioms · Decomposition rule · Armstrong's axioms are sound · Union rule · A functional dependency holds in a relation · Tuple over a schema · Restriction of a tuple · Attribute closure · Iterated closure rounds · One round of the attribute-closure algorithm · The closure algorithm decides derivability · Membership in a join of projections · Projection of a relation · Union of a list of schemes

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.