Skip to content

Functional dependencies

StructureFunctional dependency#✓fully proved

A functional dependency \(X \to Y\) over a type \(A\) of attributes consists of two finite sets of attributes \(X, Y \subseteq A\): the determining attributes \(X\) (its left side) and the determined attributes \(Y\) (its right side).

structure FD (A : Type*) where
  /-- The determining attributes. -/
  lhs : Finset A
  /-- The determined attributes. -/
  rhs : Finset A
deriving DecidableEq
Used by 47
Used byAttribute closure · Iterated closure rounds · One round of the attribute-closure algorithm · The attribute closure is a fixed point of a closure round · Closure witness relation · Decomposition rule · Derivability with Armstrong's axioms · Armstrong's theorem · The closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form · Entailment of functional dependencies · Tuples that agree on a superkey are equal · Every superkey contains a candidate key · Key-finding algorithm · The key-finding algorithm returns a candidate key · A functional dependency holds in a relation · The closure witness satisfies the dependencies · Candidate key · Candidate keys are the superkeys minimal under single removals · Superkey · The closure algorithm computes the attribute closure · Supersets of superkeys are superkeys · Pseudotransitivity rule · The attribute closure is closed under the dependencies · A relation satisfies a set of dependencies · Shrinking a key along a list · Armstrong's axioms are sound · Union rule · Adding the left side to the right side · BCNF decomposition with bounded depth · BCNF decomposition · The BCNF decomposition is lossless · Dependency-preserving decompositions · Converse of the lossless-join test for two schemes · Equivalent sets of functional dependencies · Boyce–Codd normal form · The BCNF decomposition produces BCNF schemes · BCNF violations · Heath's theorem · Lossless decomposition into two schemes · Lossless binary decompositions · Lossless binary decompositions from derivable dependencies · Projection of the dependency closure onto a scheme · Satisfying a set of dependencies on a scheme · Synthesis · Synthesis is dependency-preserving · Synthesis is lossless

DefinitionA functional dependency holds in a relation#✓fully proved

Let \(A\) be a type of attributes and \(V\) a type of values. A functional dependency \(X \to Y\) on \(A\) holds in a relation \(r\), a set of tuples \(A \to V\), when any two tuples \(t, u \in r\) that agree on every attribute of \(X\) also agree on every attribute of \(Y\).

def HoldsIn {V : Type*} (f : FD A) (r : Set (A → V)) : Prop :=
  ∀ t ∈ r, ∀ u ∈ r, (∀ a ∈ f.lhs, t a = u a) → ∀ a ∈ f.rhs, t a = u a
Uses 1 · Used by 9
Statement usesFunctional dependency
Used byCompleteness of Armstrong's axioms, two-tuple form · Entailment of functional dependencies · A relation satisfies a set of dependencies · Armstrong's axioms are sound · The BCNF decomposition is lossless · Heath's theorem · Lossless binary decompositions from derivable dependencies · Satisfying a set of dependencies on a scheme · Synthesis is lossless

DefinitionA relation satisfies a set of dependencies#✓fully proved

Let \(F\) be a finite set of functional dependencies over attributes \(A\), and let \(r\) be a relation, given as a set of tuples \(A \to V\) with values in a type \(V\). Then \(r\) satisfies \(F\) when every dependency of \(F\) holds in \(r\).

def Satisfies {V : Type*} (r : Set (A → V)) (F : Finset (FD A)) : Prop := ∀ f ∈ F, f.HoldsIn r
Uses 2 · Used by 8
Statement usesFunctional dependency · A functional dependency holds in a relation
Used byArmstrong's theorem · Completeness of Armstrong's axioms, two-tuple form · Entailment of functional dependencies · Tuples that agree on a superkey are equal · The closure witness satisfies the dependencies · Armstrong's axioms are sound · Converse of the lossless-join test for two schemes · Synthesis is lossless

DefinitionEntailment of functional dependencies#✓fully proved

Let \(A\) be a type of attributes. A finite set \(F\) of functional dependencies on \(A\) entails a functional dependency \(f\) on \(A\) when, for every type \(V\) and every relation \(r\) with values in \(V\) (a set of tuples \(A \to V\)) that satisfies \(F\), the dependency \(f\) holds in \(r\).

def Entails (F : Finset (FD A)) (f : FD A) : Prop :=
  ∀ (V : Type) (r : Set (A → V)), Satisfies r F → f.HoldsIn r
Uses 3 · Used by 1
Statement usesFunctional dependency · A functional dependency holds in a relation · A relation satisfies a set of dependencies
Used byArmstrong's theorem

InductiveDerivability with Armstrong's axioms#✓fully proved

Let \(F\) be a finite set of functional dependencies over a set \(A\) of attributes. Derivability from \(F\) is the least property of functional dependencies over \(A\) such that, for all finite sets \(X\), \(Y\), \(Z\) of attributes: every dependency of \(F\) is derivable; \(X \to Y\) is derivable whenever \(Y \subseteq X\) (reflexivity); if \(X \to Y\) is derivable, then so is \(X \cup Z \to Y \cup Z\) (augmentation); and if \(X \to Y\) and \(Y \to Z\) are derivable, then so is \(X \to Z\) (transitivity).

inductive Derives (F : Finset (FD A)) : FD A → Prop
  /-- The dependencies of `F` are derivable. -/
  | mem {f : FD A} : f ∈ F → Derives F f
  /-- Reflexivity: `X → Y` whenever `Y ⊆ X`. -/
  | refl {X Y : Finset A} : Y ⊆ X → Derives F ⟨X, Y⟩
  /-- Augmentation: from `X → Y` derive `X ∪ Z → Y ∪ Z`. -/
  | augment {X Y : Finset A} (Z : Finset A) : Derives F ⟨X, Y⟩ → Derives F ⟨X ∪ Z, Y ∪ Z⟩
  /-- Transitivity: from `X → Y` and `Y → Z` derive `X → Z`. -/
  | trans {X Y Z : Finset A} : Derives F ⟨X, Y⟩ → Derives F ⟨Y, Z⟩ → Derives F ⟨X, Z⟩
Uses 1 · Used by 25
Statement usesFunctional dependency
Used byDecomposition rule · Armstrong's theorem · The closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form · Every superkey contains a candidate key · The key-finding algorithm returns a candidate key · Superkey · The closure algorithm computes the attribute closure · Supersets of superkeys are superkeys · Pseudotransitivity rule · Armstrong's axioms are sound · Union rule · Adding the left side to the right side · The BCNF decomposition is lossless · Dependency-preserving decompositions · Converse of the lossless-join test for two schemes · Equivalent sets of functional dependencies · Boyce–Codd normal form · The BCNF decomposition produces BCNF schemes · Lossless binary decompositions · Lossless binary decompositions from derivable dependencies · Projection of the dependency closure onto a scheme · Satisfying a set of dependencies on a scheme · Synthesis is dependency-preserving · Synthesis is lossless

TheoremArmstrong's axioms are sound#✓fully proved

A derivable dependency holds in every relation satisfying F.

theorem sound {V : Type*} {r : Set (A → V)} (hr : Satisfies r F) :
    ∀ {f : FD A}, Derives F f → f.HoldsIn r
Uses 4 · Used by 5
Statement usesDerivability with Armstrong's axioms · Functional dependency · A functional dependency holds in a relation · A relation satisfies a set of dependencies
Used byArmstrong's theorem · The closure algorithm decides derivability · Tuples that agree on a superkey are equal · Converse of the lossless-join test for two schemes · Synthesis is lossless

TheoremDecomposition rule#✓fully proved

Let \(F\) be a finite set of functional dependencies and \(X\), \(Y\), \(Z\) finite sets of attributes with \(Z \subseteq Y\). If \(X \to Y\) is derivable from \(F\) with Armstrong's axioms, then so is \(X \to Z\).

theorem decompose {X Y Z : Finset A} (h : Derives F ⟨X, Y⟩) (hZ : Z ⊆ Y) : Derives F ⟨X, Z⟩
Uses 2 · Used by 4
Statement usesDerivability with Armstrong's axioms · Functional dependency
Used byThe closure algorithm decides derivability · The BCNF decomposition is lossless · The BCNF decomposition produces BCNF schemes · Synthesis is lossless

TheoremUnion rule#✓fully proved

Let \(F\) be a finite set of functional dependencies and \(X, Y, Z\) finite sets of attributes. If \(X \to Y\) and \(X \to Z\) are derivable from \(F\) with Armstrong's axioms, then so is \(X \to Y \cup Z\).

theorem union {X Y Z : Finset A} (hY : Derives F ⟨X, Y⟩) (hZ : Derives F ⟨X, Z⟩) :
    Derives F ⟨X, Y ∪ Z⟩
Uses 2 · Used by 5
Statement usesDerivability with Armstrong's axioms · Functional dependency
Used byThe closure algorithm decides derivability · Adding the left side to the right side · The BCNF decomposition is lossless · The BCNF decomposition produces BCNF schemes · Synthesis is lossless

TheoremPseudotransitivity rule#✓fully proved

Let \(F\) be a finite set of functional dependencies and \(X, Y, W, Z\) finite sets of attributes. If \(X \to Y\) and \(Y \cup W \to Z\) are derivable from \(F\) with Armstrong's axioms, then so is \(X \cup W \to Z\).

theorem pseudotrans {X Y W Z : Finset A} (h₁ : Derives F ⟨X, Y⟩) (h₂ : Derives F ⟨Y ∪ W, Z⟩) :
    Derives F ⟨X ∪ W, Z⟩
Uses 2
Statement usesDerivability with Armstrong's axioms · Functional dependency

TheoremAdding the left side to the right side#✓fully proved

Let \(F\) be a finite set of functional dependencies and \(X, Y\) finite sets of attributes. If \(X \to Y\) is derivable from \(F\) with Armstrong's axioms, then so is \(X \to X \cup Y\).

theorem union_left {X Y : Finset A} (h : Derives F ⟨X, Y⟩) : Derives F ⟨X, X ∪ Y⟩
Uses 3
Statement usesDerivability with Armstrong's axioms · Functional dependency
Proof usesUnion rule
30 fully proved

The attribute-closure algorithm

DefinitionOne round of the attribute-closure algorithm#✓fully proved

For a finite set \(F\) of functional dependencies and a finite set \(Y\) of attributes, one closure round returns \(Y\) together with the right side of every dependency of \(F\) whose left side is contained in \(Y\), that is, the set \(Y \cup \bigcup \{R : (L \to R) \in F,\ L \subseteq Y\}\).

def closureStep (F : Finset (FD A)) (Y : Finset A) : Finset A :=
  Y ∪ (F.filter fun f => f.lhs ⊆ Y).biUnion FD.rhs
Uses 1 · Used by 9
Statement usesFunctional dependency
Used byIterated closure rounds · The attribute closure is a fixed point of a closure round · The closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form · The attribute closure is closed under the dependencies · The BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · The BCNF decomposition produces BCNF schemes · Synthesis is lossless

DefinitionIterated closure rounds#✓fully proved

Let \(F\) be a finite set of functional dependencies, \(n\) a natural number and \(Y\) a finite set of attributes. The loop returns \(Y\) if \(n = 0\) or if one closure round for \(F\) leaves \(Y\) unchanged; otherwise it returns the loop with \(n - 1\) rounds started from the result of one closure round applied to \(Y\). Thus it repeats closure rounds from \(Y\) until nothing changes, for at most \(n\) rounds.

def closureLoop (F : Finset (FD A)) : ℕ → Finset A → Finset A
  | 0, Y => Y
  | n + 1, Y => if closureStep F Y = Y then Y else closureLoop F n (closureStep F Y)
Uses 2 · Used by 8
Statement usesFunctional dependency · One round of the attribute-closure algorithm
Used byAttribute closure · The attribute closure is a fixed point of a closure round · The closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form · The BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · The BCNF decomposition produces BCNF schemes · Synthesis is lossless

DefinitionAttribute closure#✓fully proved

Let \(A\) be a finite set of attributes, \(F\) a finite set of functional dependencies over \(A\) and \(X \subseteq A\). The attribute closure \(X^+\) of \(X\) under \(F\) is computed by the closure algorithm: starting from \(X\), repeat closure rounds (each adds the right side of every dependency of \(F\) whose left side is already included) until nothing changes, for at most \(|A|\) rounds.

def attrClosure (F : Finset (FD A)) (X : Finset A) : Finset A :=
  closureLoop F (Fintype.card A) X
Uses 2 · Used by 18
Statement usesFunctional dependency · Iterated closure rounds
Used byThe attribute closure is a fixed point of a closure round · Closure witness relation · The closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form · Every superkey contains a candidate key · The key-finding algorithm returns a candidate key · The closure witness satisfies the dependencies · The closure algorithm computes the attribute closure · The attribute closure is closed under the dependencies · Shrinking a key along a list · BCNF decomposition with bounded depth · The BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · The BCNF decomposition produces BCNF schemes · BCNF violations · Projection of the dependency closure onto a scheme · Synthesis is dependency-preserving · Synthesis is lossless

TheoremThe attribute closure is a fixed point of a closure round#✓fully proved

Let \(A\) be a finite set of attributes, \(F\) a finite set of functional dependencies over \(A\) and \(X \subseteq A\). Applying one closure round for \(F\) to the attribute closure \(X^+\) of \(X\) under \(F\) returns \(X^+\).

theorem closureStep_attrClosure (F : Finset (FD A)) (X : Finset A) :
    closureStep F (attrClosure F X) = attrClosure F X
Uses 4 · Used by 1
Statement usesFunctional dependency · Attribute closure · One round of the attribute-closure algorithm
Proof usesIterated closure rounds
Used byThe attribute closure is closed under the dependencies

TheoremThe attribute closure is closed under the dependencies#✓fully proved

Let \(F\) be a finite set of functional dependencies over a finite set of attributes, \(X\) a set of attributes and \(X^+\) its attribute closure under \(F\). For every dependency \(Y \to Z\) in \(F\) with \(Y \subseteq X^+\), also \(Z \subseteq X^+\).

theorem rhs_subset_attrClosure {F : Finset (FD A)} {X : Finset A} {g : FD A} (hg : g ∈ F)
    (hlhs : g.lhs ⊆ attrClosure F X) : g.rhs ⊆ attrClosure F X
Uses 4 · Used by 2
Statement usesFunctional dependency · Attribute closure
Proof usesOne round of the attribute-closure algorithm · The attribute closure is a fixed point of a closure round
Used byThe closure witness satisfies the dependencies · Converse of the lossless-join test for two schemes

DefinitionClosure witness relation#✓fully proved

Let \(A\) be a finite set of attributes, \(F\) a finite set of functional dependencies over \(A\) and \(X \subseteq A\). The closure witness relation for \(X\) is the relation with values in \(\{\mathrm{true}, \mathrm{false}\}\) whose tuples are the tuple that is \(\mathrm{true}\) on every attribute and the tuple that is \(\mathrm{true}\) exactly on the attribute closure \(X^+\) of \(X\) under \(F\). These two tuples agree exactly on \(X^+\), and they coincide when \(X^+ = A\).

def closureWitnessRelation (F : Finset (FD A)) (X : Finset A) : Finset (A → Bool) :=
  {fun _ => true, fun a => decide (a ∈ attrClosure F X)}
Uses 2 · Used by 3
Statement usesFunctional dependency · Attribute closure
Used byThe closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form · The closure witness satisfies the dependencies

TheoremThe closure witness satisfies the dependencies#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\). For every set \(X \subseteq A\) of attributes, the closure witness relation for \(X\) under \(F\) satisfies \(F\).

theorem holdsIn_closureWitnessRelation (F : Finset (FD A)) (X : Finset A) :
    Satisfies (↑(closureWitnessRelation F X) : Set (A → Bool)) F
Uses 5 · Used by 2
Statement usesFunctional dependency · A relation satisfies a set of dependencies · Closure witness relation
Proof usesAttribute closure · The attribute closure is closed under the dependencies
Used byThe closure algorithm decides derivability · Completeness of Armstrong's axioms, two-tuple form

TheoremThe closure algorithm decides derivability#✓fully proved

Let \(A\) be a finite set of attributes, \(F\) a finite set of functional dependencies over \(A\) and \(X, Y \subseteq A\). Then \(X \to Y\) is derivable from \(F\) with Armstrong's axioms if and only if \(Y \subseteq X^+\), where \(X^+\) is the attribute closure of \(X\) under \(F\) computed by the closure algorithm.

theorem derives_iff_subset_attrClosure {F : Finset (FD A)} {X Y : Finset A} :
    Derives F ⟨X, Y⟩ ↔ Y ⊆ attrClosure F X
Uses 10 · Used by 9
Statement usesDerivability with Armstrong's axioms · Functional dependency · Attribute closure
Proof usesDecomposition rule · Armstrong's axioms are sound · Union rule · Iterated closure rounds · One round of the attribute-closure algorithm · Closure witness relation · The closure witness satisfies the dependencies
Used byCompleteness of Armstrong's axioms, two-tuple form · Every superkey contains a candidate key · The key-finding algorithm returns a candidate key · The closure algorithm computes the attribute closure · Converse of the lossless-join test for two schemes · The BCNF decomposition produces BCNF schemes · Projection of the dependency closure onto a scheme · Synthesis is dependency-preserving · Synthesis is lossless

TheoremThe closure algorithm computes the attribute closure#✓fully proved

Let \(F\) be a finite set of functional dependencies over a finite set of attributes and \(X\) a set of attributes. An attribute \(a\) lies in the attribute closure \(X^+\) of \(X\) under \(F\), as computed by the closure algorithm, if and only if the dependency \(X \to \{a\}\) is derivable from \(F\) with Armstrong's axioms.

theorem mem_attrClosure {F : Finset (FD A)} {X : Finset A} {a : A} :
    a ∈ attrClosure F X ↔ Derives F ⟨X, {a}⟩
Uses 4
Statement usesDerivability with Armstrong's axioms · Functional dependency · Attribute closure
Proof usesThe closure algorithm decides derivability

TheoremCompleteness of Armstrong's axioms, two-tuple form#✓fully proved

Let \(A\) be a finite set of attributes, \(F\) a finite set of functional dependencies over \(A\) and \(f\) a functional dependency over \(A\). If \(f\) holds in every relation with values in \(\{\mathrm{true}, \mathrm{false}\}\) that has at most two tuples and satisfies every dependency of \(F\), then \(f\) is derivable from \(F\) with Armstrong's axioms.

theorem derives_of_forall_two_tuple [Finite A] {F : Finset (FD A)} {f : FD A}
    (h : ∀ r : Finset (A → Bool), r.card ≤ 2 → Satisfies (↑r : Set (A → Bool)) F →
      f.HoldsIn (↑r : Set (A → Bool))) : Derives F f
Uses 10 · Used by 1
Statement usesDerivability with Armstrong's axioms · Functional dependency · A functional dependency holds in a relation · A relation satisfies a set of dependencies
Proof usesAttribute closure · Iterated closure rounds · One round of the attribute-closure algorithm · Closure witness relation · The closure algorithm decides derivability · The closure witness satisfies the dependencies
Used byArmstrong's theorem

TheoremArmstrong's theorem#✓fully proved

Let \(A\) be a finite set of attributes, \(F\) a finite set of functional dependencies over \(A\) and \(f\) a functional dependency over \(A\). Then \(f\) is derivable from \(F\) with Armstrong's axioms if and only if \(F\) entails \(f\), that is, \(f\) holds in every relation (with values in any type) that satisfies every dependency of \(F\). In other words, Armstrong's axioms are sound and complete for functional dependencies.

theorem derives_iff_entails [Finite A] {F : Finset (FD A)} {f : FD A} :
    Derives F f ↔ Entails F f
Uses 6
Statement usesDerivability with Armstrong's axioms · Entailment of functional dependencies · Functional dependency
Proof usesArmstrong's axioms are sound · A relation satisfies a set of dependencies · Completeness of Armstrong's axioms, two-tuple form

Keys

DefinitionSuperkey#✓fully proved

Let \(F\) be a finite set of functional dependencies over a finite set of attributes \(A\). A set of attributes \(K\) is a superkey for \(F\) when the dependency \(K \to A\) is derivable from \(F\) with Armstrong's axioms, that is, \(K\) determines every attribute.

def IsSuperkey (F : Finset (FD A)) (K : Finset A) : Prop := Derives F ⟨K, Finset.univ⟩
Uses 2 · Used by 7
Statement usesDerivability with Armstrong's axioms · Functional dependency
Used byTuples that agree on a superkey are equal · Every superkey contains a candidate key · The key-finding algorithm returns a candidate key · Candidate key · Candidate keys are the superkeys minimal under single removals · Supersets of superkeys are superkeys · Synthesis is lossless

DefinitionCandidate key#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\). A set \(K \subseteq A\) of attributes is a candidate key for \(F\) when \(K\) is a superkey for \(F\) and no proper subset of \(K\) is a superkey for \(F\).

def IsCandidateKey (F : Finset (FD A)) (K : Finset A) : Prop :=
  IsSuperkey F K ∧ ∀ K' ⊂ K, ¬ IsSuperkey F K'
Uses 2 · Used by 3
Statement usesFunctional dependency · Superkey
Used byEvery superkey contains a candidate key · The key-finding algorithm returns a candidate key · Candidate keys are the superkeys minimal under single removals

TheoremSupersets of superkeys are superkeys#✓fully proved

Let \(F\) be a finite set of functional dependencies over a finite set of attributes. If \(K\) is a superkey for \(F\) and \(K \subseteq K'\), then \(K'\) is a superkey for \(F\).

theorem IsSuperkey.mono {F : Finset (FD A)} {K K' : Finset A} (h : IsSuperkey F K)
    (hKK' : K ⊆ K') : IsSuperkey F K'
Uses 3 · Used by 3
Statement usesFunctional dependency · Superkey
Proof usesDerivability with Armstrong's axioms
Used byEvery superkey contains a candidate key · The key-finding algorithm returns a candidate key · Candidate keys are the superkeys minimal under single removals

TheoremTuples that agree on a superkey are equal#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\), and let \(K\) be a superkey for \(F\). Let \(V\) be a type of values. If a relation \(r\), a set of tuples \(A \to V\), satisfies \(F\), then any two tuples \(t, u \in r\) that agree on every attribute of \(K\) are equal.

theorem IsSuperkey.eq_of_agree {V : Type*} {F : Finset (FD A)} {K : Finset A}
    (h : IsSuperkey F K) {r : Set (A → V)} (hr : Satisfies r F) {t u : A → V} (ht : t ∈ r)
    (hu : u ∈ r) (hagree : ∀ a ∈ K, t a = u a) : t = u
Uses 4
Statement usesFunctional dependency · Superkey · A relation satisfies a set of dependencies
Proof usesArmstrong's axioms are sound

TheoremCandidate keys are the superkeys minimal under single removals#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\). A set \(K \subseteq A\) of attributes is a candidate key for \(F\) if and only if \(K\) is a superkey for \(F\) and, for every \(a \in K\), the set \(K \setminus \{a\}\) is not a superkey for \(F\).

theorem isCandidateKey_iff {F : Finset (FD A)} {K : Finset A} :
    IsCandidateKey F K ↔ IsSuperkey F K ∧ ∀ a ∈ K, ¬ IsSuperkey F (K.erase a)
Uses 4 · Used by 2
Statement usesFunctional dependency · Candidate key · Superkey
Proof usesSupersets of superkeys are superkeys
Used byEvery superkey contains a candidate key · The key-finding algorithm returns a candidate key

DefinitionShrinking a key along a list#✓fully proved

Let \(F\) be a finite set of functional dependencies over a finite set of attributes. Given a list \(l\) of attributes and a set of attributes \(K\), go through \(l\) in order and, for each attribute \(a\), remove \(a\) from the current set whenever the attribute closure under \(F\) of the current set without \(a\) is the set of all attributes (that is, the set without \(a\) is still a superkey); the result is the set reached at the end of the list.

def shrinkKey (F : Finset (FD A)) : List A → Finset A → Finset A
  | [], K => K
  | a :: l, K =>
    shrinkKey F l (if attrClosure F (K.erase a) = Finset.univ then K.erase a else K)
Uses 2 · Used by 3
Statement usesFunctional dependency · Attribute closure
Used byEvery superkey contains a candidate key · Key-finding algorithm · The key-finding algorithm returns a candidate key

DefinitionKey-finding algorithm#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\), and let \(l\) be a list of attributes. The key-finding algorithm starts from the set \(K = A\) of all attributes and goes through \(l\) in order: for each listed attribute \(a\), it replaces \(K\) by \(K \setminus \{a\}\) when the attribute closure of \(K \setminus \{a\}\) under \(F\) is all of \(A\), and keeps \(K\) otherwise. It returns the final set \(K\).

def findKey (F : Finset (FD A)) (l : List A) : Finset A := shrinkKey F l Finset.univ
Uses 2 · Used by 1
Statement usesFunctional dependency · Shrinking a key along a list
Used byThe key-finding algorithm returns a candidate key

TheoremThe key-finding algorithm returns a candidate key#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\), and let \(l\) be a list in which every attribute of \(A\) occurs. Then the output of the key-finding algorithm on \(F\) and \(l\), which starts from the set of all attributes and goes through \(l\) in order, removing each listed attribute whenever what remains is still a superkey, is a candidate key for \(F\).

theorem findKey_isCandidateKey (F : Finset (FD A)) {l : List A} (hl : ∀ a, a ∈ l) :
    IsCandidateKey F (findKey F l)
Uses 10
Statement usesFunctional dependency · Candidate key · Key-finding algorithm
Proof usesDerivability with Armstrong's axioms · Superkey · Supersets of superkeys are superkeys · Attribute closure · The closure algorithm decides derivability · Candidate keys are the superkeys minimal under single removals · Shrinking a key along a list

TheoremEvery superkey contains a candidate key#✓fully proved

Let \(F\) be a finite set of functional dependencies on a finite set of attributes \(A\). Every superkey \(K\) for \(F\) has a subset \(K' \subseteq K\) that is a candidate key for \(F\).

theorem exists_isCandidateKey_subset {F : Finset (FD A)} {K : Finset A} (hK : IsSuperkey F K) :
    ∃ K' ⊆ K, IsCandidateKey F K'
Uses 9
Statement usesFunctional dependency · Candidate key · Superkey
Proof usesDerivability with Armstrong's axioms · Supersets of superkeys are superkeys · Attribute closure · The closure algorithm decides derivability · Candidate keys are the superkeys minimal under single removals · Shrinking a key along a list

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.