Pairwise-independent hashing -- definitions

This module gives the exact finite interface used by Stockmeyer-style approximate counting. A seed selects a fixed-width hash function. Each input is uniformly distributed over the range, and the outputs on two distinct inputs are jointly uniform.

structure Complexity.PairwiseIndependentHash (domainWidth rangeWidth seedWidth : ℕ) : Type

A fixed-width family of exactly pairwise-independent hash functions, represented by a uniformly random bit-string seed.

• eval : BitString seedWidth → BitString domainWidth → BitString rangeWidth

  Evaluate the seeded hash function on one domain element.

• uniform (input : BitString domainWidth) (output : BitString rangeWidth) : eventProb {seed : Fin seedWidth → Bool | self.eval seed input = output} = 1 / 2 ^ rangeWidth

  Every fixed input hashes uniformly to every fixed range element.

• pairwise {first second : BitString domainWidth} : first ≠ second → ∀ (firstOutput secondOutput : BitString rangeWidth), eventProb {seed : Fin seedWidth → Bool | self.eval seed first = firstOutput ∧ self.eval seed second = secondOutput} = 1 / 2 ^ (2 * rangeWidth)

  Two distinct inputs have jointly uniform hash outputs.

def Complexity.PairwiseIndependentHash.cell {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (seed : BitString seedWidth) : Finset (BitString domainWidth)

Members of set that a seeded hash maps to one target cell.

Equations

• hash.cell set target seed = {input ∈ set | hash.eval seed input = target}

def Complexity.PairwiseIndependentHash.cellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (seed : BitString seedWidth) : ℕ

Number of set members in one seeded target cell.

Equations

• hash.cellSize set target seed = (hash.cell set target seed).card

def Complexity.PairwiseIndependentHash.averageCellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : ℚ

Uniform rational average of the target-cell size over every seed.

Equations

• hash.averageCellSize set target = (∑ seed : Complexity.BitString seedWidth, ↑(hash.cellSize set target seed)) / 2 ^ seedWidth

def Complexity.PairwiseIndependentHash.orderedPairCellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (seed : BitString seedWidth) : ℕ

Number of ordered pairs of distinct set members that land in the same seeded target cell.

Equations

• hash.orderedPairCellSize set target seed = {pair ∈ set.offDiag | hash.eval seed pair.1 = target ∧ hash.eval seed pair.2 = target}.card

def Complexity.PairwiseIndependentHash.averageOrderedPairCellSize {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : ℚ

Uniform rational average of the ordered distinct-pair count in one target cell.

Equations

• hash.averageOrderedPairCellSize set target = (∑ seed : Complexity.BitString seedWidth, ↑(hash.orderedPairCellSize set target seed)) / 2 ^ seedWidth

def Complexity.PairwiseIndependentHash.averageCellSizeSquare {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : ℚ

Uniform rational average of the squared target-cell size.

Equations

• hash.averageCellSizeSquare set target = (∑ seed : Complexity.BitString seedWidth, ↑(hash.cellSize set target seed) ^ 2) / 2 ^ seedWidth

def Complexity.PairwiseIndependentHash.cellSizeVariance {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : ℚ

Variance of the target-cell size over a uniform hash seed.

Equations

• hash.cellSizeVariance set target = (∑ seed : Complexity.BitString seedWidth, (↑(hash.cellSize set target seed) - hash.averageCellSize set target) ^ 2) / 2 ^ seedWidth

def Complexity.PairwiseIndependentHash.deviationEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (radius : ℚ) : Finset (BitString seedWidth)

Seeds whose target-cell size deviates from its mean by at least radius.

Equations

• hash.deviationEvent set target radius = {seed : Complexity.BitString seedWidth | radius ≤ |↑(hash.cellSize set target seed) - hash.averageCellSize set target|}

def Complexity.PairwiseIndependentHash.nonemptyCellEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : Finset (BitString seedWidth)

Seeds whose target hash cell is nonempty. This is the event tested by the NP oracle in Stockmeyer counting.

Equations

• hash.nonemptyCellEvent set target = {seed : Complexity.BitString seedWidth | 0 < hash.cellSize set target seed}

def Complexity.PairwiseIndependentHash.emptyCellEvent {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) : Finset (BitString seedWidth)

Seeds whose target hash cell is empty.

Equations

• hash.emptyCellEvent set target = {seed : Complexity.BitString seedWidth | hash.cellSize set target seed = 0}