Lower Bound on Comparison-Based Sorting Algorithms

Manuel Eberl

15 March 2017


This article contains a formal proof of the well-known fact that number of comparisons that a comparison-based sorting algorithm needs to perform to sort a list of length n is at least log2 (n!) in the worst case, i. e. Ω(n log n).

For this purpose, a shallow embedding for comparison-based sorting algorithms is defined: a sorting algorithm is a recursive datatype containing either a HOL function or a query of a comparison oracle with a continuation containing the remaining computation. This makes it possible to force the algorithm to use only comparisons and to track the number of comparisons made.

BSD License

Depends On

Used by


Related Entries