Finished updating OnePass and SampleMonomial for Circuit input (Iteration 2)

This commit is contained in:
Aaron Huber 2021-02-02 11:25:26 -05:00
parent 2e7eff28df
commit c9bb2c40cc
2 changed files with 28 additions and 8 deletions

View file

@ -333,7 +333,7 @@ we first state the lemmas that summarize the relevant properties of $\onepass$ a
\begin{Lemma}\label{lem:one-pass}
The $\onepass$ function completes in $O(size(\circuit))$ time. $\onepass$ guarantees two post conditions: First, for each subcircuit $\vari{S}$ of $\circuit$, we have that $\vari{S}.\vari{partial}$ is set to $\abs{\vari{S}}(1,\ldots, 1)$. Second, when $\vari{S}.\type = \circplus$, for each $\vari{child}$ of $\vari{S}$, $\vari{child}.\vari{weight}$ is set to $\frac{\abs{\vari{S}_{\vari{child}}}(1,\ldots, 1)}{\abs{\vari{S}}(1,\ldots, 1)}$. % is correctly computed for each child of $\vari{S}.$
\end{Lemma}
To prove correctness of~\Cref{alg:mon-sam}, we only use the following fact that follows from the above lemma: for the modified circuit, $\circuit_{\vari{mod}}$, $\circuit_{\vari{mod}}.\vari{partial}=\abs{\circuit}(1,\dots,1)$.
To prove correctness of~\Cref{alg:mon-sam}, we only use the following fact that follows from the above lemma: for the modified circuit ($\circuit_{\vari{mod}}$), $\circuit_{\vari{mod}}$, $\circuit_{\vari{mod}}.\vari{partial}=\abs{\circuit}(1,\dots,1)$.
%\AH{I'm wondering if there is a better notation to use here. I myself got confused by my own notation of $\circuit_{\vari{mod}}$. \emph{But}, we need to to be referencing the modified $\circuit$ returned by $\onepass$ in the algorithm, so maybe this is the best we can do?}
%\AR{yeah, I think this is fine.}
%At the conclusion of $\onepass$, $\circuit.\vari{partial}$ will hold the sum of all coefficients in $\expansion{\abs{\circuit}}$, i.e., $\sum\limits_{(\monom, \coef) \in \expansion{\abs{\circuit}}}\coef$. $\circuit.\vari{weight}$ will hold the weighted probability that $\circuit$ is sampled from from its parent $+$ node.

View file

@ -452,30 +452,41 @@ Applying this bound in the runtime bound in~\Cref{lem:approx-alg} gives the firs
\If{$\revision{\circuit}.\type = \revision{\circplus}$}\label{alg:one-pass-equality1}
\State $\accum \gets 0$\label{alg:one-pass-plus-assign1}
\For{$child$ in $\revision{\circuit}.\vari{children}$}\Comment{Sum up all children coefficients}
\If{\revision{$child.\vari{partial} = $Null}}
\State $(child, \vari{s}) \gets \onepass(child)$
\State $\accum \gets \accum + \vari{s}$\label{alg:one-pass-plus-add}
\Else
\State \revision{$\accum \gets \accum + child.\vari{partial}$}
\EndIf
\EndFor
\State $\etree.\vari{partial} \gets \accum$\label{alg:one-pass-plus-assign2}
\State $\circuit.\vari{partial} \gets \accum$\label{alg:one-pass-plus-assign2}
\For{$child$ in $\revision{\circuit}.\vari{children}$}\Comment{Record distributions for each child}
\If{\revision{$child.\vari{weight} =$ Null}}
\State $child.\vari{weight} \gets \frac{child.\vari{partial}}{\etree.\vari{partial}}$\label{alg:one-pass-plus-prob}
\EndIf
\EndFor
%\State $\vari{sum} \gets \etree.\vari{partial}$\label{alg:one-pass-plus-assign3}
\State \Return (\revision{\circuit, \circuit}.\vari{partial})
\ElsIf{$\revision{\circuit}.\type = \revision{\circmult}$}\label{alg:one-pass-equality2}
\State $\accum \gets 1$\label{alg:one-pass-times-assign1}
\For{$child \text{ in } \revision{\circuit}.\vari{children}$}\Comment{Compute the product of all children coefficients}
\If{\revision{$child.\vari{partial} =$ Null}}
\State $(child, \vari{s}) \gets \onepass(child)$
\State $\accum \gets \accum \times \vari{s}$\label{alg:one-pass-times-product}
\Else
\State \revision{$\accum \gets \accum \times child.\vari{partial}$}
\EndIf
\EndFor
\State $\revision{\circuit}.\vari{partial}\gets \accum$\label{alg:one-pass-times-assign2}
%\State $\vari{sum} \gets \etree.\vari{partial}$\label{alg:one-pass-times-assign3}
\State \Return (\revision{\circuit, \circuit}.\vari{partial})
\ElsIf{$\revision{\circuit}.\type = numeric$}\Comment{Base case}\label{alg:one-pass-equality3}
\State $\vari{sum} \gets |\revision{\circuit}.\val|$\label{alg:one-pass-leaf-assign1}\Comment{This step effectively converts $\etree$ into $\abs{\revision{\circuit}}$}
\State \Return (\revision{\circuit}, \vari{sum})
\State \revision{$\circuit.\vari{partial} \gets |\revision{\circuit}.\val|$}\label{alg:one-pass-leaf-assign1}\Comment{This step effectively converts $\circuit$ into $\abs{\revision{\circuit}}$}
\State \Return (\revision{\circuit}, \circuit.\vari{partial})
\Else\Comment{$\revision{\circuit}.\type = \var$}\label{alg:one-pass-equality4}
%\State $\vari{sum} \gets 1$\label{alg:one-pass-global-assign}
\State \Return (\revision{\circuit},$1$) % \vari{sum})
\State \revision{\circuit.\vari{partial} $\gets 1$}
\State \Return (\revision{\circuit}, \circuit.\vari{partial}) % \vari{sum})
\EndIf
\end{algorithmic}
\end{algorithm}
@ -545,8 +556,9 @@ level 2/.style={sibling distance=0.7cm},
\subsection{Proof of~\Cref{lem:one-pass}}
\revision{RE:[\onepass pseudocode] One thing to note here, is now that we are using circuits, a check is needed for each internal node, to see if the child (in the case of duplicate children) partial and weight values have already been recursively computed. Otherwise, this algorithm is in $\size(\etree)$ instead of the improved $\size(\circuit)$.}
\revision{
\revision{1st iteration (reduction to expression tree)} --\oldstuff{
Let us first show that there exists an equivalent expression tree representation \etree for any arbitrary circuit \circuit. Note that by definition, it must be the case that each upstream node has at most two dependencies, and therefore the DAG structure is binary, and indeed a binary expression tree if there are no upstream gates (nodes) sharing the same dependency. When there exists multiple upstream gates that all share the same dependency, an equivalent expression tree duplicates the sub-circuit (as a sub-tree) in each gate (node) which depends on it. Note that this can be done, since \circuit is indeed binary. Finally, note that the evaluation of a subtree with root \etree which has a `duplicated' subtree will be the same computation over the same input data as the original circuit \circuit, since the operation of \etree is the same as its respective counterpart in \circuit, and both \circuit and \etree are working on the exact same inputs.
Thus, using the above, we construct the proof, noting that \onepass treats the input \circuit as the equivalent expression tree described above. This also allows for a unbiased weight computation across the monomials \monom in each (\monom, \coef) in \expansion{\circuit}.
@ -559,7 +571,9 @@ For the base case, $d = 0$, it is the case that the node is a leaf and therefore
%\AR{yep!}
For the inductive hypothesis, assume that for $d \leq k$ for some $k \geq 0$,~\Cref{lem:one-pass} is true for~\Cref{alg:one-pass}.
Now prove that lemma ~\ref{lem:one-pass} holds for $k + 1$. Notice that $\revision{\circuit}$ has at most two children, $\revision{\circuit}_\lchild$ and $\revision{\circuit}_\rchild$. Note also, that for each child, it is the case that $d \leq k$. Then, by inductive hypothesis, lemma ~\ref{lem:one-pass} holds for each existing child, and we are left with two possibilities for $\revision{\circuit}$. The first case is when $\revision{\circuit}$ is a \revision{$\circplus$} node. When this happens,~\Cref{alg:one-pass} computes $|\revision{\circuit}_\lchild|(1,\ldots, 1) + |\revision{\circuit}_\rchild|(1,\ldots, 1)$ on line ~\ref{alg:one-pass-plus-add} which by definition is $\abs{\revision{\circuit}}(1,\ldots, 1)$ and hence the inductive hypothesis holds in this case. For the weight computation of the children of $\revision{\circplus}$, by lines ~\ref{alg:one-pass-plus-add}, ~\ref{alg:one-pass-plus-assign2}, and ~\ref{alg:one-pass-plus-prob} algorithm ~\ref{alg:one-pass} computes $\revision{\circuit}_i.\wght = \frac{|\revision{\circuit}_i|(1,\ldots, 1)}{|\revision{\circuit}_\lchild|(1,\ldots, 1) + |\revision{\circuit}_\rchild|(1,\ldots, 1)}$ which is indeed as claimed. The second case is when the $\revision{\circuit}.\val = \times$. By inductive hypothesis, it is the case that both $\abs{\etree_\lchild}\polyinput{1}{1}$ and $\abs{\etree_\rchild}\polyinput{1}{1}$ have been correctly computed. On line~\ref{alg:one-pass-times-product} algorithm ~\ref{alg:one-pass} then computes the product of the children's partial values, $|\revision{\circuit}_\lchild|(1,\ldots, 1) \cdot |\revision{\circuit}_\rchild|(1,\ldots, 1)$ which by definition is $\abs{\revision{\circuit}}(1,\ldots, 1)$.
Now prove that lemma ~\ref{lem:one-pass} holds for $k + 1$. Notice that $\revision{\circuit}$ has at most two children, $\revision{\circuit}_\lchild$ and $\revision{\circuit}_\rchild$. Note also, that for each child, it is the case that $d \leq k$. Then, by inductive hypothesis, lemma ~\ref{lem:one-pass} holds for each existing child, and we are left with two possibilities for $\revision{\circuit}$. The first case is when $\revision{\circuit}$ is a \revision{$\circplus$} node. When this happens,~\Cref{alg:one-pass} computes $|\revision{\circuit}_\lchild|(1,\ldots, 1) + |\revision{\circuit}_\rchild|(1,\ldots, 1)$ on line ~\ref{alg:one-pass-plus-add} which by definition is $\abs{\revision{\circuit}}(1,\ldots, 1)$ and hence the inductive hypothesis holds in this case. For the weight computation of the children of $\revision{\circplus}$, by lines ~\ref{alg:one-pass-plus-add}, ~\ref{alg:one-pass-plus-assign2}, and ~\ref{alg:one-pass-plus-prob} algorithm ~\ref{alg:one-pass} computes $\revision{\circuit}_i.\wght = \frac{|\revision{\circuit}_i|(1,\ldots, 1)}{|\revision{\circuit}_\lchild|(1,\ldots, 1) + |\revision{\circuit}_\rchild|(1,\ldots, 1)}$ which is indeed as claimed. The second case is when the $\revision{\circuit}.\val = \times$. By inductive hypothesis, it is the case that both $\abs{\revision{\circuit}_\lchild}\polyinput{1}{1}$ and $\abs{\revision{\circuit}_\rchild}\polyinput{1}{1}$ have been correctly computed. On line~\ref{alg:one-pass-times-product} algorithm ~\ref{alg:one-pass} then computes the product of the children's partial values, $|\revision{\circuit}_\lchild|(1,\ldots, 1) \cdot |\revision{\circuit}_\rchild|(1,\ldots, 1)$ which by definition is $\abs{\revision{\circuit}}(1,\ldots, 1)$.
\revision{A final note to deal with the possibility where, in the inductive case, the source gate may have children who are output from the same gate. Note that this doesn't change the results described above, and in such a case, an equivalent expression tree would consist of two identical sub-trees, which is the equivalent of this possibility.}
\paragraph{Run-time Analysis}
The runtime for \textsc{OnePass} is fairly straight forward. Note first that each node is visited at most one time. Second, for each type of node visited, it can be trivially verified that there are only a constant number of operations. This concludes then with a $O\left(\size(\revision{\circuit})\right)$ runtime.
@ -567,7 +581,13 @@ The runtime for \textsc{OnePass} is fairly straight forward. Note first that ea
\subsection{Proof of~\Cref{lem:sample}}
\revision{
We use the equivalent expression tree representation discussed at the onset of ~\cref{lem:one-pass}, which \sampmon essentially implements.
While we would like to take advantage of the space efficiency gained in using a circuit \circuit instead an expression tree \etree, we do not know that such a method exists when computing a sample of the input polynomial representation.
The efficiency gains of circuits over trees is found in the multiplication of the same product of sum terms in the factorized polynomial that \circuit models. However, to avoid biased sampling, it is imperative to sample from both children of a multiplication gate, independently. When we perform separate, independent sampling of both children, the result is the same as performing the sampling computation over the space inefficient expression tree. However, this doesn't harm us, since as we show, that the bounded run time is not dependent on the size of the equivalent expression tree of the input circuit \circuit, but rather on the expression tree's depth, which is the same as the depth of \circuit.
}
\revision{
We use the equivalent expression tree representation discussed at the onset of ~\cref{lem:one-pass} (1st iteration--\oldstuff{grayed out}), which \sampmon essentially implements.
}
First, we need to show that $\sampmon$ indeed returns a monomial $\monom$,\footnote{Technically it returns $\var(\monom)$ but for less cumbersome notation we will refer to $\var(\monom)$ simply by $\monom$ in this proof.} such that $(\monom, \coef)$ is in $\expansion{\circuit}$, which we do by induction on the depth of $\circuit$.