ODIn
/
paper-BagRelationalPDBsAreHard
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Added a lemma and proof of correctnesss/runtime for Reduce algo.

master
Aaron Huber 2021-03-05 17:59:06 -05:00
parent c77ae26066
commit 3a38a8ad89
1 changed files with 32 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
hardness-app.tex
View File

@ -449,10 +449,36 @@ Please note that it is \textit{assumed} that the original call to \onepass consi
For technical reasons, we require the invariant that every subcircuit \subcircuit corresponding to an internal gate of \circuit has an input $\subcircuit_i$ such that $\degree\left(\polyf(\subcircuit_i)\right) \geq 1$. To ensure this, auxiliary algorithm ~\ref{alg:reduce} (\reduce) is called to perform any rewrites to \circuit, where an equivalent circuit \circuit' is created and returned by iteratively combining non-variable leaf nodes bottom-up until a parent node is reached which has an input \subcircuit whose subcircuit contains at least one leaf of type \var. It is trivial to see in such a case that $\subcircuit \equiv \subcircuit'$, and this implies $\circuit \equiv \circuit'$.
\begin{Lemma}\label{lem:reduce}
In linear time, algorithm \reduce inspects input circuit \circuit and outputs a modified equivalent version \circuit' of \circuit such that all subcircuits \subcircuit of \circuit' have at least one input $\subcircuit_i$ with $\degree(\subcircuit_i) \geq 1$.
\end{Lemma}
\begin{proof}[Proof of \Cref{lem:reduce}]
~\paragraph{\reduce correctness}
Note that for a leaf node \subcircuit, only when $\subcircuit.\type = \var$ is it the case that $\degree(\subcircuit) = 1$, and otherwise $\degree(\subcircuit) = 0$. This correct behavior is carried out in lines~\ref{alg:reduce-add-deg} and~\ref{alg:reduce-no-deg}.
We prove an equivalent circuit \circuit' by induction over the iteration of \topord. For the base case, consider when we have one node. In such a case, no rewriting occurs, and \reduce returns \circuit. It is trivial to note that $\circuit \equiv \circuit$.
For the I.H., we assume that for $k \geq 0$ nodes in \topord, the modified circuit $\circuit' \equiv \circuit$.
We now prove for $k + 1$ nodes in \topord that $\circuit' \equiv \circuit$. Note that if the node $\gate_{k + 1}$ is a source node, then this is again the base case and we are finished. If $\gate_{k + 1}$ is an internal node, then $\gate_{k + 1}.\type$ must either be $\circmult$ or $\circplus$.
When $\gate_{k + 1}$ is $\circmult$, then it is the case that either $\degree(\gate_{{k + 1}_\linput}) \geq 1$ or $\gate_{{k + 1}_\linput}.\type$ is $\tnum$ and likewise for $\gate_{{k + 1}_\rinput}$. There are then four possibilities, only one of which will prompt a rewrite, namely when we have that both inputs have $\degree(\gate_{{k + 1}_i}) = 0$. In such a case, $\gate_{k + 1}.\val \gets \gate_{{k + 1}_\linput}.\val \times \gate_{{k + 1}_\rinput}.\val$, and the inputs are deleted. Note that since $\gate_{{k + 1}_\linput}.\type = \gate_{{k + 1}_\rinput}.\type = \tnum$ that we have two constants being multiplied, and that for subcircuit $\subcircuit = (\times, \tnum_1, \tnum_2)$ and $\tnum' = \tnum_1 \times \tnum_2$, $\polyf(\subcircuit) = \polyf(\tnum')$ which implies that for the rewritten \subcircuit', $\subcircuit \equiv \subcircuit'$.
A symmetric argument applies when $\gate_{k + 1}.\type$ is $\circplus$.\qed
\paragraph{\reduce Run-time Analysis}.
$O(\size(\circuit))$ trivially follows by the single iterative pass over the \topord of \circuit, where, as can be seen in lines~\ref{alg:reduce-var},~\ref{alg:reduce-num},~\ref{alg:reduce-mult}, and~\ref{alg:reduce-plus} a constant number of operations are performed on each node.\qed
\end{proof}
}
\subsection{$\onepass$ Example}
\begin{Example}\label{example:one-pass}
Let $\etree$ encode the expression $(X_1 + X_2)(X_1 - X_2) + X_2^2$. After one pass, \cref{alg:one-pass-iter} would have computed the following weight distribution. For the two inputs of the root $+$ node $\etree$, $\etree.\lwght = \frac{4}{5}$ and $\etree.\rwght = \frac{1}{5}$. Similarly, let $\stree$ denote the left-subtree of $\etree_{\lchild}$, $\stree.\lwght = \stree.\rwght = \frac{1}{2}$. This is depicted in~\Cref{fig:expr-tree-T-wght}. %Note that in this example, the sampling probabilities for the children of each inner $+$ node of $\stree$ are equal to one another because both parents have the same number of children, and, in each case, the children of each parent $+$ node share the same $|\coef_i|$.
@ -526,18 +552,18 @@ level 2/.style={sibling distance=0.7cm},
\Require \circuit: Circuit
\Ensure \circuit: Reduced Circuit
\For{\gate in \topord(\circuit)}\label{alg:reduce-loop}\Comment{\topord($\cdot$) is the topological order of \circuit}
\If{\gate.\type $=$ \var}
\State \gate.\degval $\gets 1$
\ElsIf{\gate.\type $=$ \tnum}
\State \gate.\degval $\gets 0$
\ElsIf{\gate.\type $= \circmult$}
\If{\gate.\type $=$ \var}\label{alg:reduce-var}
\State \gate.\degval $\gets 1$\label{alg:reduce-add-deg}
\ElsIf{\gate.\type $=$ \tnum}\label{alg:reduce-num}
\State \gate.\degval $\gets 0$\label{alg:reduce-no-deg}
\ElsIf{\gate.\type $= \circmult$}\label{alg:reduce-mult}
\State \gate.\degval $\gets \gate_\linput.\degval + \gate_\rinput.\degval$
\If{\gate.\degval $= 0$}
\State \gate.\type $\gets \tnum$
\State $\gate.\val \gets \gate_\linput.\val \times \gate_\rinput.\val$
\State $\gate_\linput, \gate_\rinput \gets \nullval$
\EndIf
\Else
\Else \label{alg:reduce-plus}
\State \gate.\degval $\gets \max(\gate_\linput.\degval, \gate_\rinput.\degval)$
\If{\gate.\degval $= 0$}
\State \gate.\type $\gets \tnum$