Mergesort
General Information
Algorithmic problem: Sorting based on pairwise comparison
Type of algorithm: recursion
Abstract View
Invariant: After a recursive call, the input sequence of this recursive call is sorted.
Variant: For a recursive call on a subsequence [math]\displaystyle{ S' }[/math] of [math]\displaystyle{ S }[/math], let [math]\displaystyle{ S_1' }[/math] and [math]\displaystyle{ S_2' }[/math] denote the subsequences of [math]\displaystyle{ S' }[/math] with which Mergesort is called recursively from that call. Then it is [math]\displaystyle{ |S_1'| \leq \lceil|S'| /2\rceil }[/math] and [math]\displaystyle{ |S_2'| \leq \lceil|S'| /2\rceil }[/math].
Break condition: The current subsequence of the recursive call is empty or a singleton.
Induction Basis
Abstract view: Nothing to do on an empty sequence or a singleton.
Implementation: Ditto.
Proof: An empty set or singleton is trivially sorted.
Induction Step
Abstract view: The sequence is divided into two subsequences of approximately half size, it does not matter at all in which way this is done. Both subsequences are sorted recursively using Mergesort. The sorted subsequences are "merged" to one using algorithm Merge.
Implementation: Obvious.
Correctness: By induction hypothesis, the recursive calls sort and correctly. Algorithm Merge unites two sorted sequences into one sorted sequence.