Initial Commit
This commit is contained in:
parent
6c7ea8706e
commit
718d689622
1
gitlab
1
gitlab
|
|
@ -1 +0,0 @@
|
|||
Subproject commit f09cbfc1f7e89e818b81ec8422411abd8cd1ec49
|
||||
255
notation.tex
255
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*}
|
||||
|
||||
|
||||
%}
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue