Quickselect

DefinitionQuickselect#✓fully proved

Deterministic quickselect takes a list \(L\) over a linear order and a zero-based rank \(k\) and returns an element or no element, together with its cost, the number of element comparisons it makes. If \(k \ge |L|\), it returns no element at no cost. Otherwise it runs the following recursion, starting from the list \(L\) and the rank \(k\). On an empty list it returns no element. On a list with first entry \(p\) and remaining entries \(T\), and a rank \(r\), it forms the three-way partition of \(T\) around \(p\), with blocks \(B\), \(E\), \(A\) of entries below, equal to and above \(p\), at a cost of \(|T|\) comparisons. If \(r < |B|\), it recurses on \(B\) with rank \(r\); if \(|B| \le r < |B| + |E| + 1\), it returns \(p\); otherwise it recurses on \(A\) with rank \(r - (|B| + |E| + 1)\).

The recursion carries a fuel counter that starts at \(|L|\) and drops by one per call, and it returns no element when the fuel is exhausted; since every recursive call is on a strictly shorter list, the fuel never runs out on a nonempty list.

def quickselect (xs : List α) (k : Nat) : TimeM Nat (Option α) :=
  let rec loop : Nat → List α → Nat → TimeM Nat (Option α)
    | 0, _, _ => pure none
    | _ + 1, [], _ => pure none
    | fuel + 1, pivot :: tail, rank => do
        let parts ← partition3 pivot tail
        if rank < parts.below.length then
          loop fuel parts.below rank
        else if rank < parts.below.length + parts.equal.length + 1 then
          return some pivot
        else
          loop fuel parts.above
            (rank - (parts.below.length + parts.equal.length + 1))
  if k < xs.length then loop xs.length xs k else pure none

Uses 2 · Used by 15

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

Used byMedian-of-medians selection · Correctness of median-of-medians selection on short lists · Comparison bound for median-of-medians selection on short lists · Correctness of median-of-medians selection · Median-of-medians selection agrees with sorting · Out-of-range ranks cost no comparisons · Median-of-medians selection is quickselect on short lists · Median-of-medians selection succeeds on valid ranks · Group medians are lower medians of their blocks · Median of medians makes linearly many comparisons · Correctness of quickselect · Quickselect agrees with sorting · Quickselect fails exactly out of range · Rank inequalities determine the quickselect value · Worst-case comparison bound for quickselect

TheoremQuickselect fails exactly out of range#✓fully proved

Let \(L\) be a list over a linear order and let \(k\) be a natural number. Quickselect on \(L\) with zero-based rank \(k\) returns no element if and only if \(|L| \le k\).

theorem quickselect_eq_none_iff (xs : List α) (k : Nat) :
    (quickselect xs k).ret = none ↔ xs.length ≤ k

Uses 4 · Used by 2

Statement usesQuickselect

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

Used byMedian-of-medians selection succeeds on valid ranks · Quickselect agrees with sorting

TheoremCounting through the below block#✓fully proved

Let \(L\) be a list over a linear order, let \(p\) be an element, let \(q\) be a Boolean predicate on the elements, and let \(B\), \(E\), \(A\) be the blocks of entries below, equal to and above \(p\) in the three-way partition of \(L\) around \(p\). If \(q\) is false on every entry of \(E\) and on every entry of \(A\), then the number of entries of \(L\) satisfying \(q\) equals the number of entries of \(B\) satisfying \(q\), both counted with multiplicity.

theorem partition3_countP_eq_below {α : Type u} [LinearOrder α]
    (pivot : α) (xs : List α) (p : α → Bool)
    (hequal : ∀ x ∈ (partition3 pivot xs).ret.equal, p x = false)
    (habove : ∀ x ∈ (partition3 pivot xs).ret.above, p x = false) :
    xs.countP p = (partition3 pivot xs).ret.below.countP p

Uses 3 · Used by 3

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

Proof usesCorrectness of the stable three-way partition

Used byCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Median of medians makes linearly many comparisons

TheoremCounting through the above block#✓fully proved

Let \(L\) be a list over a linear order, let \(p\) be an element, let \(q\) be a Boolean predicate on the elements, and let \(B\), \(E\), \(A\) be the blocks of entries below, equal to and above \(p\) in the three-way partition of \(L\) around \(p\). If \(q\) is true on every entry of \(B\) and on every entry of \(E\), then the number of entries of \(L\) satisfying \(q\) equals \(|B| + |E|\) plus the number of entries of \(A\) satisfying \(q\), all counted with multiplicity.

theorem partition3_countP_eq_block_add_above {α : Type u} [LinearOrder α]
    (pivot : α) (xs : List α) (p : α → Bool)
    (hbelow : ∀ x ∈ (partition3 pivot xs).ret.below, p x = true)
    (hequal : ∀ x ∈ (partition3 pivot xs).ret.equal, p x = true) :
    xs.countP p = (partition3 pivot xs).ret.below.length +
      (partition3 pivot xs).ret.equal.length + (partition3 pivot xs).ret.above.countP p

Uses 3 · Used by 3

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

Proof usesCorrectness of the stable three-way partition

Used byCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Median of medians makes linearly many comparisons

TheoremEntries below the pivot#✓fully proved

Let \(L\) be a list over a linear order, let \(p\) be an element, and let \(B\) be the block of entries below \(p\) in the three-way partition of \(L\) around \(p\). Then the number of entries of \(L\) that are strictly less than \(p\), counted with multiplicity, equals \(|B|\).

theorem partition3_count_lt {α : Type u} [LinearOrder α] (pivot : α) (xs : List α) :
    xs.countP (fun x => decide (x < pivot)) = (partition3 pivot xs).ret.below.length

Uses 3 · Used by 4

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

Proof usesCorrectness of the stable three-way partition

Used byCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Set rank of a median-of-medians result · Median of medians makes linearly many comparisons

TheoremEntries at most the pivot#✓fully proved

Let \(L\) be a list over a linear order, let \(p\) be an element, and let \(B\) and \(E\) be the blocks of entries below and equal to \(p\) in the three-way partition of \(L\) around \(p\). Then the number of entries of \(L\) that are at most \(p\), counted with multiplicity, equals \(|B| + |E|\).

theorem partition3_count_le {α : Type u} [LinearOrder α] (pivot : α) (xs : List α) :
    xs.countP (fun x => decide (x ≤ pivot)) =
      (partition3 pivot xs).ret.below.length + (partition3 pivot xs).ret.equal.length

Uses 3 · Used by 4

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

Proof usesCorrectness of the stable three-way partition

Used byCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Set rank of a median-of-medians result · Median of medians makes linearly many comparisons

TheoremCorrectness of quickselect#✓fully proved

Let \(L\) be a list over a linear order and let \(k\) be a natural number. If quickselect on \(L\) with zero-based rank \(k\) returns an element \(x\), then \(x\) is an entry of \(L\), and, counting entries of \(L\) with multiplicity, the number of entries less than \(x\) is at most \(k\) and \(k\) is less than the number of entries at most \(x\).

Thus \(x\) occupies zero-based position \(k\) in the sorted order of \(L\), also when \(x\) is repeated.

theorem quickselect_correct {xs : List α} {k : Nat} {x : α}
    (hresult : (quickselect xs k).ret = some x) :
    x ∈ xs ∧
      xs.countP (fun y => decide (y < x)) ≤ k ∧
      k < xs.countP (fun y => decide (y ≤ x))

Uses 5 · Used by 6

Statement usesQuickselect

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

Used byCorrectness of median-of-medians selection on short lists · Correctness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Group medians are lower medians of their blocks · Median of medians makes linearly many comparisons · Quickselect agrees with sorting

TheoremQuickselect agrees with sorting#✓fully proved

Let \(L\) be a list over a linear order, let \(S\) be the insertion sort of \(L\) in nondecreasing order, and let \(k\) be a natural number. If \(k < |L|\), quickselect on \(L\) with zero-based rank \(k\) returns the entry of \(S\) at zero-based position \(k\); if \(k \ge |L|\), it returns no element.

theorem quickselect_eq_getElem?_insertionSort (xs : List α) (k : Nat) :
    (quickselect xs k).ret = (xs.insertionSort (· ≤ ·))[k]?

Uses 3 · Used by 3

Statement usesQuickselect

Proof usesCorrectness of quickselect · Quickselect fails exactly out of range

Used byMedian-of-medians selection agrees with sorting · Group medians are lower medians of their blocks · Rank inequalities determine the quickselect value

TheoremRank inequalities determine the quickselect value#✓fully proved

Let \(L\) be a list over a linear order, let \(k\) be a natural number and let \(x\) be an element. Counting entries of \(L\) with multiplicity, if the number of entries less than \(x\) is at most \(k\) and \(k\) is less than the number of entries at most \(x\), then quickselect on \(L\) with zero-based rank \(k\) returns \(x\).

theorem quickselect_eq_some_of_count_rank {α : Type u} [LinearOrder α]
    {xs : List α} {k : Nat} {x : α}
    (hlt : xs.countP (fun y => decide (y < x)) ≤ k)
    (hle : k < xs.countP (fun y => decide (y ≤ x))) :
    (quickselect xs k).ret = some x

Uses 2 · Used by 1

Statement usesQuickselect

Proof usesQuickselect agrees with sorting

Used byMedian-of-medians selection agrees with sorting

TheoremWorst-case comparison bound for quickselect#✓fully proved

For every list \(L\) over a linear order, of length \(n\), and every natural number \(k\), quickselect on \(L\) with rank \(k\) makes at most \(n(n-1)/2\) comparisons.

theorem quickselect_time (xs : List α) (k : Nat) :
    (quickselect xs k).time ≤ xs.length * (xs.length - 1) / 2

Uses 5 · Used by 1

Statement usesQuickselect

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

Used byComparison bound for median-of-medians selection on short lists

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.