The philosophy of programming: Logical thinking-good software

2. Validate general principles by deduction

How do we make sure the algorithm’s principles are correct? We can either increase our confidence by testing the principle against more input examples, or, more effectively, we can find a rigorous mathematical proof.

Like an a priori proposition in philosophy, the correctness of an algorithm is independent of its execution. In other words, testing cannot guarantee the correctness of algorithms. We need to prove it.

Here’s the basic flow of the proof:

1. For all visited vertices, we find the shortest paths.

2. The destination is visited.

3. Therefore, we find the shortest path to the destination.

Don’t they seem somewhat familiar? Like this:

1. All men are mortal.

2. Socrate is a man.

3. Therefore, Socrate is mortal.

In fact, this is Syllogism, a classic form of deductive reasoning. This is pretty much what logicians are doing.

Another interesting historical fact: the formal concept of computation was first come up by logicians in 1930s. They needed to know if certain logical problems are actually solvable at all (so they could avoid wasting their time solving something unsolvable). To answer that, they come up with the notion of computability.

Later in 1936, Alonzo Church and Alan Turing developed the formal definition of Computability, independently, at the same time. This paper gives a historical review of computation.

The conclusion’s correctness depends on the first two premises. In our proof, the second premise is trivial, since our algorithm is literally visiting all nodes. Yet proving the first premise, that we find the shortest path by the time we visit a node, needs some work.

Mathematical induction can help. It is actually one of the most useful techniques to prove the correctness of a lot of other algorithms.

The general flow goes as follows. First, if an algorithm works on input 0, and second, if the fact that it works on input n implies that it works on input n+1as well, then it works for all input greater or equal to 0. At this point you are able to guarantee the correctness of your algorithm.