1 files changed, 25 insertions, 8 deletions
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 66d5b4a..cc8d3ba 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -130,11 +130,31 @@ algorithm is presented in Listing \ref{algo:kleene}.
 For each iteration the entire system is evaluated, irrespective of
 whether it could possibly have changed value. This results in a
 considerable inefficiency in practice, requiring the evaluation of
-$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.
+many right-hand-sides repeatedly for the same value. Thus an
+approach which can evaluate smaller portions of the system in each
+iteration would be a significant improvement.
+
+An additional deficiency of Kleene iteration is that it is not
+guaranteed to terminate. In some cases Kleene iteration must iterate
+an infinite number of times in order to reach a fixpoint. An example
+system is presented as Figure \ref{fig:kleene-infinite}. In this case
+$x$ will take the value of $0$ in the first iteration, then $y$ will
+evaluate to $-1$. In the next iteration $x$ will also take the value
+$-1$, thereby requiring $y$ to take the value $-2$. This will continue
+without bound, resulting in the Kleene iteration never reaching the
+greatest fixpoint of $\{ x \mapsto -\infty, y \mapsto -\infty \}$.
+
+\begin{figure}[H]
+  \begin{align*}
+    x &= \min(0, x) \\
+    y &= x - 1
+  \end{align*}
+  \caption{An example equation system for which Kleene iteration will
+    not terminate}
+  \label{fig:kleene-infinite}
+\end{figure}
 
-\subsection{W-DFS algorithm} \ref{sec:wdfs}
+\subsection{W-DFS algorithm} \label{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 +275,7 @@ problem it is possible
 \end{algorithm}
 
 
-\subsection{Adapted W-DFS algorithm} \ref{sec:adapted-wdfs}
+\subsection{Adapted W-DFS algorithm} \label{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
@@ -532,7 +552,6 @@ 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
@@ -568,8 +587,6 @@ $\max$-expression. The invalidation for $\max$-expressions consists of
 transitively invalidating everything which depends on the
 $\max$-expression, as well as itself.
 
-
-
 \begin{algorithm}[H]
   \begin{algorithmic}    
     \Function {solvestrategy} {$x \in E_{\max}$}