# 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 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. 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{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