Analogies between programs and proofs

This page describes informally some of the connections between proof in mathematics and programs. It should help you see some of the similarities between the two processes, writing a program and writing a proof, and help you apply some of what you have learnt in programming to mathematics in general. It will also provide a number of additional programming examples for you to study.

1. Programs and proofs as expressions in a formal language

Proofs in mathematics aim to be arguments that are so rigorous and are based so tightly on a set of stated assumptions that are incontravertibly true, that no-one can deny the truth of a statement when it is proved. The necessity of such proofs comes from the observation that, in mathematics like in real life, some facts about the world are surprising and were we to base our work on guesses (even guesses backed up by hundreds of examples) many of the conclusions we would draw would be wrong and we'd be left in a muddle as to which of our guesses were correct and which were not.

Ideally, any mathematician should be able to check a proof and assert whether it is a correct proof or not. A more ambitious goal is to axiomatise the language and rules of proof so that these are so precise that a computer could be programmed to check proofs and assert whether they are correct or not. You will see if you take the 3rd year "Logic" module that this goal can be realised and proofs can be written in such a precise rigorous symbolic way.

The compiler when it reads your C++ code checks it in a very similar way: it checks your code to see that you did not break one of the many syntactical traps C++ offers you, and only if all these checks go through does the compiler generate executable code for you. Thus the C++ compiler is a bit like a proof checker, where C++ is a formal language analogous to the language of proofs.

In fact the connections between proofs and computer programs is very tight indeed and computer programs written in certain specialised programming languages can be viewed as proofs, and conversely there are usually very general methods for converting a proof into a computer program. Much of these details take us into postgraduate work in certain areas of the mathematical study of logic or theoretical computer science, and explaining detailed connections is outside the scope of this module. However, an appreciation of some of the similarities between the two discipline will help you on the one hand write better and clearer proofs, and on the other hand help you understand some of the more subtle issues in programming languages.

2. An example: the proof there are infinitely many primes

Almost everyone's favourite example proof is Euclid's argument that there are infinitely many primes, and you will all know this. So this is the example we work with here.

Unfortunately, this proof as usually presented is based on reductio ad absurdum. It so happens that such "proofs by contradiction" are less "constructive" than direct proofs, and the connections between "proofs by contradiction" and computer programs more difficult to see. However almost all proofs in mathematics can be re-cast in a more constructive way, and in the majority of these the use of reductio ad absurdum is actually unnecessary, and is simply there because it is conventional and convenient to start proofs like this. Euclid's argument for infinitely many primes is one such example. Here then is a restatement and proof of this theorem.

Euclid's theorem that there are infinitely many primes.

For every natural number $x$ there is a prime $p$ such that $p > x$ .

Proof.

Given $x \in ℕ$ , by a known fact about numbers, there is some positive $y \in ℕ$ such that every positive integer $z ⩽ x$ is a factor of $y$ . Take some such $y$ and consider $w = y + 1$ . This number $w \in ℕ$ is at least $2$ , but it may not be prime. By another known fact, there will be a prime $p$ which is a factor of $w$ , and this is the prime we are interested in. We will show that $p > x$ .

Here it really is convenient to use proof by contradiction: we suppose that $p ⩽ x$ and we will get a contradiction. Using the assumption that $p ⩽ x$ and the definition of $y$ we see that $p$ divides $y$ . Since also $p$ divides $w = y + 1$ we conclude that $p$ divides $w - y = 1$ . Thus $p$ divides $1$ but this means that $p$ being positive must equal $1$ , and this contradicts the definition of "prime" which says that $1$ is not prime. Hence the assumption was wrong and $p > x$ . Thus the theorem is proved.

Notes:

The definition of "prime" used here is that $p$ is prime if $p$ is a positive integer not equal to $1$ such that whenever $u, v \in ℕ$ and $u v = p$ then either $u = 1$ and $v = p$ or else $u = p$ and $v = 1$ . Many more advanced readers will recognise this as being the definition of " $p$ is irreducible" whereas " $p$ is prime" actually means something else. I was never sure why so many maths teachers promote this particular (white? or grey?) lie, but for simplicity I will use the above definition throughout.
Note that the statement "there are infinitely many primes" has been changed to "there are unboundedly many primes". This second statement is more precise and more interesting. (In fact there are situations in which these two statements are not equivalent, and the second is stronger and more interesting.)
The proof by contradiction in the second paragraph is interesting. Firstly, because the original proof then surely would have had two nested proofs by contradiction showing this is indeed a valid method of proof. (There are historical examples where nested proofs by contradiction have been misunderstood and the innermost contradiction has incorrectly been used as evidence for the falsity of the outermost assumption.) Secondly because it does have a constructive character. It says: if you give me a natural number $1 < q ⩽ x$ , then I will show you why it cannot be the case that $q$ is a divisor of $w$ .

Here is the same proof written as a C++ function. For convenience I use the C++ type int throughout for integers and ignore its manifest limitations. (There are C++ packages that you can #include that avoid these limitations.)

// Euclid's proof in C++

int euclidprime(int x) {
    if (x<=1) return 2;
    int y = lcmofallbelow(x+1);
    int w = y + 1;
    int p = leastprimedivisor(w);	      
    return p;
}

Notes:

Not all the information in the proof is present in the C++ program. That's because C++ is not expressive enough to carry arguments as well as calculations. Some formal languages can carry this information, however.
The theorem becomes a function. The "input variable" $x$ is declared as an int and the output is also an int. In more sophisticated analogies betweek proof and programs there is also a "proof" that the resulting value $p$ that is returned is bigger than $x$ . This "proof" could also be returned from the function, using call-by-reference perhaps.
Notice that the two "known facts" used in the proof have been converted to function calls. In other words these "known facts" would themselves have originally been lemmas, and they would have been converted to programs in the same way. These programs would be functions that are called in the usual way in C++. See below for examples.

There are a number of other important things to notice.

In proofs, like in programming, all variables should be declared. That means that if you introduce a variable you should say what its name is (e.g., y,p,w) and what its type is (in the case, int or integer) and usually also what its (initial) value is. Without this your proof can be misread and is certainly not rigorous.

In proofs, like in programming, all variables have a scope or section of the text in which they "live". Thus the variables $x, y, w, p$ only have the meaning indicated in the proof of Euclid's theorem, and may mean something completely different in the mathematics you do tomorrow. This should be "obvious", but somehow the analogous thing for programming languages is not so clear to beginners.

Some mathematicians have special conventions such as " $t$ always means time" and " $T$ always means temperature". This is analogous to certain conventions in certain (unusual or obsolete) programming languages. For example old versions of the FORTRAN language had the convention that a variable with a name starting with one of the letters I,J,K,L,M,N was always an int and every other variable was always a float (a low precision version of double). You can imagine what programming mistakes ensued, with variables such as COUNT, MASS, STEPNUMBER, and LIMIT. These old-style languages are not used any more and the small disadvantage of having to write an extra line of code to declare a variable is considered minimal compared to the huge advantage of having the compiler check much of your working automatically. Generally speaking, mathematicians have been slower to understand the issue in proofs, but most careful mathematicians explain every variable or notation as it is introduced, and most realise that with a convention such as " $t$ always means time" and " $T$ always means temperature" you cannot use the letter $t$ or $T$ to mean the tension in a spring.

One common exception is that many mathematicians regard the variable $x$ as "the independent variable" so $f (x)$ is a function of $x$ . This is a highly dangerous notation i.e. one that can lead to errors or lack of rigour in mathematics. Computer programs require you to separate the function f (which has type function<double(double)>) from the expression f(x) (which has type double but is only valid when x has type double). My personal view is that such a large number of implicit and unstated assumptions actually make it more difficult for the learner, and a more precise but slightly more complicated notation actually makes life easier. I will leave it to you to decide if you agree, but it is certainly true that many mathematical mistakes (some of them subtle and serious) have been made because of misunderstanding unstated conventions in notation.

3. Continuation of the example

You should have noticed that the reason we like to split programs into smaller functions is the same as the reason we like to split a long proof into many lemmas. (Officially, a "lemma" is a supporting statement that is used in the course of a proof. It is not supposed to have any independent interest, but it is often the case that, as soon as the lemma has been identified, it (like a function) turns out to be very useful. This is just like in programming where, once a useful function has been identified and coded, it finds many applications, some going beyond the original intention, and shortens code considererably.)

A second reason to split programs and proofs into many smaller functions or lemmas is to help us keep track of the variables. Many small functions have fewer variables each, with smaller scope, and it is easier to understand or check such code (proof).

So in this way we continue to explore the number theory behind Euclid's proof.

HCF lemma

For all integers $u, v ⩾ 1$ there is a positive $h \in ℕ$ such that $h$ divides both $u, v$ and is the greatest positive integer to do so.

Proof.

If $u = 1$ or $v = 1$ then $h = 1$ has the required properties. If $u = v$ then $h = u$ works. So suppose that $1 < u < v$ .

Let $w$ be the remainder on dividing $v$ by $u$ so $0 ⩽ w < u ⩽ v$ and $v = a u + w$ for some integer $a$ . If $w = 0$ then $u$ is a factor of $v$ so $h = u$ is the required HCF. Else $1 ⩽ w < u$ and since these are smaller, by recursion/induction, there is some $h = hcf (w, u)$ . So $h$ divides both $w, u$ and is the largest such. But then $h$ divides both $u, v$ since $v = a u + w$ and is the largest such since if $h'$ is larger and divides $u, v$ then $h'$ would divide $w = v - a u$ . Hence $h$ is the HCF of $u, v$ .

Subproof.

This is really a proof by induction: the (implicit) induction assumption should be,

$H (n)$ : whenever integers $1 ⩽ u, v ⩽ n$ are given, then there is a positive $h \in ℕ$ such that $h$ divides both $u, v$ and is the least positive integer to do so.

You should re-examine the proof checking that the base case $H (1)$ was proved, and also " $H (n)$ implies $H (n +1)$ " for all $n$ .

The corresponding C++ function is defined using recursion as follows.

// hcf function

int hcf(int u, int v) {
    if (u<1 || v<1) { std::cerr << "Error: inputs to hcf should be positive" << std::endl; }
    if (u==1 || v==1) { return 1; }
    // assume without loss of generality that u <= v										 
    if (u > v) { int temp = u; u = v; v = temp; }
    int w = v%u ;
    if (w==0) return u;
    else return hcf(w,u);
}

Exercise.

Program the function

int hcf(int u, int v, int& a, int& b) {...}

that, given u,v>0, as well as returning the hcf h of u,v, also sets a,b to be integers such that h == a*u+b*v.

Sometimes loops are used to find the "least" value satisfying something.

Least divisor

For all integers $u > 1$ there is a least divisor $p > 1$ of $u$ . This $p$ is prime.

Proof.

Let $p > 1$ be least such that $p > 1$ and $p$ divides $u$ . Note that $u > 1$ itself divides $u$ so there is some such integer. Then $p$ is prime since if $p = a b$ then both $a, b ⩽ p$ and both divide $u$ . So either $a = p$ and $b = 1$ or else $a = 1$ and $b = p$ .

Here are two related functions using a loop for you to study. I've left out the commentary and comments. You should be able to work out what's going on. First, leastprimedivisor,

// least prime divisor function

int leastprimedivisor(int u) {
    if (u<=1) { std::cerr << "Error: input to leastprimedivisor should be greater than 1" << std::endl; }
    for (int p=2; p<u; p++) {
        if (u%p == 0) return p;
    }
    return u;
}

And here is lcmofallbelow,

// lcm of { 1,2,...,u-1 }

int lcmofallbelow(int u) {
    if (u<1) { std::cerr << "Error: input to lcmofallbelow should be greater than 0" << std::endl; }
    int lcm = 1;
    for (int i=1; i<u; i++) {
        int h = hcf(lcm,i);
        int factor = i / h; // exact division here
        lcm = lcm * factor;
    }
    return lcm;
}

Try to think of your work in an "algorithmic" context as well as a "proof" context. This should improve your proof-writing skills (because you use programming skills to write and check your proofs) and also improve your understanding of the theorems and their proofs (because you will understand better how proofs can be used as methods to calculate certain things).

Postscript: I have worked through the code above and demostrated it lectures. The final code produced is here: primes.cpp. Note that as a method of calculating large primes, Euclid's method is particularly useless. The numbers lcmofallbelow(u) are so large int overflow occurs very very rapidly. The current version of the program detects these errors and quits early. (Older versions of the program did not detect these problems and this was the main issue with them.)