Some more contribution fixing stuff.

1 files changed, 145 insertions, 60 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index b5d47db..44e5e7d 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -10,12 +10,15 @@
 \newcommand\system{\mathcal{E}} %\mathsf{system}}
 \newcommand\parent{\mathsf{parent}}
 \newcommand\parents{\mathsf{parents}}
+\newcommand\val{\mathsf{val}}
 \newcommand\old{\mathsf{old}}
+\newcommand\best{\mathsf{best}}
+\newcommand\all{\mathsf{all}}
 
 \newcommand\Operators{\mathcal{O}}
 \newcommand\Systems{\varepsilon}
 
-
+\newcommand\improve{\mathsf{\textsc{improve}}}
 \newcommand\init{\mathsf{\textsc{init}}}
 \newcommand\eval{\mathsf{\textsc{eval}}}
 \newcommand\stabilise{\mathsf{\textsc{stabilise}}}
@@ -24,8 +27,9 @@
 \newcommand\fixpoint{\mathsf{\textsc{fixpoint}}}
 \newcommand\strategy{\mathsf{\textsc{strategy}}}
 
-\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} 
-\algblockx[Assume]{Assumptions}{EndAssumptions}{\textbf{Assume:\\}}{} 
+\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{}
+\algblockx[Assume]{Assumptions}{EndAssumptions}{\textbf{Assume:\\}}{}
+\algblockdefx[ReturnLambdaFn]{ReturnLambdaFn}{EndReturnLambdaFn}[1]{\textbf{return function} (#1)}{\textbf{end function}}
 
 
 \chapter{Contribution} \label{chap:contribution}
@@ -92,21 +96,25 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
   : (X \to \CZ) \to \CZ$, a mapping from a variable assignment to the
   expression's value in that assignment.
 
-  Expressions have two possible forms:
+  Expressions have three possible forms:
   \begin{itemize}
-    \item $e = f( e_1, e_2, ..., e_k )$, with $f: \CZ^k \to \CZ$ and
+    \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(v)$
+      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$
   \end{itemize}
   
   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
   as \emph{$\max$-expressions}, denoted by $E_{\max} \subset E$.
 
-  For an expression $e$, the set of expressions containing it, $\{
-  e_\parent \mid e_\parent = o\{ e_1, e_2, ... e_k \}, o \in \O, e_i
-  \in E \}$, is denoted $\parents(e)$.
+  We define a function $\parents: E \to 2^E$, taking an expression,
+  $e$, to the set of expressions containing $e$, $\{ e_\parent \mid
+  e_\parent = f\{ ..., e, ... \}, f: \CZ^k \to \CZ \}$. $e$ is then
+  said to be a \emph{subexpression} of $e_{\parent}$.
 \end{definition}
 
 \begin{definition}
@@ -135,8 +143,8 @@ variables. We will also define $\CZ = \Z \cup \{-\infty, \infty\}$.
 
   We define an inverse mapping, $\system^{-1} : E \to 2^X$, taking an
   expression, $e$, to the set of variables, $x$ for which it is a
-  ``subexpression'' of $\system[x]$. This is captured in the following
-  definition:
+  transitive subexpression of $\system[x]$. This is captured in the
+  following definition:
   \begin{align*}
     \system^{-1}(e) &= \{ x \mid system(x) = e \} \cup \{
     \system^{-1}(e_\parent) \mid e_\parent \in parents(e) \}
@@ -317,16 +325,46 @@ The W-DFS algorithm provides us with a \emph{local},
 fixpoint problems.
 
 \begin{figure}[H]
-  \begin{align*}
-    x &= \min(0, y) \\
-    y &= x \\
-    a &= \min(0, b) \\
-    b &= c \\
-    c &= d \\
-    d &= e \\
-    e &= a \
-  \end{align*}
-  \caption{Example equation system for a W-DFS solve}
+  \begin{tikzpicture}
+    \node[draw] (full) at (0,-2) {
+      \begin{minipage}{0.3\textwidth}
+        \begin{align*}
+          x &= \min(0, y) \\
+          y &= x \\
+          a &= \min(0, b) \\
+          b &= c \\
+          c &= d \\
+          d &= e \\
+          e &= a
+        \end{align*}
+      \end{minipage}
+    };
+
+    \node[draw] (first) at (10, 1) {
+      \begin{minipage}{0.3\textwidth}
+        \begin{align*}
+          x &= \min(0, y) \\
+          y &= x
+        \end{align*}
+      \end{minipage}
+    };
+    \node[draw] (second) at (10,-4) {
+      \begin{minipage}{0.3\textwidth}
+        \begin{align*}
+          a &= \min(0, b) \\
+          b &= c \\
+          c &= d \\
+          d &= e \\
+          e &= a
+        \end{align*}
+      \end{minipage}
+    };
+
+    \draw[->] (full) -- (first);
+    \draw[->] (full) -- (second);
+  \end{tikzpicture}
+  \caption{Example of an equation system which can be separated into
+    two independent sub-systems}
   \label{fig:wdfs-example}
 \end{figure}
 
@@ -336,14 +374,14 @@ 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.
+value of a variable in either of these subsystems it is necessary to
+evaluate the entire subsystem, but it is not necessary to evaluate the
+other subsystem. To compute the value of $x$ in the greatest fixpoint
+it is unnecessary to compute the value of the variable $d$, but it is
+necessary to compute the value of $y$. The W-DFS algorithm, will only
+evaluate the necessary subsystem for a requested variable, leaving the
+other system 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
@@ -360,9 +398,11 @@ greatest-fixpoint problems.
 
 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 use $\sigma: \Systems \to \Systems$ as a
+subexpression. 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)$. Similarly
+$\sigma_{\all}: E \to E$ will denote the expression obtained by
+replacing each $\max$-subexpression in $e$ with $\sigma(e)$.
 
 In the particular case of \emph{monotonic}, \emph{expansive} operators
 it has been shown\cite{Gawlitza:2007:PFC:1762174.1762203} that this
@@ -372,19 +412,45 @@ 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, $P_{\max}: ((E_{\max} \to E) \times (X \to D))
-\to (E_{\max} \to E)$, is used below as a ``strategy improvement
-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:
+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:
 \begin{align*}
   \sigma(\system)(\rho) \le \varsigma(\system)(\rho)
 \end{align*}
 
-If it is possible for $\sigma$ to be improved then $P_{\max}$ will
-return an improvement, otherwise it will return $\sigma$ unchanged.
+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.
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Function {improve} {$\sigma: E_{\max} \to E$, $\rho: X \to D$}
+      \ReturnLambdaFn {$e \in E_{\max}$}
+        \State $e_{\best} = \sigma(e)$
+        \State $\val_{\best} = \sigma_{\all}(e_{\old})(\rho)$
+        \For {$e_i \in e$}
+          \If {$\sigma_{\all}(e_i)(\rho) > \val_{\best}$}
+            \State $e_{\best} = e_i$
+            \State $\val_{\best} = \sigma(e_i)(\rho)$
+          \EndIf
+        \EndFor
+        \State \Return $e_{\best}$
+      \EndReturnLambdaFn
+    \EndFunction
+  \end{algorithmic}
+  \caption{The variation of $\improve$ used in our algorithm}
+  \label{algo:pmax}
+\end{algorithm}
 
 \subsection{Naive approach}
 
@@ -405,7 +471,7 @@ the approach presented in Listing \ref{algo:naive-strategy}.
 
         $\rho$ & $: X \to D$, a variable assignment \\
 
-        $P_{\max}$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max}
+        $\improve$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max}
         \to E)$, a $\max$-strategy improvement operator \\
       \end{tabularx}
     \EndAssumptions
@@ -415,7 +481,7 @@ the approach presented in Listing \ref{algo:naive-strategy}.
       \State $\sigma_0 = \{ x \mapsto -\infty \mid \forall x \in X \}$
       \State $\rho_0 = \underline{-\infty}$
       \Repeat
-        \State $\sigma_{k+1} = P_{\max}(\sigma_k, \rho_k)$
+        \State $\sigma_{k+1} = \improve(\sigma_k, \rho_k)$
         \State $\rho_{k+1} = \solve \fixpoint(\sigma_{k+1}(\system))$
         \State $k = k + 1$
       \Until {$\sigma_{k-1} = \sigma_k$}
@@ -454,14 +520,14 @@ solve $\max$-strategy iteration problems.
       $\max$-expressions to a subexpression \\
 
       $\inflSI$ & $: (E_{\max} \to 2^{E_{\max}}$, a mapping from a
-      $\max$-expression to the sub-expressions it influences \\
+      $\max$-expression to the subexpressions it influences \\
 
       $\stableSI$ & $\subseteq E_{\max}$, the set of all
       $\max$-expressions whose strategies are stable \\
 
       $\system$ & $\in \Systems$, an equation system \\
       
-      $P_{\max}$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max}
+      $\improve$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to (E_{\max}
       \to E)$, a $\max$-strategy improvement operator \\
     \end{tabularx}
     \EndGlobals
@@ -491,7 +557,7 @@ solve $\max$-strategy iteration problems.
     \If {$x \not \in \stableSI$}
       \State $\stableSI = \stableSI \cup \{x\}$
       \State $\rho = \solve \fixpoint(\sigma(\system))$
-      \State $v = P_{\max}(\lambda y . \eval(x, y), \rho)[x]$
+      \State $v = \improve(\lambda y . \eval(x, y), \rho)[x]$
       \If {$v \ne \sigma[x]$}
         \State $\sigma = \{ x \mapsto v\} \oplus \sigma$
         \State $W = \inflSI[x]$
@@ -516,11 +582,11 @@ only attempt to improve the strategy for a given $\max$-expression if
 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]$; we improve the
+property of $\improve$. In Listing \ref{algo:adapted-wdfs} we take the
+value of $\improve(\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
+algorithm to be correct $\improve$ must always improve the strategy at
+$x$ if it is possible to do so. If $\improve$ 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
@@ -528,15 +594,20 @@ 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.
+not reached the solution of our $\max$-strategy iteration. The
+particular $\improve$ that we are using (see Listing \ref{algo:pmax})
+satisfies this assumption, as it attempts to improve the strategy at
+the point of individual $\max$-expressions.
 
-Additionally, in order to remain efficient, $P_{\max}$ should not
+Additionally, in order to remain efficient, $\improve$ should not
 attempt to improve the strategy for any $\max$-expressions until that
-expression is requested. Whether or not $P_{\max}$ is lazy in this way
+expression is requested. Whether or not $\improve$ 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.
+will be discarded with only $\improve(...)[x]$ being used. The
+particular $\improve$ that we are using (see Listing \ref{algo:pmax})
+satisfies this property by way of its anonymous function.
 
 \section{Local Demand-driven Strategy Improvement (LDSI)}
 
@@ -631,12 +702,12 @@ This algorithm is presented in three parts.
       $\max$-expressions to a subexpression \\
 
       $\inflSI$ & $: E_{\max} \to 2^{E_{\max}}$, a mapping from a
-      $\max$-expression to the sub-expressions it influences \\
+      $\max$-expression to the subexpressions it influences \\
 
       $\stableSI$ & $\subseteq E_{\max}$, the set of all
       $\max$-expressions whose strategies are stable \\
 
-      $P_{\max}$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to
+      $\improve$ & $: ((E_{\max} \to E) \times (X \to \CZ)) \to
       (E_{\max} \to E)$, a $\max$-strategy improvement operator \\
       
       \\
@@ -892,14 +963,16 @@ themselves destabilised as well.
     \Procedure {solvestrategy} {$x \in E_{\max}$}
     \If {$x \not \in \stableSI$}
       \State $\stableSI = \stableSI_{\max} \cup \{x\}$
-      \State $e = P_{\max}(\lambda y . \eval \strategy(x,y),
-                          \lambda y . \eval \strategy \fixpoint(x, y))[x]$
+      \State $e = \improve(\lambda y . \eval \strategy(x,y),
+                           \lambda z . \eval \strategy \fixpoint(x, z))[x]$
       \If {$e \ne \sigma[x]$}
         \State $\sigma = \{ x \mapsto e \} \oplus \sigma$
-        \State $\invalidate \fixpoint(\system^{-1}(x))$
+        \For {$v \in \system^{-1}(x)$}
+          \State $\invalidate \fixpoint(\system^{-1}(x))$
+        \EndFor
         \State $\stableSI = \stableSI \backslash I[x]$
         \For {$v \in \inflSI[x]$}
-          \State $\solve(v)$
+          \State $\solve \strategy(v)$
         \EndFor
       \EndIf
     \EndIf
@@ -911,8 +984,18 @@ 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.
@@ -938,3 +1021,5 @@ 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}