Quicksort

DefinitionQuicksort#✓fully proved

Deterministic quicksort on lists over a linear order, using the first entry as pivot and counting comparisons. The empty list is returned unchanged at no cost. On a list with first entry \(p\) and tail \(t\), the algorithm stably splits \(t\) into the entries less than \(p\), equal to \(p\) and greater than \(p\), using one comparison per entry of \(t\); it then recursively sorts the lesser and greater parts and returns the sorted lesser part, followed by \(p\), the entries equal to \(p\) in their original order, and the sorted greater part. The cost is the total number of comparisons.

def quickSort (xs : List α) : TimeM Nat (List α) :=
  let rec loop : Nat → List α → TimeM Nat (List α)
    | 0, _ => pure []
    | _ + 1, [] => pure []
    | fuel + 1, pivot :: tail => do
        let parts ← partition3 pivot tail
        let below ← loop fuel parts.below
        let above ← loop fuel parts.above
        return below ++ (pivot :: (parts.equal ++ above))
  loop xs.length xs

Uses 2 · Used by 4

Statement usesThree-way partition record · Stable three-way partition

Used byCorrectness of quicksort · Expected comparisons of quicksort on a random permutation · Expected comparisons of quicksort on a random permutation, as a real number · Worst-case comparison bound for quicksort

TheoremCorrectness of quicksort#✓fully proved

For every list \(\ell\) over a linear order, the output of quicksort on \(\ell\) is sorted in nondecreasing order and is a permutation of \(\ell\); in particular every value occurs in the output exactly as often as in \(\ell\).

theorem quickSort_correct (xs : List α) :
    List.Pairwise (fun x y => x ≤ y) (quickSort xs).ret ∧
      List.Perm (quickSort xs).ret xs

Uses 5

Statement usesQuicksort

Proof usesThree-way partition record · Stable three-way partition · Correctness of the stable three-way partition · Sizes of the three parts of a three-way partition

TheoremWorst-case comparison bound for quicksort#✓fully proved

For every list of length \(n\) over a linear order, quicksort performs at most \(n(n-1)/2\) comparisons.

theorem quickSort_time (xs : List α) :
    (quickSort xs).time ≤ xs.length * (xs.length - 1) / 2

Uses 5

Statement usesQuicksort

Proof usesThree-way partition record · Stable three-way partition · Sizes of the three parts of a three-way partition · Cost of the stable three-way partition

DefinitionNumber of list entries strictly between two values#✓fully proved

For a list \(\ell\) over a linear order and elements \(a\) and \(b\), this is the number of entries \(x\) of \(\ell\), counted with multiplicity, such that \(a < x < b\).

public def betweenCount (xs : List α) (a b : α) : ℕ :=
  (xs.filter (fun x => a < x ∧ x < b)).length

Used by 2

Used byExpected comparisons of quicksort on a random permutation · Expected comparisons of quicksort on a random permutation, as a real number

TheoremExpected comparisons of quicksort on a random permutation#✓fully proved

Let \(\ell\) be a list without repeated entries over a linear order. The expected number of comparisons made by quicksort on the list obtained by rearranging the entries of \(\ell\) by a uniformly random permutation of their positions, computed in the extended nonnegative reals \([0, \infty]\), equals

\[\sum_{a < b} \frac{2}{d(a, b) + 2},\]

where the sum runs over pairs of entries \(a < b\) of \(\ell\) and \(d(a, b)\) is the number of entries of \(\ell\) strictly between \(a\) and \(b\) (CLRS Section 7.4).

public theorem quickSort_expectedTime_uniformPermutation
    (xs : List α) (hxs : xs.Nodup) :
    expectedTime quickSort (uniformPermutation xs) =
      ∑ p ∈ (xs.toFinset ×ˢ xs.toFinset).filter (fun p => p.1 < p.2),
        (2 : ℝ≥0∞) * ((betweenCount xs p.1 p.2 + 2 : ℝ≥0∞))⁻¹

Uses 12 · Used by 1

Statement usesNumber of list entries strictly between two values · Expected running time · Quicksort · Uniformly random rearrangement of a list

Proof usesThree-way partition record · Average formula for the expected time over random orderings · Stable three-way partition · The above list of a three-way partition is a filter · The below list of a three-way partition is a filter · The equal list of a three-way partition is a filter · Sizes of the three parts of a three-way partition · Cost of the stable three-way partition

Used byExpected comparisons of quicksort on a random permutation, as a real number

TheoremExpected comparisons of quicksort on a random permutation, as a real number#✓fully proved

Let \(\ell\) be a list without repeated entries over a linear order. Take the expected number of comparisons made by quicksort on the list obtained by rearranging the entries of \(\ell\) by a uniformly random permutation of their positions, which is an element of \([0, \infty]\), and convert it to a real number. The result equals the real sum

\[\sum_{a < b} \frac{2}{d(a, b) + 2},\]

where the sum runs over pairs of entries \(a < b\) of \(\ell\) and \(d(a, b)\) is the number of entries of \(\ell\) strictly between \(a\) and \(b\).

public theorem quickSort_expectedTime_uniformPermutation_toReal
    (xs : List α) (hxs : xs.Nodup) :
    (expectedTime quickSort (uniformPermutation xs)).toReal =
      ∑ p ∈ (xs.toFinset ×ˢ xs.toFinset).filter (fun p => p.1 < p.2),
        (2 : ℝ) / (betweenCount xs p.1 p.2 + 2)

Uses 5

Statement usesNumber of list entries strictly between two values · Expected running time · Quicksort · Uniformly random rearrangement of a list

Proof usesExpected comparisons of quicksort on a random permutation

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.