Thesis stuff. Contribution & lit review.

1 files changed, 226 insertions, 134 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 44e5e7d..e41a39f 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -1,9 +1,11 @@
 \floatname{algorithm}{Listing}
 
 \newcommand\inflFP{\mathsf{infl^{FP}}}
+\newcommand\depFP{\mathsf{dep^{FP}}}
 \newcommand\stableFP{\mathsf{stable^{FP}}}
 \newcommand\touchedFP{\mathsf{touched^{FP}}}
 \newcommand\inflSI{\mathsf{infl^{SI}}}
+\newcommand\depSI{\mathsf{dep^{SI}}}
 \newcommand\stableSI{\mathsf{stable^{SI}}}
 
 \newcommand\stable{\mathsf{stable}}
@@ -15,8 +17,14 @@
 \newcommand\best{\mathsf{best}}
 \newcommand\all{\mathsf{all}}
 
+\newcommand\fix{\mathsf{fix}}
+\newcommand\soln{\mathsf{soln}}
+
+\newcommand\post{\mathsf{post}}
+\newcommand\pre{\mathsf{pre}}
+
 \newcommand\Operators{\mathcal{O}}
-\newcommand\Systems{\varepsilon}
+\newcommand\Systems{\mathbb{E}}
 
 \newcommand\improve{\mathsf{\textsc{improve}}}
 \newcommand\init{\mathsf{\textsc{init}}}
@@ -32,7 +40,7 @@
 \algblockdefx[ReturnLambdaFn]{ReturnLambdaFn}{EndReturnLambdaFn}[1]{\textbf{return function} (#1)}{\textbf{end function}}
 
 
-\chapter{Contribution} \label{chap:contribution}
+\chapter{Demand-driven strategy improvement} \label{chap:contribution}
 
 In this chapter the main theoretical contribution of this thesis is
 presented: an extension on a $\max$-strategy iteration algorithm for
@@ -56,14 +64,10 @@ operations consists of naively ``evaluating'' the system repeatedly
 until a further evaluation results in no change. Gawlitza et
 al.~proved that these iterations must converge in a finite number of
 steps\cite{Gawlitza:2007:PFC:1762174.1762203} , but in practice this
-naive approach performs many more operations than are necessary, in
-many cases re-calculating results which are already known.
+naive approach performs a large number of re-calculations of results
+which are already known.
 % TODO: add something here about variable dependencies
 
-%By considering which variables depend on, and influence, each other it
-%is possible to reduce the amount of work that is to be done quite
-%considerably.
-
 \section{Preliminaries}
 
 In order to aid our explanation of these algorithms we will now define
@@ -71,41 +75,48 @@ a few terms and notations. We will assume a fixed, finite set $X$ of
 variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
 
 \begin{definition}
-  A \textbf{Variable Assignment} is a partial function, $\rho: X \to
-  \CZ$, from a variable to a value. The domain of a variable
+  A \textbf{variable assignment} is a partial function, $\rho: X \to
+  \CZ$ that maps variables to values. The domain of a variable
   assignment, $\rho$, is represented by $\mathsf{domain}(\rho)
-  \subseteq X$.
-
-  An underlined value, $\underline{a}$ indicates a variable assignment
-  $\{ x \mapsto a \mid \forall x \in X \}$.
-
-  Variable assignments $\rho \in X \to \CZ$ and $\varrho \in X \to
-  \CZ$ may be composed with the $\oplus$ operator in the following
-  way:
+  \subseteq X$. An underlined value, $\underline{a}$, indicates a
+  variable assignment $\{ x \mapsto a \mid \forall x \in X \}$.
 
+  Variable assignments $\rho : X \to \CZ$ and $\varrho : X \to \CZ$
+  may be composed with the $\oplus$ operator in the following way:
   \begin{align*}
-    \rho \oplus \varrho = \left\{\begin{array}{lc}
+    (\rho \oplus \varrho)(x) = \left\{\begin{array}{lc}
         \varrho(x) & x \in \mathsf{domain}(\varrho) \\
         \rho(x) & \mbox{otherwise}
-      \end{array}\right.
+      \end{array}\right., \forall x \in X
   \end{align*} 
 \end{definition}
 
 \begin{definition}
-  \textbf{Expressions:} We will consider expressions, $e \in E$, as $e
-  : (X \to \CZ) \to \CZ$, a mapping from a variable assignment to the
-  expression's value in that assignment.
+  \textbf{Expressions:} 
 
-  Expressions have three possible forms:
+  The class of expressions, $E$, is defined inductively:
   \begin{itemize}
     \item
-      $e = f( e_1, e_2, ..., e_k )$, \\
-      with $f: \CZ^k \to \CZ$ and
-      $e_1, e_2, ... e_k \in E$ and $e(\rho) = f(e_1(\rho),
-      e_2(\rho), ..., e_k(\rho))$
-    \item $e = x \in X$, with $e(\rho) = \rho(x)$
-    \item $e = z \in \CZ$, with $e(\rho) = z$
+      If $z \in \CZ$ then $z \in E$
+    \item
+      If $x \in X$ then $x \in E$
+    \item
+      If $f : \CZ^k \to \CZ$ and $e_1,...,e_k \in E$ then
+      $f(e_1,...,e_k) \in E$
+    \item
+      Nothing else is in E.
   \end{itemize}
+
+  We then define the semantics of these expressions by:
+  \begin{align*}
+    \llb z \rrb &= \lambda \rho . z  & \forall z \in \CZ \\
+    \llb x \rrb &= \lambda \rho . \rho(x) & \forall x \in X \\
+    \llb f(e_1,...,e_k) \rrb &=
+      \lambda \rho . f(\llb e_1 \rrb(\rho),...,\llb e_k \rrb(\rho))
+  \end{align*}
+
+  By abusing our notation we will consider expressions, $e \in E$, as
+  $e : (X \to \CZ) \to \CZ$ defined by $e = \llb e \rrb$.
   
   The subset of expressions of the form $\max\{ e_1, e_2, ... e_k \}$,
   with $e_1, e_2, ..., e_k \in E$ are referred to
@@ -119,16 +130,20 @@ 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_\system$, where
-  $E_\system \subset E$. As each element of $E$ is also a function $(X
-  \to \CZ) \to \CZ$, so an equation system can be considered as a
-  function $\system : X \to ((X \to \CZ) \to \CZ)$ (which is
-  equivalent to the above).
+  variables to expressions. $\system : X \to E$. We define
+  $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
+  ((X \to \CZ) \to \CZ)$ (which is equivalent to the above).
 
   Alternatively an equation system can be represented as a function
   $\system : (X \to \CZ) \to (X \to \CZ)$, $\system(\rho)[x] =
   e_x(\rho)$, taking a variable assignment $\rho$ and returning the
-  result of each $e_x$'s evaluation in $\rho$.
+  result of each $e_x$'s evaluation in $\rho$. We use this second form
+  as a convenience for when we are evaluating the entire equation
+  system in the context of a variable assignment: we get a new value
+  for each variable and thus a new variable assignment as a result.
 
   These two functional forms are equivalent and correspond to changing
   the argument order in the following way: $\system(\rho)[x] =
@@ -192,7 +207,7 @@ algorithm is presented in Listing \ref{algo:kleene}.
 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
+approach which evaluates smaller portions of the system in each
 iteration would be a significant improvement.
 
 An additional deficiency of Kleene iteration is that it is not
@@ -215,20 +230,20 @@ x \mapsto -\infty, y \mapsto -\infty \}$.
   \label{fig:kleene-infinite}
 \end{figure}
 
-This particular non-termination of Kleene iteration is not a
-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|^3)$ right hand side evaluations, which is
-very inefficient.
+It has been shown by Gawlitza et
+al.\cite{Gawlitza:2007:PFC:1762174.1762203} that Kleene iteration is
+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.
 
 \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 it can leave portions of the system unevaluated when it
-is certain that those values have not changed. The algorithm is
+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}
@@ -302,9 +317,9 @@ 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
+value is requested, whether externally or internally. Once a value is
 requested the right-hand-side is evaluated, which may in turn request
-the values of other variables (through the $\eval$ function).
+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 is calculated we
@@ -360,8 +375,8 @@ fixpoint problems.
       \end{minipage}
     };
 
-    \draw[->] (full) -- (first);
-    \draw[->] (full) -- (second);
+    \draw (full) -- (first.west);
+    \draw (full) -- (second.west);
   \end{tikzpicture}
   \caption{Example of an equation system which can be separated into
     two independent sub-systems}
@@ -412,25 +427,25 @@ strategy. This means that each time we improve our strategy we must
 make it greater in at least one $\max$-expression, and no worse in the
 others.
 
-To this end a new function, $\improve: ((E_{\max} \to E) \times
-(X \to D)) \to (E_{\max} \to E)$, is used below as a \emph{strategy
-  improvement operator}. $\improve$ 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 = \improve(\sigma,
-\rho)$. Then:
+A new function, $\improve: ((E_{\max} \to E) \times (X \to D)) \to
+(E_{\max} \to E)$, is used below as a \emph{strategy improvement
+  operator}. $\improve$ 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 = \improve(\sigma, \rho)$. Then
 \begin{align*}
   \sigma(\system)(\rho) \le \varsigma(\system)(\rho)
 \end{align*}
 
-If it is possible for $\sigma$ to be improved then $\improve$ will
-return an improvement, otherwise it will return $\sigma$
-unchanged. One possible implementation of $\improve$ is presented in
-Listing \ref{algo:pmax}. It will try every option of subexpressions
-for this $\max$-expression and will then return the best. The use of
-an anonymous function as the returned strategy is so the evaluation of
-each strategy is only done when requested.
+If there is a possible improvement to be made on $\sigma$ then
+$\improve$ will return an improvement, otherwise it will return
+$\sigma$ unchanged. One possible implementation of $\improve$ is
+presented in Listing \ref{algo:pmax}. This implementation will try
+every option of subexpressions for this $\max$-expression and will
+then return the best. The use of an anonymous function as the returned
+strategy is so the evaluation of each strategy is only done when
+requested.
 
 \begin{algorithm}
   \begin{algorithmic}
@@ -495,10 +510,9 @@ the approach presented in Listing \ref{algo:naive-strategy}.
 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. 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.
+approach is inefficient, however, in the same way 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}
 
@@ -576,10 +590,11 @@ solve $\max$-strategy iteration problems.
 \end{algorithm}
 
 This approach retains the benefits of the W-DFS algorithm for solving
-fixpoints, but applies them to $\max$-strategy iteration problems. It
-will take into account dependencies between the $\max$-expressions and
-only attempt to improve the strategy for a given $\max$-expression if
-some of the $\max$-expressions which may influence it are changed.
+fixpoints, but applies them to $\max$-strategy iteration
+problems. Dependencies between $\max$-expressions are considered and
+an improvement on the strategy at an expression $e$ is only attempted
+if some of the $\max$-expressions which influence $e$ themselves
+improve strategy.
 
 For this particular algorithm to work, however, we must assume another
 property of $\improve$. In Listing \ref{algo:adapted-wdfs} we take the
@@ -611,16 +626,16 @@ satisfies this property by way of its anonymous function.
 
 \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 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.
+W-DFS speeds up both the $\max$-strategy iteration and the fixpoint
+iteration as two independent processes, but each time we 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
@@ -760,7 +775,7 @@ $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
+The type of this function is different to either of the original
 $\init$ functions. $\init : \Systems \to (X \to \CZ)$. The function
 returned by $\init$ performs the entire process of $\max$-strategy
 iteration and fixpoint iteration and calculates the final value of
@@ -770,14 +785,14 @@ each variable for the least fixpoint, returning a value in $\CZ$.
 
 \subsection{Fixpoint iteration} \label{sec:ldsi:fixpoint}
 
-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 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.
+The process of fixpoint iteration is similar to the fixpoint iteration
+algorithm presented in Section \ref{sec:wdfs}. The only 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 stored in this procedure to identify
+\emph{changed} values, rather than only \emph{unstable} ones.
 
 \begin{algorithm}[H]
   \begin{algorithmic}
@@ -795,8 +810,8 @@ identify \emph{changed} values, rather than only \emph{unstable} ones.
 
 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 Listing \ref{algo:wdfs}.
+$\solve \fixpoint$. $\eval \fixpoint$ performs the same function as
+the $\eval$ function in Listing \ref{algo:wdfs}.
 
 \begin{algorithm}[H]
   \begin{algorithmic}
@@ -827,15 +842,15 @@ communicate with the fixpoint-iteration. A call to $\invalidate
 \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).
+solving of which is delayed until requested by the $\solve \fixpoint$
+procedure).
 
-While invalidating variables we also note their $\old$ value, and mark
+While invalidating variables we store their $\old$ value, and mark
 them as ``touched''. As the $\old$ value is only set in this
 procedure, and only when $x$ is stable, it gives us the ability to see
 whether a variable has stabilised to a new value, or whether it has
-merely re-stabilised to the same value as last time. This can prevent
-us from doing extra work in the $\max$-strategy iteration phase.
+merely re-stabilised to the same value as last time. This refines the
+set of changed variables for the $\max$-strategy iteration phase.
 
 
 
@@ -863,11 +878,11 @@ us from doing extra work in the $\max$-strategy iteration phase.
   \label{algo:ldsi:fixpoint:solve}
 \end{algorithm}
 
-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])$. We use $\sigma$ to provide the
+The $\solve \fixpoint$ procedure is 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])$. 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
@@ -901,9 +916,9 @@ being stabilised.
           \For {$w \in \inflSI[\strategy(\system[v])]$}
             \State $\invalidate \strategy(\system[v])$
           \EndFor
+          \State $\touchedFP = \touchedFP \backslash \{v\}$
         \EndIf
       \EndFor
-      
       \State \Return $D[y]$
     \EndFunction
   \end{algorithmic}
@@ -988,38 +1003,115 @@ themselves destabilised as well.
 
 \subsection{Correctness} \label{sec:ldsi:correctness}
 
-To argue the correctness of our LDSI algorithm we will first establish
-some invariants, after which it should be much easier to see why our
-algorithm is correct.
-
-%\begin{invariant}
-First of all $\fixpoint \solve$. 
-%\end{invariant}
-
-In order to argue that LDSI is correct we must first assume that the
-W-DFS algorithm of Seidl et al.~is correct and will solve the equation
-system for its least/greatest fixpoint.
-
-
-
+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, $\soln(s) : X \to D$ for the system $s
+= \sigma(\system)$. If we consider all valid fixpoints, $\fix(s) = \{
+\rho \mid \rho = s(\rho) \}$, then we find that $\soln(s) \in \fix(s)$
+and $\soln(s) \ge \rho ~ \forall \rho \in \fix(s)$. Our general
+approach will be to consider our variable assignment $D \ge \soln(s)$
+and show that it decreases until $D \in \fix(s)$ and thus $D =
+\soln(s)$.
+
+We begin by stating two invariants of the LDSI algorithm. The set
+$\depFP^{+}(x)$ is the set of all variables which $x$ may depend
+on. $\depFP^{+}$ is defined as the transitive closure of $\depFP$,
+which is defined by $\depFP(x) = \{ y \in X \mid x \in \inflFP(y)
+\}$. $R \subseteq X$ is defined as the variables currently on our
+recursion stack.
+\begin{align}
+  D &\ge \soln(s) \label{eqn:fp-inv1} \\
+%
+  D &= \soln(s)[x] & \mbox{if }
+      x \in \stableFP,
+      x \not \in R,
+      \depFP^{+}(x) \cap R = \emptyset
+    \label{eqn:fp-inv2} \\
+%
+  x \in \inflFP[y] & \forall x \in \stableFP, y \in \depFP(x)
+    \label{eqn:fp-inv3}
+\end{align}
+
+(\ref{eqn:fp-inv1}) follows from monotonicity. We begin our iteration
+at some variable assignment $D \ge \soln(s)$ and monotonically descend
+from there. Each evaluation of a variable remains greater than
+$\soln(s)[x]$ because our variable assignment $D$ always satisfies $D
+\ge soln(s)$. We cannot jump below the greatest fixpoint because to do
+so would imply that we could ``turn around'' for at least one
+variable, thereby breaking our monotonicity assumption.
+
+For (\ref{eqn:fp-inv2}) we will examine what has happened when each of
+the conditions is false:
+\begin{itemize}
+\item
+  If $x \not \in \stableFP$ then a re-evaluation of $x$ will occur
+  with the next call to $\solve \fixpoint(x)$. This may result in a
+  change to the value of $D[x]$, or it may leave $D[x]$ stable for the
+  moment. In either case, the value of $D[x]$ will be decreased, given
+  the value of the other variables in $X \backslash {x}$. If we denote
+  the variable assignment before the evaluation of $x$ by $D_{\pre}$,
+  and the variable assignment after the evaluation of $x$ by
+  $D_{\post}$ then we find that $D_{\post} \le D_{\pre}$.
 
-This algorithm relies on the correctness of the underlying W-DFS
-algorithm. This algorithm was presented in
-\cite{DBLP:tr/trier/MI96-11}.
+\item
+  If $\depFP^{+}(x) \cap R \ne \emptyset$ then a variable which $x$
+  depends on is in $R$ at the moment. This will result in the
+  re-evaluation of $x$ if the value of any of the variables in
+  $\depFP^{+}(x) \cap R$ have changed.
 
-If we assume that W-DFS is correct then we only have to prove that the
-combination algorithm is correct. For this it is sufficient to show
-that the invalidate calls in both directions preserve the correctness
-of the original algorithm.
+\item
+  If $x \in R$ then we are currently in the context of an earlier
+  evaluation of $x$, so the value of $D[x]$ will be changed again by
+  that earlier call. In addition, we conclude that $x \in
+  \depFP^{+}(x)$ and thus, from the previous condition, that $x$ will
+  be entirely re-evaluated at some point after this one.
+\end{itemize}
 
-The fixpoint iteration step invalidates anything that \emph{might}
-depend on $x$ while it invalidates $x$, thereby ensuring that any
-further calls to $\solve \fixpoint$ will result in a correct value for
-the given strategy.
+(\ref{eqn:fp-inv3}) follows from the use of the $\eval \fixpoint$
+function. Each variable lookup results in a direct insertion into
+$\inflFP$, so during the evaluation of $x$ all relevant $\inflFP$ sets
+are updated.
+
+After an evaluation of $\solve \fixpoint(x)$ we know that $x \in
+\solve \fixpoint(x)$. If it is also the case that $R = \emptyset$, as
+is the case for top-level calls to $\solve \fixpoint$, then we know
+that $D[x] = \soln(s)[x]$. This means that a function $\lambda x
+. (\solve \fixpoint(x); D[x])$ will act as a variable assignment
+solving for the greatest fixpoint of $s = \sigma(\system)$, as is
+required by our $\max$-strategy iteration. As the $\max$-strategy
+iteration changes $\sigma$ it also induces a change in $s =
+\sigma(\system)$, so in order to maintain the correctness of this
+algorithm we must show that our above are maintained by this process.
+
+When the $\max$-strategy iteration portion invalidates a part of the
+fixpoint iteration it does two things: it removes the variable $x$
+from the $\stableFP$ set, and it sets $D[x] = \infty$. The
+invalidation of variables is then propagated to each variable which
+transitively depends on $x$: $\{ y \in X \mid x \in \depFP^{+}(y) \}$,
+or $\{ y \in X \mid y \in \inflFP^{+}(x) \}$, where $\inflFP^{+}$ is
+the transitive closure of $\inflFP$. We know from (\ref{eqn:fp-inv3})
+that this transitive closure of $\inflFP$ will identify the entire
+subsystem which may depend on the value of $x$. The invalidation of
+transitive dependencies ensures that (\ref{eqn:fp-inv1}) and
+(\ref{eqn:fp-inv2}) hold for the entire subsystem which is affected by
+the change in strategy, and thus that our invariants hold for our
+entire system.
+
+This is sufficient for us to be confident that the fixpoint iteration
+portion of the algorithm is correct. The invariants ensure that $D$ is
+approaching $\soln(s)$ and we know that our invariants are maintained
+by the $\max$-strategy invalidating the fixpoint iteration.
+
+
+
+We move now to the $\max$-strategy iteration.
+% TODO: finish the proof
 
-The strategy-iteration step invalidates anything that \emph{might}
-depend on $\system[x]$ while it invalidates $x$, thereby ensuring that
-any further calls to $\solve \strategy$ will result in a correct value
-for the given strategy.
 
 \subsection{Implementation} \label{sec:ldsi:implementation}