A bunch more writing. Write write write.

1 files changed, 53 insertions, 49 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 48a5e73..fac83c9 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -50,8 +50,8 @@ In this chapter the main theoretical contribution of this thesis is
 presented: an extension on a $\max$-strategy iteration algorithm for
 solving fixpoint equations over the integers with monotonic
 operators\cite{Gawlitza:2007:PFC:1762174.1762203} (see Section
-\ref{sec:gawlitza-algorithm}). We devise an algorithm which runs in
-linear time in the best case.
+\ref{sec:gawlitza-algorithm}). We devise an algorithm which performs
+considerably better for practical equation systems.
 
 In this chapter we will begin by presenting the Work-list Depth First
 Search (W-DFS) fixpoint algorithm developed by Seidl et
@@ -135,7 +135,7 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
 \begin{definition}
   \textbf{Equation System:} An equation system is a mapping from
   variables to expressions. $\system : X \to E$. We define
-  $E_\system \subset E$ to be the preimage of system, that is
+  $E_\system \subset E$ to be the preimage of $\system$, that is
   $E_\system = \{ e \in E \mid system(x) = e, \forall x \in X \}$. As
   each element of $E$ is also a function $(X \to \CZ) \to \CZ$, so an
   equation system is considered as a function $\system : X \to
@@ -170,16 +170,6 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
   \end{align*}
 \end{definition}
 
-\begin{definition}
-  A variable or expression $x$ is said to \textbf{depend} on $y$ if
-  $x(\rho) \ne x(\varrho)$ and
-  \begin{align*}
-    \rho(z) &= \varrho(z) & \forall z \in X \backslash \{y\} \\
-    \rho(y) &\ne \varrho(y)
-  \end{align*}
-
-  If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$.
-\end{definition}
 
 \section{Fixpoint Iteration}
 \subsection{Kleene Iteration}
@@ -191,7 +181,7 @@ reach the least/greatest solution if there is one to be found, but it
 will often perform many more evaluations than are necessary. This
 algorithm is presented in Listing \ref{algo:kleene}.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Function {solvefixpoint} {$\system \in \Systems$}
       \State $k = 0$
@@ -223,7 +213,7 @@ iteration will continue without bound, tending towards $\{ x \mapsto
 -\infty, y \mapsto 0 \}$ rather than the greatest fixpoint of $\{
 x \mapsto -\infty, y \mapsto -\infty \}$.
 
-\begin{figure}[H]
+\begin{figure}[tbphH]
   \begin{align*}
     x &= \min(0, x - 1) \\
     y &= \min(0, \infty \oplus x) &
@@ -240,15 +230,41 @@ at most restricted to $|X|$ iterations in the particular case of the
 $\max$-strategy iteration algorithm considered in this thesis. Kleene
 iteration is therefore restricted to $\Theta(|X|^3)$ right hand side
 evaluations at most in our application. We seek to improve on this
-performance in the next section.
+performance in the next section by taking into account dependencies
+between expressions.
+
+\begin{definition}
+  An expression $x$ is said to \textbf{depend} on $y$ if and only if
+  $x(\rho) \ne x(\varrho)$ and
+  \begin{align*}
+    \rho(z) &= \varrho(z) & \forall z \in X \backslash \{y\} \\
+    \rho(y) &\ne \varrho(y)
+  \end{align*}
+
+  Intuitively, $x$ depends on $y$ if and only if a change in the value
+  of $y$ induces a change in the value of $x$.
+
+  If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$.
+\end{definition}
+
 
 \subsection{W-DFS algorithm} \label{sec:wdfs}
 
-The W-DFS algorithm of Seidl et al.~takes into account dependencies
-between variables as it solves the system. By taking into account
-dependencies we can leave portions of the system unevaluated when we
-are certain that those values have not changed. The algorithm is
-presented in Listing \ref{algo:wdfs}.
+Several algorithms have been presented in literature for finding
+solutions to general fixpoint equation systems. In particular has been
+the \emph{topdown solver} of Charlier and Van
+Hentenryck\cite{TD-fixpoint} and the \emph{worklist} solver of
+Kildall\cite{Kildall:1973:UAG:512927.512945} which has been further
+extended by others\cite{Jorgensen94findingfixpoints,FP-efficient}. The
+W-DFS algorithm of Seidl et al.\cite{DBLP:tr/trier/MI96-11} is an
+attempt to combine the best aspects of these general fixpoint
+algorithms.
+
+The W-DFS algorithm takes into account dependencies between variables
+as it solves the system. By taking into account dependencies we can
+leave portions of the system unevaluated when we are certain that
+those values have not changed. The algorithm is presented in Listing
+\ref{algo:wdfs}.
 
 \begin{algorithm}
   \begin{algorithmic}
@@ -343,7 +359,7 @@ The W-DFS algorithm provides us with a \emph{local},
 \emph{demand-driven} solver for greatest fixpoints of monotonic
 fixpoint problems.
 
-\begin{figure}[H]
+\begin{figure}[tbphH]
   \begin{tikzpicture}
     \node[draw] (full) at (0,-2) {
       \begin{minipage}{0.3\textwidth}
@@ -399,14 +415,10 @@ other subsystem. To compute the value of $x$ in the greatest fixpoint
 it is unnecessary to compute the value of the variable $d$, but it is
 necessary to compute the value of $y$. The W-DFS algorithm, will only
 evaluate the necessary subsystem for a requested variable, leaving the
-other system unevaluated. In order to capture this property we will
-define the notion of a \emph{local} solver.
+other subsystem unevaluated. We call this algorithm \emph{local},
+because it considers only as many variables as are necessary to
+compute the requested values.
 
-\begin{definition}
-  \textbf{Local:} A solver is said be \emph{local} if, for some
-  equation system, $\system$, and some $e \in E_\system$, it will
-  solve for $e_x$ without evaluating every element of $E_\system$.
-\end{definition}
 
 
 \section{$\max$-strategy Iteration}
@@ -475,7 +487,7 @@ approach is to perform a loop, improving the strategy at each step,
 until an equilibrium point is reached. The approach is presented in
 Listing \ref{algo:naive-strategy}.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Assumptions
       \begin{tabularx}{0.9\textwidth}{rX}
@@ -526,7 +538,7 @@ the W-DFS algorithm presented above in Section \ref{sec:wdfs}. Listing
 \ref{algo:adapted-wdfs} presents one variation on W-DFS to solve
 $\max$-strategy iteration problems.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Globals
     \begin{tabularx}{0.9\textwidth}{rX}
@@ -665,7 +677,8 @@ stabilises (at which point the fixpoint will also stabilise).
 Both portions of the LDSI algorithm are \emph{demand driven}, and so
 any necessary evaluation of strategies or fixpoint values is delayed
 until the point when it is required. This means that the solver will
-be \emph{local} (see Section \ref{sec:wdfs}).
+be \emph{local}, considering only the subset of variables necessary to
+calculate the values we are interested in..
 
 
 
@@ -701,7 +714,7 @@ This algorithm is presented in three parts.
 
 \subsection{Top level} \label{sec:ldsi:top-level}
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Globals
     \begin{tabularx}{0.9\textwidth}{rX}
@@ -749,7 +762,7 @@ in Sections \ref{sec:wdfs} and \ref{sec:adapted-wdfs}. The only
 exception is $\touchedFP$, which is a newly introduced variable to
 track variables which are touched by the fixpoint iteration steps.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Function {init} {$s \in \Systems$}
       \State $D = \underline{-\infty}$
@@ -803,7 +816,7 @@ have already been computed to avoid performing additional work. The
 last stable value is stored in this procedure to identify
 \emph{changed} values, rather than only \emph{unstable} ones.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Function {evalfixpoint} {$x \in X$, $y \in X$}
       \State $\solve \fixpoint(y)$
@@ -822,7 +835,7 @@ algorithm, except for the fact that $\solve$ has been renamed to
 $\solve \fixpoint$. $\eval \fixpoint$ performs the same function as
 the $\eval$ function in Listing \ref{algo:wdfs}.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Procedure {invalidatefixpoint} {$x \in X$}
     \Comment{Invalidate a fixpoint variable}
@@ -863,7 +876,7 @@ set of changed variables for the $\max$-strategy iteration phase.
 
 
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Procedure {solvefixpoint} {$x \in X$}
     \If {$x \not \in \stableFP$}
@@ -909,7 +922,7 @@ being stabilised.
 
 
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}
     \Function {evalstrategy} {$x \in E_{\max}$, $y \in E_{\max}$}
       \State $\solve \strategy(y)$
@@ -957,7 +970,7 @@ directly, but if it is dependent on its own value (as in $\{ x = x + 1
 \}$, for example), then it will be destabilised by the transitivity of
 $\invalidate \strategy$.
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic} 
     \Procedure {invalidatestrategy} {$x \in E_{\max}$}
       \If {$x \in \stableSI$}
@@ -982,7 +995,7 @@ by a $\solve \strategy$ call. All $\max$-expressions which
 (transitively) depend on $x$ are destabilised recursively.
 
 
-\begin{algorithm}[H]
+\begin{algorithm}[tbphH]
   \begin{algorithmic}    
     \Procedure {solvestrategy} {$x \in E_{\max}$}
     \If {$x \not \in \stableSI$}
@@ -1019,13 +1032,6 @@ Section \ref{sec:adapted-wdfs}.
 
 \subsection{Correctness} \label{sec:ldsi:correctness}
 
-To argue the correctness of our LDSI algorithm we will first argue the
-correctness of the fixpoint iteration portion of the algorithm. We
-will then argue the correctness of the $\max$-strategy iteration
-portion, including the communication between the fixpoint iteration
-and $\max$-strategy iteration.
-
-
 The fixpoint iteration portion of the algorithm is concerned with
 finding the greatest fixpoint, $\solnFP(s) : X \to D$ for the system $s
 = \sigma(\system)$. If we consider all valid fixpoints, $\fix(s) = \{
@@ -1187,6 +1193,4 @@ correctly solve their respective portions of the problem, and the
 communication between them is correct, then we know that the overall
 algorithm is correct.
 
-
 \subsection{Implementation} \label{sec:ldsi:implementation}
-