From: Christoph Fuerst Date: Sat, 20 May 2017 07:03:51 +0000 (+0200) Subject: Edited Report X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=3022850b634f3456df4207d0561795b3bc2ecee6;p=cfuerst%2Fformal-numbers.git Edited Report --- diff --git a/report/formal.pdf b/report/formal.pdf index bfe3efc..f6bc5ba 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 13ae054..24d7843 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -59,7 +59,7 @@ stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered tabsize=2, % sets default tabsize to 2 spaces } -\usepackage{hyperref} +\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 ++}}} @@ -130,8 +130,10 @@ One of the most fundamental notions in mathematics is without doubt the term \emph{divisor}, we say for $a,c\in\mathbb{Z}$, that \emph{$a$ divides $c$}, and write $a|c$, if there is a number $b\in\mathbb{Z}$ such that $c = a\cdot b$. Every number $n\in\mathbb{N}$ has at least -two divisors, a \emph{prime number} $p\in\mathbb{N}$ is a number $p$ -that has exactly two divisors, $1$ and $p$. Let now be given two numbers +two divisors 1 and $n$, a \emph{prime number} $p\in\mathbb{N}$ is a number $p$ +that has exactly two divisors, 1 and $p$. Obviously, 1 divides every natural number, +which we exclude by considering only \emph{proper divisors} greater 1. +Let now be given two numbers $a,b\in\mathbb{N}$. Among all divisors of two numbers $a$,$b$ there is a unique \emph{greatest common divisor} of $a$ and $b$, denoted by $\gcd(a,b)$, that is computed by the \emph{Euclidean algorithm}. The \emph{extended Euclidean algorithm} @@ -194,9 +196,26 @@ first non-trivial Theorems in number theory. Every natural number can be written as product of primes uniquely up to order. \end{thm} A constructive proof of the fundamental theorem is obtained, by showing that the -smallest divisor $p_1$ of $n\in\mathbb{N}$ (with both, $n$ and $p_1$, greater than one) +smallest proper divisor $p_1$ of $n\in\mathbb{N}$ (with both, $n$ greater than one) is prime. An algorithm for computing the prime decomposition proceeds recursively considering -$n/p_1$. This steps are performed until $n/(p_1\ldots p_k) = 1$.\\ +$n/p_1$. This steps are performed until $n/(p_1\ldots p_k) = 1$. + +\begin{lem}\label{lem:leastelemisprime} + Let $n$ be a natural number greater equal 2. Then, the least proper divisor of $n$ is a prime. +\end{lem} +\begin{proof} + We consider the set $D(n) := \{m\in \mathbb{N}: m|n\}$. Obviously, $D(n)$ is not empty (e.g. + $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 | n' \wedge n' | n \Rightarrow a | n + $$ + contradicting the minimal property. +\end{proof} + + The first algorithm we will be concerned with the (more or less) opposite problem. Given a natural number $n$, we are interested in answering the question: @@ -204,10 +223,13 @@ number $n$, we are interested in answering the question: \text{Describe the set }\, P(n) := \{p\in\mathbb{N}: 2 \leq p\leq n \wedge p \text{ is prime}\}.\tag{{\rm Q1}} \end{equation} The cardinality of the set $P$ is in classic textbooks referred by $\pi(n)$. -The famous prime number theorem gives information about the asymptotic growth +The famous prime number theorem gives information about the asymptotic growth of $\pi(n)$ as $n$ tends to +infinity. +\begin{thm}[Prime Number Theorem] $$ \lim\limits_{n \rightarrow \infty}\pi(n) \sim \frac{n}{\log(n)} $$ +\end{thm} Given an natural number $n\geq 2$, the answer to question \eqref{eq:q1} is given by the \emph{Sieve of Erathostenes}. The classic algorithm proceeds by starting with the set $N := \{2,\ldots,n\}$ successively erasing non-prime numbers. Although this algorithm is not particular performant (compared to tuned versions, such as \emph{Aitken's Sieve}), @@ -266,6 +288,10 @@ would proceed as follows. \caption{Integer-Square-Root} \label{alg:1} \end{algorithm} +\begin{thm} + Algorithm \ref{alg:1} is correct, and terminates in a finite number of steps. +\end{thm} +\begin{proof} The first step of Algorithm \ref{alg:1} is the initialization of the result $x$ and two temporary variables $y$ and $z$. As for the While-Loop, we observe that initially \begin{align} @@ -294,6 +320,7 @@ $$ y > n \Leftrightarrow (x^2+z) > n \Leftrightarrow x^2+2x+1 > n \Leftrightarrow (x+1)^2 > n, $$ hence we have shown $x^2\leq n < (x+1)^2$, and taking square roots shows the claim. +\end{proof} \subsection{The Sieve of Erathostenes I} We have described the algorithm for computing the set of prime numbers less equal $n$ in section \ref{sec:math}. @@ -310,7 +337,7 @@ While this seems obvious when written, we must not forget, that the computer can mathematically inclined people would already provide \emph{per se}, as a formal proof system could not use intuition.\\ -However, we now present one possible answer to question \eqref{eq:q1}, by considering the following algorithm. +Based on that, we now present one possible answer to question \eqref{eq:q1}, by considering the following algorithm. \begin{algorithm}[H] \begin{algorithmic}[1] \Require{$n\in\mathbb{N}$ such that $n>2$} @@ -318,17 +345,47 @@ However, we now present one possible answer to question \eqref{eq:q1}, by consid \State $P \leftarrow \emptyset$; \State $Q \leftarrow \{2,\ldots,n\}$; \While{$Q \neq \emptyset$} -\State $P\leftarrow P \cup \{\min(Q)\}$; -\State $Q\leftarrow Q - \{m\in Q: \min(Q)|m\}$; +\State $r \leftarrow \min(Q)$; +\State $P\leftarrow P \cup \{r\}$; +\State $Q\leftarrow Q - \{s\in Q: r|s\}$; \EndWhile \State\Return $P$. \end{algorithmic} \caption{Sieve of Erathostenes I} \label{alg:2} \end{algorithm} -Algorithm \ref{alg:2} provides several points for discussion. First of all, both sets, $P$ and $Q$ are -at all steps obviously subsets of $\{2,\ldots,n\}$. As this condition holds at each execution of the while -loop, we identify this as a \emph{loop invariant}. +Let us now discuss the 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}. + +\subsubsection*{Identifying Loop Invariants} +First of all, both sets, $P$ and $Q$ are subsets of $\{2,\ldots,n\}$. Therefore, +at all stages of the algorithm, we have +$$ +P, Q\subseteq \{2,\ldots,n\}. +$$ +The set $P$ holds prime numbers only, as this is true initially (i.e. $P$ is the empty set and every +element of the empty set is a prime number). For the inductive step, if $P$ holds prime numbers only and +is extended by the least element of the set $Q$, it retains this property (in clear correspondence +with Lemma \ref{lem:leastelemisprime}). Hence, a second invariant describing $P$ is, that every element of $P$ +is prime (and hence, the same applies for the intermediate sets $P$ obtained within this loop).\\ + +Let us now quantify the numbers $2,\ldots,n$ in more detail. Each number $k$ is either prime or composite. +If $k\in P$, then by the preceeding discussion $k$ is prime. Conversely, if $k\in \{2,\ldots,n\}$ is prime, +it is never removed from the set $Q$, and therefore after finitely many steps the minimal element of $Q$ and +therefore transferred to the set $P$. Hence, the algorithm ensures the equivalence $x\in P \Leftrightarrow x \text{ is prime}$.\\ + +As a final observation, we remark, that every element of $P$ is smaller than any element of the set $Q$, +as follows immediately from $a | n \Rightarrow a\leq b$ and the fact that $P$ contains only prime numbers +and therefore proper divisors. + +\subsubsection*{Termination of the Algorithm} +The termination of the algorithm is ensured by the so called \emph{termination term}. +In the beginning, the set $Q$ is not empty, but at each execution step, elements of $Q$ are removed +(as the set $\{s\in Q: \min(Q)|s\}$ is not empty), and therefore, the cardinality of $Q$ decreases. +Therefore, the termination of the algorithm is a consequence of the fact that $|Q|$ decreases, +and this descent can only be performed finitely often. + \subsection{The Sieve of Erathostenes II} @@ -338,16 +395,24 @@ loop, we identify this as a \emph{loop invariant}. \begin{thebibliography}{9} +\bibitem{FuriaMeyer} +C. A. Furia and B. Meyer. \textit{Inferring Loop Invariants Using Postconditions} +A. Blass, N. Dershowitz, and W. Reisig (Eds.): Gurevich Festschrift, LNCS 6300, pp. 277–300, 2010. + +\bibitem{FuriaMeyer2} +C. A. Furia, B. Meyer and S. Velder. \textit{Loop Invariants: Analysis, Classification, and Examples} +ACM Computing Surveys, Vol. 46, No. 3, Article 34, January 2014. + \bibitem{hardylittlewood} G.H. Hardy and E.M. Wright. \textit{An Introduction to the Theory of Numbers}. Oxford University Press, 6. edition. 2008. \bibitem{JML} -\text{Java Modelling Language JML} -\url{http://www.eecs.ucf.edu/~leavens/JML//index.shtml} +\text{The Java Modelling Language (JML)} Home page, February +2013 \url{http://www.jmlspecs.org} \bibitem{Larch} -\text{The Larch System}. +\text{The Larch System} Home page, May 2017 \url{https://www.cs.cmu.edu/afs/cs/project/larch/www/home.html} \bibitem{LidlNiederreiter}