Lower bound on comparison-based sorting algorithms


Title: Lower bound on comparison-based sorting algorithms
Author: Manuel Eberl
Submission date: 2017-03-15

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.

  author  = {Manuel Eberl},
  title   = {Lower bound on comparison-based sorting algorithms},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2017,
  note    = {\url{https://isa-afp.org/entries/Comparison_Sort_Lower_Bound.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Landau_Symbols, List-Index, Stirling_Formula
Used by: Quick_Sort_Cost, Treaps