$n\in D(n)$), and $D(n)\subseteq \mathbb{N}$. The natural numbers are well-ordered, hence
every non-empty subset of $\mathbb{N}$ has a least element. Denote this least element element by $n'$. If $n'$ is
prime, we are finished. On the other hand, if $n'$ is composite, say $n'=ab$ where $a,b>1$, then
- $a,b < n'$ and
+ $a,b < n'$ and
$$
a | n' \wedge n' | n \Rightarrow a | n
$$
Obviously, the largest prime factor of $n$ is less equal $\lfloor \sqrt{n}\rfloor$, where
$$
-\lfloor x\rfloor := \min\{k\in \mathbb{Z}: k\leq x\},\qquad x\in \mathbb{R}
+\lfloor x\rfloor := \max\{k\in \mathbb{Z}: k\leq x\},\qquad x\in \mathbb{R}
$$
We initialize $P \leftarrow \emptyset$. The smallest number contained in $N$ is the prime number 2.
In the first iteration, we put $P' \leftarrow P\cup \{2\}$ and exclude from $N$ all even numbers, i.e. all numbers divisible by 2.
\subsection{(Slightly more) Advanced Number Theory}
Describe the algorithm for discrete logarithm here
-\section{The Formalization}
+\section{Analysis of the Algorithms}
The first step in formalization is to do the necessary paper-work. We start by analyzing the expected input and output
behavior, and put advance payment into the task of formalizing, to obtain two possible (simple) implementations
of the \emph{Sieve of Erathostenes} algorithm, in order to answer \eqref{eq:q1} properly. Each approach comes with its
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 our consideration 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$;
\label{alg:2}
\end{algorithm}
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,
+We want to identify steps that hold at each execution step of the while loop,
and are therefore \emph{loop invariants}.
\subsubsection*{Identifying Loop Invariants}
\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
+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.
+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
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$.
+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 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
\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}$
+ \If{$B[i] = \texttt{true}$}
+ \State $B[i\cdot(k+1)] \leftarrow \texttt{false}$
\EndIf
\EndFor
\EndFor
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.
+the entry $i$ is \texttt{true} if and only if $i$ is prime, and \texttt{false} if $i$ is not prime.\\
+
+As for the second (inner) loop, we are in a position, where a prime factor $p$ has been identified. All numbers, that have $p$
+as a divisor, except for $p$ self, can obviously not be prime. Hence, the task of the inner loop is, to remove all multiples
+of $p$. Hence, we can note an invariant about the already processed numbers, that multiples of all primes we have considered so
+far are marked by \texttt{false}.
+
+\subsubsection*{Termination of the Algorithm}
+The algorithm proceeds by constructing a partial solution, where first all even numbers are removed, then all multiples of 3
+and so on. We have to consider all numbers which are less or equal than $\lfloor \sqrt{n}\rfloor$. In the range
+$2\leq x\leq \lfloor \sqrt{n}\rfloor$, there are finitely numbers, and therefore finitely many primes. If all of them are
+considered, no further numbers greater $\lfloor \sqrt{n}\rfloor$ need to be considered and hence the algorithm terminates in
+a finite number of steps.
+
+\subsection{Discrete Logarithm - Algorithm of Tonelli}
+
+\section{The RISCAL Formalization}
+
+\section{Outlook}
\appendix
projects / cfuerst / formal-numbers.git / commitdiff