Berlin, Germany - Sunday, May 29 2016
Whilst training some minions for the 2015 MCPC and ACPC, I remember constantly bitching about how unwise it is to go ahead with the implementation of an algorithm without having a clear proof of its correctness and halt. Halt definitely comes before correctness. I mean how the living fuck is an algorithm correct if it runs infinitely.
Moving on. I was having a discussion with some colleagues a couple ‘o days ago and we brought up mathematical induction and I made a point about how most iterative and recursive algorithms can be modeled mathematically and proven as such. That discussion escalated and evidently turned into an argument. Insertion sort came up and well, we had to model and prove its halt and correctness mathematically.
If you don’t know what insertion sort is, what in seven hells are you even doing here? How the living fuck did you read this far? Kudos to you! Be a good lad, click that link and read up.
To the lazy ass who can’t click a link or just for the fuck of it, I will give a brief explanation of insertion sort. Ever tried to sort a shuffled deck of cards? What most people do is insertion sort. Basically, you have a sequence of unsorted elements, starting from the first element to the last, you pick an element and you insert this chosen element in the sorted list before it in a way that the list before it stay sorted after insertion. For the minds that need illustration
Before, we have this
[ 1 3 5 11 9 24 3 6 3 10 ]
after arriving at the index 5, we have a sorted prefix, the element at index 5 and an unsorted suffix
[ 1 3 5 11 ] 9 [ 24 3 6 3 10 ]
9 in the list before it we must put it in between
11 to keep the list sorted. We do the same for every number after
Shit is about to get real now. Brace yourselves.
Let us define a vector of length with the following ordering operations.
We also define the partial vector with containing exactly the first elements of sorted if and only if
Observe that this also implies the following
Now we define the insertion operation such that
The goal is to prove by induction that the insert operation always keep the list sorted (correctness) and that after insert operations (halt) we have .
The first thing we will do is assume that arriving at requires exactly insertion operations. So yes, we assume the halt because fuck it!
We know is sorted because it is empty, we also know is sorted because it has only one element.
Either way, is sorted and validates the above sort condition. If now we assume that for any with , is sorted how do we prove that is also sorted?
Supposing that such exists with since is sorted, then and . If not then since is the . This also implies that . Therefore we can conclude that inserting just before keeps the array sorted and gives us
What happens when we can’t find such , when , then we simply insert at the end of the list. I probably should have mentioned that beforehand but…
We have successfully shown that the insert operation is finite. We have also shown that the entire sorting requires insert operations thus also finite. So yeah insertion sort doesn’t run forever! But you probably knew that already. The most import thing is that by induction we’ve proven that the insertion sort indeed sorts.