Documentation

Complexity.Algorithms.WordRAM.FusionTree.Query

Concrete fusion-tree RAM predecessor endpoint #

At each physical word width, one standard-basis program with 1024 registers traverses any represented preprocessed tree. Its code depends only on width, with a uniform code-size bound. Query, record base, keys and all node parameters are runtime data. The query returns an inclusive predecessor as presence in register 32 and a full key in register 33; key zero is distinct from absence. The flat program halts with register 33, and the proved final state also exposes register 32.

For a sorted distinct list of n fitting full keys, initialization, traversal, all node calls, pointer loads, loop overhead and halt together take at most 3100000 * (Nat.log w n + 1) instructions for every w ≥ 2. The concrete representation uses at most 126n + 18 words, including empty roots. The arena's one-past-end frontier must fit a word separately from the keys and query. No RAM preprocessing-time bound is claimed; preprocessing is a classical static construction.

Main definitions #

Main results #

References #

source
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.size_code (w : ℕ) :
(code w).size ≤ 201050

One fixed size bound for all physical widths. Only width selects the node code.

source
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.length_program (w : ℕ) :
List.length (program w) ≤ 201051

The compiled family has a uniform finite size bound, including its final halt.

source
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec {w q p : ℕ} {t : Lean.FusionTree.Tree} {x : WordRAM.Data registers} (hxq : x.regs query = q) (hxp : x.regs pointer = p) (ht : Lean.FusionTree.Tree.Valid (Lean.FusionTree.branching w) t) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) t.keys) (hk : ∀ k ∈ t.keys, WordRAM.Fits w k) (hr : Rep (parameterWords w) t p x.mem) (ha : ArenaFits w p t) (hq : WordRAM.Fits w q) :
∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (code w) x y (201022 * (t.height + 1) + 7) ∧ Done q (Lean.FusionTree.Tree.predecessor q t) x.mem y

Complete structured query, including installation of every persistent constant. Only the query and initial pointer need to be supplied in registers.

source
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_build {w q p : ℕ} {xs : List ℕ} {x : WordRAM.Data registers} (hw : 2 ≤ w) (hxq : x.regs query = q) (hxp : x.regs pointer = p) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs) (hk : ∀ k ∈ xs, WordRAM.Fits w k) (hr : Rep (parameterWords w) (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs) p x.mem) (ha : ArenaFits w p (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) (hq : WordRAM.Fits w q) :
∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (code w) x y (3100000 * (Nat.log w xs.length + 1) - 1) ∧ Done q (Lean.FusionTree.Tree.predecessor q (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) x.mem y

The constructed tree has a uniform word-logarithmic query bound. One instruction is reserved for the flat program's halt. All node and representation premises are discharged from the sorted full keys and actual preprocessing, with no node oracle.

source
noncomputable def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.initial (w : ℕ) (xs : List ℕ) (p q : ℕ) :
WordRAM.Data registers

Concrete preprocessed RAM, with only query and record base in the register file. All other registers initially hold zero. This is static construction, not a RAM instruction.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.initial_bounded {w p q : ℕ} {xs : List ℕ} (hk : ∀ k ∈ xs, WordRAM.Fits w k) (ha : ArenaFits w p (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) (hq : WordRAM.Fits w q) :
    WordRAM.Data.Bounded w (initial w xs p q)

    The actual initial register and memory words fit under the explicit query/key/arena bounds.

    source
    theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.query_spec {w p q : ℕ} {xs : List ℕ} (hw : 2 ≤ w) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs) (hk : ∀ k ∈ xs, WordRAM.Fits w k) (ha : ArenaFits w p (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) (hq : WordRAM.Fits w q) :
    WordRAM.Data.Bounded w (initial w xs p q) ∧ (encode (parameterWords w) p (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)).length ≤ 126 * xs.length + 18 ∧ ∃ (y : WordRAM.Data registers) (k : ℕ), k + 1 ≤ 3100000 * (Nat.log w xs.length + 1) ∧ WordRAM.Runs w (program w) { pc := 0, data := initial w xs p q } { pc := (code w).size, data := y } k ∧ WordRAM.Executes w (program w) { pc := 0, data := initial w xs p q } (y.regs value) (k + 1) ∧ Done q (Lean.FusionTree.Tree.predecessor q (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) (initial w xs p q).mem y

    Full concrete endpoint. The final-state observation exposes the presence flag as well as the halted value. The bound includes the halt; memory and query are preserved exactly. Allocation is O(n+1) for all inputs and O(n) for nonempty inputs.

    source
    theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.answer_some_iff {w q a : ℕ} {xs : List ℕ} {mem : ℕ → ℕ} {y : WordRAM.Data registers} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs) (hy : Done q (Lean.FusionTree.Tree.predecessor q (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) mem y) :
    answer y = some a ↔ a ∈ xs ∧ a ≤ q ∧ ∀ k ∈ xs, k ≤ q → k ≤ a

    Returned full keys are exactly the inclusive predecessors of the stored set.

    source
    theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.answer_none_iff {w q : ℕ} {xs : List ℕ} {mem : ℕ → ℕ} {y : WordRAM.Data registers} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs) (hy : Done q (Lean.FusionTree.Tree.predecessor q (Lean.FusionTree.Tree.build (Lean.FusionTree.branching w) xs)) mem y) :
    answer y = none ↔ ∀ k ∈ xs, q < k

    Absence is exactly the case where every stored key is greater than the query.