diff --git a/semester4/dmdb/data-modelling-databases-summary.pdf b/semester4/dmdb/data-modelling-databases-summary.pdf index 84539a0..4f69c20 100644 Binary files a/semester4/dmdb/data-modelling-databases-summary.pdf and b/semester4/dmdb/data-modelling-databases-summary.pdf differ diff --git a/semester4/dmdb/data-modelling-databases-summary.tex b/semester4/dmdb/data-modelling-databases-summary.tex index 3f590e6..cc70759 100644 --- a/semester4/dmdb/data-modelling-databases-summary.tex +++ b/semester4/dmdb/data-modelling-databases-summary.tex @@ -81,6 +81,7 @@ In addition, the end user does not have to worry about optimization too much. Th \include{parts/00_relational-model_logic/main.tex} \include{parts/01_sql/main.tex} +\include{parts/02_theory-background/main.tex} \printGlossary diff --git a/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/00_intro.tex b/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/00_intro.tex new file mode 100644 index 0000000..cfd40b8 --- /dev/null +++ b/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$ diff --git a/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/01_inference.tex b/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/01_inference.tex new file mode 100644 index 0000000..c3583e4 --- /dev/null +++ b/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} diff --git a/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/02_armstrong-axioms.tex b/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/02_armstrong-axioms.tex new file mode 100644 index 0000000..7bf0261 --- /dev/null +++ b/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^+ +\] diff --git a/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/03_other-rules.tex b/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/03_other-rules.tex new file mode 100644 index 0000000..856128e --- /dev/null +++ b/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} diff --git a/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/04_closure.tex b/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/04_closure.tex new file mode 100644 index 0000000..a6cf3b5 --- /dev/null +++ b/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} diff --git a/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/05_using.tex b/semester4/dmdb/parts/02_theory-background/00_functional-dependencies/05_using.tex new file mode 100644 index 0000000..7dbc351 --- /dev/null +++ b/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. diff --git a/semester4/dmdb/parts/02_theory-background/main.tex b/semester4/dmdb/parts/02_theory-background/main.tex new file mode 100644 index 0000000..d42b2ed --- /dev/null +++ b/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/}