Hiring problem

DefinitionThe hire-assistant scan#✓fully proved

Given candidates \(x_0, \dots, x_{n-1}\) in a linearly ordered type, the scan interviews them in order while keeping a current manager, initially none, which counts as below every candidate. Candidate \(i\) is hired exactly when \(x_i\) is strictly greater than the value of the current manager, and then becomes the new manager; ties keep the earlier manager. The scan returns the zero-based index of the final manager (none for the empty list) and the list of hired indices in the order they were hired, and its cost is the pair (number of interviews, number of hires).

public def hireAssistant {α : Type u} [LinearOrder α] (xs : List α) :
    TimeM (Nat × Nat) (Option Nat × List Nat) :=
  let state : TimeM (Nat × Nat) (Option (α × Nat) × Array Nat) :=
    xs.zipIdx.foldlM (interview (α := α)) (none, #[])
  ⟨(state.ret.1.map Prod.snd, state.ret.2.toList), state.time⟩

Used by 10

Used byExpected number of hires under a random permutation · Expected number of hires as a real harmonic sum · Expected number of hires is the harmonic number · Hire-count bounds for the hire-assistant scan · The hire-assistant scan hires exactly the strict prefix maxima · Strictly increasing input hires every candidate · Hire-assistant scan on no candidates · The hire-assistant scan returns the earliest best candidate · Hire-assistant scan on one candidate · Cost of the hire-assistant scan

TheoremThe hire-assistant scan returns the earliest best candidate#✓fully proved

For every list \(x_0, \dots, x_{n-1}\) in a linearly ordered type, the manager returned by the hire-assistant scan is none when the list is empty, and otherwise is the smallest index \(i\) such that \(x_i\) is a maximum of the list.

public theorem hireAssistant_ret {α : Type u} [LinearOrder α] (xs : List α) :
    (hireAssistant xs).ret.1 = xs.maxIdxOn? id

Uses 1

Statement usesThe hire-assistant scan

TheoremThe hire-assistant scan hires exactly the strict prefix maxima#✓fully proved

For every list \(x_0, \dots, x_{n-1}\) in a linearly ordered type, the list of indices hired by the hire-assistant scan, in chronological order, is the increasing list of all indices \(i < n\) such that \(x_j < x_i\) for every \(j < i\).

public theorem hireAssistant_hires {α : Type u} [LinearOrder α] (xs : List α) :
    (hireAssistant xs).ret.2 =
      (xs.zipIdx.filter (fun p => (xs.take p.2).all (fun a => decide (a < p.1)))).map
        Prod.snd

Uses 1 · Used by 3

Statement usesThe hire-assistant scan

Used byExpected number of hires under a random permutation · Hire-count bounds for the hire-assistant scan · Strictly increasing input hires every candidate

TheoremCost of the hire-assistant scan#✓fully proved

For every list of \(n\) candidates in a linearly ordered type, the cost pair of the hire-assistant scan is \((n, h)\), where \(h\) is the length of the list of hired indices that the scan returns.

public theorem hireAssistant_time {α : Type u} [LinearOrder α] (xs : List α) :
    (hireAssistant xs).time = (xs.length, (hireAssistant xs).ret.2.length)

Uses 1 · Used by 3

Statement usesThe hire-assistant scan

Used byExpected number of hires under a random permutation · Hire-count bounds for the hire-assistant scan · Strictly increasing input hires every candidate

TheoremHire-assistant scan on no candidates#✓fully proved

On the empty list, the hire-assistant scan returns no manager and an empty list of hires, with cost pair \((0, 0)\).

public theorem hireAssistant_nil {α : Type u} [LinearOrder α] :
    hireAssistant ([] : List α) = ⟨(none, []), (0, 0)⟩

Uses 1

Statement usesThe hire-assistant scan

TheoremHire-assistant scan on one candidate#✓fully proved

For every element \(a\) of a linearly ordered type, on the one-element list \([a]\) the hire-assistant scan returns manager index \(0\) and hire list \([0]\), with cost pair \((1, 1)\): the single candidate is hired regardless of its quality.

public theorem hireAssistant_singleton {α : Type u} [LinearOrder α] (a : α) :
    hireAssistant [a] = ⟨(some 0, [0]), (1, 1)⟩

Uses 1

Statement usesThe hire-assistant scan

TheoremHire-count bounds for the hire-assistant scan#✓fully proved

For every nonempty list of \(n\) candidates in a linearly ordered type, the number of hires \(h\) recorded in the cost pair of the hire-assistant scan satisfies \(1 \le h \le n\).

public theorem hireAssistant_hire_bounds {α : Type u} [LinearOrder α] (xs : List α)
    (h : xs ≠ []) :
    1 ≤ (hireAssistant xs).time.2 ∧ (hireAssistant xs).time.2 ≤ xs.length

Uses 3

Statement usesThe hire-assistant scan

Proof usesThe hire-assistant scan hires exactly the strict prefix maxima · Cost of the hire-assistant scan

TheoremStrictly increasing input hires every candidate#✓fully proved

For every strictly increasing list \(x_0 < x_1 < \dots < x_{n-1}\) in a linearly ordered type, including the empty list, the hire-assistant scan hires the indices \(0, 1, \dots, n - 1\) in that order, and its cost pair is \((n, n)\).

public theorem hireAssistant_increasing {α : Type u} [LinearOrder α] (xs : List α)
    (h : xs.Pairwise (· < ·)) :
    (hireAssistant xs).ret.2 = List.range xs.length ∧
      (hireAssistant xs).time = (xs.length, xs.length)

Uses 3

Statement usesThe hire-assistant scan

Proof usesThe hire-assistant scan hires exactly the strict prefix maxima · Cost of the hire-assistant scan

TheoremExpected number of hires under a random permutation#✓fully proved

Let \(x\) be a list of \(n\) pairwise distinct elements of a linearly ordered type, and rearrange its entries by a uniformly random permutation of the indices. The expected number of hires, valued in \([0, \infty]\), that the hire-assistant procedure (interview the entries in order, hiring each one strictly better than every earlier one) makes on the rearranged list equals \(\sum_{i=0}^{n-1} \frac{1}{i+1}\).

public theorem hireAssistant_expectedHires (xs : List α) (hxs : xs.Nodup) :
    (uniformPermutation xs).expectENN
        (fun ys => ((hireAssistant ys).time.2 : ℝ≥0∞)) =
      ∑ i : Fin xs.length, ((i.val + 1 : ℝ≥0∞))⁻¹

Sources

• CLRS Section 5.2.

Uses 8 · Used by 1

Statement usesThe hire-assistant scan · Uniformly random rearrangement of a list · Extended expectation

Proof usesThe hire-assistant scan hires exactly the strict prefix maxima · Cost of the hire-assistant scan · Change of variables for extended expectation · Extended expectation under the uniform distribution · Uniform distribution on a finite type

Used byExpected number of hires as a real harmonic sum

TheoremExpected number of hires as a real harmonic sum#✓fully proved

Let \(x\) be a list of \(n\) pairwise distinct elements of a linearly ordered type, and rearrange its entries by a uniformly random permutation of the indices. The expected number of hires that the hire-assistant procedure (interview the entries in order, hiring each one strictly better than every earlier one) makes on the rearranged list, an element of \([0, \infty]\), converted to a real number, equals \(\sum_{i=0}^{n-1} \frac{1}{i+1}\).

public theorem hireAssistant_expectedHires_toReal (xs : List α)
    (hxs : xs.Nodup) :
    ((uniformPermutation xs).expectENN
        (fun ys => ((hireAssistant ys).time.2 : ℝ≥0∞))).toReal =
      ∑ i : Fin xs.length, (1 : ℝ) / (i.val + 1)

Uses 4 · Used by 1

Statement usesThe hire-assistant scan · Uniformly random rearrangement of a list · Extended expectation

Proof usesExpected number of hires under a random permutation

Used byExpected number of hires is the harmonic number

TheoremExpected number of hires is the harmonic number#✓fully proved

Let \(x\) be a list of \(n\) pairwise distinct elements of a linearly ordered type, and rearrange its entries by a uniformly random permutation of the indices. The expected number of hires that the hire-assistant procedure (interview the entries in order, hiring each one strictly better than every earlier one) makes on the rearranged list, an element of \([0, \infty]\), converted to a real number, equals the harmonic number \(H_n = \sum_{k=1}^{n} \frac{1}{k}\).

public theorem hireAssistant_expectedHires_toReal_eq_harmonic
    (xs : List α) (hxs : xs.Nodup) :
    ((uniformPermutation xs).expectENN
        (fun ys => ((hireAssistant ys).time.2 : ℝ≥0∞))).toReal =
      (harmonic xs.length : ℝ)

Uses 4

Statement usesThe hire-assistant scan · Uniformly random rearrangement of a list · Extended expectation

Proof usesExpected number of hires as a real harmonic sum

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.