Documentation

Complexity.Algorithms.Lean.FusionTree.Sketch

Significant bits and perfect sketches #

The perfect sketch used in fusion trees retains the most significant differing bit of each adjacent pair of stored keys. Packing these selected bits preserves strict order on the stored keys. It need not preserve the position of an arbitrary query among those keys: query correction is a separate step. This module makes no claim about word-RAM running time.

Main definitions #

Main results #

References #

See [FW93] and MIT 6.851, Spring 2021, Lecture 12, sections 4–5.

source
def Cslib.Algorithms.Lean.FusionTree.relevantBits {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) :
Finset ℕ

Select the highest differing bit of each adjacent pair of keys. Equal adjacent keys select the default position zero; the order-preservation theorem assumes strictly increasing keys.

Instances For
    source
    theorem Cslib.Algorithms.Lean.FusionTree.relevantBits_card_le {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) :
    (relevantBits w keys).card ≤ n - 1

    There are at most n - 1 relevant positions for n keys, including the empty case.

    source
    theorem Cslib.Algorithms.Lean.FusionTree.relevantBits_subset_range {n w : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) :
    relevantBits w keys ⊆ Finset.range w

    For strictly increasing bounded keys, every relevant bit lies within the word width.

    source
    theorem Cslib.Algorithms.Lean.FusionTree.highestDiff_mem_relevantBits {n : ℕ} (w : ℕ) (keys : Fin (n + 1) → ℕ) (i : Fin n) :
    BitString.highestDiff w (keys i.castSucc) (keys i.succ) ∈ relevantBits w keys

    The significant bit of any adjacent pair is selected.

    source
    theorem Cslib.Algorithms.Lean.FusionTree.strictMono_sketch {n w : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) :
    StrictMono fun (i : Fin n) => BitString.sketch (relevantBits w keys) (keys i)

    Perfect sketches preserve strict order on all stored keys. This statement concerns stored keys only, and does not justify locating an arbitrary query by its sketch alone.

    source
    theorem Cslib.Algorithms.Lean.FusionTree.sketch_injective {n w : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) :
    Function.Injective fun (i : Fin n) => BitString.sketch (relevantBits w keys) (keys i)

    In particular, the stored keys have distinct perfect sketches.

    source
    theorem Cslib.Algorithms.Lean.FusionTree.sketch_relevantBits_lt_two_pow {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (x : ℕ) :
    BitString.sketch (relevantBits w keys) x < 2 ^ (n - 1)

    The sketch of any word, including a query, uses at most n - 1 bits.