Skip to content

Perfect hashing

27 fully proved

Perfect Hashing

StructureTwo-level perfect hash table#✓fully proved

Fix a type \(\alpha\) of keys, a type \(\beta\) of values and a primary hash function \(h : \alpha \to \mathbb{N}\). A two-level (FKS) perfect hash table consists of a number \(b > 0\) of buckets and, for each bucket \(i < b\), a secondary size \(m_i \in \mathbb{N}\), a secondary hash function \(h_i : \alpha \to \mathbb{N}\) and a secondary table of \(m_i\) slots, each of which is empty or holds one binding \((k, v)\) with \(k \in \alpha\) and \(v \in \beta\).

The intended position of a key \(k\) is slot \(h_i(k) \bmod m_i\) of bucket \(i = h(k) \bmod b\). The structure itself imposes no condition on the hash functions and does not require bindings to sit at their intended positions; that requirement is the separate validity condition.

public structure PerfectHashing (α : Type u) (β : Type v) (primaryHash : α → Nat) where
  /-- The positive number of primary buckets. -/
  bucketCount : Nat
  /-- The table has at least one bucket. -/
  bucketCount_pos : 0 < bucketCount
  /-- The number of slots in each bucket's secondary table. -/
  secondarySize : Fin bucketCount → Nat
  /-- The secondary hash function of each bucket, reduced modulo the bucket size. -/
  secondaryHash : Fin bucketCount → α → Nat
  /-- The secondary tables, one optional binding per slot. -/
  secondaryTable : ∀ i : Fin bucketCount, Vector (Option (α × β)) (secondarySize i)
Used by 24
Used byOccupancy of a perfect-hashing bucket · Bucket occupancy is at most the secondary table size · Empty perfect hash table · Entries of a perfect hash table · Placement implies secondary injectivity · Lookup in a perfect hash table · Lookup fails exactly on unstored keys · Lookup finds every entry · Lookup finds every stored binding · Entries of a perfect hash table are its stored bindings · Successful perfect-hash lookups return entries · Placement suffices for validity of a perfect hash table · The empty perfect hash table stores nothing · Each secondary table fits in the total secondary space · FKS square sizing rule · Bindings stored in a perfect hash table · Soundness of perfect-hash lookup · Stored values in a valid perfect hash table are unique · Total number of keys of a perfect hash table · Total secondary space of a perfect hash table · Total secondary space under square sizing · Quadratic space bound under square sizing · Valid perfect hash table · The empty perfect hash table is valid

DefinitionLookup in a perfect hash table#✓fully proved

To look up a key \(k\) in a two-level perfect hash table with \(b\) buckets, primary hash \(h\), secondary sizes \(m_i\) and secondary hashes \(h_i\), let \(i = h(k) \bmod b\). If \(m_i = 0\), the lookup returns nothing. Otherwise it inspects the single slot \(h_i(k) \bmod m_i\) of the secondary table of bucket \(i\): if that slot holds a binding \((k, v)\), the lookup returns \(v\); if the slot is empty or holds a binding with a different key, the lookup returns nothing.

public def lookup [DecidableEq α] (key : α) (table : PerfectHashing α β primaryHash) :
    Option β :=
  let i : Fin table.bucketCount :=
    ⟨primaryHash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩
  if hs : 0 < table.secondarySize i then
    match (table.secondaryTable i).get
        ⟨table.secondaryHash i key % table.secondarySize i, Nat.mod_lt _ hs⟩ with
    | some (k', v) => if k' = key then some v else none
    | none => none
  else
    none
Uses 1 · Used by 6
Statement usesTwo-level perfect hash table
Used byLookup in the empty perfect hash table fails · Lookup fails exactly on unstored keys · Lookup finds every entry · Lookup finds every stored binding · Successful perfect-hash lookups return entries · Soundness of perfect-hash lookup

DefinitionEmpty perfect hash table#✓fully proved

Given a primary hash function \(h\) from keys to natural numbers, a number of buckets \(b > 0\), and for each bucket \(i < b\) a secondary table size \(m_i\) and a secondary hash function \(h_i\), the empty table is the two-level perfect hash table with primary hash \(h\), \(b\) buckets, secondary sizes \(m_i\) and secondary hashes \(h_i\) in which every slot of every secondary table is vacant.

public def empty (primaryHash : α → Nat) (bucketCount : Nat)
    (bucketCount_pos : 0 < bucketCount) (secondarySize : Fin bucketCount → Nat)
    (secondaryHash : Fin bucketCount → α → Nat) :
    PerfectHashing α β primaryHash where
  bucketCount := bucketCount
  bucketCount_pos := bucketCount_pos
  secondarySize := secondarySize
  secondaryHash := secondaryHash
  secondaryTable := fun i => Vector.replicate (secondarySize i) none
Uses 1 · Used by 4
Statement usesTwo-level perfect hash table
Used byThe empty perfect hash table has no entries · Lookup in the empty perfect hash table fails · The empty perfect hash table stores nothing · The empty perfect hash table is valid

DefinitionBindings stored in a perfect hash table#✓fully proved

A key \(k\) and a value \(v\) are stored in a two-level perfect hash table \(T\) when some secondary slot, in some bucket of \(T\), holds the binding \((k, v)\).

public def Stored (table : PerfectHashing α β primaryHash) (key : α) (value : β) :
    Prop :=
  ∃ (i : Fin table.bucketCount) (j : Fin (table.secondarySize i)),
    (table.secondaryTable i).get j = some (key, value)
Uses 1 · Used by 10
Statement usesTwo-level perfect hash table
Used byThe empty perfect hash table has no entries · Lookup in the empty perfect hash table fails · Lookup fails exactly on unstored keys · Lookup finds every entry · Lookup finds every stored binding · Entries of a perfect hash table are its stored bindings · Successful perfect-hash lookups return entries · The empty perfect hash table stores nothing · Soundness of perfect-hash lookup · Stored values in a valid perfect hash table are unique

DefinitionEntries of a perfect hash table#✓fully proved

The entries of a two-level perfect hash table form the list of the bindings \((k, v)\) held in its occupied secondary slots, listed bucket by bucket in increasing bucket order and, within each bucket, in increasing slot order.

A pair \((k, v)\) is a member of this list exactly when it is held in some slot of the table.

public def entries (table : PerfectHashing α β primaryHash) : List (α × β) :=
  (List.finRange table.bucketCount).flatMap fun i =>
    (List.finRange (table.secondarySize i)).filterMap fun j =>
      (table.secondaryTable i).get j
Uses 1 · Used by 4
Statement usesTwo-level perfect hash table
Used byThe empty perfect hash table has no entries · Lookup finds every entry · Entries of a perfect hash table are its stored bindings · Successful perfect-hash lookups return entries

StructureValid perfect hash table#✓fully proved

Let \(T\) be a two-level perfect hash table with primary hash \(h\), \(b\) buckets, secondary table sizes \(m_i\) and secondary hashes \(g_i\). Then \(T\) is valid when two conditions hold. Placement: whenever slot \(j\) of bucket \(i\) holds a binding \((k, v)\), we have \(i = h(k) \bmod b\) and \(j = g_i(k) \bmod m_i\). Injectivity: for every bucket \(i\), if keys \(k_1\) and \(k_2\) both occur in bindings stored in bucket \(i\) and \(g_i(k_1) \bmod m_i = g_i(k_2) \bmod m_i\), then \(k_1 = k_2\).

The injectivity condition follows from placement. It is recorded separately because choosing secondary hash functions that are injective on each bucket's keys is the task of the FKS construction.

Cslib.Algorithms.Lean.PerfectHashing.Valid · 17 lines 
public structure Valid (table : PerfectHashing α β primaryHash) : Prop where
  /-- Every binding sits at the slot its key hashes to at both levels. -/
  placed : ∀ (i : Fin table.bucketCount) (j : Fin (table.secondarySize i))
      (key : α) (value : β),
    (table.secondaryTable i).get j = some (key, value) →
      (⟨primaryHash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩ :
        Fin table.bucketCount) = i ∧
        j.val = table.secondaryHash i key % table.secondarySize i
  /-- Each bucket's secondary hash does not collide on its stored keys. -/
  injective : ∀ (i : Fin table.bucketCount) (key₁ key₂ : α),
    (∃ (j : Fin (table.secondarySize i)) (value : β),
      (table.secondaryTable i).get j = some (key₁, value)) →
    (∃ (j : Fin (table.secondarySize i)) (value : β),
      (table.secondaryTable i).get j = some (key₂, value)) →
    table.secondaryHash i key₁ % table.secondarySize i =
      table.secondaryHash i key₂ % table.secondarySize i →
    key₁ = key₂
Uses 1 · Used by 6
Statement usesTwo-level perfect hash table
Used byLookup fails exactly on unstored keys · Lookup finds every entry · Lookup finds every stored binding · Placement suffices for validity of a perfect hash table · Stored values in a valid perfect hash table are unique · The empty perfect hash table is valid

Valid

TheoremPlacement implies secondary injectivity#✓fully proved

Let \(T\) be a two-level perfect hash table with \(b\) buckets and primary hash \(h\), and for each bucket \(i\) let \(m_i\) be its secondary table size and \(h_i\) its secondary hash. Suppose every binding \((k, v)\) held in slot \(j\) of bucket \(i\) satisfies \(h(k) \bmod b = i\) and \(j = h_i(k) \bmod m_i\). Then for every bucket \(i\) and all keys \(k_1, k_2\) that are each held, with some value, in some slot of bucket \(i\), if \(h_i(k_1) \bmod m_i = h_i(k_2) \bmod m_i\), then \(k_1 = k_2\).

Cslib.Algorithms.Lean.PerfectHashing.Valid.injective_of_placed · 15 lines 
public theorem injective_of_placed {table : PerfectHashing α β primaryHash}
    (placed : ∀ (i : Fin table.bucketCount) (j : Fin (table.secondarySize i))
      (key : α) (value : β),
      (table.secondaryTable i).get j = some (key, value) →
        (⟨primaryHash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩ :
          Fin table.bucketCount) = i ∧
          j.val = table.secondaryHash i key % table.secondarySize i) :
    ∀ (i : Fin table.bucketCount) (key₁ key₂ : α),
      (∃ (j : Fin (table.secondarySize i)) (value : β),
        (table.secondaryTable i).get j = some (key₁, value)) →
      (∃ (j : Fin (table.secondarySize i)) (value : β),
        (table.secondaryTable i).get j = some (key₂, value)) →
      table.secondaryHash i key₁ % table.secondarySize i =
        table.secondaryHash i key₂ % table.secondarySize i →
      key₁ = key₂
Uses 1 · Used by 1
Statement usesTwo-level perfect hash table
Used byPlacement suffices for validity of a perfect hash table

TheoremPlacement suffices for validity of a perfect hash table#✓fully proved

Let \(T\) be a two-level perfect hash table with \(b\) buckets, primary hash \(h\), secondary sizes \(m_i\) and secondary hashes \(h_i\). If, whenever slot \(j\) of the secondary table of bucket \(i\) holds a binding \((k, v)\), we have \(h(k) \bmod b = i\) and \(j = h_i(k) \bmod m_i\), then \(T\) is valid.

public theorem mk_of_placed {table : PerfectHashing α β primaryHash}
    (placed : ∀ (i : Fin table.bucketCount) (j : Fin (table.secondarySize i))
      (key : α) (value : β),
      (table.secondaryTable i).get j = some (key, value) →
        (⟨primaryHash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩ :
          Fin table.bucketCount) = i ∧
          j.val = table.secondaryHash i key % table.secondarySize i) :
    Valid table
Uses 3 · Used by 1
Statement usesTwo-level perfect hash table · Valid perfect hash table
Proof usesPlacement implies secondary injectivity
Used byThe empty perfect hash table is valid

Perfect Hashing

TheoremEntries of a perfect hash table are its stored bindings#✓fully proved

For every two-level perfect hash table, every key \(k\) and every value \(v\), the pair \((k, v)\) belongs to the list of entries of the table (the contents of its occupied secondary slots, bucket by bucket) if and only if some secondary slot of the table holds the binding \((k, v)\).

public theorem mem_entries_iff (table : PerfectHashing α β primaryHash) (key : α)
    (value : β) :
    (key, value) ∈ table.entries ↔ Stored table key value
Uses 3 · Used by 3
Statement usesTwo-level perfect hash table · Bindings stored in a perfect hash table · Entries of a perfect hash table
Used byThe empty perfect hash table has no entries · Lookup finds every entry · Successful perfect-hash lookups return entries

TheoremThe empty perfect hash table is valid#✓fully proved

For every primary hash function, every positive number of buckets, and every choice of secondary table sizes and secondary hash functions, the empty two-level perfect hash table with these parameters is valid: no slot is occupied, so both conditions of validity hold vacuously.

public theorem valid_empty (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount)
    (secondarySize : Fin bucketCount → Nat)
    (secondaryHash : Fin bucketCount → α → Nat) :
    Valid (empty primaryHash bucketCount bucketCount_pos secondarySize secondaryHash :
      PerfectHashing α β primaryHash)
Uses 4 · Used by 1
Statement usesValid perfect hash table · Empty perfect hash table
Proof usesTwo-level perfect hash table · Placement suffices for validity of a perfect hash table
Used byLookup in the empty perfect hash table fails

TheoremThe empty perfect hash table stores nothing#✓fully proved

For every primary hash function, every number \(b > 0\) of buckets, every choice of secondary sizes and secondary hash functions, every key \(k\) and every value \(v\), no secondary slot of the empty two-level perfect hash table with these data holds the binding \((k, v)\).

public theorem not_stored_empty (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount)
    (secondarySize : Fin bucketCount → Nat)
    (secondaryHash : Fin bucketCount → α → Nat) (key : α) (value : β) :
    ¬ Stored (empty primaryHash bucketCount bucketCount_pos secondarySize secondaryHash :
      PerfectHashing α β primaryHash) key value
Uses 3 · Used by 2
Statement usesBindings stored in a perfect hash table · Empty perfect hash table
Proof usesTwo-level perfect hash table
Used byThe empty perfect hash table has no entries · Lookup in the empty perfect hash table fails

TheoremSoundness of perfect-hash lookup#✓fully proved

For a two-level perfect hash table with decidable equality on keys, and with no validity hypothesis, if looking up a key \(k\) returns a value \(v\), then some secondary slot of the table holds the binding \((k, v)\).

public theorem stored_of_lookup_eq_some [DecidableEq α]
    {table : PerfectHashing α β primaryHash} {key : α} {value : β}
    (h : lookup key table = some value) : Stored table key value
Uses 3 · Used by 2
Statement usesTwo-level perfect hash table · Bindings stored in a perfect hash table · Lookup in a perfect hash table
Used byLookup fails exactly on unstored keys · Successful perfect-hash lookups return entries

TheoremLookup finds every stored binding#✓fully proved

For a valid two-level perfect hash table, if the binding \((k, v)\) is held in some slot of the table, then looking up \(k\) returns \(v\).

public theorem lookup_eq_some_of_stored [DecidableEq α]
    {table : PerfectHashing α β primaryHash} (valid : Valid table) {key : α}
    {value : β} (h : Stored table key value) :
    lookup key table = some value
Uses 4 · Used by 2
Statement usesTwo-level perfect hash table · Bindings stored in a perfect hash table · Valid perfect hash table · Lookup in a perfect hash table
Used byLookup fails exactly on unstored keys · Lookup finds every entry

TheoremStored values in a valid perfect hash table are unique#✓fully proved

In a valid two-level perfect hash table, if some secondary slots hold bindings \((k, v_1)\) and \((k, v_2)\) with the same key \(k\), then \(v_1 = v_2\).

This is a direct consequence of placement (both bindings would occupy the one slot their shared key hashes to), so it needs no decidable equality on keys.

public theorem stored_unique
    {table : PerfectHashing α β primaryHash} (valid : Valid table) {key : α}
    {value₁ value₂ : β} (h₁ : Stored table key value₁)
    (h₂ : Stored table key value₂) : value₁ = value₂
Uses 3
Statement usesTwo-level perfect hash table · Bindings stored in a perfect hash table · Valid perfect hash table

TheoremLookup fails exactly on unstored keys#✓fully proved

For a valid two-level perfect hash table and any key \(k\), looking up \(k\) returns no value if and only if there is no value \(v\) such that the binding \((k, v)\) is held in some slot of the table.

public theorem lookup_eq_none_iff [DecidableEq α]
    {table : PerfectHashing α β primaryHash} (valid : Valid table) (key : α) :
    lookup key table = none ↔ ∀ value : β, ¬ Stored table key value
Uses 6 · Used by 1
Statement usesTwo-level perfect hash table · Bindings stored in a perfect hash table · Valid perfect hash table · Lookup in a perfect hash table
Proof usesLookup finds every stored binding · Soundness of perfect-hash lookup
Used byLookup in the empty perfect hash table fails

TheoremLookup finds every entry#✓fully proved

For a valid two-level perfect hash table, if the pair \((k, v)\) belongs to the list of entries of the table, then looking up \(k\) returns \(v\).

public theorem lookup_eq_some_of_mem_entries [DecidableEq α]
    {table : PerfectHashing α β primaryHash} (valid : Valid table) {key : α}
    {value : β} (h : (key, value) ∈ table.entries) :
    lookup key table = some value
Uses 7
Statement usesTwo-level perfect hash table · Valid perfect hash table · Entries of a perfect hash table · Lookup in a perfect hash table
Proof usesBindings stored in a perfect hash table · Lookup finds every stored binding · Entries of a perfect hash table are its stored bindings

TheoremSuccessful perfect-hash lookups return entries#✓fully proved

For a two-level perfect hash table with decidable equality on keys, if looking up a key \(k\) returns a value \(v\), then \((k, v)\) belongs to the list of entries of the table. No validity hypothesis is needed.

public theorem mem_entries_of_lookup_eq_some [DecidableEq α]
    {table : PerfectHashing α β primaryHash} {key : α} {value : β}
    (h : lookup key table = some value) : (key, value) ∈ table.entries
Uses 6
Statement usesTwo-level perfect hash table · Entries of a perfect hash table · Lookup in a perfect hash table
Proof usesBindings stored in a perfect hash table · Entries of a perfect hash table are its stored bindings · Soundness of perfect-hash lookup

TheoremLookup in the empty perfect hash table fails#✓fully proved

For every primary hash function, every number of buckets \(b > 0\), all secondary table sizes and secondary hash functions, and every key \(k\), looking up \(k\) in the empty table returns no value.

@[simp]
public theorem lookup_empty [DecidableEq α] (bucketCount : Nat)
    (bucketCount_pos : 0 < bucketCount) (secondarySize : Fin bucketCount → Nat)
    (secondaryHash : Fin bucketCount → α → Nat) (key : α) :
    lookup key (empty primaryHash bucketCount bucketCount_pos secondarySize
      secondaryHash : PerfectHashing α β primaryHash) = none
Uses 6
Statement usesEmpty perfect hash table · Lookup in a perfect hash table
Proof usesBindings stored in a perfect hash table · Lookup fails exactly on unstored keys · The empty perfect hash table stores nothing · The empty perfect hash table is valid

TheoremThe empty perfect hash table has no entries#✓fully proved

For every primary hash function, every number of buckets \(b > 0\), and all secondary table sizes and secondary hash functions, the list of entries of the empty table is the empty list.

@[simp]
public theorem entries_empty (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount)
    (secondarySize : Fin bucketCount → Nat)
    (secondaryHash : Fin bucketCount → α → Nat) :
    entries (empty primaryHash bucketCount bucketCount_pos secondarySize secondaryHash :
      PerfectHashing α β primaryHash) = []
Uses 5
Statement usesEmpty perfect hash table · Entries of a perfect hash table
Proof usesBindings stored in a perfect hash table · Entries of a perfect hash table are its stored bindings · The empty perfect hash table stores nothing

DefinitionOccupancy of a perfect-hashing bucket#✓fully proved

For a two-level perfect hash table and a bucket \(i\), the occupancy \(n_i\) of bucket \(i\) is the number of slots of the secondary table of bucket \(i\) that hold a binding. It is the \(n_i\) of the Fredman–Komlós–Szemerédi analysis.

public def bucketSize (table : PerfectHashing α β primaryHash)
    (i : Fin table.bucketCount) : Nat :=
  ((List.finRange (table.secondarySize i)).filter fun j =>
    ((table.secondaryTable i).get j).isSome).length
Uses 1 · Used by 5
Statement usesTwo-level perfect hash table
Used byBucket occupancy is at most the secondary table size · FKS square sizing rule · Total number of keys of a perfect hash table · Total secondary space under square sizing · Quadratic space bound under square sizing

DefinitionTotal number of keys of a perfect hash table#✓fully proved

For a two-level perfect hash table, write \(n_i\) for the number of occupied secondary slots of bucket \(i\). The total number of keys of the table is \(\sum_i n_i\), the number of occupied secondary slots over all buckets.

public def totalKeys (table : PerfectHashing α β primaryHash) : Nat :=
  ∑ i : Fin table.bucketCount, bucketSize table i
Uses 2 · Used by 1
Statement usesTwo-level perfect hash table · Occupancy of a perfect-hashing bucket
Used byQuadratic space bound under square sizing

DefinitionTotal secondary space of a perfect hash table#✓fully proved

For a two-level perfect hash table, write \(m_i\) for the number of slots of the secondary table of bucket \(i\). The total secondary space of the table is \(\sum_i m_i\), the number of secondary slots over all buckets.

public def totalSecondarySpace (table : PerfectHashing α β primaryHash) : Nat :=
  ∑ i : Fin table.bucketCount, table.secondarySize i
Uses 1 · Used by 3
Statement usesTwo-level perfect hash table
Used byEach secondary table fits in the total secondary space · Total secondary space under square sizing · Quadratic space bound under square sizing

DefinitionFKS square sizing rule#✓fully proved

A two-level perfect hash table with \(b\) buckets is square-sized when, for every bucket \(i < b\), the size \(m_i\) of its secondary table equals \(n_i^2\), where \(n_i\) is the number of occupied slots of that secondary table.

public def SquareSized (table : PerfectHashing α β primaryHash) : Prop :=
  ∀ i : Fin table.bucketCount, table.secondarySize i = (bucketSize table i) ^ 2
Uses 2 · Used by 2
Statement usesTwo-level perfect hash table · Occupancy of a perfect-hashing bucket
Used byTotal secondary space under square sizing · Quadratic space bound under square sizing

TheoremBucket occupancy is at most the secondary table size#✓fully proved

For every two-level perfect hash table and every bucket \(i\), the number \(n_i\) of occupied slots of bucket \(i\) is at most the number \(m_i\) of slots of the secondary table of bucket \(i\).

public theorem bucketSize_le_secondarySize (table : PerfectHashing α β primaryHash)
    (i : Fin table.bucketCount) :
    bucketSize table i ≤ table.secondarySize i
Uses 2
Statement usesTwo-level perfect hash table · Occupancy of a perfect-hashing bucket

TheoremEach secondary table fits in the total secondary space#✓fully proved

In a two-level perfect hash table with \(b\) buckets and secondary sizes \(m_0, \dots, m_{b-1}\), every bucket \(i < b\) satisfies \(m_i \le \sum_{j < b} m_j\), the total secondary space.

public theorem secondarySize_le_totalSecondarySpace
    (table : PerfectHashing α β primaryHash) (i : Fin table.bucketCount) :
    table.secondarySize i ≤ totalSecondarySpace table
Uses 2
Statement usesTwo-level perfect hash table · Total secondary space of a perfect hash table

TheoremTotal secondary space under square sizing#✓fully proved

Let \(T\) be a two-level perfect hash table satisfying the FKS sizing rule, and write \(n_i\) for the number of occupied secondary slots of bucket \(i\). Then the total secondary space of \(T\) equals \(\sum_i n_i^2\), the sum over all buckets \(i\).

public theorem totalSecondarySpace_eq_sum_sq
    {table : PerfectHashing α β primaryHash} (hsq : SquareSized table) :
    totalSecondarySpace table =
      ∑ i : Fin table.bucketCount, (bucketSize table i) ^ 2
Uses 4 · Used by 1
Statement usesTwo-level perfect hash table · FKS square sizing rule · Occupancy of a perfect-hashing bucket · Total secondary space of a perfect hash table
Used byQuadratic space bound under square sizing

TheoremQuadratic space bound under square sizing#✓fully proved

If a two-level perfect hash table satisfies the FKS sizing rule, then its total secondary space is at most the square of its total number of keys.

This is weaker than the linear space bound of Fredman, Komlós and Szemerédi, which also depends on the choice of a good primary hash function.

public theorem totalSecondarySpace_le_totalKeys_sq
    {table : PerfectHashing α β primaryHash} (hsq : SquareSized table) :
    totalSecondarySpace table ≤ (totalKeys table) ^ 2
Uses 6
Statement usesTwo-level perfect hash table · FKS square sizing rule · Total number of keys of a perfect hash table · Total secondary space of a perfect hash table
Proof usesOccupancy of a perfect-hashing bucket · Total secondary space under square sizing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.