Chapter 11 - Hash Tables

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, and CLRS.Chapter11.expectedUnsuccessfulSearchCost_finiteHashInsert.

Current Gaps

The deterministic insert/delete/search layer is compiler-clean, and the finite-uniform bucket layer now proves the load-factor, nonnegativity, and single-insert expected-cost interfaces. The remaining probability gap is a full model over random keys or random hash functions with independence assumptions.