\documentclass{article} % noweave -delay -index primes.nw > primes.tex; latex primes.tex % notangle -Rprimes.hs primes.nw > primes.hs \usepackage{noweb,url,amsmath,amsthm,textcomp} \usepackage[colorlinks=true,urlcolor=blue,citecolor=blue, linkbordercolor={1 1 1},urlbordercolor={1 1 1},pdfborder={1 1 1}]{hyperref} \pagestyle{noweb} \newcommand{\nix}[1]{} \newcommand{\N}{\mathbf{N}} \newtheorem{proposition}{Proposition} \theoremstyle{definition} \newtheorem{exercise}{Exercise} \begin{document} \title{\Large\textbf{From Proofs to Programs}} \author{\large Andreas Klappenecker} \date{} \maketitle \def\nwendcode{\endtrivlist \endgroup \vfil\penalty500\vfilneg} \paragraph{Primes.} Let $\mathbf{N}=\{1,2,3,\dots\}$ be the set of natural numbers. We say that a natural number $b$ \textbf{divides} a natural number $a$ if and only if there exists a natural number $c$ such that $a=bc$. A natural number $p$ greater than 1 is called \textbf{prime} if and only if $1$ and $p$ are the only natural numbers dividing $p$. A natural number $n>1$ that is not prime is called \textbf{composite}. Our goal is to write a program that allows us to test whether a given natural number $n$ greater than 1 is a prime. We will choose the functional programming language Haskell for the implementation. Let us denote by $\N_{2}=\N\setminus \{1\}$ the set of natural numbers greater than 1. Let $\ell\colon \mathbf{N_2}\rightarrow \mathbf{N_2}$ denote the function such that $\ell(n)$ is the least natural number greater than 1 dividing $n$. The function $\ell$ is well-defined, since there always exist a divisor of $n$ that is greater than 1, namely $n$ itself; thus, there must exist a smallest divisor $k=\ell(n)$ of $n$ in the range $2\le k\le n$. Let us collect some simple observations about the function $\ell$. \begin{proposition}\label{p:prime} The value $\ell(n)$ is a prime number for all $n$ in $\N_2$. \end{proposition} \begin{proof} Seeking a contradiction, we assume that there exists a number $n$ in $\N_2$ such that $\ell(n)$ is not a prime. This implies that there exist numbers $a$ and $b$ in $\N_2$ such that $\ell(n)=ab$. However, this would mean that $a$ divides $n$ and $a<\ell(n)$, contradicting the fact that $\ell(n)$ is the smallest natural number greater than 1 dividing $n$. Therefore, $\ell(n)$ must be prime for all $n$ in $\N_2$, as claimed. \end{proof} Therefore, if $n$ is composite, then $\ell(n)$ must be smaller than $n$. In fact, the next proposition shows that $\ell(n)$ is \textit{considerably} smaller than $n$ when $n$ is composite. \begin{proposition}\label{p:composite} If $n$ in $\N_2$ is a composite number, then $\ell(n)^2\le n$. \end{proposition} \begin{proof} Let $p=\ell(n)$. Since $n$ is not prime, we have $n=pa$ for some $a$ in the range $p\le a< n$. Therefore, $\ell(n)^2= p^2\le pa=n$, which proves the claim. \end{proof} The last observation alone suffices to design a simple primality test. The basic idea is to test whether any $k$ in the range $2\le k\le \sqrt{n}$ divides $n$. If we can find such a divisor $k$ then $n$ is evidently not a prime number; otherwise, $n$ must be a prime number. Indeed, the contrapositive of Proposition~\ref{p:composite} states that if $k^2=\ell(n)^2>n$, then $n$ must be a prime number. \paragraph{Haskell.} We choose the programming language Haskell for the implementation. This is a functional programming language named after the logician Haskell Curry. You can find a copy of the Haskell interpreter \texttt{hugs} at the web site \texttt{www.haskell.org}. After starting hugs, you can load a program file by typing \\ \texttt{:l myfilename.hs} \\ where \texttt{myfilename.hs} is the filename of your program. \paragraph{Implementation.} We present the program in the literate programming style introduced by Donald Knuth. Our program will be extracted from this text into the file \texttt{primes.hs}; this is indicated by the first label in angled brackets. The program contained in $\langle\textit{primes.hs}\rangle$ is structured into four different parts, as follows: <>= <> <> <> <> @ \noindent The first part $\langle\textit{primality test}\rangle$ of the program contains the primality test, and the other three parts contain the functions needed to implement this function. You can think of the terms in angled brackets as macros that will be expanded somewhere in this document. Since you are probably not familiar with Haskell, we start by explaining the simplest function, which is contained in $\langle\textit{division test}\rangle$. Recall that we can express a natural number $n$ as a multiple of a natural number $d$ plus a remainder~$r$, $$ n = qd+r,$$ where $0\le r>= divides d n = rem n d == 0 @ \noindent Here, \texttt{divides} is a function that takes two arguments, \texttt{d} and \texttt{n}. It returns \texttt{True} if and only if $d$ divides $n$. The function \texttt{divides d n} is implemented by checking whether the remainder of $n$ divided by $d$ is 0. Our main function will be called \texttt{prime} and it takes one argument \texttt{n}. Thus, \texttt{prime n} is supposed to return \texttt{True} if $n$ is a prime number, otherwise it should return \texttt{False}. It is assumed that the input $n$ is an integer greater than 1. The primality test takes advantage of the function $\ell$ that we have defined above. Recall that $n\ge 2$ is a prime number if and only if $n=\ell(n)$. In our Haskell program, the function $\ell$ will be called \texttt{ld}. Thus, \texttt{prime n} simply checks whether \texttt{ld n} is equal to \texttt{n}. In other words, the primality test is implemented as follows: <>= prime n = ld n == n @ The function $\ell$, or \texttt{ld} is Haskell, will be implemented in terms of a function \texttt{ldf} that takes two arguments, \texttt{k} and \texttt{n}, and returns the least divisor of $n$ in the range from $k$ to $n$, assuming that no divisor in the range $[2,k-1]=\{2,\dots,k-1\}$ has been found. <>= ld n = ldf 2 n @ All the work will be done in the function \texttt{ldf}. It is clear that \texttt{ldf k n} should return the value $k$ if $k$ divides $n$. If $k^2$ exceeds $n$, then $n$ does not have any divisors $m$ in the range $k\le m\le \sqrt{n}$, so it should return $n$. Otherwise, \texttt{ldf k n} is the same as \texttt{ldf (k+1) n}. In other words, we would like to define \texttt{ldf} using three different cases. Haskell allows us to do such case-by-case definitions of functions with the help of so-called guarded equations. One writes $$ \texttt{myfunction arg1 arg2 | mycondition = mydefinition } $$ This means that the function \texttt{myfunction} has two arguments \texttt{arg1} and \texttt{arg2} and is defined in terms of \texttt{mydefinition} given that the condition \texttt{mycondition} holds. The condition is called a \textit{guarded equation} in Haskell. Our function \texttt{ldf k n} that returns the smallest divisor $m$ of $n$ in the range $k\le m\le n$ is defined as follows: <>= ldf k n | divides k n = k | k^2 > n = n | otherwise = ldf (k+1) n @ \noindent You will immediately recognize the three different cases in the implementation of the function \texttt{ldf}. The last case is a recursive call to \texttt{ldf}. This is called a \textit{tail recursion}, and it is a simple way to implement the equivalent of a loop in a functional programming language. This completes our implementation of the primality test. If you load the file \texttt{primes.hs} into Haskell and type \texttt{prime 1111} then the Haskell interpreter will respond with \texttt{False}, since 11 is the least divisor of 1111. \pagebreak \paragraph{Literate Programming.} Even though we have not specified the literate programming macros in order, the extracted program follows precisely the outline given above. The content of the file \texttt{primes.hs} is: \begin{verbatim} prime n = ld n == n ld n = ldf 2 n ldf k n | divides k n = k | k^2 > n = n | otherwise = ldf (k+1) n divides d n = rem n d == 0 \end{verbatim} This document was created with noweb by Norman Ramsey and \LaTeX\ by Donald Knuth and Leslie Lamport. You should get familiar with \LaTeX, since it is the best way to produce documents that are nicely typeset. The literate programming paradigm is that programs should be written in a form that is a pleasure to read for humans, rather than in a form that is easily understood by a computer. Of course, you do not need literate programming to understand a tiny program with 6 lines of code. However, there is little hope to understand a scarcely documented program consisting of thousands of lines of code. In my experience, I insert more explanations when using literate programming, simply because I want to make the \LaTeX\ document look better. Norman Ramsey's noweb scripts are a simple way to use literate programming for any programming language. The documentation for noweb consists of a single page, so you can easily learn it. One of the most striking examples of literate programming is illustrated in [D.E.~Knuth, \textit{Computers \& Typesetting, Volume B: \TeX: The Program}, Addison-Wesley, Reading, MA, 1986, xviii+600pp.]. This book contains the full implementation of the typesetting system \TeX, on which \LaTeX\ is based. Knuth offers \$327.68=$2^{15}$\textcent\ for every error found in this program. Talk about confidence! You can learn more about Haskell and its usage in discrete mathematics in [K.~Doerts, J. van Eijck, \textit{The Haskell Road to Logics, Maths, and Programming}, King's College Publications, London, 2004]. I have taken the example discussed here from the first chapter of this book. You can find more details on Haskell there. \begin{exercise} Download and install \texttt{hugs} on your computer. \end{exercise} \begin{exercise} Experiment with the program \texttt{primes.hs}. Modify it so that the function arguments are of type integer. Make it robust so that it reports an error if the integer provided is less than 2. \end{exercise} \begin{exercise} Use Proposition~\ref{p:prime} and design a Haskell program to factor a natural number into primes numbers. The program should return a list of prime numbers such that their product is equal to the input. \end{exercise} \end{document}