edited report

diff --git a/report/formal.pdf b/report/formal.pdf
index f6bc5ba..abd1ac6 100644 (file)
Binary files a/report/formal.pdf and b/report/formal.pdf differ

diff --git a/report/formal.tex b/report/formal.tex
index 24d7843..1f20e62 100644 (file)
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -61,7 +61,7 @@
 }
 \usepackage[hidelinks]{hyperref}
 \newcommand{\CC}{C\nolinebreak\hspace{-.05em}\raisebox{.4ex}{\tiny\bf +}\nolinebreak\hspace{-.10em}\raisebox{.4ex}{\tiny\bf +}}
-\def\CC{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}}
+\def\CC{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}\,}
 
 %opening
 \title{Formalization of Two Algorithms arising in Number Theory}
@@ -327,7 +327,7 @@ We have described the algorithm for computing the set of prime numbers less equa
 While this description is rather general, we have several different ways to implement it. First, we will show an
 implementation that is based on the mathematical category of sets. In mathematics, we learn that the natural numbers
 are well-ordered, meaning, that every non-empty (possibly infinite) subset of $\mathbb{N}$ has a least element.
-Let us treat this formally. If we consider a non-empty (and lets restrict for the moment to finite sets) set
+Let us treat this formally. If we consider a non-empty (and lets restrict our consideration to finite sets) set 
 $N:=\{n_1,\ldots,n_k\}$, its minimal element $h$ is characterized by two properties:
 \begin{itemize}
  \item $h\in N$;
@@ -354,7 +354,7 @@ Based on that, we now present one possible answer to question \eqref{eq:q1}, by
         \caption{Sieve of Erathostenes I}
         \label{alg:2}
 \end{algorithm}
-Let us now discuss the steps of Algorithm \ref{alg:2}.
+Let us now discuss the intermediate steps of Algorithm \ref{alg:2}.
 We want to identify steps that hold at each execution step of the while loop, 
 and are therefore \emph{loop invariants}.
 
@@ -388,6 +388,57 @@ and this descent can only be performed finitely often.
 
 
 \subsection{The Sieve of Erathostenes II}
+In modern programming languages, such as C, \CC and Java, one distinguishes between \emph{primitive datatypes},
+and \emph{compound datatypes}. For example, in C one can consider \texttt{char}, \texttt{int}, \texttt{long},  \texttt{float} and  
+\texttt{double} as primitive datatypes. If data elements consist of multiple values, e.g. a playing card consisting of
+its numerical value and its suit, on can use the concept of \texttt{struct}, which is a first example of a compound datatype. 
+In \CC and Java one can additionally use the object oriented concept of \emph{classes}.\\
+
+However, in either case the mathematical category of \emph{set} is not in the standard instruction set available and
+a programmer who wants to use sets is in position to implement the data structure and hence produces a source of errors
+in the final program. To that end, programmers might prefer the second representation of the Sieve of Erathostenes,
+that we are going to develop in this section.\\
+
+Suppose, we want to answer question \eqref{eq:q1} for a nonnegative integer $n>2$. 
+To that end, we list all natural numbers up to $n$ in a linear boolean array, initialized with \texttt{true}, meaning
+that initially all elements are considered as prime (this is, the entry $i$ is \texttt{true} if and only if $i$ is prime).
+We start as pre-processing step by marking 0 and 1 as \texttt{false}, because they are clearly not prime. As before, 
+we identify the first prime number as 2, and set all even $i$ greater than 2 as \texttt{false}, because they would be
+divisible by 2. In the next step, we consider the least \texttt{true} element that has not yet been considered (which is
+3), and repeat our procedure. Proceeding likewise, we mark all multiples of 3 by \texttt{false}. This steps are repeated
+until we have reached the integer root of $n$.
+
+\begin{algorithm}[H]
+\begin{algorithmic}[1]
+\Require{$n\in\mathbb{N}$ such that $n>2$}
+\Ensure{$B \in \mathbb{B}^n$ where $B[i] = \texttt{true} \Leftrightarrow i $ is prime }
+\State $B \leftarrow (\texttt{true},\texttt{true},\ldots,\texttt{true}) \in \mathbb{B}^n$;
+\State $B[0],B[1] \leftarrow \texttt{false}$;
+\State $m \leftarrow \lfloor\sqrt{n}\rfloor$;
+\For{$i$ \textbf{from} 2 \textbf{to} $m$ \textbf{by} 1}
+  \For{$k$ \textbf{from} 1 \textbf{to} irgendwas \textbf{by} 1}
+        \If{$B[i] = \texttt{true}$} 
+         \State $B[i\cdot(k+1)] \leftarrow \texttt{false}$ 
+       \EndIf
+  \EndFor
+\EndFor
+\State\Return $B$.
+\end{algorithmic}
+        \caption{Sieve of Erathostenes II}
+        \label{alg:3}
+\end{algorithm}
+Although algorithm \ref{alg:2} and \ref{alg:3} look different, they implement the same mathematical idea for the Sieve of
+Erathostenes. Both use algorithm \ref{alg:1} as a subroutine. As the concept is different, we can't in general expect that
+the same invariants apply. Let us develop the invariants for this (cascaded loop) approach.
+
+\subsubsection*{Identifying Loop Invariants}
+After the initialization of $B, m$ and removal of $B[0],B[1]$, we deal with two cascaded loops, one for figuring out prime
+numbers (the first $i$-loop), one for removing all multiples greater than $i$ (which is the inner $j$-loop). Both loops
+carry certain invariants.\\
+
+The first loop, is iterating over all numbers and book-keeping about identified prime numbers. Hence, if we consider the
+elements from 0 to $i$, we find out, that this elements already satisfy the characteristic property of our result, this is,
+the entry $i$ is \texttt{true} if and only if $i$ is prime, and \texttt{false} if $i$ is not prime.
 
 \appendix