Quicksort
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: In each recursive call, the sequence of the callee is strictly shorter than that of the caller.
Break condition: The sequence is empty or a singleton.
Induction basis
Abstract view: Nothing to do on an empty sequence or a singleton.
Implementation: Ditto.
Proof: Empty sequences and singletons are trivially sorted.
Induction step
Abstract view:
- Choose a pivot value [math]\displaystyle{ p \in [min\{x|x \in S\},\dots,max\{x|x \in S\}] }[/math] (note that [math]\displaystyle{ p }[/math] is not required to be an element of [math]\displaystyle{ S }[/math].
- Partition [math]\displaystyle{ S }[/math] into sequences, [math]\displaystyle{ S_1 }[/math], [math]\displaystyle{ S_2 }[/math] and [math]\displaystyle{ S_3 }[/math], such that [math]\displaystyle{ x \lt p }[/math] for [math]\displaystyle{ x \in S_1 }[/math], [math]\displaystyle{ x = p }[/math] for [math]\displaystyle{ x \in S_2 }[/math], and [math]\displaystyle{ x \gt p }[/math] for [math]\displaystyle{ x \in S_3 }[/math].
- Sort [math]\displaystyle{ S_1 }[/math] and [math]\displaystyle{ S_3 }[/math] recursively.
- The concatenation of all three lists, [math]\displaystyle{ S_1 \| S_2 \| S_3 }[/math], is the result of the algorithm.