Lower bound on comparison-based sorting algorithms (Q7361878)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Comparison_Sort_Lower_Bound
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Lower bound on comparison-based sorting algorithms |
AFP entry Comparison_Sort_Lower_Bound |
Statements
15 March 2017
0 references
Manuel Eberl
0 references
Lower bound on comparison-based sorting algorithms (English)
0 references
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 2 (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.
0 references
