Count-Min as a probabilistic program

sampleSketch independently repeats a caller-supplied seed sampler and processes a weighted insertion stream with the resulting hash rows. Its output retains both the row seeds and the materialized counter table, so later queries use the same hashes. sampleQuery constructs a sketch and returns one point query. The hash family is supplied separately and must remain fixed between construction and queries.

When one seed is exactly uniform, repeated calls give the uniform distribution on row-seed tuples. This identifies the output law of the program with the deterministic construction analyzed in CountMin.Probability, giving its fixed-query failure bound. The stream and query are fixed before the seeds are sampled. No running-time or representation cost is asserted for the supplied sampler, hash function, or program.

Main definitions

• Cslib.CountMin.Sketch: row seeds together with the stored counter table.
• Cslib.CountMin.buildSketch, Cslib.CountMin.Sketch.query: deterministic construction and point queries retaining the construction's hashes.
• Cslib.CountMin.sampleSketch, Cslib.CountMin.sampleQuery: probabilistic construction and a fixed point query.

Main results

• Cslib.CountMin.eval_sampleSketch, Cslib.CountMin.eval_sampleQuery: output laws under a uniform seed sampler.
• Cslib.CountMin.frequency_le_of_mem_support_sampleQuery: every possible query result avoids underestimation, without any uniformity assumption.
• Cslib.CountMin.sampleQuery_error_le_inv_two_pow: failure probability at most 2⁻ᵈ when 2 ≤ w * ε, for a two-universal hash family and a uniform seed sampler.

References

• G. Cormode, S. Muthukrishnan, An Improved Data Stream Summary: The Count-Min Sketch and its Applications, Section 4.1, Theorem 1.

structure Cslib.CountMin.Sketch (Seed : Type) (d w : ℕ) : Type

A stored sketch retains its sampled row seeds and materialized counter table.

• seeds : Fin d → Seed

  One seed for each hash row.

• table : Table d w

  The counters updated using these row seeds.

def Cslib.CountMin.buildSketch {X : Type u_1} {Seed : Type} {d w : ℕ} (hash : Seed → X → Fin w) (s : List (X × ℕ)) (seeds : Fin d → Seed) : Sketch Seed d w

Process a stream with a fixed row-seed tuple, retaining it for later queries.

def Cslib.CountMin.Sketch.query {X : Type u_1} {Seed : Type} {d w : ℕ} [NeZero d] (sketch : Sketch Seed d w) (hash : Seed → X → Fin w) (x : X) : ℕ

Query the stored table using the same hash family as in its construction.

def Cslib.CountMin.sampleSketch {X : Type u_1} {Seed : Type} {d w : ℕ} (sampleSeed : ProbComp Seed) (hash : Seed → X → Fin w) (s : List (X × ℕ)) : ProbComp (Sketch Seed d w)

Draw independent row seeds and build the stored sketch for the supplied stream.

def Cslib.CountMin.sampleQuery {X : Type u_1} {Seed : Type} {d w : ℕ} [NeZero d] (sampleSeed : ProbComp Seed) (hash : Seed → X → Fin w) (s : List (X × ℕ)) (x : X) : ProbComp ℕ

Build a sketch and return its estimate for one fixed point query.

theorem Cslib.CountMin.eval_sampleSketch {X : Type u_1} {Seed : Type} {d w : ℕ} [Fintype Seed] [Nonempty Seed] (sampleSeed : ProbComp Seed) (hs : sampleSeed.eval = Probability.PMF.uniformOfFintype Seed) (hash : Seed → X → Fin w) (s : List (X × ℕ)) : (sampleSketch sampleSeed hash s).eval = PMF.map (buildSketch hash s) (Probability.PMF.uniformOfFintype (Fin d → Seed))

A uniform seed sampler gives the deterministic construction a uniform row-seed tuple.

theorem Cslib.CountMin.eval_sampleQuery {X : Type u_1} {Seed : Type} {d w : ℕ} [Fintype Seed] [Nonempty Seed] [NeZero d] (sampleSeed : ProbComp Seed) (hs : sampleSeed.eval = Probability.PMF.uniformOfFintype Seed) (hash : Seed → X → Fin w) (s : List (X × ℕ)) (x : X) : (sampleQuery sampleSeed hash s x).eval = PMF.map (fun (seeds : Fin d → Seed) => estimate (fun (r : Fin d) => hash (seeds r)) (run (fun (r : Fin d) => hash (seeds r)) s) x) (Probability.PMF.uniformOfFintype (Fin d → Seed))

The point-query program has the law of querying a uniformly sampled hash bank.

theorem Cslib.CountMin.frequency_le_of_mem_support_sampleQuery {X : Type u_1} {Seed : Type} {d w : ℕ} [DecidableEq X] [NeZero d] (sampleSeed : ProbComp Seed) (hash : Seed → X → Fin w) (s : List (X × ℕ)) (x : X) {answer : ℕ} (ha : answer ∈ (sampleQuery sampleSeed hash s x).eval.support) : frequency s x ≤ answer

Every possible output of the point-query program is at least the true frequency.

theorem Cslib.CountMin.sampleQuery_error_le_inv_two_pow {X : Type u_1} {Seed : Type} {d w : ℕ} [DecidableEq X] [Fintype Seed] [Nonempty Seed] [NeZero d] [NeZero w] (sampleSeed : ProbComp Seed) (hs : sampleSeed.eval = Probability.PMF.uniformOfFintype Seed) (hash : Seed → X → Fin w) (hh : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) {ε : ℝ} (hε : 0 < ε) (hw : 2 ≤ ↑w * ε) : ((sampleQuery sampleSeed hash s x).eval.toOuterMeasure {answer : ℕ | ↑(frequency s x) + ε * ↑(mass s) < ↑answer}).toReal ≤ (2 ^ d)⁻¹

The actual point-query program has failure probability at most 2⁻ᵈ with at least 2 / ε buckets and independently uniform seeds for a two-universal hash family.