Chapter 11 — Hash Tables

Native fourth-edition chapter guide.

Current source

This guide sources fourth-edition §11.1–§11.5 from the native section modules under CLRSLean.FourthEdition.Chapter_11. Declarations retain the CLRS.Chapter11 namespace; the legacy import CLRSLean.Chapter_11 and its Section_11_* modules forward to these sources during the compatibility period.

Chapter 11 introduces direct-address tables and hash tables. The current CLRS-Lean pass separates deterministic table correctness from probabilistic performance analysis. Section 11.2 now includes a finite-uniform bucket interface: when the searched bucket is uniformly distributed, expected chain length is exactly the load factor, and one insertion increases load factor and unsuccessful-search cost by 1/m.

Sections

• 11.1 Direct-address tables: proved for the functional table model. Main results: CLRS.Chapter11.search_insert_same, CLRS.Chapter11.search_insert_other, CLRS.Chapter11.search_delete_same.

• 11.2 Hash tables: partial. Main results: CLRS.Chapter11.bucket_hashInsert_same, CLRS.Chapter11.hashSearch_hashInsert_self, CLRS.Chapter11.hashSearch_hashInsert_iff, CLRS.Chapter11.hashSearch_hashDelete_self, CLRS.Chapter11.hashSearch_hashDelete_iff, CLRS.Chapter11.uniformAverageFin_indicator_singleton, CLRS.Chapter11.uniformAverageFin_add, CLRS.Chapter11.uniformAverageFin_nonneg, CLRS.Chapter11.finiteHashLoadFactor_nonneg, CLRS.Chapter11.expectedSearchChainLength_eq_loadFactor, CLRS.Chapter11.expectedSearchChainLength_nonneg, CLRS.Chapter11.expectedUnsuccessfulSearchCost_eq_one_plus_loadFactor, CLRS.Chapter11.expectedUnsuccessfulSearchCost_ge_one, CLRS.Chapter11.expectedSearchChainLength_finiteHashInsert, CLRS.Chapter11.finiteHashLoadFactor_finiteHashInsert, CLRS.Chapter11.expectedUnsuccessfulSearchCost_finiteHashInsert, CLRS.Chapter11.expectedRandomChainLength_eq_loadFactor, CLRS.Chapter11.expectedRandomUnsuccessfulSearchCost, CLRS.Chapter11.pairCollisionProb, CLRS.Chapter11.expectedRandomSuccessfulSearchCost, CLRS.Chapter11.universal_expected_collisions, and CLRS.Chapter11.universal_expected_search_cost.

• 11.3 Hash functions: proved. Main results: CLRS.Chapter11.divisionHash_lt, CLRS.Chapter11.multiplicationHash_lt, CLRS.Chapter11.affineHash_isUniversal, CLRS.Chapter11.affineHash_expected_collisions, CLRS.Chapter11.affineHash_expected_search_cost, and CLRS.Chapter11.affineHashMod_isUniversal (CLRS Theorem 11.5, the general mod-m affine family).

• 11.4 Open addressing: proved. Main results: CLRS.Chapter11.openSearch_openInsert, CLRS.Chapter11.openSearch_eq_false_of_absent, CLRS.Chapter11.linearProbe_bijective, CLRS.Chapter11.doubleHashProbe_bijective, CLRS.Chapter11.expectedUnsuccessfulProbes_le, CLRS.Chapter11.expectedSuccessfulProbes_le, and CLRS.Chapter11.expectedSuccessfulProbes_le_ln (CLRS Theorem 11.8, logarithmic form).

• 11.5 Perfect hashing: proved. Main results: CLRS.Chapter11.perfectSearch_iff_mem, CLRS.Chapter11.perfectHash_collision_free_prob_ge_half, and CLRS.Chapter11.perfectHash_expected_total_space_lt_2n.

Current Gaps

The deterministic insert/delete/search layer is compiler-clean, and the finite-uniform bucket layer proves the load-factor, nonnegativity, and single-insert expected-cost interfaces. The SUHA layer proves the expected chain length, unsuccessful-search cost 1 + α, and successful-search cost 1 + (n-1)/(2m) as true expectations, and a universal random-hash-function family bounds expected collisions by α and search cost by 1 + α. Section 11.3 supplies a concrete universal family (the prime-field affine family h_{a,b}(k) = a * k + b) that discharges the IsUniversal hypothesis, so the universal-hashing bounds are no longer conditional. Section 11.4 formalises the open addressing model with probe sequences (linear, quadratic, double hashing) and proves the uniform-hashing expected-probe bounds: unsuccessful search and insertion ≤ 1/(1-α) (CLRS Theorems 11.6-11.7) and successful search (1/α) · ∑_{j<n} 1/(m-j) (CLRS Theorem 11.8 harmonic form), refined to the closed form (1/α) · ln(1/(1-α)) (CLRS.Chapter11.expectedSuccessfulProbes_le_ln). Section 11.5 formalises the two-level perfect-hashing scheme: a primary hash into m = n buckets plus per-bucket secondary tables of size n_j², which are collision-free with probability ≥ 1/2 (Theorem 11.9) and collectively use expected O(n) space (Theorem 11.10). The remaining gap is RAM / probe-count operational semantics.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.