Some reasons to do proofs

Sometimes you might not have a choice

One of the easiest way to verify an algorithm idea you have is to code up the algorithm and then test it on some (say random) inputs. However, sometimes this might not be a choice. E.g. if you work on Quantum Computing , then you do not have a quantum computer to run your quantum code on! So currently pretty much the only choice you have is to prove that your algorithm is indeed correct. For example, one of the crowning achievements of quantum computing is Shor's algorithm to computes the factors of large numbers efficiently on a quantum computer (that recall does not exist yet!). (You might also want to read Scott Aaronson's high level description of Shor's algorithm .) The reason why factoring large numbers is important is that if one can solve this problem efficiently then one can break the RSA cryptosystem . RSA is used everywhere (e.g. when you use your credit card online, RSA is used to make the transaction secure), so this is a big deal.

Below is a TED talk by Scott that gives a very high level overview of quantum computing (starting roughly in the middle of the talk).

Someone's life might depend on it

This might sounds a bit dramatic but think of how many critical system we use that are running programs: e.g. airplanes and medical devices. Bugs in these software can literally take lives. Even if no lives are at stake, software bugs can have significant financial consequences. See e.g. this Wikipedia page of notable software bug or this list of infamous software bugs . Software Testing is definitely one way to weed out bugs but for mission/life-critical applications, it would be better if you could be "double sure" that the software works correctly. Formal verification is one way to do this: this is the process of coming up with a formal proof that the software indeed works as it is supposed to. It is kind of cool that computers are used to generate proofs!

Computers have also been used to generate proofs where stakes are maybe slightly less higher: e.g. all the current known proof of the Four Color Theorem are computer generated! This video has an overview of the statement of the theorem, its history and some more details on the proof:

Proofs can be a debugging tool

We already mentioned that computer generated proofs are used to check for correctness of software (and hardware as well). However, even human generated proofs can be useful for debugging programs. Testing with random inputs is a fine way to test your program for random inputs. However, such testing is very unlikely to catch pathological corner cases. One of my friends who works with Google maps once told me that he tries to prove the correctness of algorithms he is implementing as that helps him identify corner cases. (And when you are at Google "corner cases" might not be that rare.)²

To gain a better understanding of algorithms

This one (at least at the surface) might be most philosophical of the reasons to work on proofs: a proof is a distillation of a solid understanding of the algorithm you are considering. In many cases in your jobs you will just use existing implementations of algorithms as a blackbox (and of course you should do this!) But if you had to modify the code you would need to understand the algorithm that the library implements. Proving the correctness of an algorithm is many a times a great way to really understand what an algorithm is doing. In 331 we will see many such examples when we do greedy algorithms. In particular, when we look at our first scheduling problem, we will see multiple potential algorithms all of whom look plausible but only one works. More confusingly, it is not clear why the "chosen one" works while the others don't. The best way I know to convince oneself that the chosen algorithm works is to prove that it works: and this is what we will do when we get to greedy algorithms in the course.

However, we will only get to greedy algorithms close to the mid-term exams, so instead of making you wait with bated breath, next we will look at the specific problem of generating permutations and two algorithms that are increasingly less obvious that they work. And then we will prove that they work. (Well, I'll leave the crux of the proof of correctness of the second algorithm as an exercise.)

Generating all permutations

Lest you think that this problem is some obscure mathematical problem, people have been using algorithms to generate all permutations for change ringing for church bells as early as 1621(!) for $n=4$. A solution for up to $n=6$ was listed in a book by Fabian Stedman from the second half of 1600s. By some accounts , he might be the first group theorist in math. (Group theory is now a very well studied and still active field of math.)

Generating all permutations is also useful in more recent times. See e.g. this survey by Robert Sedgewick . On a more personal note, some years back I interviewed at one of the Wall street firms. One of the phone interview questions was to design an efficient algorithms to generate all permutations. The interviewee said that they frequently needed to do this task.³

Algorithms

Steinhaus–Johnson–Trotter algorithm

                                //Input: A[i] for 0<= i<n

				//Define data structures to rember the direction and states
				bool direction[n]; //0 denotes "left" and 1 denotes "right"
				bool isActive[n]; //0 denotes "inactive" and 1 denotes "active"

				//Initialize the data structures
				for(i=0; i<n; i++)
					direction[i]=0; //All numbers first point "left"
				for(i=1; i<n; i++)
					isActive[i]=1;
				isActive[0]=0;// All but the smallest number is active

				int c = getCursor(isActive);

				while(true)
				{
					print(A); //Print the current permutation

					c = getCursor(isActive);
					if (c == -1) // There are no active numbers left
						break;
					
					int nbr = getNeighbor(c, direction);

					Swap( A[c], A[nbr]); // Need to prove that nbr is never out of bounds here
					// Also swap the flags
					Swap(direction[c], direction[nbr]);
					Swap(isActive[c], isActive[nbr]);

					c = nbr; // Update the index of the cursor

					//Reactivate all i s.t. A[i] > A[c]
					for(i=c+1; i<n; i++)
						if(A[i] > A[c])
							isActive[i]=true;

					//Now check if c is stuck
					nbr = getNeighbor(c, direction);
					if( nbr == -1 or (nbr != -1 and A[c] < A[nbr])) // c is stuck
					{
						direction[c] = !direction[c]; // Reverse direction of c
						isActive[c] = false; //Deactivate c
					}

				}


				//Function that returns the value of cursor
				//It returns if there is no active number
				int getCursor(bool isActive[])
				{
					int c=-1;
					for(i=0; i<n; i++)
						if(isActive[i])
							if(c == -1) // Encountered an active number for the first time
								c=i;
							else if (A[i]>A[c]) // Update if found a larger active number
								c=i;

					return c;
				}

				//Function that returns the neighbor of a number i
				// It returns -1 if i has no neighbors
				int getNeighbor(int i, bool direction[])
				{
					int nbr;

					if(direction[i]) // Direction is "right"
						nbr = i+1;
					else // Direction is "left"
						nbr = i-1;

					if(nbr >=n) // If there is no right neighbor
						nbr = -1;

					return nbr;						
				}

                        

Proof of Correctness

Runtime analysis

Heap's Algorithm

                                	//Input: A[i] for 0<= i<n

					permId = new int[n];

					//Initialize the permId data structure
					for( i=0; i<n; i++)
						permId[i]=0;

					print(A); // Print the current permutation

					//The main loop
                                        j=1;
					while(j< n)
					{
						if(permId[j]<j) //Do a swap to generate the next permutation
						{

							if( j is odd)
								swapId =permId[j];
							else
								swapId=0;

							Swap(A[swapId], A[j]);

							print(A); // Print the current permutation

							//Update the book-keeping
							permId[j]++;
							j=1;
						}
						else
							permId[j++]=0;
					} 

				

Proof of Correctness

The above run (like in the run of the Steinhaus–Johnson–Trotter algorithm) reveals a nice pattern: for now just concentrate on the last column. Each of the numbers appear $(n-1)!=6$ time. In particular, the prefix of size three contains all the $(n-1)!=6$ permutations on $a_0,a_1,a_2$. Further, this is true for every subsequent chunk of $(n-1)!$ permutation. This suggests that one could do some sort of inductive proof. The main issue is what to induct on. You might have noticed another strong pattern: the numbers in the last column appear in the order $a_3,a_2,a_1,a_0$. In particular, they appear in the reverse order of the initial permutation. In fact this is also true of the six distinct prefixes of size three for each of the six consecutive permutation. If this was true recursively for general $n$, this would be enough to carry out a proof of correctness by induction. Unfortunately, this stronger claim on how thw last column looks like is not true: consider a run for $n=5$.⁷ Thus, this is a great example of how our initial intuition can be wrong!

Of course one could try and feel more comfortable about Heap's algorithm by running it on larger examples but the problem with an runtime of $\Omega((n+1)!)$ is that this becomes infeaible very quickly. Thus, we would ideally like to have a proof of correctness for Heap's algorithm, which is left as an exercise.⁸

Runtime analysis

Further Reading

I found these slides from a talk by Sedgewick to be useful. In particular, it presents a recursive version of Heap's algorithm and then develops the iterative version (which is was is presented above) from it, which makes it more intuitive.

Here is a Youtube video on proofs that walks through some classical mathematical proofs:

Here is a video by Alan Cline that walks thourgh three results and talks about what insights the proofs give for those problems:

If you want a textbook to practice proofs, students have found How to Prove It by Daniel J. Velleman to be helpful.