Work a bit more on contribution stuff.

1 files changed, 157 insertions, 157 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index ff75e9b..18d956f 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -145,7 +145,7 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
 
 \begin{definition}
   \textbf{Dependencies:} A variable or expression $x$ is said to
-  \emph{depend on} $y$ if $x(\rho) \ne x(\varrho)$, when
+  \emph{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)
@@ -154,12 +154,6 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
   If $x$ depends on $y$ then $y$ is said to \emph{influence} $x$.
 \end{definition}
 
-\begin{definition}
-  \textbf{Local:} A solver is said be 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{Fixpoint Iteration}
 \subsection{Kleene Iteration}
 
@@ -187,28 +181,20 @@ algorithm is presented in Listing \ref{algo:kleene}.
   \label{algo:kleene}
 \end{algorithm}
 
-For each iteration the entire system is evaluated, irrespective of
-whether it could possibly have changed value. This results in a
-considerable inefficiency in practice, requiring the evaluation of
-many right-hand-sides repeatedly for the same value. Thus an
+For each iteration the entire system is evaluated, resulting in a
+considerable inefficiency in practice, requiring the repeated
+evaluation of many right-hand-sides for the same value. Thus an
 approach which can evaluate smaller portions of the system in each
 iteration would be a significant improvement.
 
 An additional deficiency of Kleene iteration is that it is not
 guaranteed to terminate for all fixpoints. An example system is
-presented in Figure \ref{fig:kleene-infinite}. In this case our first
-iteration will give us $\{ x \mapsto 0, y \mapsto 0 \}$, leading to a
-second iteration resulting in $\{ x \mapsto -1, y \mapsto 0\}$. This
-will continue without bound resulting 
-
-In some cases Kleene iteration must iterate an infinite number of
-times in order to reach a fixpoint. An example system is presented as
-Figure \ref{fig:kleene-infinite}. In this case $x$ will take the value
-of $0$ in the first iteration, then $y$ will evaluate to $-1$. In the
-next iteration $x$ will also take the value $-1$, thereby requiring
-$y$ to take the value $-2$. This will continue without bound,
-resulting in the Kleene iteration never reaching the greatest fixpoint
-of $\{ x \mapsto -\infty, y \mapsto -\infty \}$.
+presented in Figure \ref{fig:kleene-infinite}, where our first
+iteration will give $\{ x \mapsto 0, y \mapsto 0 \}$, leading to a
+second iteration resulting in $\{ x \mapsto -1, y \mapsto 0\}$. The
+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{align*}
@@ -226,25 +212,25 @@ significant problem in our application, however, as it has been shown
 in the work of Gawlitza et
 al.\cite{Gawlitza:2007:PFC:1762174.1762203}, that Kleene iteration in
 this specific case is restricted to at most $|X|$ iterations. It does,
-however, require $\Theta(|X|)$ right hand side evaluations, which is
+however, require $\Theta(|X|^3)$ right hand side evaluations, which is
 very inefficient.
 
 \subsection{W-DFS algorithm} \label{sec:wdfs}
 
-The W-DFS algorithm of Seidl et al.~takes into account some form of
-data-dependencies as it solves the system. This gives it the ability
-to leave portions of the system unevaluated when it is certain that
-those values have not changed. The algorithm is presented in Listing
-\ref{algo: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 it can leave portions of the system unevaluated when it
+is certain that those values have not changed. The algorithm is
+presented in Listing \ref{algo:wdfs}.
 
 \begin{algorithm}
   \begin{algorithmic}
     \Globals
     \begin{tabularx}{0.9\textwidth}{rX}
-      $D$ & $\in X \to \CZ$, a mapping from variables to their current
+      $D$ & $: X \to \CZ$, a mapping from variables to their current
       values \\
       
-      $\inflFP$ & $\in X \to 2^X$, a mapping from a variable to the
+      $\inflFP$ & $: X \to 2^X$, a mapping from a variable to the
       variables it \emph{may} influence \\
 
       $\stableFP$ & $\subseteq X$, a set of ``stable'' variables \\
@@ -300,11 +286,12 @@ those values have not changed. The algorithm is presented in Listing
   \label{algo:wdfs}
 \end{algorithm}
 
-The function $\init$ in Listing \ref{algo:wdfs:init} is of the type
-$\Systems \to (X \to D)$. It takes an equation system and returns a
-function to query the greatest fixpoint. Each fixpoint value is solved
-on demand and will only evaluate the subset of the equation system
-which is required to ensure the correct solution is found.
+The function $\init: \Systems \to (X \to D)$ in
+Listing \ref{algo:wdfs:init} takes an equation system as its argument
+and returns a function to query the greatest fixpoint. Each fixpoint
+value is solved on demand and will only evaluate the subset of the
+equation system which is required to ensure the correct solution is
+found.
 
 The algorithm performs no evaluation of any variables unless their
 value is requested (whether externally or internally). Once a value is
@@ -312,10 +299,10 @@ requested the right-hand-side is evaluated, which may in turn request
 the values of other variables (through the $\eval$ function).
 
 In the case of mutually-recursive variables this would result in
-infinite recursion, as each time the variable's value must be
-calculated it must first calculate its own value. In order to prevent
-this a $\stable$ set is maintained of variables whose values are
-either currently being computed or whose values have already been
+infinite recursion, as each time the variable's value is calculated we
+must first calculate the variable's value. In order to prevent this a
+$\stable$ set is maintained of variables whose values are either
+currently being computed or whose values have already been
 computed. This set provides a ``base'' for the recursion to terminate,
 at which point the value is simply looked up in $D$.
 
@@ -329,12 +316,7 @@ The W-DFS algorithm provides us with a \emph{local},
 \emph{demand-driven} solver for greatest fixpoints of monotonic
 fixpoint problems.
 
-Because each value is only computed when requested, the solver avoids
-calculating results which are irrelevant to the final outcome. To
-provide a more tangible example, consider the equation system
-presented in Figure \ref{fig:wdfs-example}.
-
-\begin{figure}
+\begin{figure}[H]
   \begin{align*}
     x &= \min(0, y) \\
     y &= x \\
@@ -348,22 +330,29 @@ presented in Figure \ref{fig:wdfs-example}.
   \label{fig:wdfs-example}
 \end{figure}
 
-It is clear by inspecting this system that it could be split into two
-equation systems, one consisting of $\{x, y\}$ and the other of $\{a,
-b, c, d, e\}$. In order to find the value of a variable in either of
-these sub-systems it is necessary to evaluate the entire sub-system,
-but it is not necessary to evaluate the other sub-system. So, for
-example, to find the value of $x$ in the greatest fixpoint it is
-unnecessary to find the value of the variable $d$.
-
-W-DFS, in this case, would only evaluate the sub-system containing the
-requested variable and would leave the other sub-system entirely
-unsolved until a variable within it has its value requested.
-
-This means that W-DFS can avoid evaluating a large portion of some
-equation systems, thereby making it a \emph{local} solver.
+Because each value is only computed when requested, the solver avoids
+calculating results which are irrelevant to the final outcome. To
+provide a more concrete example, consider the equation system
+presented in Figure \ref{fig:wdfs-example}. This equation system can
+be separated into two independent equation systems, one consisting of
+$\{x, y\}$ and the other of $\{a, b, c, d, e\}$. In order to find the
+value of a variable in either of these sub-systems it is necessary to
+evaluate the entire sub-system, but it is not necessary to evaluate
+the other sub-system. 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 untouched. In order to capture this property
+we will define the notion of a \emph{local} solver.
 
+\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}
 
+W-DFS provides us with a \emph{local}, \emph{demand-driven} solver for
+greatest-fixpoint problems.
 
 
 
@@ -371,26 +360,25 @@ equation systems, thereby making it a \emph{local} solver.
 
 The problem of $\max$-strategy iteration is trying to find a mapping
 $\sigma: E_{\max} \to E$ from each $\max$-expression to its greatest
-sub-expression. (We will also use $\sigma: \Systems \to \Systems$ as a
+sub-expression. We will use $\sigma: \Systems \to \Systems$ as a
 shorthand to denote the system obtained by replacing each
-$\max$-expression, $x$, in $\system$ with $\sigma(x)$.)
+$\max$-expression, $x$, in $\system$ with $\sigma(x)$.
 
 In the particular case of \emph{monotonic}, \emph{expansive} operators
 it has been shown\cite{Gawlitza:2007:PFC:1762174.1762203} that this
 process will take a finite number of iterations if we ensure at each
 iteration that we make a \emph{strict} improvement on our
 strategy. This means that each time we improve our strategy we must
-make it \emph{better} in at least one $\max$-expression, and no worse
-in the others.
+make it greater in at least one $\max$-expression, and no worse in the
+others.
 
 To this end a new function, $P_{\max}: ((E_{\max} \to E), (X \to D))
 \to (E_{\max} \to E)$, is used below as a ``strategy improvement
-operator''. It takes a $\max$-strategy and a variable assignment and
-returns a new $\max$-strategy which constitutes an `improvement' of
-the strategy in the variable assignment $\rho$.
-
-In more precise terms, if have a $\max$-strategy $\sigma$, a variable
-assignment $\rho$ and $\varsigma = P_{\max}(\sigma, \rho)$. Then:
+operator''. $P_{\max}$ takes a $\max$-strategy and a variable
+assignment and returns a new $\max$-strategy which constitutes an
+`improvement' of the strategy in the variable assignment $\rho$. If
+have a $\max$-strategy $\sigma$, a variable assignment $\rho$ and
+$\varsigma = P_{\max}(\sigma, \rho)$. Then:
 \begin{align*}
   \sigma(\system)(\rho) \le \varsigma(\system)(\rho)
 \end{align*}
@@ -438,13 +426,13 @@ the approach presented in Listing \ref{algo:naive-strategy}.
   \label{algo:naive-strategy}
 \end{algorithm}
 
-This approach is quite similar to that of Kleene iteration, but from
+This approach is quite similar to that of Kleene iteration, and from
 the results of Gawlitza et al.\cite{Gawlitza:2007:PFC:1762174.1762203}
-it is known that this iteration is guaranteed to terminate. It is
-still an inefficient way to solve this problem, however, for many of
-the same reasons as Kleene iteration. It may spend significant time
-attempting to improve strategies which can not have changed and thus
-may perform a significant amount of unnecessary work.
+it is known that this iteration is guaranteed to terminate. This naive
+approach is an inefficient way to solve this problem, however, for
+many of the same reasons as Kleene iteration. A large amount of time
+will be spent attempting to improve portions of the strategy for which
+no improvement can be made.
 
 \subsection{Adapted W-DFS algorithm} \label{sec:adapted-wdfs}
 
@@ -529,51 +517,60 @@ some of the $\max$-expressions which may influence it are changed.
 
 For this particular algorithm to work, however, we must assume another
 property of $P_{\max}$. In Listing \ref{algo:adapted-wdfs} we take the
-value of $P_{\max}(\lambda y . \eval(x, y), \rho)[x]$. That is:
-improve the strategy, then use only the strategy for $x$. In order for
-this algorithm to be correct $P_{\max}$ must always improve the
-strategy at $x$ if it is possible to do so.
+value of $P_{\max}(\lambda y . \eval(x, y), \rho)[x]$; we improve the
+strategy, then use only the strategy for $x$. In order for this
+algorithm to be correct $P_{\max}$ must always improve the strategy at
+$x$ if it is possible to do so. If $P_{\max}$ did not improve the
+strategy at $x$, while a permissible improvement existed, then we
+would consider $x$ to be ``stable'' and would not attempt to improve
+our strategy at $x$ until the improvement of another portion of our
+strategy invalidated $x$. It is not guaranteed that another strategy
+improvement will invalidate the strategy at $x$, however, so the
+strategy at $x$ may still be able to be improved when the algorithm
+terminates. If the strategy at $x$ can still be improved then we have
+not reached the solution of our $\max$-strategy iteration.
 
 Additionally, in order to remain efficient, $P_{\max}$ should not
 attempt to improve the strategy for any $\max$-expressions until that
-expression is requested. This will not affect the correctness of the
-algorithm, but will significantly improve the performance of it.
+expression is requested. Whether or not $P_{\max}$ is lazy in this way
+will not affect the correctness of the algorithm, as it will only
+result in the $\max$-strategy improvement at each step being more
+expensive. The extra work to improve other portions of the strategy
+will be discarded with only $P_{\max}(...)[x]$ being used.
 
 \section{Local Demand-driven Strategy Improvement (LDSI)}
 
 W-DFS can be used to speed up both the $\max$-strategy iteration and
 the fixpoint iteration as two independent processes, but each time we
-seek to improve our strategy we must compute at least a subset of the
-fixpoint from a base of no information. Ideally we would be able to
-provide some channel for communication between the two W-DFS instances
-to reduce the amount of work that must be done at each stage. By
-supplying each other with information about which parts of the system
-have changed we can jump in partway through the process of finding a
-fixpoint, thereby avoiding repeating work that we have already done
-when it is unnecessary to do so.
+seek to improve our strategy we compute at least a subset of the
+greatest fixpoint from a base of no information. We would like to be
+able to provide some channel for communication between the two W-DFS
+instances to reduce the amount of work that must be done at each
+stage. By supplying each other with information about which parts of
+the system have changed we can jump in partway through the process of
+finding a fixpoint, thereby avoiding repeating work that we have
+already done when it is unnecessary to do so.
 
 The new \emph{Local Demand-driven Strategy Improvement} algorithm,
 \emph{LDSI}, seeks to do this. By adding an ``invalidate'' procedure
 to the fixpoint iteration we provide a method for the $\max$-strategy
 to invalidate fixpoint variables, and we can modify the fixpoint
 iteration algorithm to report which variables it has modified with
-each fixpoint iteration step.
-
-This essentially results in a $\max$-strategy iteration which, at each
-strategy-improvement step, invalidates a portion of the current
-fixpoint iteration which may depend on the changed strategy. The
-fixpoint iteration then re-stabilises each variable as it is
-requested, tracking which values have changed since the last time they
-were stabilised. The $\max$-strategy iteration then uses this list of
-changed variables to determine which portions of the current strategy
-must be re-stabilised once more. This process continues until the
-$\max$-strategy stabilises (at which point the fixpoint will also
-stabilise).
+each fixpoint iteration step. We then have a $\max$-strategy iteration
+which, at each strategy-improvement step, invalidates a portion of the
+current fixpoint iteration which may depend on the changed
+strategy. The fixpoint iteration then re-stabilises each variable as
+it is requested, tracking which values have changed since the last
+time they were stabilised. The $\max$-strategy iteration then uses
+this list of changed variables to determine which portions of the
+current strategy must be re-stabilised once more. This process
+continues until the $\max$-strategy stabilises (at which point the
+fixpoint will also stabilise).
 
-This entire approach is \emph{demand driven}, and so any necessary
-evaluation of strategies or fixpoint values is delayed until the point
-when it is actually required. This means that the solver will be
-\emph{local}.
+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}).
 
 
 
@@ -582,24 +579,30 @@ when it is actually required. This means that the solver will be
 
 This algorithm is presented in three parts.
 
-Section \ref{sec:ldsi:top-level} presents the global state and entry
-point to the algorithm.
-
-Section \ref{sec:ldsi:fixpoint} presents the fixpoint portion of
-the algorithm. This portion bears many similarities to the W-DFS
-algorithm presented in Section \ref{sec:wdfs}, with a few
-modifications to track changes and allow external invalidations of
-parts of the solution.
-
-Section \ref{sec:ldsi:max-strategy} presents the $\max$-strategy portion
-of the algorithm. This portion is quite similar to the Adapted W-DFS
-algorithm presented in Section \ref{sec:adapted-wdfs}, with some
-modifications to allow for communication with the fixpoint portion of
-the algorithm.
-
-Section \ref{sec:ldsi:correctness} argues the correctness of this
-approach for finding the least fixpoints of monotonic, expansive
-equation systems involving $\max$-expressions.
+\begin{itemize}
+\item
+  Section \ref{sec:ldsi:top-level} presents the global state and entry
+  point to the algorithm.
+
+\item
+  Section \ref{sec:ldsi:fixpoint} presents the fixpoint portion of the
+  algorithm. This portion bears many similarities to the W-DFS
+  algorithm presented in Section \ref{sec:wdfs}, with a few
+  modifications to track changes and allow external invalidations of
+  parts of the solution.
+
+\item
+  Section \ref{sec:ldsi:max-strategy} presents the $\max$-strategy
+  portion of the algorithm. This portion is quite similar to the
+  Adapted W-DFS algorithm presented in Section \ref{sec:adapted-wdfs},
+  with some modifications to allow for communication with the fixpoint
+  portion of the algorithm.
+
+\item
+  Section \ref{sec:ldsi:correctness} argues the correctness of this
+  approach for finding the least fixpoints of monotonic, expansive
+  equation systems involving $\max$-expressions.
+\end{itemize}
 
 \subsection{Top level} \label{sec:ldsi:top-level}
 
@@ -680,14 +683,11 @@ functions presented in Sections \ref{sec:wdfs} and
 also initialised, as they was not present in either of the previous
 $\init$ functions.
 
-It is important to note, also, that $D$ and $D_\old$ are both
-initialised to \underline{$-\infty$} and $\stableFP$ is initially the
-entire set of variables. This is because we are beginning with a known
-strategy mapping every max expression to $-\infty$, so we already know
-that each fixpoint value must be stable at $-\infty$, so we can save
-an entire fixpoint iteration step by taking this into account. This
-state corresponds to an already complete fixpoint iteration with the
-given initial strategy.
+$D$ and $D_\old$ are both initialised to \underline{$-\infty$} and
+$\stableFP$ is initially the entire set of variables. The values of
+$D$, $D_\old$ and $\stableFP$ are set to their result after a complete
+fixpoint iteration over each variable with the initial
+$\max$-strategy.
 
 The type of this function is also different to either of the original
 $\init$ functions. $\init : \Systems \to (X \to \CZ)$. The function
@@ -701,12 +701,12 @@ each variable for the least fixpoint, returning a value in $\CZ$.
 
 The process of fixpoint iteration is extremely similar to the fixpoint
 iteration algorithm presented in Section \ref{sec:wdfs}. The only
-difference is that we have an $\invalidate \fixpoint$ procedure which
-allows the $\max$-strategy iteration to invalidate a portion of the
-system to ensure its value is recalculated by the fixpoint iteration
-process. The last stable value is also stored in this procedure to
-allow \emph{changed} values to be identified, not merely
-\emph{invalidated} ones.
+difference is that we have an $\invalidate \fixpoint$ procedure for
+the $\max$-strategy iteration to invalidate a portion of the
+system. By invalidating only a portion of the system we reuse the
+values which have already been computed to avoid performing additional
+work. The last stable value is also stored in this procedure to
+identify \emph{changed} values, rather than only \emph{unstable} ones.
 
 \begin{algorithm}[H]
   \begin{algorithmic}
@@ -722,12 +722,10 @@ allow \emph{changed} values to be identified, not merely
   \label{algo:ldsi:fixpoint:eval}
 \end{algorithm}
 
-This procedure is exactly the same as the equivalent method in the
-W-DFS algorithm, except for the fact that $\solve$ has been renamed to
-$\solve \fixpoint$. It allows us to track dependencies between
-fixpoint variables by injecting this function as our variable-lookup
-function. It then both calculates a new value for the variable (the
-$\solve \fixpoint$ call) and notes the dependency between $x$ and $y$.
+This procedure is similar to the equivalent method in the W-DFS
+algorithm, except for the fact that $\solve$ has been renamed to
+$\solve \fixpoint$. $\eval \fixpoint$ performs exactly the same
+function as the $\eval$ function in Figure \ref{algo:wdfs}.
 
 \begin{algorithm}[H]
   \begin{algorithmic}
@@ -753,11 +751,13 @@ $\solve \fixpoint$ call) and notes the dependency between $x$ and $y$.
 
 This procedure is not called in the fixpoint iteration process, but is
 rather the method by which the $\max$-strategy iteration can
-communicate with the fixpoint-iteration. It allows the $\max$-strategy
-iteration to inform the fixpoint-iteration which values have changed
-and will require re-evaluation. This makes it possible to only
-re-evaluate a partial system (the solving of which is also be delayed
-until requested by the $\solve \fixpoint$ procedure).
+communicate with the fixpoint-iteration. A call to $\invalidate
+\fixpoint$ indicates to the fixpoint-iteration that a variable's value
+\emph{may} have changed as a result of a $\max$-strategy improvement,
+and that it will require re-calculation. The invalidation provided by
+this procedure permits us to only re-evaluate a partial system (the
+solving of which is also be delayed until requested by the $\solve
+\fixpoint$ procedure).
 
 While invalidating variables we also note their $\old$ value, and mark
 them as ``touched''. As the $\old$ value is only set in this
@@ -794,13 +794,13 @@ us from doing extra work in the $\max$-strategy iteration phase.
 
 The $\solve \fixpoint$ procedure is extremely similar to the $\solve$
 procedure presented in Listing \ref{algo:wdfs}. There are two main
-differences: the self-recursive call has been renamed (to reflect the
-change in the function's name), and instead of using $\system[x]$ we
-must use $\sigma(\system[x])$. The use of $\sigma$ is to ensure that
-the fixpoint is solving the variable using the current
-$\max$-strategy. This $\max$-strategy is stable for the duration of
-the $\solve \fixpoint$ execution, so it will result in fixpoint
-iteration being performed over a stable system.
+differences: the self-recursive call has been renamed to reflect the
+change in the function's name, and instead of using $\system[x]$ we
+must use $\sigma(\system[x])$. We use $\sigma$ to provide the
+fixpoint-iteration with the current $\max$-strategy. $\sigma$ is
+stable for the duration of the $\solve \fixpoint$ execution, so it
+will result in fixpoint iteration being performed over a stable
+system.
 
 After an evaluation of the $\solve \fixpoint$ procedure, the variable
 $x$ will have its value in the current $\max$-strategy's greatest