Lower bound on comparison-based sorting algorithms

Title:	Lower bound on comparison-based sorting algorithms
Author:	Manuel Eberl
Submission date:	2017-03-15
Abstract:	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 log₂ (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.
BibTeX:	@article{Comparison_Sort_Lower_Bound-AFP, author = {Manuel Eberl}, title = {Lower bound on comparison-based sorting algorithms}, journal = {Archive of Formal Proofs}, month = mar, year = 2017, note = {\url{http://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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.