summaryrefslogtreecommitdiff
path: root/tex
diff options
context:
space:
mode:
Diffstat (limited to 'tex')
-rw-r--r--tex/thesis/contribution/contribution.tex33
-rw-r--r--tex/thesis/thesis.tex2
2 files changed, 27 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}$}
diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex
index 8f64c07..2397833 100644
--- a/tex/thesis/thesis.tex
+++ b/tex/thesis/thesis.tex
@@ -91,6 +91,8 @@
\begin{document}
+\allowdisplaybreaks
+
% initial page numbers: i, ii, iii, ...
\renewcommand{\thepage}{\roman{page}}