Remove _var_influence and do some writeup

_var_influence was really just duplicating data that was available
elsewhere, so I got rid of it.

I also did some writing about the algorithm and stuff for the thesis.

2 files changed, 159 insertions, 67 deletions

diff --git a/tex/thesis/Makefile b/tex/thesis/Makefile
index 5022129..ee64d9e 100644
--- a/tex/thesis/Makefile
+++ b/tex/thesis/Makefile
@@ -11,6 +11,11 @@ pdf: clean
 	pdflatex $(PROJ)
 	pdflatex $(PROJ)
 
+remote:
+	rsync -r * honours:honours/tex/thesis/
+	ssh honours "cd honours/tex/thesis; make"
+	rsync honours:honours/tex/thesis/thesis.pdf .
+
 wc:
 	wc `find . -name "*.tex"`
 
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 7d12299..66d5b4a 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -134,7 +134,7 @@ $O(n^3)$ right-hand-sides, and thus an approach which can evaluate
 smaller portions of the system in each iteration would be a
 significant improvement.
 
-\subsection{W-DFS algorithm}
+\subsection{W-DFS algorithm} \ref{sec:wdfs}
 
 The W-DFS algorithm presented by Seidl, et al. takes into account some
 form of data-dependencies as it solves the system. This gives it the
@@ -255,7 +255,7 @@ problem it is possible
 \end{algorithm}
 
 
-\subsection{Adapted W-DFS algorithm}
+\subsection{Adapted W-DFS algorithm} \ref{sec:adapted-wdfs}
 
 This, then, allows us to use the W-DFS algorithm to re-evaluate only
 those parts of the strategy which have changed. Listing
@@ -327,17 +327,26 @@ be evaluated.
 The new \emph{Local Demand-driven Strategy Improvement} algorithm,
 \emph{LDSI}, seeks to do this. By adding an ``invalidate''
 function to both W-DFS instances we provide an interface for the two
-sides of the algorithm to indicate which values have changed. The
-fixpoint-iteration operation can then be provided with a ``stabilise''
-function to solve a partially-unstable system.
+sides of the algorithm to indicate which values have changed and
+``destabilise'' that portion of the system.
 
 This essentially results in a $\max$-strategy iteration which, at each
 strategy-improvement step, invalidates a portion of the current
-fixpoint iteration. The fixpoint iteration then re-stabilises itself
-by evaluating what values have been changed before returning control
-to the $\max$-strategy iteration to change the system again. The back
-and forth continues in this way until the $\max$-strategy can not
-improve the strategy any further.
+fixpoint iteration which may depend on the changed strategy. The
+fixpoint iteration then re-stabilises itself by evaluating what values
+have been changed, but only when such values are requested by the
+$\max$-strategy iteration. The $\max$-strategy can continue as normal,
+invalidating the fixpoint-iteration as required, and simply assume
+that the fixpoint-iteration will provide it with the correct values
+from the greatest fixpoint.
+
+
+This entire approach is demand driven, and so any necessary evaluation
+is delayed until the point when it is actually required. Additionally,
+if it is not necessary to evaluate a particular right hand side in
+order to make a decision then the algorithm will attempt to avoid
+evaluating it.
+
 
 
 
@@ -356,23 +365,23 @@ correctness of this new algorithm is argued in
   \begin{algorithmic}
     \Globals
     \begin{tabularx}{0.9\textwidth}{rX}
-      $V$ & $\{X \to \D\}$ - a mapping from variables to values,
+      $D$ & $X \to \D$ - a mapping from variables to values,
       starting at $\{ x \mapsto \infty \}$ \\
 
-      $I_{X,X}$ & $\{X \to X\}$ - a mapping from a variable to the
+      $\sigma$ & $E_{\max} \to E$ - a mapping from $\max$-expressions
+      to their sub-expressions (a $\max$-strategy) \\
+
+      $I_{X,X}$ & $X \to X$ - a mapping from a variable to the
       variables it influences \\
 
-      $I_{\max,\max}$ & $\{E_{\max} \to E_{\max}\}$ - a mapping from a
+      $I_{\max,\max}$ & $E_{\max} \to E_{\max}$ - a mapping from a
       $\max$-expression to the $\max$-expressions it influences \\
 
-      $I_{X,\max}$ & $\{X \to E_{\max}\}$ - a mapping from a variable
-      to the $\max$-expressions it influences \\
-
       $U_{X}$ & The set of all variables whose values have not
       stabilised to a final fixpoint value (unstable variables) \\
 
-      $U_{\max}$ & The set of all $\max$ expressions whose strategies
-      have not yet stabilised to their final strategy (unstable
+      $S_{\max}$ & The set of all $\max$ expressions whose strategies
+      have stabilised to their final strategy (stable
       $\max$-expressions) \\
 
       $\varepsilon$ & The equation system, a mapping from a variable
@@ -384,12 +393,27 @@ correctness of this new algorithm is argued in
   \label{algo:ldsi:fixpoint:globals}
 \end{algorithm}
 
+A few things are of particular note for the global variables. In
+particular the difference between $U_X$ being an unstable set and
+$S_{\max}$ being a stable set. In reality these two are entirely
+equivalent, but because the fixpoint-iteration will be started as
+being entirely ``stable'' (with values of $-\infty$) it is of more
+practical benefit to avoid the extra work populating the ``stable''
+set by instead storing unstable values.
+
+The other variables are just the state from each of the previous
+algorithms for intelligently performing $\max$-strategy iteration and
+fixpoint iteration (as were presented in Sections \ref{sec:wdfs}
+and \ref{sec:adapted-wdfs}). $D$ and $I_{X,X}$ are taken from the
+W-DFS algorithm, while $\sigma$ and $I_{\max,\max}$ are taken from the
+Adapted W-DFS algorithm.
+
 
 
 
 \begin{algorithm}[H]
   \begin{algorithmic}
-    \Function {evalfixpoint} {$x$, $y$}
+    \Function {evalfixpoint} {$x \in X$, $y \in X$}
       \State $\solve \fixpoint(y)$
       \State $I_{X,X}[y] = I_{X,X}[y] \cup \{x\}$
       \State \Return $D[y]$
@@ -399,9 +423,17 @@ correctness of this new algorithm is argued in
   \label{algo:ldsi:fixpoint:eval}
 \end{algorithm}
 
+This procedure is exactly the same as the equivalent method in the
+W-DFS algorithm. It allows us to more easily 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$.
+
 \begin{algorithm}[H]
   \begin{algorithmic}
-    \Function {invalidatefixpoint} {$x$}
+    \Function {invalidatefixpoint} {$x \in X$}
+    \Comment{Invalidate a fixpoint variable}
     \If {$x \not \in U_X$}
       \State $U_X = U_X \cup \{x\}$
       \State $D[x] = \infty$
@@ -418,6 +450,16 @@ correctness of this new algorithm is argued in
   \label{algo:ldsi:fixpoint:invalidate}
 \end{algorithm}
 
+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).
+
+
+
 \begin{algorithm}[H]
   \begin{algorithmic}
     \Function {solvefixpoint} {$x$}
@@ -425,7 +467,7 @@ correctness of this new algorithm is argued in
     \If {$x \in U_X$}
       \State $f = \system[x]$
       \State $U_X = U_X \backslash \{x\}$
-      \State $v = f( \lambda y . \eval(x, y) )$
+      \State $v = \sigma(\system[x])( \lambda y . \eval \fixpoint(x, y) )$
       \If {$v \ne D[x]$}
         \State $D = \{ x \mapsto v \} \oplus D$
         \State $W = I_{X,X}[x]$
@@ -446,62 +488,110 @@ correctness of this new algorithm is argued in
 
 After an evaluation of the $\solve \fixpoint$ procedure, the variable
 supplied as its argument will have been stabilised within the current
-$\max$-strategy.
+$\max$-strategy. This means that it will have taken on the same value
+as it would take in the greatest fixpoint of this system. Because the
+$\solve \fixpoint$ calls need not be made immediately it's possible
+for a variable to be invalidated by several $\max$-strategy
+improvements without being re-evaluated.
+
 
-After an evaluation of the $\stabilise \fixpoint$ procedure all
-currently ``unstable'' variables in the current fixpoint will be
-solved. This correlates to performing an entire fixpoint-iteration for
-the greatest-fixpoint of the unstable portion of the equation
-system. This is meant to be used to perform a sufficient
-fixpoint-iteration to allow for the next $\max$-strategy improvement
-step, but this relies on the $\max$-strategy solver to correctly
-invalidate the fixpoint-iteration portion of the algorithm.
 
 
 \begin{algorithm}[H]
   \begin{algorithmic}
-    \Function {evalstrategy} {$x$, $y$}
-    \Comment{Evaluate $y$ for its value and note that when $y$
-      changes, $x$ must be re-evaluated}
-      \State $\solve(y)$
-      \State $I[y] = I[y] \cup \{x\}$
+    \Function {evalstrategy} {$x \in E_{\max}$, $y \in E_{\max}$}
+      \Comment{Evaluate $y$ for its value and note that when $y$
+        changes, $x$ must be re-evaluated}
+      \State $\solve \strategy(y)$
+      \State $I_{\max,\max}[y] = I_{\max,\max}[y] \cup \{x\}$
       \State \Return $\sigma[y]$
     \EndFunction
+    \Function {evalstrategyfixpoint} {$x \in E_{\max}$, $y \in X$}
+      \Comment{Evaluate $y$ for its value and note that when $y$
+        changes, $x$ must be re-evaluated}
+      \State $\solve \fixpoint(y)$
+      \State $I_{\max,\max}[y] = I_{\max,\max}[\system[y]] \cup \{x\}$
+      \State \Return $D[y]$
+    \EndFunction
+  \end{algorithmic}
+  \label{algo:ldsi:strategy:eval}
+  \caption{Evaluate a portion of the $\max$-strategy and note a
+    dependency}
+\end{algorithm}
+
+The $\eval \strategy$ function is essentially the same as the $\eval
+\fixpoint$ function, except that it notes the dependencies in a
+different variable, $I_{\max,\max}$. This is because the dependency
+information for the $\max$-strategy iteration is entirely separate to
+that of the fixpoint iteration.
+
+The $\solve \fixpoint$ calls in $\eval \strategy \fixpoint$ are
+top-level calls, meaning that upon their return we know that $D$
+contains the value it would take in the greatest fixpoint of the
+current strategy $\sigma$. This function, therefore, acts as a simple
+intermediate layer between the fixpoint-iteration and the
+$\max$-strategy iteration to allow for dependencies to be tracked.
 
+
+\begin{algorithm}[H]
+  \begin{algorithmic}
     \Function {invalidatestrategy} {$x \in X$} \Comment{$x$ is a
         \emph{variable}}
-      \If {$x \not \in U_X$}
-        \State $U_X = U_X \cup \{x\}$
-        \State $W = I[x]$
-        \State $I[x] = \emptyset$
-        \For {$v \in W$}
-          \State $\invalidate \fixpoint(v)$
+      \For {$v \in I_{\max,\max}(\system[x])$} \Comment{$v$ is
+        influenced by $x$}
+        \State $\invalidate \strategy (v)$
+      \EndFor
+    \EndFunction
+
+    \Function {invalidatestrategy} {$x \in E_{\max}$} \Comment{$x$ is
+      a \emph{$\max$-expression}}
+      \If {$x \in S_{\max}$}
+        \State $S_{\max} = S_{\max} \backslash \{x\}$
+        \For {$v \in I_{\max,\max}$} \Comment {$v$ is influenced by $x$}
+          \State $\invalidate \strategy (v)$
         \EndFor
       \EndIf
     \EndFunction
+  \end{algorithmic}    
+  \label{algo:ldsi:strategy:invalidate}
+  \caption{Evaluate a portion of the $\max$-strategy and note a
+    dependency}
+\end{algorithm}
+
+Invalidating the $\max$-strategy iteration is slightly more
+complicated than invalidating the fixpoint iteration stage. As the
+invalidation interface consists of variables, we must first translate
+a variable into a $\max$-expression (which is easily done by looking
+it up in the equation system). We must then invalidate the strategies
+for each variable which depends on this resultant
+$\max$-expression. The invalidation for $\max$-expressions consists of
+transitively invalidating everything which depends on the
+$\max$-expression, as well as itself.
+
+
 
-    \Function {solvestrategy} {$x$}
+\begin{algorithm}[H]
+  \begin{algorithmic}    
+    \Function {solvestrategy} {$x \in E_{\max}$}
     \Comment{Solve a specific variable and place its value in $\sigma$}
-    \If {$x \not \in \stable$}
-      \State $f = \system[x]$
-      \State $\stable = \stable \cup \{x\}$
-      \State $v = bestStrategy(f, \sigma(), \lambda y . \eval(x, y))$
-      \If {$v \ne \sigma[x]$}
-        \State $\sigma = \{ x \mapsto v \} \oplus \sigma$
-        \State $W = I[x]$
-        \State $I(x) = \emptyset$
-        \State $\invalidate \fixpoint(\mathsf{lookupVarFor}(x))$
-        \State $\stable = \stable \backslash W$
-        \For {$v \in W$}
+    \If {$x \not \in S_{\max}$}
+      \State $S_{\max} = S_{\max} \cup \{x\}$
+      \State $\sigma_{dynamic} = \lambda y . \eval \strategy(x,y)$
+      \State $e = P_{\max}(\sigma_{dynamic},
+                          \lambda y . \eval \strategy \fixpoint(x, y))(x)$
+      \If {$e \ne \sigma[x]$}
+        \State $\sigma = \{ x \mapsto e \} \oplus \sigma$
+        \State $\invalidate \fixpoint(\system^{-1}(x))$
+        \State $S_{\max} = S_{\max} \backslash I[x]$
+        \For {$v \in I[x]$}
           \State $\solve(v)$
         \EndFor
       \EndIf
     \EndIf
     \EndFunction
   \end{algorithmic}
-
   \caption{The $\max$-strategy portion of the Combined W-DFS.}
-  \label{algo:combined-max}
+  \label{algo:ldsi:solve}
 \end{algorithm}
 
 
@@ -516,15 +606,12 @@ 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.
 
-// TODO finish this.
-General idea:
-\begin{itemize}
-  \item
-    Invalidate calls from fixpoint $\to$ max strategy are correct if
-    the calls the other way are, because it completely re-solves the
-    equations
-  \item
-    Invalidate calls from max strategy $\to$ fixpoint are correct
-    because they effectively ``reset'' that part of the system,
-    creating it to be entirely re-calculated.
-\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.
+
+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.