Finished cleaning pass on Appendix A.

app_notation-background.tex

@@ -124,11 +124,14 @@ Note that any $\poly$ in factorized form is equivalent to its \abbrSMB expansion
 
 
 
-\subsection{Proof for Lemma~\ref{lem:tidb-reduce-poly}}\label{subsec:proof-exp-poly-rpoly}
+\subsection{Proof for Lemma~\ref{lem:tidb-reduce-poly} and~\Cref{lem:bin-bidb-phi-eq-redphi}}\label{subsec:proof-exp-poly-rpoly}
 \begin{proof}
 Let $\poly$ be a polynomial of $\numvar$ variables with highest degree $= \hideg$, defined as follows: 
 \[\poly(X_1,\ldots, X_\numvar) = \sum_{\vct{d} \in \{0,\ldots, \hideg\}^\numvar}c_{\vct{d}}\cdot \prod_{\substack{i = 1\\s.t. d_i \geq 1}}^\numvar X_i^{d_i}.\]
-Let the boolean function $\isInd{\cdot}$ take $\vct{d}$ as input and return true if there does not exist any dependent variables in $\vct{d}$, i.e., $\not\exists ~\block, i\neq j\suchthat d_{\block, i}, d_{\block, j} \geq 1$.\footnote{This \abbrBIDB notation is used and discussed in \cref{subsec:tidbs-and-bidbs}}.
+
+If we can prove that $\poly\inparen{\vct{W}} = \rpoly\inparen{\vct{W}}$ for any $\poly\inparen{\vct{X}}$ and any $\vct{W}$, then the proof holds for any $\refpoly{}\inparen{\vct{W}}$ since $\refpoly{}\inparen{\vct{W}}$ is \emph{itself} a polynomial as defined above.\footnote{This can be seen in converting $\refpoly{}\inparen{\vct{X}}$ into \abbrSMB.}
+Let the boolean function $\isInd{\cdot}$ take $\vct{d}$ as input and return true if there does not exist any dependent variables in $\vct{d}$, i.e., for block $\block$ and $i, j\in\pbox{\numvar}$, $\not\exists ~\block, i\neq j\suchthat \block\supseteq\inset{\tup_i, \tup_j} \wedge d_{i}, d_{j} \geq 1$.\footnote{For generality of the proof, we are using a slightly different notation than the main paper, which treats a specific form of \abbrBIDB}  For clarity, a \abbrOneBIDB polynomial $\poly\inparen{\vct{X}}$ with any variable $X_i$ such that $X_i\in\inset{0, \bound_\tup}, \bound_\tup\neq 1$ can equivalently replace $X_i$ with $\bound_\tup X_i$ while coercing the domain of $X_i$ to be $\inset{0, 1}$.  Note that this setup addresses the general \abbrBIDB.  In what follows, we assume that $\vct{X}$ (and hence $\vct{W}$) has a domain of $\inset{0, 1}$.
+
 Then in expectation we have
 \begin{align}
 \expct_{\vct{\randWorld}}\pbox{\poly(\vct{\randWorld})} &= \expct_{\vct{\randWorld}}\pbox{\sum_{\substack{\vct{d} \in \{0,\ldots,\hideg\}^\numvar\\\wedge~\isInd{\vct{d}}}}c_{\vct{d}}\cdot \prod_{\substack{i = 1\\s.t. d_i \geq 1}}^\numvar \randWorld_i^{d_i} + \sum_{\substack{\vct{d} \in \{0,\ldots, \hideg\}^\numvar\\\wedge ~\neg\isInd{\vct{d}}}} c_{\vct{d}}\cdot\prod_{\substack{i = 1\\s.t. d_i \geq 1}}^\numvar\randWorld_i^{d_i}}\label{p1-s1a}\\

binarybidb.tex

@@ -101,7 +101,7 @@ We now define the reduced polynomial $\rpoly'$ of a \abbrOneBIDB.
 Given a polynomial $\poly'\inparen{\vct{X}}$ generated from a \abbrOneBIDB and let $\rpoly'\inparen{\vct{X}}$ denote the reduced form of $\poly'\inparen{\vct{X}}$ derived as follows:  i) compute $\smbOf{\poly'\inparen{\vct{X}}}$ eliminating all monomials with cross terms $X_{\tup}X_{\tup'}$ for $\tup\neq \tup' \in \block_i$ and  ii) reduce all \emph{variable} exponents $e > 1$ to $1$.
 \end{Definition}
 Then given $\worldvec\in\inset{0,1}^{\tupset'}$ over the reduced \abbrOneBIDB of~\Cref{prop:ctidb-reduct}, the disjoint requirement and the semantics for constructing the lineage polynomial over a \abbrOneBIDB, $\poly'\inparen{\worldvec}$ is of the same structure as the reformulated polynomial $\refpoly{}\inparen{\worldvec}$ of step i) from~\Cref{def:reduced-poly}, which then implies that $\rpoly'$ is the reduced polynomial that results from step ii) of both~\Cref{def:reduced-poly} and~\Cref{def:reduced-poly-one-bidb}, and further that~\Cref{lem:tidb-reduce-poly} immediately follows for \abbrOneBIDB polynomials.
-\begin{Lemma}
+\begin{Lemma}\label{lem:bin-bidb-phi-eq-redphi}
 Given any \emph{\abbrOneBIDB} $\pdb'$, $\raPlus$ query $\query$, and lineage polynomial
  $\poly'\inparen{\vct{X}}=\poly'\pbox{\query,\tupset',\tup}\inparen{\vct{X}}$, it holds that $
 	\expct_{\vct{W} \sim \pdassign'}\pbox{\poly'\inparen{\vct{W}}} = \rpoly'\inparen{\probAllTup}.

introduction.tex

@@ -127,7 +127,7 @@ $$
 $$
 To compute $\expct\pbox{\poly_1^2}$ we can use linearity of expectation and push the expectation through each summand.  To keep things simple, let us focus on the monomial $\poly_1^{\inparen{ABX}^2} = A^2X^2B^2$ as the procedure is the same for all other monomials of $\poly_1^2$.  Let $\randWorld_X$ be the random variable corresponding to a lineage variable $X$. Because the distinct variables in the product are independent, we can push expectation through them yielding $\expct\pbox{\randWorld_A^2\randWorld_X^2\randWorld_B^2}=\expct\pbox{\randWorld_A^2}\expct\pbox{\randWorld_X^2}\expct\pbox{\randWorld_B^2}$.  Since $\randWorld_A, \randWorld_B\in \inset{0, 1}$ we can further derive $\expct\pbox{\randWorld_A}\expct\pbox{\randWorld_X^2}\expct\pbox{\randWorld_B}$ by the fact that for any $W\in \inset{0, 1}$, $W^2 = W$.  Observe that if $X\in\inset{0, 1}$, then we further would have $\expct\pbox{\randWorld_A}\expct\pbox{\randWorld_X}\expct\pbox{\randWorld_B} = \prob_A\cdot\prob_X\cdot\prob_B$ (denoting $\probOf\pbox{\randWorld_A = 1} = \prob_A$) $= \rpoly_1^{\inparen{ABX}^2}\inparen{\prob_A, \prob_X, \prob_B}$ (see $ii)$ of~\Cref{def:reduced-poly}).  However, in this example, we get stuck with $\expct\pbox{\randWorld_X^2}$, since $\randWorld_X\in\inset{0, 1, 2}$ and for $\randWorld_X \gets 2$, $\randWorld_X^2 \neq \randWorld_X$.
 
-Denote the variables of $\poly$ to be $\vars{\poly}.$  In the \abbrCTIDB setting, $\poly\inparen{\vct{X}}$ has an equivalent reformulation $\inparen{\refpoly{}\inparen{\vct{X_R}}}$ that is of use to us, where $\abs{\vct{X_R}} = \bound\cdot\abs{\vct{X}}$ .  Given $X_\tup \in\vars{\poly}$ and integer valuation $X_\tup \in\inset{0,\ldots, c}$.  We can replace $X_\tup$ by $\sum_{j\in\pbox{\bound}}jX_{\tup, j}$ where the variables $\inparen{X_{\tup, j}}_{j\in\pbox{\bound}}$ are disjoint with integer assignments $X_\tup\in\inset{0, 1}$.  Then for any $\worldvec\in\worlds$ and corresponding reformulated world $\worldvec_{\vct{R}}\in\inset{0, 1}^{\tupset\bound}$, we set $\worldvec_{\vct{R}_{\tup, j}} = 1$ for $\worldvec_\tup = j$, while $\worldvec_{\vct{R}_{\tup, j'}} = 0$ for all $j'\neq j\in\pbox{\bound}$.  By construction then $\poly\inparen{\vct{X}}\equiv\refpoly{}\inparen{\vct{X_R}}$ $\inparen{\vct{X_R} = \vars{\refpoly{}}}$ since for any integer valuation $X_\tup\in\pbox{\bound}$, $X_j\in\inset{0, 1}$ we have the equality $X_\tup = j = \sum_{j\in\pbox{\bound}}jX_j$.
+Denote the variables of $\poly$ to be $\vars{\poly}.$  In the \abbrCTIDB setting, $\poly\inparen{\vct{X}}$ has an equivalent reformulation $\inparen{\refpoly{}\inparen{\vct{X_R}}}$ that is of use to us, where $\abs{\vct{X_R}} = \bound\cdot\abs{\vct{X}}$ .  Given $X_\tup \in\vars{\poly}$ and integer valuation $X_\tup \in\inset{0,\ldots, c}$.  We can replace $X_\tup$ by $\sum_{j\in\pbox{\bound}}jX_{\tup, j}$ where the variables $\inparen{X_{\tup, j}}_{j\in\pbox{\bound}}$ are disjoint with integer assignments $X_\tup\in\inset{0, 1}$.  Then for any $\worldvec\in\worlds$ and corresponding reformulated world $\worldvec_{\vct{R}}\in\inset{0, 1}^{\tupset\bound}$, we set $\worldvec_{\vct{R}_{\tup, j}} = 1$ for $\worldvec_\tup = j$, while $\worldvec_{\vct{R}_{\tup, j'}} = 0$ for all $j'\neq j\in\pbox{\bound}$.  By construction then $\poly\inparen{\vct{X}}\equiv\refpoly{}\inparen{\vct{X_R}}$ $\inparen{\vct{X_R} = \vars{\refpoly{}}}$ since for any integer valuation $X_\tup\in\pbox{\bound}$, $X_{\tup, j}\in\inset{0, 1}$ we have the equality $X_\tup = j = \sum_{j\in\pbox{\bound}}jX_{t, j}$.
 
 Considering again our example,
 \begin{multline*}

main.out

@@ -22,7 +22,7 @@
 \BOOKMARK [2][-]{subsection.A.1}{\376\377\000A\000.\0001\000\040\000B\000a\000c\000k\000g\000r\000o\000u\000n\000d\000\040\000d\000e\000t\000a\000i\000l\000s\000\040\000f\000o\000r\000\040\000p\000r\000o\000o\000f\000\040\000o\000f\000\040\000p\000r\000o\000p\000:\000e\000x\000p\000e\000c\000t\000i\000o\000n\000-\000o\000f\000-\000p\000o\000l\000y\000n\000o\000m}{appendix.A}% 22
 \BOOKMARK [2][-]{subsection.A.2}{\376\377\000A\000.\0002\000\040\000P\000r\000o\000o\000f\000\040\000o\000f\000\040\000p\000r\000o\000p\000:\000e\000x\000p\000e\000c\000t\000i\000o\000n\000-\000o\000f\000-\000p\000o\000l\000y\000n\000o\000m}{appendix.A}% 23
 \BOOKMARK [2][-]{subsection.A.3}{\376\377\000A\000.\0003\000\040\000P\000r\000o\000p\000o\000s\000i\000t\000i\000o\000n\000\040\000A\000.\0004}{appendix.A}% 24
-\BOOKMARK [2][-]{subsection.A.4}{\376\377\000A\000.\0004\000\040\000P\000r\000o\000o\000f\000\040\000f\000o\000r\000\040\000L\000e\000m\000m\000a\000\040\0001\000.\0004}{appendix.A}% 25
+\BOOKMARK [2][-]{subsection.A.4}{\376\377\000A\000.\0004\000\040\000P\000r\000o\000o\000f\000\040\000f\000o\000r\000\040\000L\000e\000m\000m\000a\000\040\0001\000.\0004\000\040\000a\000n\000d\000\040\000l\000e\000m\000:\000b\000i\000n\000-\000b\000i\000d\000b\000-\000p\000h\000i\000-\000e\000q\000-\000r\000e\000d\000p\000h\000i}{appendix.A}% 25
 \BOOKMARK [2][-]{subsection.A.5}{\376\377\000A\000.\0005\000\040\000P\000r\000o\000o\000f\000\040\000F\000o\000r\000\040\000C\000o\000r\000o\000l\000l\000a\000r\000y\000\040\0002\000.\0007}{appendix.A}% 26
 \BOOKMARK [1][-]{appendix.B}{\376\377\000B\000\040\000M\000i\000s\000s\000i\000n\000g\000\040\000d\000e\000t\000a\000i\000l\000s\000\040\000f\000r\000o\000m\000\040\000S\000e\000c\000t\000i\000o\000n\000\040\0003}{}% 27
 \BOOKMARK [2][-]{subsection.B.1}{\376\377\000B\000.\0001\000\040\000l\000e\000m\000:\000p\000d\000b\000-\000f\000o\000r\000-\000d\000e\000f\000-\000q\000k}{appendix.B}% 28