### Abstract

We give a formal proof of the well-known results about the number of comparisons performed by two variants of QuickSort: first, the expected number of comparisons of randomised QuickSort (i. e. QuickSort with random pivot choice) is 2 (n+1) Hn - 4 n, which is asymptotically equivalent to 2 n ln n; second, the number of comparisons performed by the classic non-randomised QuickSort has the same distribution in the average case as the randomised one.

### License

BSD License

### Topics

- Computer science/Algorithms
- Computer science/Algorithms/Randomized

### Session Quick_Sort_Cost

- Randomised_Quick_Sort
- Quick_Sort_Average_Case

### Depends on

- Lower bound on comparison-based sorting algorithms
- Landau Symbols
- List Index
- Regular Sets and Expressions

### Used by

- Expected Shape of Random Binary Search Trees

### Auto-related entries

- Euler’s Polyhedron Formula
- Wetzel’s Problem and the Continuum Hypothesis
- Lucas’s Theorem
- The Cartan Fixed Point Theorems
- An Axiomatic Characterization of the Single-Source Shortest Path Problem

## Cite

×

Quick_Sort_Cost-AFP

    @article{Quick_Sort_Cost-AFP,
      author  = {Manuel Eberl},
      title   = {The number of comparisons in QuickSort},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Quick_Sort_Cost.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Mar 16, 2017 : Isabelle2016-1