OnePass Algo proof revised.

approx_alg.tex

@@ -50,8 +50,8 @@ The logical view of \revision{\expansion{\circuit}} is a list of tuples $(\monom
 \begin{multline*}
 \expansion{\circuit} =
 \begin{cases}
-					\revision{\expansion{\circuit_\lchild} \circ \expansion{\circuit_\rchild}}		&\textbf{ if }\revision{\circuit.\type = OR-gate}\\
-					\left\{(\monom_\lchild \cup \monom_\rchild, \coef_\lchild \cdot \coef_\rchild) ~|~\right.&\\ 							\quad \left.(\monom_\lchild, \coef_\lchild) \in \revision{\expansion{\circuit_\lchild}}, (\monom_\rchild, \coef_\rchild) \in \revision{\expansion{\circuit_\rchild}}\right\} 		&\textbf{ if }\revision{\circuit.\type = AND-gate}\\
+					\revision{\expansion{\circuit_\lchild} \circ \expansion{\circuit_\rchild}}		&\textbf{ if }\revision{\circuit.\type = \circplus}\\
+					\left\{(\monom_\lchild \cup \monom_\rchild, \coef_\lchild \cdot \coef_\rchild) ~|~\right.&\\ 							\quad \left.(\monom_\lchild, \coef_\lchild) \in \revision{\expansion{\circuit_\lchild}}, (\monom_\rchild, \coef_\rchild) \in \revision{\expansion{\circuit_\rchild}}\right\} 		&\textbf{ if }\revision{\circuit.\type = \circmult}\\
 					\elist{(\emptyset, \revision{\circuit.\val})}								&\textbf{ if }\revision{\circuit}.\type = \tnum\\
 					\elist{(\{\revision{\circuit}.\val\}, 1)}									&\textbf{ if }\revision{\circuit}.\type = \var.\\
 				\end{cases}

hardness-app.tex

@@ -449,7 +449,7 @@ Applying this bound in the runtime bound in~\Cref{lem:approx-alg} gives the firs
 	\Require \revision{\circuit}: \revision{Circuit}
 	\Ensure \revision{\circuit}: \revision{Circuit}
 	\Ensure \vari{sum} $\in \reals$
-	\If{$\revision{\circuit}.\type = \revision{\andgate}$}\label{alg:one-pass-equality1}
+	\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}
 			\State $(child, \vari{s}) \gets \onepass(child)$
@@ -461,7 +461,7 @@ Applying this bound in the runtime bound in~\Cref{lem:approx-alg} gives the firs
 		\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{\orgate}$}\label{alg:one-pass-equality2}
+	\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}
 			\State $(child, \vari{s}) \gets \onepass(child)$
@@ -546,6 +546,12 @@ level 2/.style={sibling distance=0.7cm},
 
 \subsection{Proof of~\Cref{lem:one-pass}}
 
+\revision{
+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}.
 
 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.
@@ -553,7 +559,7 @@ 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 an $\orgate$ 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 $\orgate$, 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{\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)$.
 
 \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(\treesize(\revision{\circuit})\right)$ runtime.

macros.tex

@@ -69,12 +69,12 @@
 %Pseudo Code Notation
 \newcommand{\plus}{\texttt{+}}
 \newcommand{\mult}{\texttt{\times}}
-\newcommand{\algname}[1]{\textsc{#1}}
+\newcommand{\algname}[1]{\textsc{#1}\xspace}
 \newcommand{\approxq}{\algname{Approximate$\rpoly$}}
 \newcommand{\onepass}{\algname{OnePass}}
 \newcommand{\sampmon}{\algname{SampleMonomial}}
 \newcommand{\ceil}[1]{\left\lceil #1 \right\rceil}
-\newcommand{\vari}[1]{\texttt{#1}}
+\newcommand{\vari}[1]{\texttt{#1}\xspace}
 \newcommand{\accum}{\vari{acc}}
 \newcommand{\numsamp}{\vari{N}}
 \newcommand{\numedge}{m}
@@ -270,20 +270,18 @@
 %\newcommand{\BG}[1]{}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%God Loves You Aaron Huber! <3
 %Revision Parameters
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \newcommand{\revision}[1]{\color{blue}{#1}\color{black}\xspace}
 \newcommand{\oldstuff}[1]{\color{gray}{#1}\color{black}\xspace}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%God Loves You Aaron Huber! <3
 %Circuit Notation
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \newcommand{\circuit}{\vari{C}\xspace}
 \newcommand{\circuitset}[1]{\vari{CSet}(#1)}
-\newcommand{\andgate}{AND}
-\newcommand{\orgate}{OR}
+\newcommand{\circmult}{\times}
+\newcommand{\circplus}{+}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %Sets

ra-to-poly.tex

@@ -103,9 +103,9 @@ tree, whose internal nodes are from the set $\{+, \times\}$, with leaf nodes bei
 
 \revision{
 \begin{Definition}[Circuit]\label{def:circuit}
-A circuit $\circuit$ is a Directed Acyclic Graph (DAG) whose source nodes consist of elements in either $\reals$ or $\vct{X}$.  The internal nodes and the sink node of $\circuit$ have binary input and are either AND ($\otimes$) or OR ($\oplus$) - gates.  Further, the outdegree of any internal node can grow with the circuit size.
+A circuit $\circuit$ is a data structure which consists of a Directed Acyclic Graph (DAG) whose source nodes (in degree of $0$) consist of elements in either $\reals$ or $\vct{X}$.  The internal and sink nodes of $\circuit$ have binary input and are either sum ($\circplus$) or product ($\circmult$) gates.  Further, the out degree of any internal node can grow with the circuit size.
 
-The members of $\circuit$ are \type, \val, \vari{partial}, \vari{children}, and \vari{weight}, where \type is the type of value stored in the node $\circuit$ (i.e. one of $\{OR-gate, AND-gate, \var, \tnum\}$, \val is the value stored, and \vari{children} is the list of \circuit 's children where $\circuit_\lchild$ is the left child and $\circuit_\rchild$ the right child.
+Circuit $\circuit$ additionally has the following members: \type, \val, \vari{partial}, \vari{children}, and \vari{weight}, where \type is the type of value stored in the node $\circuit$ (i.e. one of $\{\circplus, \circmult, \var, \tnum\}$, \val is the value stored, and \vari{children} is the list of \circuit 's children where $\circuit_\lchild$ is the left child and $\circuit_\rchild$ the right child.
 \end{Definition}
 }
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%