diff --git a/gitlab b/gitlab deleted file mode 160000 index f09cbfc..0000000 --- a/gitlab +++ /dev/null @@ -1 +0,0 @@ -Subproject commit f09cbfc1f7e89e818b81ec8422411abd8cd1ec49 diff --git a/notation.tex b/notation.tex index 9644c3b..6bedefe 100644 --- a/notation.tex +++ b/notation.tex @@ -6,258 +6,3 @@ The following notation is used to reason about the sketching of world membership When referring to Tuple Independent Databases (TIDB), a database $\relation$ contains $\numTup$ tuples, with $\numWorlds$ possible worlds $\pw$. $\pw$ is denoted as $\{0, 1\}^\numTup$, where a specific world $\wVec$ is defined as $\wVec \in \{0, 1\}^\numTup$. An indicator function $\wIndicator$ defined as $\wIndicator : \{0, 1\}^\numTup \rightarrow \kDom$ is used to determine the tuple's $\kDom$ annotation for a given world. -%For correct labelings, it is a necessary condition that two $\pwkDom$ vectors being combined share a possible world where both vectors contain a subset of the combination of the greatest lower bounds from each vector. -%\AH{I question if we need to classify semirings as TONI, TOI,...,etc. since we are now requiring all semirings to obey the cancellative law for multiplication and addition.} -%We prove this by classifying non-negative -%\begin{comment} -%A counter example for co-occurring minima being a necessary condition for correct labelings in sets that range below zero: -%In the set Z (integers) the two vectors -%[-1, 2] -%[3, 1] -%produce CERT(k_1 * k_2) = CERT([-3, 2]) = -3 while CERT([-1, 2]) * CERT([-3, 1]) = -1 * 1 = -1. -%\end{comment} -% $\kDom$~semirings into one of four categories,: Totally Ordered and Non-Idempotent (TONI), Totally Ordered and Idempotent (TOI), Partially Ordered and Non-Idempotent (PONI), and, lastly, Partially Ordered and Idempotent (POI). We also assume that neither semiring operator is the min operator. -%\begin{comment} -%Again, if either one of the semiring operators is min, then we will still guarantee correctness results without co-occurring minima because, in both -%calculations, the lowest value will be filtered out, whether by labeling or by scanning all possible worlds. -%\end{comment} -% -%\begin{Definition}[co-occurring minima] -%$k_1$ and $k_2$ have co-occurring minima, denoted $\pwHaveCoMinima{k_1}{k_2}$, if and only if -%$$\exists i \in W : k_1[i] = \glbKof{k_1} ~~~~~\textbf{and}~~~~~ k_2[i] = \glbKof{k_2}$$ -%\end{Definition} -% -%We start with the first category, TONI $\kDom$~semirings, showing that co-occuring minima is a necessary condition for correct labelings. -% -%\begin{Theorem}\label{theo:nec-co-min} -%Given a TONI \kDom~semiring and two elements $k_1, k_2 \in \pwkDom$ such that $\pwNotHaveCoMinima{k_1}{k_2}$. Then it holds that: -%\begin{align*} -%\pwCertain (k_1 \pwAdd k_2) \neq \pwCertain (k_1) -%\addK \pwCertain (k_2) \\ -%\end{align*} -%\end{Theorem} -% -%\proof{ -%\setcounter{equation}{0} -%$\pwAdd$ -% -%By construction, Theorem ~\ref{theo:nec-co-min} has the following condition: $\forall i \in \pwDom, \forall m, n \in [1,2]: k_m[i] = \glbKof{k_m} \implies k_n > \glbKof{k_n}$. We prove by cases. -% -%\begin{align*} -%&\textit{Case 1}: k_1[i] = \glbKof{k_1}\nonumber \\ -%&k_2[i] \nleq \glbKof{k_2}&\textit{by construction} \\ -%&\nexists c:\glbKof{k_2} = k_2[i] \addK c&\textit{by natural order} \\ -%&\nexists c: \glbKof{k_1} \addK \glbKof{k_2} = k_1[i] \addK k_2[i] \addK c&\textit{by substition of values} \\ -%&\glbKof{k_1} \addK \glbKof{k_2}\ngeq k_1[i] \addK k_2[i]&\textit{by natural order} \\ -%&k_1[i] \addK k_2[i] > \glbKof{k_1} \addK \glbKof{k_2}&\textit{by equivalence} -%\end{align*} -% -%Case 2: $k_2[i] = \glbKof{k_2}$ -%\newline The proof is analogous to the proof for Case 1. -%\newline\newline Case 3: $k_1[i] > \glbKof{k_1} \bigwedge k_2[i] > \glbKof{k_2}$ -% -% -%\begin{align*} -%&k_1[i] \nleq \glbKof{k_1} \wedge k_2[i] \nleq \glbKof{k_2}&\textit{by construction} \\ -%&\nexists c_1, c_2:\glbKof{k_1} = k_1[i] \addK c_1 \nonumber \\ -%&~~\wedge \glbKof{k_2} = k_2[i] \addK c_2&\textit{by natural order} \\ -%&\nexists c_1, c_2:\glbKof{k_1} \addK \glbKof{k_2} = k_1[i]\addK c_1 \nonumber \\ -%&~~\addK k_2[i] \addK c_2&\textit{by substition of values} \\ -%&\glbKof{k_1} \addK \glbKof{k_2} \ngeq k_1[i] \addK k_2[i]&\textit{by natural order} \\ -%&k_1[i] \addK k_2[i] > \glbKof{k_1} \addK \glbKof{k_2}&\textit{by equivalence} -%\end{align*} -% -%$\pwMult$ -%\setcounter{equation}{0} -% -% -%For the $\multK$ operator we further require $\glbKof{k_1}, \glbKof{k_2} \neq \zeroK$. This is due to the property that $\zeroK$ nullifies its corresponding $\multK$ operand, leading to a correct labeling even without co-occurring minima. In such a case, $\pwCertain$ and $\multK$ commute. -%\begin{Theorem} -%Given a TONI \kDom~semiring and two elements $k_1, k_2 \in \pwkDom$ such that $\pwNotHaveCoMinima{k_1}{k_2}~ \bigwedge~ \glbKof{k_1}, \glbKof{k_2} \neq \zeroK$. Then it holds that: -%\begin{align*} -%\pwCertain (k_1 \pwMult k_2) \neq \pwCertain (k_1) -%\multK \pwCertain (k_2) -%\end{align*} -%\end{Theorem} -%$Case 1: k_1[i] = \glbKof{k_1}$ -%\begin{align*} -%&k_2[i] \nleq \glbKof{k_2}&\textit{by construction} \\ -%&\nexists c: k_2[i] \addK c = \glbKof{k_2}&\textit{by natural order} \\ -%&\nexists c: \glbKof{k_1} \multK \glbKof{k_2} = k_1[i]\multK \nonumber \\ -%&~~ ( k_2[i]\addK c)&\textit{by substitution} \\ -%&\glbKof{k_1} \multK \glbKof{k_2} \ngeq k_1[i] \multK k_2[i]&\textit{by natural order} \\ -%&k_1[i] \multK k_2[i] > \glbKof{k_1} \multK \glbKof{k_2}&\textit{by equivalence} -%\end{align*} -% -%Case 2: $k_2[i] = \glbKof{k_2}$ -%\newline The proof is analogous to the proof for Case 1. -%\newline\newline Case 3: $k_1[i] > \glbKof{k_1} \bigwedge k_2[i] > \glbKof{k_2}$ -% -%\begin{align*} -%&k_1[i] \nleq \glbKof{k_1} \wedge k_2[i] \nleq \glbKof{k_2}&\textit{by construction}\\ -%&\nexists c_1, c_2: k_1[i] \addK c_1 = \glbKof{k_1} \nonumber \\ -%&~~\wedge k_2[i] \addK c_2 = \glbKof{k_2}&\textit{by natural order} \\ -%&\nexists c_1, c_2:\glbKof{k_1} \multK \glbKof{k_2} = ( k_1[i] \addK c_1) \nonumber \\ -%&~~\multK ( k_2[i] \addK c_2)&\textit{by substition of values} \\ -%& \glbKof{k_1} \multK \glbKof{k_2} \ngeq k_1[i] \multK k_2[i]&\textit{by natural order} \\ -%&k_1[i] \multK k_2[i] > \glbKof{k_1} \multK \glbKof{k_2}&\textit{by equivalence} -%\end{align*} -%} -% -% -%Building onto the above proofs we now prove the necessary condition of globally co-occurring minima to obtain a correct labeling for an arbitrary number of $\pwkDom$ vectors. -%\begin{Definition}[Globally Co-occurring Minima] -%For a given set of $n~\pwkDom$ vectors, we say that it has globally co-occurring minima -%, denoted $\pwHaveGlobalMinima{k_n}$, if and only if -%$$\forall j \in n,~ \exists i \in W : k_j[i] = \glbKof{k_j}$$ -%\end{Definition} -%\begin{Theorem} -%Given a TONI \kDom~semiring and $n$ elements $k_1, \ldots, k_n \in \pwkDom$ such that $\pwNotHaveGlobalMinima{k_n}$. Then it holds that: -%\begin{align*} -%\pwCertain (k_1 \pwAdd \ldots \pwAdd k_n) \neq \pwCertain (k_1) -%\addK \ldots \addK \pwCertain (k_n) \\ -%\end{align*} -%\end{Theorem} -%\proof{ -%We prove that if $\forall i \in \pwDom, \exists g, h \in n: ~ g \neq h \bigwedge \pwNotHaveCoMinima{k_g}{k_h}$, we will not have a correct labeling.\newline\newline -% -%$\pwAdd$ -%\setcounter{equation}{0} -%For each $i \in \pwDom$: -% -%Case 1: $k_g[i] = \glbKof{k_g}$ -% -%\AH{In step 3, note that positive sets are defined later on in this paper.} -%\begin{align*} -%&k_h[i] \nleq \glbKof{k_h}&\textit{by construction}\\ -%&\nexists c : \glbKof{k_h} = k_h[i]\addK c &\textit{by natural order}\\ -%&\nexists c :\glbKof{k_g} \addK \glbKof{k_h} = k_g[i] \addK k_h[i] \addK c&\textit{by natural order of pos. sets}\\ -%&\glbKof{k_g} \addK \glbKof{k_h} \ngeq k_g[i] \addK k_h[i]&\textit{by natural order}\\ -%&\glbKof{k_g} \addK \glbKof{k_h} \addK \sum_{f: f \in n \wedge f \neq g, h}\glbKof{k_f} \ngeq \nonumber \\ -%&~~~~~k_g[i] \addK k_h[i] \addK \sum_{f: f \in n\wedge f \neq g, h}k_f[i] \\ -%&~~~~~~~\textit{by def of glb, nat order of pos. sets}\nonumber \\ -%&\sum_{f: f \in n}\glbKof{k_f} \ngeq \sum_{f: f\in n}k_f[i]&\textit{by equivalence}\\ -%&\sum_{f: f\in n}k_f[i] > \sum_{f: f \in n}\glbKof{k_f}&\textit{by equivalence} -%\end{align*} -% -%Case 2: $k_g[i] > \glbKof{k_g}$ -% -%\begin{align*} -%&\glbKof{k_g} \ngeq k_g[i]&\textit{by construction}\\ -%&\nexists c: \glbKof{k_g} = k_g[i] \addK ~c&\textit{by natural order}\\ -%&\nexists c: \glbKof{k_g} \addK \glbKof{k_h} = k_g[i] \addK ~c \addK k_h[i]&\textit{by nat order of pos sets}\\ -%&\glbKof{k_g} \addK \glbKof{k_h} \ngeq k_g[i] \addK k_h[i]&\textit{by natural order}\\ -%&\glbKof{k_g} \addK \glbKof{k_h} \addK \sum_{f: f \in n \wedge f \neq g, h}\glbKof{k_n} \ngeq \nonumber \\ -%&~~~~~k_g[i] \addK k_h[i] \addK \sum_{f: f \in n \wedge f \neq g, h}k_n[i] &\textit{by nat order of pos sets}\\ -%&\sum_{f: f \in n}\glbKof{k_f} \ngeq \sum_{f:f \in n}k_n[i]&\textit{by equivalence}\\ -%&\sum_{f: f \in n}k_n[i] > \sum_{f: f \in n}\glbKof{k_n}&\textit{by equivalence} -%\end{align*} -%\AH{Why do we include this case? I argue that by definition of GLB such a case (case 3) can never exists.} -%Case 3: $k_g[i] < \glbKof{k_g}$ -%\begin{align*} -%&\forall i \in \pwDom \glbKof{k_g} \leq k_g[i]&\textit{by def of glb}\\ -%&\forall i \in \pwDom k_g[i] \geq \glbKof{k_g}&\textit{by step 1}\\ -%&k_g[i] \geq \glbKof{k_g}&\textit{by step 1, 2} -%\end{align*} -% -%%%%%%%%%%%%%%%%%%%%%%%% -%% \otimes -%%%%%%%%%%%%%%%%%%%%%%%% -%$\pwMult$ -%\setcounter{equation}{0} -%\newline\newline For each $i \in \pwDom$: -%\newline\newline Case 1: $k_g[i] = \glbKof{k_g}$ -% -%\begin{align*} -%&\glbKof{k_h} \ngeq k_h[i] \\ -%&\textit{by construction} \nonumber \\ -%&\nexists c: \glbKof{k_h} = k_h[i] \addK c \\ -%&\textit{by natural order} \nonumber\\ -%&\nexists c: \glbKof{k_g} \multK \glbKof{k_h} = k_g[i] \multK (k_h[i] \addK c) \\ -%&\textit{by natural order of positive sets} \nonumber \\ -%&\glbKof{k_g} \multK \glbKof{k_h} \ngeq k_g[i] \multK k_h[i] \\ -%&\textit{by natural order} \nonumber \\ -%&\glbKof{k_g} \multK \glbKof{k_h} \multK \prod_{f: f \in n \wedge f \neq g}\glbKof{k_f} \ngeq \nonumber \\ -%&~~~~~k_g[i] \multK k_h[i] \multK \prod_{f: f \in n \wedge f \neq g}k_f[i] \\ -%&\textit{by equation equivalence} \nonumber \\ -%&\prod_{f: f \in n}\glbKof{k_f} \ngeq \prod_{f: f \in n} k_f[i] \\ -%&\textit{by equivalence} \nonumber \\ -%&\prod_{f: f \in n}k_f[i] > \prod_{f: f \in n}\glbKof{k_f} \\ -%&\textit{by equivalence} \nonumber -%\end{align*} -%Case 2: $k_g[i] > \glbKof{k_g}$ -% -%\begin{align*} -%&\glbKof{k_g} \ngeq k_g[i] \\ -%&\textit{by consturction} \nonumber \\ -%&\nexists c: \glbKof{k_g} = k_g[i] \addK c \\ -%&\textit{by natural order} \nonumber \\ -%&\nexists c: \glbKof{k_g} \multK \glbKof{k_h} = (k_g[i] \addK c) \multK k_h[i] \\ -%&\textit{by equational equivalence} \nonumber \\ -%&\glbKof{k_g} \multK \glbKof{k_h} \ngeq k_g[i] \multK k_h[i] \\ -%&\textit{by equivalence} \nonumber \\ -%&\glbKof{k_g} \multK \glbKof{k_h} \multK \prod_{f: f \in n \wedge f \neq g}\glbKof{k_f} \ngeq \nonumber \\ -%&~~~~~k_g[i] \multK k_h[i] \multK \prod_{f: f \in n \wedge f \neq g}k_f[i] \\ -%&\textit{by equation equivalence} \nonumber \\ -%&\prod_{f: f \in n}\glbKof{k_f} \ngeq \prod_{f: f \in n} k_f[i] \\ -%&\textit{by equivalence} \nonumber \\ -%&\prod_{f: f \in n}k_f[i] > \prod_{f: f \in n}\glbKof{k_f} \\ -%&\textit{by equivalence} \nonumber -%\end{align*} -%Case 3: $k_g[i] < \glbKof{k_g}$ -%\newline The proof is the same as for $\addK$ -% -%} -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%% Sufficiency Proof for \multK -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%\proof{ -%\begin{Lemma}\label{lem:mult-less-than} -%For any $\kDom$ elements, $k_1, k_2, k_3, k_4$ fulfilling the conditions $k_1 \leq k_2, k_3 \leq k_4$ we have: -%$$k_1 \multK k_3 \leq k_2 \multK k_4$$ -%\proof{ -%\setcounter{equation}{0} -%\begin{align*} -%&\exists c_1: k_2 = k_1 \addK c_1 \\ -%&\textit{by natural order} \nonumber\\ -%&\exists c_2: k_4 = k_3 \addK c_2 \\ -%&\textit{by natural order} \nonumber \\ -%&k_1 \multK k_3 \leq k_2 \multK k_4 = (k_1 \addK c_1) \multK (k_3 \addK c_2) \nonumber \\ -%&~~~~ = (k_1 \multK k_3) \addK (k_1 \multK c_2) \addK (k_2 \multK c_1) \addK (c_1 \multK c_2) \\ -%&\textit{by additional terms on the right hand side} \nonumber -%\end{align*} -%} -%\end{Lemma} -%\begin{Theorem} -%Given a TONI \kDom~semiring and $n$ elements $k_1, \ldots, k_n \in \pwkDom$ such that $\pwHaveGlobalMinima{k_n}$ OR $\exists j \in n: \glbKof{k_j} = 0$, it then holds that: -%\begin{align*} -%\pwCertain (k_1 \pwMult \ldots \pwMult k_n) = \pwCertain (k_1) -%\multK \ldots \multK \pwCertain (k_n) \\ -%\end{align*} -%\end{Theorem} -%Case 1: $\exists i \in \pwDom: \forall j \in n: k_j[i] = \glbKof{k_j}$ -%\setcounter{equation}{0} -%\begin{align*} -%&\forall g \in \pwDom, j \in n: k_j[i] \leq k_j[g] \\ -%&\textit{by definition of glb} \nonumber \\ -%&\forall g \in \pwDom: \prod_{j \in n}k_j[i] \leq \prod_{j \in n}k_j[g] \\ -%&\textit{by Lemma ~\ref{lem:mult-less-than}} \nonumber -%\end{align*} -% -%Case 2: $\exists j \in n: \glbKof{k_j} = \zeroK$ -%\begin{align*} -%&\forall i \in \kDom: 0 \multK i = \zeroK \\ -%&\textit{by multiplication by zero} \nonumber \\ -%&\exists i \in \pwDom: k_j[i] = \glbKof{k_j} = \zeroK \\ -%&\textit{by definition of $\pwkDom$} \nonumber \\ -%&\prod_{j \in n} k_j[i] = \prod_{j \in n} \glbKof{k_j} = \zeroK \\ -%&\textit{by $\multK$ of $\zeroK$} \nonumber -%\end{align*} - - -%} - - -