[DMDB] Functional dependencies

semester4/dmdb/parts/02_theory-background/00_functional-dependencies/00_intro.tex

@@ -0,0 +1,21 @@
+\subsection{Functional Dependency}
+As with relational algebra, we again define a schema to be a relation, e.g. $\cR(A:D_A, B:D_B, C:D_C, D: D_D)$,
+with an instance of it being $R \subseteq D_A \times D_B \times D_C \times D_D$.
+
+Then, we let $\alpha, \beta \subseteq \cR$, i.e. they each have a subset of the columns of $\cR$.
+
+$\alpha \rightarrow \beta$ ($\beta$ is a functional dependency of $\alpha$) if and only if $\forall r, s \in R : r.\alpha = s.\alpha \implies r.\beta = s.\beta$
+
+We write $R \models \alpha \rightarrow \beta$ if $R$ satisfies $\alpha \rightarrow \beta$ semantically,
+and $R \vdash \alpha \rightarrow \beta$ if the same applies syntactically (i.e. we can apply inference rules over Functional Dependencies).
+
+\inlineintuition This means that there is a function that maps the values of columns $\alpha$ to the values of columns $\beta$.
+
+
+\inlinedefinition $\alpha \subseteq \R$ is a \bi{superkey} if and only if $\alpha \rightarrow \cR$.
+
+\inlineintuition This means that if we know the values of columns $\alpha$, we know the value of the rest of the columns in $\cR$
+
+
+\inlinedefinition $\alpha \rightarrow \beta$ is minimal if and only if $\forall A \in \alpha : (\alpha - \{ A \}) \centernot{\rightarrow} \beta$.
+These are denoted $\alpha \rightarrow ^.\beta$

semester4/dmdb/parts/02_theory-background/00_functional-dependencies/01_inference.tex

@@ -0,0 +1,10 @@
+\subsubsection{Inference}
+A fundamental result for a given set of Functional Dependencies $F$ is $F \models \alpha \rightarrow \beta \Leftrightarrow F \vdash \alpha \rightarrow \beta$
+(assuming $\vdash$ is defined by Armstrong's Axioms)
+
+The goal is to find new FDs that can are implied from a set of FDs $F$ on scheme $\cR$. Let $\alpha \rightarrow \beta$ be another FD on $\cR$. Then:
+\begin{itemize}
+    \item $F$ implies $\alpha \rightarrow \beta$, if every relation instance $R$ of $\cR$ that satisfies all FDs in $F$ also satisfies $\alpha \rightarrow \beta$.
+    \item The \bi{closure} $F+$ of $F$ is the set of all FDs implied by $F$.
+    \item Let $G$ be another set of FDs on scheme $\cR$. $F$ and $G$ are \bi{equivalent} ($F \equiv G$) if $F \models G$ and $G \models F$
+\end{itemize}

semester4/dmdb/parts/02_theory-background/00_functional-dependencies/02_armstrong-axioms.tex

@@ -0,0 +1,25 @@
+\subsubsection{Armstrong's Axioms}
+\begin{itemize}
+    \item \bi{Reflexivity} $\alpha \subseteq \beta \implies \beta \rightarrow \alpha$, special case: $\cR \rightarrow \alpha$ (referred to as \textit{trivial FDs})
+    \item \bi{Augmentation} $\alpha \rightarrow \beta \implies \alpha \gamma \rightarrow \beta \gamma$, with $\alpha \gamma = \alpha \cup \gamma$
+    \item \bi{Transitivity} $\alpha \rightarrow \beta \land \beta \rightarrow \gamma \implies \alpha \rightarrow \gamma$
+\end{itemize}
+These three axioms are all complete and sound.
+All other possible FDs can be implied from these axioms.
+
+% TODO: Want the proofs?
+
+\begin{itemize}
+    \item $F$ \bi{derives} $f = \alpha \rightarrow \beta$, denoted $F \vdash f$, if there is a derivation for $f$ using only Armstrong's axioms.
+    \item $F$ \bi{implies} $f$, denoted $F \models f$, if for every relation instance $R$ of $\cR$ that satisfies all FD in $F$ also satisfies $f$.
+\end{itemize}
+
+\inlinedefinition[Soundness] $F \vdash f \rightarrow \implies F \models f$
+
+\inlinedefinition[Completeness] $F \models f \implies F \vdash f$
+
+\inlinedefinition[Closure] of $\alpha$ with respect to $F$ $\alpha^+$ is the set of all attributes $y \in \cR$ such that $\alpha \rightarrow y$ can be derived from $F$
+using Armstrong's axioms:
+\[
+    \alpha^+ = \{ y \in \cR \divider F \vdash \alpha \rightarrow y \} \qquad F \vdash \alpha \rightarrow \beta \Leftrightarrow \beta \subseteq \alpha^+
+\]

semester4/dmdb/parts/02_theory-background/00_functional-dependencies/03_other-rules.tex

@@ -0,0 +1,6 @@
+\subsubsection{Other rules}
+\begin{itemize}
+    \item \bi{Union of FDs} $\alpha \rightarrow \beta \land \alpha \rightarrow \gamma \implies \alpha \rightarrow \beta \gamma$
+    \item \bi{Decomposition} $\alpha \rightarrow \beta \gamma \implies \alpha \rightarrow \beta \land \alpha \rightarrow \gamma$
+    \item \bi{Pseudo Transitivity} $\alpha \rightarrow \beta \land \beta \gamma \rightarrow \theta \implies \alpha \gamma \rightarrow \theta$
+\end{itemize}

semester4/dmdb/parts/02_theory-background/00_functional-dependencies/04_closure.tex

@@ -0,0 +1,50 @@
+\subsubsection{Closure Algorithm}
+For the definition of the closure, see above.
+
+Finding a closure $\alpha^+$ using an algorithm\footnote{Yes, I did name the algorithm that. Sorry about that, the pun was too good to skip}:
+
+\begin{algorithm}
+    \caption{Finding Closure}
+    \begin{algorithmic}[1]
+        \Procedure{FindClosure}{$F$}
+            \State $\alpha^+ \gets \alpha$
+            \Repeat
+                \State $\alpha^+_\text{old} \gets \alpha^+$
+                \For{\textbf{each} FD $\beta \rightarrow \gamma \in F$}
+                    \If{$\beta \subseteq \alpha^+$}
+                        \State $\alpha^+ \gets \alpha^+ \cup \gamma$
+                    \EndIf
+                \EndFor
+            \Until{$\alpha^+ = \alpha^+_\text{old}$}
+            \State \Return $\alpha^+$
+        \EndProcedure
+    \end{algorithmic}
+\end{algorithm}
+
+We can use that to check the following:
+\begin{itemize}
+    \item $F \vdash \alpha \rightarrow \gamma$: Calculate $\alpha^+$ and check $\gamma \in \alpha^+$
+    \item $F \vdash G$: For each $\alpha \rightarrow \gamma \in G$, check $F \vdash \alpha \rightarrow \gamma$
+    \item $F$ equivalent to $G$: Check $F \vdash G$ and $G \vdash F$
+    \item $K \subseteq \cR$ superkey for $F$: Check $F \vdash K \rightarrow \cR$:
+\end{itemize}
+
+
+\begin{definition}[]{Minimal Cover}
+    A minimal cover (or minimum basis) of $F$ is a set of FDs $G$ that has the following properties:
+    \begin{itemize}
+        \item $G \equiv F$
+        \item All FDs in $G$ have form $X \rightarrow A$, with $A$ being a single attribute
+        \item It is not possible to make $G$ ``smaller'', i.e. if deleting a FD, $G - \{ X \rightarrow A \} \centernot{\equiv} G$,
+              or $G - \{ XA \rightarrow B \} + \{ X \rightarrow B \} \centernot{\equiv} G$, for any FD $XA \rightarrow B \in G$
+    \end{itemize}
+\end{definition}
+
+Computing the minimum basis:
+\begin{enumerate}
+    \item $G$ set of FDs obtained from $F$ by decomposing the right hand sides of each FD to single attribute
+    \item Remove trivial FDs
+    \item Remove redundant attributes from LHS of FDs in $G$ (by, for each $X \rightarrow Y$ taking each attribute $x \in X$ and,
+          if $X - \{ x \} \rightarrow Y$ implies $X \rightarrow Y$, replacing $X \rightarrow Y$ with $X - \{ x \} \rightarrow Y$)
+    \item Remove all redundant FDs
+\end{enumerate}

semester4/dmdb/parts/02_theory-background/00_functional-dependencies/05_using.tex

@@ -0,0 +1,3 @@
+\subsubsection{Using Functional Dependencies}
+Functional dependencies help with decomposing relations into several relations that each contain just one concept,
+since relations combining several concepts are bad.

semester4/dmdb/parts/02_theory-background/main.tex

@@ -0,0 +1,12 @@
+% TODO: Spacing of enumerate, itemize
+\newsection
+\section{Theoretical Background}
+\input{parts/02_theory-background/00_functional-dependencies/00_intro.tex}
+\input{parts/02_theory-background/00_functional-dependencies/01_inference.tex}
+\input{parts/02_theory-background/00_functional-dependencies/02_armstrong-axioms.tex}
+\input{parts/02_theory-background/00_functional-dependencies/03_other-rules.tex}
+\input{parts/02_theory-background/00_functional-dependencies/04_closure.tex}
+\input{parts/02_theory-background/00_functional-dependencies/05_using.tex}
+% \input{parts/02_theory-background/00_functional-dependencies/}
+
+% \input{parts/02_theory-background/}