Added proof for Onepass Iterative Algorithm.
This commit is contained in:
parent
d4717bc249
commit
2a359b6068
185
hardness-app.tex
185
hardness-app.tex
|
|
@ -447,55 +447,57 @@ Applying this bound in the runtime bound in~\Cref{lem:approx-alg} gives the firs
|
|||
Please note that it is \textit{assumed} that the original call to \onepass consists of a call on an input circuit \circuit such that the values of members \prt, \lwght and \rwght have been initialized to Null across all gates.
|
||||
}
|
||||
|
||||
|
||||
\begin{algorithm}[h!]
|
||||
\caption{\onepass$(\revision{\circuit})$}
|
||||
\label{alg:one-pass}
|
||||
\begin{algorithmic}[1]
|
||||
\Require \revision{\circuit}: \revision{Circuit}
|
||||
\Ensure \revision{\circuit}: \revision{Circuit}
|
||||
\Ensure \vari{sum} $\in \reals$
|
||||
\If{$\revision{\circuit}.\type = \revision{\circplus}$}\label{alg:one-pass-equality1}
|
||||
\State $\accum \gets 0$\label{alg:one-pass-plus-assign1}
|
||||
\For{$input$ in $\revision{\circuit}.\inputs$}\Comment{Sum up all input coefficients}
|
||||
\If{\revision{$input.\prt = $Null}}
|
||||
\State $(input, \vari{s}) \gets \onepass(input)$
|
||||
\State $\accum \gets \accum + \vari{s}$\label{alg:one-pass-plus-add}
|
||||
\Else
|
||||
\State \revision{$\accum \gets \accum + input.\prt$}\label{alg:one-pass-revisit1}
|
||||
\EndIf
|
||||
\EndFor
|
||||
\State $\circuit.\prt \gets \accum$\label{alg:one-pass-plus-assign2}
|
||||
\For{$input$ in $\revision{\circuit}.\inputs$}\Comment{Record distributions for each input}
|
||||
\If{\revision{$input\vari{weight} =$ Null}}
|
||||
\State $input.\vari{weight} \gets \frac{input.\prt}{\circuit.\prt}$\label{alg:one-pass-plus-prob}
|
||||
\EndIf
|
||||
\EndFor
|
||||
%\State $\vari{sum} \gets \etree.\prt$\label{alg:one-pass-plus-assign3}
|
||||
\State \Return (\revision{\circuit, \circuit}.\prt)
|
||||
\ElsIf{$\revision{\circuit}.\type = \revision{\circmult}$}\label{alg:one-pass-equality2}
|
||||
\State $\accum \gets 1$\label{alg:one-pass-times-assign1}
|
||||
\For{$input\text{ in } \revision{\circuit}.\inputs$}\Comment{Compute the product of all input coefficients}
|
||||
\If{\revision{$input.\prt =$ Null}}
|
||||
\State $(input, \vari{s}) \gets \onepass(input)$
|
||||
\State $\accum \gets \accum \times \vari{s}$\label{alg:one-pass-times-product}
|
||||
\Else
|
||||
\State \revision{$\accum \gets \accum \times input.\prt$}\label{alg:one-pass-revisit2}
|
||||
\EndIf
|
||||
\EndFor
|
||||
\State $\revision{\circuit}.\prt\gets \accum$\label{alg:one-pass-times-assign2}
|
||||
%\State $\vari{sum} \gets \etree.\prt$\label{alg:one-pass-times-assign3}
|
||||
\State \Return (\revision{\circuit, \circuit}.\prt)
|
||||
\ElsIf{$\revision{\circuit}.\type = numeric$}\Comment{Base case}\label{alg:one-pass-equality3}
|
||||
\State \revision{$\circuit.\prt \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.\prt)
|
||||
\Else\Comment{$\revision{\circuit}.\type = \var$}\label{alg:one-pass-equality4}
|
||||
%\State $\vari{sum} \gets 1$\label{alg:one-pass-global-assign}
|
||||
\State \revision{\circuit.\prt $\gets 1$}
|
||||
\State \Return (\revision{\circuit}, \circuit.\prt) % \vari{sum})
|
||||
\EndIf
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
%\oldstuff{
|
||||
%
|
||||
%\begin{algorithm}[h!]
|
||||
% \caption{\onepass$(\revision{\circuit})$}
|
||||
% \label{alg:one-pass}
|
||||
%\begin{algorithmic}[1]
|
||||
% \Require \revision{\circuit}: \revision{Circuit}
|
||||
% \Ensure \revision{\circuit}: \revision{Circuit}
|
||||
% \Ensure \vari{sum} $\in \reals$
|
||||
% \If{$\revision{\circuit}.\type = \revision{\circplus}$}\label{alg:one-pass-equality1}
|
||||
% \State $\accum \gets 0$\label{alg:one-pass-plus-assign1}
|
||||
% \For{$input$ in $\revision{\circuit}.\inputs$}\Comment{Sum up all input coefficients}
|
||||
% \If{\revision{$input.\prt = $Null}}
|
||||
% \State $(input, \vari{s}) \gets \onepass(input)$
|
||||
% \State $\accum \gets \accum + \vari{s}$\label{alg:one-pass-plus-add}
|
||||
% \Else
|
||||
% \State \revision{$\accum \gets \accum + input.\prt$}\label{alg:one-pass-revisit1}
|
||||
% \EndIf
|
||||
% \EndFor
|
||||
% \State $\circuit.\prt \gets \accum$\label{alg:one-pass-plus-assign2}
|
||||
% \For{$input$ in $\revision{\circuit}.\inputs$}\Comment{Record distributions for each input}
|
||||
% \If{\revision{$input\vari{weight} =$ Null}}
|
||||
% \State $input.\vari{weight} \gets \frac{input.\prt}{\circuit.\prt}$\label{alg:one-pass-plus-prob}
|
||||
% \EndIf
|
||||
% \EndFor
|
||||
% %\State $\vari{sum} \gets \etree.\prt$\label{alg:one-pass-plus-assign3}
|
||||
% \State \Return (\revision{\circuit, \circuit}.\prt)
|
||||
% \ElsIf{$\revision{\circuit}.\type = \revision{\circmult}$}\label{alg:one-pass-equality2}
|
||||
% \State $\accum \gets 1$\label{alg:one-pass-times-assign1}
|
||||
% \For{$input\text{ in } \revision{\circuit}.\inputs$}\Comment{Compute the product of all input coefficients}
|
||||
% \If{\revision{$input.\prt =$ Null}}
|
||||
% \State $(input, \vari{s}) \gets \onepass(input)$
|
||||
% \State $\accum \gets \accum \times \vari{s}$\label{alg:one-pass-times-product}
|
||||
% \Else
|
||||
% \State \revision{$\accum \gets \accum \times input.\prt$}\label{alg:one-pass-revisit2}
|
||||
% \EndIf
|
||||
% \EndFor
|
||||
% \State $\revision{\circuit}.\prt\gets \accum$\label{alg:one-pass-times-assign2}
|
||||
% %\State $\vari{sum} \gets \etree.\prt$\label{alg:one-pass-times-assign3}
|
||||
% \State \Return (\revision{\circuit, \circuit}.\prt)
|
||||
% \ElsIf{$\revision{\circuit}.\type = numeric$}\Comment{Base case}\label{alg:one-pass-equality3}
|
||||
% \State \revision{$\circuit.\prt \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.\prt)
|
||||
% \Else\Comment{$\revision{\circuit}.\type = \var$}\label{alg:one-pass-equality4}
|
||||
% %\State $\vari{sum} \gets 1$\label{alg:one-pass-global-assign}
|
||||
% \State \revision{\circuit.\prt $\gets 1$}
|
||||
% \State \Return (\revision{\circuit}, \circuit.\prt) % \vari{sum})
|
||||
% \EndIf
|
||||
%\end{algorithmic}
|
||||
%\end{algorithm}
|
||||
%}
|
||||
|
||||
\subsection{$\onepass$ Example}
|
||||
\begin{Example}\label{example:one-pass}
|
||||
|
|
@ -560,43 +562,44 @@ level 2/.style={sibling distance=0.7cm},
|
|||
\label{fig:expr-tree-T-wght}
|
||||
\end{figure}
|
||||
|
||||
|
||||
\subsection{\onepass Notes}
|
||||
\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 input (in the case of duplicate inputs) partial and weight values have already been recursively computed. Otherwise, this algorithm is in $\size(\etree)$ instead of the improved $\size(\circuit)$.
|
||||
|
||||
Another consideration is the possibility where a gate may have inputs from the same gate, or a gate might have two parents. Note that this doesn't change the results described above, and in such a case, noting the reduction descibed susequently to an expression tree, an equivalent expression tree would repeated subtrees in either case, which is the equivalent of this possibility.}
|
||||
|
||||
\subsection{Proof of~\Cref{lem:one-pass}}
|
||||
|
||||
\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}.
|
||||
}
|
||||
|
||||
We prove the first part of lemma ~\ref{lem:one-pass}, i.e., correctness, by structural induction over the depth $d$ of the \revision{circuit \circuit}, \revision{
|
||||
\textit{specifically} after the first call to \onepass on \circuit. Note by the recursive nature of \onepass that it is a fact that after this first call, all subcircuits \subcircuit will have their repsective \prt, \lwght, and \rwght members set to values other than Null.
|
||||
|
||||
}
|
||||
|
||||
For the base case, $d = 0$, it is the case that the node is a leaf and therefore by definition ~\ref{def:express-tree} must be a variable or coefficient. When it is a variable, \textsc{OnePass} returns $1$, and we have in this case that $\polyf(\revision{\circuit}) = X_i = \polyf(\abs{\revision{\circuit}})$ for some $i$ in $[\numvar]$, and this evaluated at all $1$'s indeed gives $1$, verifying the correctness of the returned value of $\abs{\revision{\circuit}}(1,\ldots, 1) = 1$. When the root is a coefficient, the absolute value of the coefficient is returned, which is indeed $\abs{\revision{\circuit}}(1,\ldots, 1)$. This proves the base case.
|
||||
%\AH{The inductive step assumes $k \geq 0$ rather than $k \geq 1$, correct?}
|
||||
%\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 the inductive hypothesis holds for $k + 1$. Notice that $\revision{\circuit}$ has at most two inputs, $\revision{\circuit}_\lchild$ and $\revision{\circuit}_\rchild$. Note also, that for each input, it is the case that $d \leq k$. Then,
|
||||
\revision{
|
||||
by inductive hypothesis, all gates in all subcircuits \subcircuit of \circuit have been correctly annotated.
|
||||
}
|
||||
% lemma ~\ref{lem:one-pass} holds for each existing input, and we are left
|
||||
This leaves us 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 inputs 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 \circuit.\prt as the product of the inputs' 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)$.
|
||||
|
||||
|
||||
\paragraph{Run-time Analysis}
|
||||
The runtime for \textsc{OnePass} is fairly straight forward. \revision{
|
||||
Note that due to the property of each gate having potentially a linear number of outputs in the size of the circuit, each node can be upper bounded to being visited $\numvar$ times for a circuit of size $\numvar$. However, we can produce a tighter bound based on the property that each gate has at most $2$ inputs. This implies that there exist at most $2\numvar$ edges, and $O(\numvar)$ edges implies a total of $< 2\numvar$ node visitations (recall that source nodes have no inputs). It is therefore the case that we still have $O(\numvar)$ visitations across the entire circuit.
|
||||
}
|
||||
Next consider 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.
|
||||
%\oldstuff{
|
||||
%\subsection{\onepass Notes}
|
||||
%\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 input (in the case of duplicate inputs) partial and weight values have already been recursively computed. Otherwise, this algorithm is in $\size(\etree)$ instead of the improved $\size(\circuit)$.
|
||||
%
|
||||
%Another consideration is the possibility where a gate may have inputs from the same gate, or a gate might have two parents. Note that this doesn't change the results described above, and in such a case, noting the reduction descibed susequently to an expression tree, an equivalent expression tree would repeated subtrees in either case, which is the equivalent of this possibility.}
|
||||
%
|
||||
%\subsection{Proof of~\Cref{lem:one-pass}}
|
||||
%
|
||||
%\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}.
|
||||
%}
|
||||
%
|
||||
%We prove the first part of lemma ~\ref{lem:one-pass}, i.e., correctness, by structural induction over the depth $d$ of the \revision{circuit \circuit}, \revision{
|
||||
%\textit{specifically} after the first call to \onepass on \circuit. Note by the recursive nature of \onepass that it is a fact that after this first call, all subcircuits \subcircuit will have their repsective \prt, \lwght, and \rwght members set to values other than Null.
|
||||
%
|
||||
%}
|
||||
%
|
||||
%For the base case, $d = 0$, it is the case that the node is a leaf and therefore by definition ~\ref{def:express-tree} must be a variable or coefficient. When it is a variable, \textsc{OnePass} returns $1$, and we have in this case that $\polyf(\revision{\circuit}) = X_i = \polyf(\abs{\revision{\circuit}})$ for some $i$ in $[\numvar]$, and this evaluated at all $1$'s indeed gives $1$, verifying the correctness of the returned value of $\abs{\revision{\circuit}}(1,\ldots, 1) = 1$. When the root is a coefficient, the absolute value of the coefficient is returned, which is indeed $\abs{\revision{\circuit}}(1,\ldots, 1)$. This proves the base case.
|
||||
%%\AH{The inductive step assumes $k \geq 0$ rather than $k \geq 1$, correct?}
|
||||
%%\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 the inductive hypothesis holds for $k + 1$. Notice that $\revision{\circuit}$ has at most two inputs, $\revision{\circuit}_\lchild$ and $\revision{\circuit}_\rchild$. Note also, that for each input, it is the case that $d \leq k$. Then,
|
||||
%\revision{
|
||||
%by inductive hypothesis, all gates in all subcircuits \subcircuit of \circuit have been correctly annotated.
|
||||
%}
|
||||
%% lemma ~\ref{lem:one-pass} holds for each existing input, and we are left
|
||||
%This leaves us 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 inputs 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 \circuit.\prt as the product of the inputs' 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)$.
|
||||
%
|
||||
%
|
||||
%\paragraph{Run-time Analysis}
|
||||
%The runtime for \textsc{OnePass} is fairly straight forward. \revision{
|
||||
%Note that due to the property of each gate having potentially a linear number of outputs in the size of the circuit, each node can be upper bounded to being visited $\numvar$ times for a circuit of size $\numvar$. However, we can produce a tighter bound based on the property that each gate has at most $2$ inputs. This implies that there exist at most $2\numvar$ edges, and $O(\numvar)$ edges implies a total of $< 2\numvar$ node visitations (recall that source nodes have no inputs). It is therefore the case that we still have $O(\numvar)$ visitations across the entire circuit.
|
||||
%}
|
||||
%Next consider 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.
|
||||
%}
|
||||
|
||||
\subsection{\onepass Iterative}
|
||||
\revision{
|
||||
|
|
@ -627,8 +630,16 @@ Next consider for each type of node visited, it can be trivially verified that t
|
|||
\end{algorithm}
|
||||
}
|
||||
|
||||
\subsection{Proof of ~\Cref{lem:one-pass} Iterative}
|
||||
\revision{
|
||||
|
||||
\subsection{Proof of ~\Cref{lem:one-pass} Iterative}
|
||||
\paragraph{\onepass Correctness}
|
||||
We first note that all DAGs have a topological ordering. By definition, a topological ordering will always order the source nodes first, since if there exists an edge $(u, v)$ in the set of edges $E$, then gate $u$ will be ordered before gate $v$, since the edge goes from $u$ to $v$. Therefore \onepass will visit all source (leaf) nodes first, correctly annotating the \prt values. Recall that all internal gates are either $\circplus$ or $\circmult$. The parent gates of the source gates will be the visited next in \topord(\circuit). If a parent node \subcircuit is $\circplus$, \onepass will add the values of the two source nodes $\subcircuit_\linput.\prt + \subcircuit_\rinput.\prt$ to correctly annotate \subcircuit.\prt. Further \subcircuit.\lwght will be computed correctly as $\frac{\subcircuit_\linput.\prt}{\subcircuit.\prt}$ and analogously for \subcircuit.\rwght. If the parent gate \subcircuit visited is a $\circmult$, then \onepass will correctly annotate \subcircuit.\prt as $\subcircuit_\linput.\prt \times \subcircuit_\rinput.\prt$. As gates further in the order are subsequently visited, note that it is the case that all previous gates visited will always contain the correct \prt values and it follows that all subsequent gates visited in \topord(\circuit) will correctly compute their respective \prt values. Since \lwght and \rwght are computed dependent only on \prt values, it follows that all \lwght and \rwght values will then be computed correctly.
|
||||
|
||||
\paragraph{\onepass Runtime}
|
||||
By the iterative nature of \onepass, each node is indeed visited once. Note that for each \type, there a constant number of operations, and this yields a runtime of $O(\size(\circuit)$.
|
||||
|
||||
}
|
||||
|
||||
\subsection{\sampmon Notes}
|
||||
\revision{
|
||||
|
|
|
|||
Loading…
Reference in a new issue