\chapter{Contribution} \label{chap:contribution}

The main theoretical contribution of this paper is an improvement on
the algorithm presented in \cite{Gawlitza:2007:PFC:1762174.1762203}
for solving fixpoint equations over the integers with monotonic
operators. The algorithm is presented in section
\ref{section:basic-algorithm}.

The algorithm consists of two iterative operations: fixpoint iteration
and max-strategy iteration. Each of these operations can be made
significantly faster by the application of the algorithms presented in
\cite{DBLP:tr/trier/MI96-11}. In particular the algorithm W-DFS (which
is alluded to in \cite{DBLP:tr/trier/MI96-11} and presented in
\cite{fixpoint-slides}) provides a considerable speed up by taking
into account dynamic dependency information to minimise the number of
re-evaluations that must be done. The W-DFS algorithm is presented as
algorithm \ref{algo:w-dfs}.


\section{W-DFS}

\subsection{Fixpoint Iteration}

\newcommand\stable{\mathsf{stable}}
\newcommand\eval{\mathsf{eval}}
\newcommand\solve{\mathsf{solve}}
\newcommand\system{\mathsf{system}}
\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} 

\begin{algorithm}
  \begin{algorithmic}
    \Globals
    \begin{tabular}{rl}
      D & A mapping from variables to their current values, starting
      at $\{ x \mapsto \infty | \forall x \in X \}$ \\ 
      I & A mapping from a variable to the variables which depend on
      it in their evaluation \\
      stable & The set of all variables whose values have stabilised \\ 
      system & The equation system, a mapping from a variable to its
      associated function \\
    \end{tabular}
    \EndGlobals

    \Function {eval} {$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\}$
      \State \Return $D[y]$
    \EndFunction

    \Function {solve} {$x$}
    \Comment{Solve a specific variable and place its value in $D$}
    \If {$x \not \in \stable$}
      \State $f = \system[x]$
      \State $\stable = \stable \cup \{x\}$
      \State $v = f( \lambda y . \eval(x, y) )$
      \If {$v \ne D[x]$}
        \State $D = \{ x \mapsto v, \alpha \mapsto D[\alpha] \}
        \forall \alpha \ne x$
        \State $W = I[x]$
        \State $I(x) = \emptyset$
        \State $\stable = \stable \backslash W$
        \For {$v \in W$}
          \State $\solve(v)$
        \EndFor
      \EndIf
    \EndIf
    \EndFunction
  \end{algorithmic}

  \caption{The W-DFS alluded to in \cite{DBLP:tr/trier/MI96-11} and
    presented in \cite{fixpoint-slides}, modified to find
    greatest-fixpoints of monotonic fixpoint equations}
  \label{algo:w-dfs}
\end{algorithm}

W-DFS can be used to quickly find the solutions to systems of fixpoint
equations and, in the case of monotonic right hand sides, will always
return the least fixpoint. The algorithm also functions
\emph{locally}, only taking into account the subset of the equation
system that it is necessary to examine to solve for the requested
variable's value.

One simple modification to the presented algorithm for solving a
system of equations involving $\max$- and $\min$-expressions is to
replace the Bellman-Ford sub-procedure with the W-DFS fixpoint
solver. This alone can give a considerable speed increase by reducing
the amount of work to be done in each $\max$-strategy iteration step.

Another simple optimisation can be to utilise the W-DFS algorithm to
speed up the max-strategy iteration. This optimisation is not as
obvious as using W-DFS to solve the fixpoint-iteration step, so some
justification is necessary.

\subsection{Max-Strategy Iteration}

The $\max$-strategy iteration can be viewed as a fixpoint problem. We
are attempting to find a strategy, $\sigma: E_{\max} \to E$ that will
result in the greatest value for each $e \in E_{\max}$. Therefore if
we consider our ``variables'' to be $\max$-expressions, our ``values''
to be their subexpressions and our ``comparison'' to be carried out
using the result of evaluating the system with that strategy.

This, then, allows us to use the W-DFS algorithm to re-evaluate only
those parts of the strategy which have changed. Algorithm
\ref{algo:w-dfs-max} presents this variation on W-DFS.

\begin{algorithm}
  \begin{algorithmic}
    \Globals
    \begin{tabular}{rl}
      $\sigma$ & A mapping from $\max$-expressions to their current
      sub-expressions, starting by \\& mapping to the first
      sub-expression \\
      I & A mapping from a $\max$-expression to the sub-expressions
      which depend on it \\& in their evaluation \\
      stable & The set of all $\max$-expressions whose strategies have
      stabilised \\
      system & The equation system, a mapping from a variable to its
      associated function \\
      bestStrategy & A function $(E_{\max}, (X \to D)) \to E$ mapping
      from an expression and a variable \\& assignment to the greatest
      subexpression in that context
    \end{tabular}
    \EndGlobals

    \Function {eval} {$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\}$
      \State \Return $\sigma[y]$
    \EndFunction

    \Function {solve} {$x$}
    \Comment{Solve a specific expression and place its value in $\sigma$}
    \If {$x \not \in \stable$}
      \State $f = \system[x]$
      \State $\stable = \stable \cup \{x\}$
      \State $v = bestStrategy(x, \lambda y . \eval(x, y))$
      \If {$v \ne \sigma[x]$}
        \State $\sigma = \{ x \mapsto v, \alpha \mapsto \sigma[\alpha]
        \} \forall \alpha \ne x $
        \State $W = I[x]$
        \State $I(x) = \emptyset$
        \State $\stable = \stable \backslash W$
        \For {$v \in W$}
        \State $\solve(v)$
        \EndFor
      \EndIf
    \EndIf
    \EndFunction
  \end{algorithmic}

  \caption{W-DFS, this time modified to find the best $\max$-strategy.}
  \label{algo:w-dfs-max}
\end{algorithm}


\section{Combined W-DFS}

W-DFS can be used to speed up both the $\max$-strategy iteration and
the fixpoint iteration as two independent processes, but each
fixpoint-iteration step still requires at least one complete
evaluation of the equation system per $\max$-strategy improvement
step. Ideally we would be able to adapt the W-DFS algorithm so that
the fixpoint-iteration and $\max$-strategy iteration steps could
provide some information to each other about what values have changed
so that at each step only a subset of the entire system would have to
be evaluated.

The new algorithm, \emph{Combined W-DFS} seeks to do this. By adding
an ``invalidate'' method to both W-DFS instances we provide an
interface for the two sides of the algorithm to indicate which values
have changed. This gives the other side enough information to avoid
evaluating irrelevant portions of the equation system.

This algorithm is presented in two parts. Algorithm
\ref{algo:combined-fixpoint} presents the fixpoint-iteration portion
of the algorithm, while \ref{algo:combined-max} presents the
$\max$-strategy portion.  The correctness of this new algorithm is
argued in \ref{sec:combined-correctness}.


\begin{algorithm}
  \begin{algorithmic}
    \Globals
    \begin{tabular}{rl}
      D & A mapping from variables to their current values, starting
      at $\{ x \mapsto \infty \}$ \\ 
      I & A mapping from a variable to the variables which depend on
      it in their evaluation \\
      stable & The set of all variables whose values have stabilised \\ 
      system & The equation system, a mapping from a variable to its
      associated function \\
    \end{tabular}
    \EndGlobals

    \Function {eval} {$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\}$
      \State \Return $D[y]$
    \EndFunction

    \Function {invalidate} {$x$}
    \If {$x \in \stable$}
      \State $\stable = \stable \backslash \{x\}$
      \State $D[x] = \infty$
      \State $W = I[x]$
      \State $I[x] = \emptyset$
      \For {$v \in W$}
        invalidate(v)
      \EndFor
    \EndIf
    \EndFunction

    \Function {solve} {$x$}
    \Comment{Solve a specific expression and place its value in $D$}
    \If {$x \not \in \stable$}
      \State $f = \system[x]$
      \State $\stable = \stable \cup \{x\}$
      \State $v = f( \lambda y . \eval(x, y) )$
      \If {$v \ne D[x]$}
        \State $D = \{ x \mapsto v, \alpha \mapsto D[\alpha] \}
        \forall \alpha \ne x$
        \State $W = I[x]$
        \State $I(x) = \emptyset$
        \State strategy::invalidate($x$)
        \State $\stable = \stable \backslash W$
        \For {$v \in W$}
        \State $\solve(v)$
        \EndFor
      \EndIf
    \EndIf
    \EndFunction
  \end{algorithmic}

  \caption{The fixpoint portion of the Combined W-DFS.}
  \label{algo:combined-fixpoint}
\end{algorithm}


\begin{algorithm}
  \begin{algorithmic}
    \Globals
    \begin{tabular}{rl}
      $\sigma$ & A mapping from $\max$-expressions to their current
      sub-expressions, starting by \\& mapping to the first
      sub-expression \\
      D & A \emph{dynamic} variable assignment which will stay updated
      as $\sigma$ changes \\
      $I$ & A mapping from a $\max$-expression to the sub-expressions
      which depend on it \\& in their evaluation \\
      $I_V$ & A mapping from a variable to the $\max-$ expressions which
      depend on it in their \\& evaluation \\
      stable & The set of all $\max$-expressions whose strategies have
      stabilised \\
      system & The equation system, a mapping from a variable to its
      associated function \\
      bestStrategy & A function $(E_{\max}, (X \to D)) \to E$ mapping
      from an expression and a variable \\& assignment to the greatest
      subexpression in that context
    \end{tabular}
    \EndGlobals

    \Function {eval} {$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\}$
      \State \Return $\sigma[y]$
    \EndFunction

    \Function {invalidate} {$x \in X$} \Comment{X is vars}
      \State $\stable = \stable \backslash I[x]$
      \State $W = I_v[x]$
      \State $I_V = \emptyset$
      \For {$v \in W$}
        \State solve(v)
      \EndFor
    \EndFunction

    \Function {solve} {$x$}
    \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(x,
                               \lambda y . \eval(x, y))$
      \If {$v \ne \sigma[x]$}
        \State $\sigma = \{ x \mapsto v, \alpha \mapsto \sigma[\alpha]
        \} \forall \alpha \ne x $
        \State $W = I[x]$
        \State $I(x) = \emptyset$
        \State fixpoint::invalidate$(\mathsf{lookupVarFor}(x))$
        \State $\stable = \stable \backslash W$
        \For {$v \in W$}
          \State $\solve(v)$
        \EndFor
      \EndIf
    \EndIf
    \EndFunction
  \end{algorithmic}

  \caption{The $\max$-strategy portion of the Combined W-DFS.}
  \label{algo:combined-max}
\end{algorithm}


\subsection{Correctness} \label{sec:combined-correctness}

This algorithm relies on the correctness of the underlying W-DFS
algorithm. This algorithm was presented in
\cite{DBLP:tr/trier/MI96-11}.

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.

// 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}