4.1. Updates and Queries🔗

Cslib.DataStructure.CountMin.Table d w is a vector of d rows, each with w natural-number counters. A hash bank h : Fin d → X → Fin w selects one bucket per row for each item. An update adds its weight to those buckets. Cslib.DataStructure.CountMin.run folds the update function over the stream, starting from zero. A query takes the minimum of its addressed counters, so queries require at least one row.

Here two rows hash the low and high bits of four possible items. Item 3 is absent from the stream, and the other three items have different weights.

def exampleHash (r : Fin 2) (x : Fin 4) : Fin 2 :=
  if r = 0 then ⟨x.val % 2, Nat.mod_lt _ (byr:Fin 2x:Fin 4⊢ 0 < 2 decideAll goals completed! 🐙)⟩
  else ⟨x.val / 2, byr:Fin 2x:Fin 4⊢ ↑x / 2 < 2 omegaAll goals completed! 🐙⟩

def exampleStream : List (Fin 4 × ℕ) := [(0, 2), (1, 3), (2, 5)]

example : (run exampleHash exampleStream).toList.map Vector.toList =
    [[7, 3], [5, 5]] := by⊢ List.map Vector.toList (Vector.toList (run exampleHash exampleStream)) = [[7, 3], [5, 5]]
  decideAll goals completed! 🐙

example : List.ofFn (fun x : Fin 4 =>
    estimate exampleHash (run exampleHash exampleStream) x) =
      [5, 3, 5, 3] := by⊢ (List.ofFn fun x => estimate exampleHash (run exampleHash exampleStream) x) = [5, 3, 5, 3]
  decideAll goals completed! 🐙

The true frequencies are 2, 3, 5, 0. Collisions increase the estimates for items 0 and 3. An absent item can therefore have a positive estimate. The deterministic guarantee is Cslib.DataStructure.CountMin.frequency_le_estimate_run:

example (x : Fin 4) : frequency exampleStream x ≤
    estimate exampleHash (run exampleHash exampleStream) x :=
  frequency_le_estimate_run exampleHash exampleStream x