Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bloom-filter

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/bloom_filter.clj1 definitions, 3 theorems

AHoF Bloom Filter: a space-efficient probabilistic set that answers membership with NO FALSE NEGATIVES (if it says absent, the element was never added) but possible false positives. An element sets k hash-indexed bits on insertion; a query returns 'possibly present' only when ALL k of its bits are set: possibly-present? bit-a bit-b = bit-a AND bit-b (shown for k = 2 hash bits), over booleans. Defined: the membership test as a boolean conjunction of the queried bits (via logic/if-data over Bool). Proved native and axiom-free, as worked instances: bits (true, true) give possibly present, and bits (false, true) and (true, false) each give absent. The structure's classical no-false-negatives guarantee is not proved here. The hash functions and the bit array are executable. Requires data/Bool, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.bloom-filter` prints this classification.

bloom-filter/possibly-present? :
  (x₁ x₂ : data/Bool)
  → data/Bool

bloom-filter/all-bits-set-possibly-present :
  → bloom-filter/possibly-present? data/true data/true = data/true

bloom-filter/unset-first-bit-absent :
  → bloom-filter/possibly-present? data/false data/true = data/false

bloom-filter/unset-second-bit-absent :
  → bloom-filter/possibly-present? data/true data/false = data/false