Average-case running time

DefinitionExpected running time#✓fully proved

Let \(A\) be an algorithm on inputs of a type \(\gamma\) whose running time \(T_A(x)\) on each input \(x\) is a natural number, and let \(D\) be a probability mass function on \(\gamma\). The expected running time of \(A\) under \(D\) is the extended nonnegative expectation \(\sum_{x \in \gamma} D(x)\, T_A(x) \in [0, \infty]\) of the running time, the sum taken over all inputs.

Valuing the expectation in \([0, \infty]\) records a divergent expected time as \(\infty\); a real-valued integral would collapse it to \(0\).

noncomputable def expectedTime (algo : γ → TimeM Nat β)
    (dist : PMF γ) : ℝ≥0∞ :=
  dist.expectENN (fun xs => ((algo xs).time : ℝ≥0∞))

Uses 1 · Used by 6

Statement usesExtended expectation

Used byConstant running time on the support gives that expected time · Average formula for the expected time over random orderings · Constant running time on all rearrangements gives that expected time · Average formula for the expected time over random orderings, in the reals · Expected comparisons of quicksort on a random permutation · Expected comparisons of quicksort on a random permutation, as a real number

DefinitionUniformly random rearrangement of a list#✓fully proved

For a list \(x = (x_0, \dots, x_{n-1})\), the uniform permutation of \(x\) is the probability distribution on lists obtained by choosing a permutation \(\sigma\) of \(\{0, \dots, n-1\}\) uniformly at random and outputting \((x_{\sigma(0)}, \dots, x_{\sigma(n-1)})\).

noncomputable def uniformPermutation (xs : List α) : PMF (List α) :=
  (Cslib.Probability.PMF.uniformOfFintype (Equiv.Perm (Fin xs.length))).map
    (fun σ => List.ofFn (fun p => xs.get (σ p)))

Used by 10

Used byAverage formula for the expected time over random orderings · Constant running time on all rearrangements gives that expected time · Average formula for the expected time over random orderings, in the reals · Rearrangements preserve length · Rearrangements are permutations · Expected number of hires under a random permutation · Expected number of hires as a real harmonic sum · Expected number of hires is the harmonic number · Expected comparisons of quicksort on a random permutation · Expected comparisons of quicksort on a random permutation, as a real number

TheoremRearrangements preserve length#✓fully proved

For a list \(x\), every list in the support of the uniform permutation of \(x\) has the same length as \(x\).

theorem uniformPermutation_length (xs : List α)
    (ys : List α) (hys : ys ∈ (uniformPermutation xs).support) :
    ys.length = xs.length

Uses 1

Statement usesUniformly random rearrangement of a list

TheoremRearrangements are permutations#✓fully proved

For a list \(x\), every list in the support of the uniform permutation of \(x\) is a permutation of \(x\), that is, it has the same entries with the same multiplicities.

theorem uniformPermutation_perm (xs : List α)
    (ys : List α) (hys : ys ∈ (uniformPermutation xs).support) :
    List.Perm ys xs

Uses 1

Statement usesUniformly random rearrangement of a list

TheoremAverage formula for the expected time over random orderings#✓fully proved

Let \(A\) be an algorithm on lists whose running time \(T_A(y)\) on each list \(y\) is a natural number, and let \(x = (x_0, \dots, x_{n-1})\) be a list of length \(n\). The expected running time of \(A\) when its input is \(x\) rearranged by a uniformly random permutation equals

\[\frac{1}{n!} \sum_{\sigma} T_A(x_{\sigma(0)}, \dots, x_{\sigma(n-1)}),\]

the sum running over all permutations \(\sigma\) of \(\{0, \dots, n-1\}\) and computed in \([0, \infty]\).

theorem expectedTime_uniformPermutation (algo : List α → TimeM Nat β)
    (xs : List α) :
    expectedTime algo (uniformPermutation xs) =
      (Nat.factorial xs.length : ℝ≥0∞)⁻¹ *
        ∑ σ : Equiv.Perm (Fin xs.length),
          ((algo (List.ofFn (fun p => xs.get (σ p)))).time : ℝ≥0∞)

Uses 6 · Used by 2

Statement usesExpected running time · Uniformly random rearrangement of a list

Proof usesExtended expectation · Change of variables for extended expectation · Extended expectation under the uniform distribution · Uniform distribution on a finite type

Used byAverage formula for the expected time over random orderings, in the reals · Expected comparisons of quicksort on a random permutation

TheoremConstant running time on the support gives that expected time#✓fully proved

Let \(A\) be an algorithm on inputs of a type \(\gamma\) whose running time \(T_A(x)\) on each input \(x\) is a natural number, let \(D\) be a probability mass function on \(\gamma\), and let \(c\) be a natural number. If \(T_A(x) = c\) for every input \(x\) in the support of \(D\), then the expected running time of \(A\) under \(D\) equals \(c\).

Inputs outside the support have probability \(0\), so their running times do not contribute.

theorem expectedTime_eq_of_time_eq (algo : γ → TimeM Nat β)
    (dist : PMF γ) (c : ℕ)
    (h : ∀ ys ∈ dist.support, (algo ys).time = c) :
    expectedTime algo dist = (c : ℝ≥0∞)

Uses 3 · Used by 1

Statement usesExpected running time

Proof usesExtended expectation · Extended expectation of a constant

Used byConstant running time on all rearrangements gives that expected time

TheoremConstant running time on all rearrangements gives that expected time#✓fully proved

Let \(A\) be an algorithm on lists whose running time \(T_A(y)\) on each list \(y\) is a natural number, let \(x = (x_0, \dots, x_{n-1})\) be a list of length \(n\), and let \(c\) be a natural number. If \(T_A(x_{\sigma(0)}, \dots, x_{\sigma(n-1)}) = c\) for every permutation \(\sigma\) of \(\{0, \dots, n-1\}\), then the expected running time of \(A\) when its input is \(x\) rearranged by a uniformly random permutation equals \(c\).

theorem expectedTime_uniformPermutation_eq_of_time_eq
    (algo : List α → TimeM Nat β) (xs : List α) (c : ℕ)
    (h : ∀ σ : Equiv.Perm (Fin xs.length),
      (algo (List.ofFn (fun p => xs.get (σ p)))).time = c) :
    expectedTime algo (uniformPermutation xs) = (c : ℝ≥0∞)

Uses 3

Statement usesExpected running time · Uniformly random rearrangement of a list

Proof usesConstant running time on the support gives that expected time

TheoremAverage formula for the expected time over random orderings, in the reals#✓fully proved

Let \(A\) be an algorithm on lists whose running time \(T_A(y)\) on each list \(y\) is a natural number, and let \(x = (x_0, \dots, x_{n-1})\) be a list of length \(n\). The expected running time of \(A\) when its input is \(x\) rearranged by a uniformly random permutation, converted from \([0, \infty]\) to a real number, equals

\[\frac{1}{n!} \sum_{\sigma} T_A(x_{\sigma(0)}, \dots, x_{\sigma(n-1)}),\]

the sum running over all permutations \(\sigma\) of \(\{0, \dots, n-1\}\) and computed in \(\mathbb{R}\).

Every term of the average is a natural number, so the expected time is finite and the conversion loses nothing.

theorem expectedTime_uniformPermutation_toReal
    (algo : List α → TimeM Nat β) (xs : List α) :
    (expectedTime algo (uniformPermutation xs)).toReal =
      (Nat.factorial xs.length : ℝ)⁻¹ *
        ∑ σ : Equiv.Perm (Fin xs.length),
          ((algo (List.ofFn (fun p => xs.get (σ p)))).time : ℝ)

Uses 3

Statement usesExpected running time · Uniformly random rearrangement of a list

Proof usesAverage formula for the expected time over random orderings

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.