summaryrefslogtreecommitdiff
path: root/tex/thesis/contribution
diff options
context:
space:
mode:
authorCarlo Zancanaro <carlo@carlo-laptop>2012-11-19 10:34:25 +1100
committerCarlo Zancanaro <carlo@carlo-laptop>2012-11-19 10:34:25 +1100
commitcd087d4597ec8119f8a25271797589db15c25b9e (patch)
tree9782bd446f2b12e7f080693f4ea42d5ba2b5dd00 /tex/thesis/contribution
parent409251d3b24b19ee39c84816bb8b3c562c2bdebe (diff)
Thesis stuff. Contribution & lit review.
Diffstat (limited to 'tex/thesis/contribution')
-rw-r--r--tex/thesis/contribution/contribution.tex360
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}