Editing Relational model (section)

=== Key constraints and functional dependencies ===
One of the simplest and most important types of relation [[constraint (database)|constraint]]s is the ''key constraint''. It tells us that in every instance of a certain relational schema the tuples can be identified by their values for certain attributes.

; [[Superkey]]
A superkey is a set of column headers for which the values of those columns concatenated are unique across all rows. Formally:
: A superkey is written as a finite set of attribute names.
: A superkey <math>K</math> holds in a relation <math>(H, B)</math> if:
:* <math>K \subseteq H</math> and
:* there exist no two distinct tuples <math>t_1, t_2 \in B</math> such that <math>t_1[K] = t_2[K]</math>.
: A superkey holds in a relation universe <math>U</math> if it holds in all relations in <math>U</math>.
: '''Theorem:''' A superkey <math>K</math> holds in a relation universe <math>U</math> over <math>H</math> if and only if <math>K \subseteq H</math> and <math>K \rightarrow H</math> holds in <math>U</math>.
; [[Candidate key]]
A candidate key is a superkey that cannot be further subdivided to form another superkey.
: A superkey <math>K</math> holds as a candidate key for a relation universe <math>U</math> if it holds as a superkey for <math>U</math> and there is no [[proper subset]] of <math>K</math> that also holds as a superkey for <math>U</math>.
; [[Functional dependency]]
Functional dependency is the property that a value in a tuple may be derived from another value in that tuple.
: A functional dependency (FD for short) is written as <math>X \rightarrow Y</math> for <math>X, Y</math> finite sets of attribute names.
: A functional dependency <math>X \rightarrow Y</math> holds in a relation <math>(H, B)</math> if:
:* <math>X, Y \subseteq H</math> and
:* <math>\forall</math> tuples <math>t_1, t_2 \in B</math>, <math>t_1[X] = t_2[X]~\Rightarrow~t_1[Y] = t_2[Y]</math>
: A functional dependency <math>X \rightarrow Y</math> holds in a relation universe <math>U</math> if it holds in all relations in <math>U</math>.
; Trivial functional dependency
: A functional dependency is trivial under a header <math>H</math> if it holds in all relation universes over <math>H</math>.
: '''Theorem:''' An FD <math>X \rightarrow Y</math> is trivial under a header <math>H</math> if and only if <math>Y \subseteq X \subseteq H</math>.
; Closure
: [[Armstrong's axioms]]: The closure of a set of FDs <math>S</math> under a header <math>H</math>, written as <math>S^+</math>, is the smallest superset of <math>S</math> such that:
:* <math>Y \subseteq X \subseteq H~\Rightarrow~X \rightarrow Y \in S^+</math> (reflexivity)
:* <math>X \rightarrow Y \in S^+ \land Y \rightarrow Z \in S^+~\Rightarrow~X \rightarrow Z \in S^+</math> (transitivity) and
:* <math>X \rightarrow Y \in S^+ \land Z \subseteq H~\Rightarrow~(X \cup Z) \rightarrow (Y \cup Z) \in S^+</math> (augmentation)
: '''Theorem:''' Armstrong's axioms are sound and complete; given a header <math>H</math> and a set <math>S</math> of FDs that only contain subsets of <math>H</math>, <math>X \rightarrow Y \in S^+</math> if and only if <math>X \rightarrow Y</math> holds in all relation universes over <math>H</math> in which all FDs in <math>S</math> hold.
; Completion
: The completion of a finite set of attributes <math>X</math> under a finite set of FDs <math>S</math>, written as <math>X^+</math>, is the smallest superset of <math>X</math> such that:
:* <math>Y \rightarrow Z \in S \land Y \subseteq X^+~\Rightarrow~Z \subseteq X^+</math>
: The completion of an attribute set can be used to compute if a certain dependency is in the closure of a set of FDs.
: '''Theorem:''' Given a set <math>S</math> of FDs, <math>X \rightarrow Y \in S^+</math> if and only if <math>Y \subseteq X^+</math>.
; Irreducible cover
: An irreducible cover of a set <math>S</math> of FDs is a set <math>T</math> of FDs such that:
:* <math>S^+ = T^+</math>
:* there exists no <math>U \subset T</math> such that <math>S^+ = U^+</math>
:* <math>X \rightarrow Y \in T~\Rightarrow Y</math> is a singleton set and
:* <math>X \rightarrow Y \in T \land Z \subset X~\Rightarrow~Z \rightarrow Y \notin S^+</math>.