Universe sizes and a contiguous van Emde Boas layout

At depth d the universe has size 2 ^ (2 ^ d). A node has a five-word header, with presence, minimum, maximum, split size and child span at offsets 0 through 4. At positive depth, the header is followed by one recursive summary and then one recursive cluster for each element of the smaller universe. All recursive records are allocated, including empty ones.

This is address arithmetic for the modern minimum-excluded variant described in [Dem15], pp. 4–5. The five-word header and contiguous allocation are choices of this formalization. The original priority-queue construction is due to van Emde Boas, Kaas and Zijlstra [vEBKZ77]; we do not identify these layout choices with that paper's construction. No memory representation or RAM running-time theorem is established here.

Main definitions

• universeSize: the recursively squared universe size.
• span: the number of words in the fully allocated recursive record.
• summaryOffset, clusterOffset: the starts of the recursive records relative to their parent.

Main results

• universeSize_eq_two_pow: the closed form 2 ^ (2 ^ d).
• universeSize_mono, span_mono: monotonicity of universeSize and span in the depth.
• span_le: the explicit linear bound span d ≤ 10 * universeSize d.
• summary_word_lt_span, cluster_word_lt_span: all recursive words lie within their parent.
• summary_end_le_clusterOffset, cluster_end_le_clusterOffset: recursive records do not overlap.

References

• Erik Demaine, Lecture 4: Divide and Conquer: van Emde Boas Trees, MIT 6.046J, Spring 2015
• Peter van Emde Boas, R. Kaas and E. Zijlstra, Design and implementation of an efficient priority queue

def Cslib.Algorithms.Lean.VanEmdeBoas.universeSize : ℕ → ℕ

Size of the depth-d universe; each step squares the previous size.

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.universeSize_zero : universeSize 0 = 2

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.universeSize_succ (d : ℕ) : universeSize (d + 1) = universeSize d * universeSize d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.two_le_universeSize (d : ℕ) : 2 ≤ universeSize d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.universeSize_pos (d : ℕ) : 0 < universeSize d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.universeSize_eq_two_pow (d : ℕ) : universeSize d = 2 ^ 2 ^ d

Depth counts repeated square roots of the universe size, down to the two-element base.

def Cslib.Algorithms.Lean.VanEmdeBoas.span : ℕ → ℕ

Number of words in a fully allocated record, including the five-word header.

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.span_zero : span 0 = 5

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.span_succ (d : ℕ) : span (d + 1) = 5 + (universeSize d + 1) * span d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.five_le_span (d : ℕ) : 5 ≤ span d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.span_pos (d : ℕ) : 0 < span d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.span_add_fifteen_le (d : ℕ) : span d + 15 ≤ 10 * universeSize d

A strengthened linear bound that leaves enough slack for the recursive header.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.span_le (d : ℕ) : span d ≤ 10 * universeSize d

The fully allocated record occupies at most ten words per universe element.

def Cslib.Algorithms.Lean.VanEmdeBoas.summaryOffset : ℕ

Relative start of the summary, immediately after the five-word header.

def Cslib.Algorithms.Lean.VanEmdeBoas.clusterOffset (d i : ℕ) : ℕ

Relative start of cluster i in a depth-d + 1 record. The summary occupies slot zero.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.header_word_lt_span (d : ℕ) {h : ℕ} (hh : h < 5) : h < span d

theorem Cslib.Algorithms.Lean.VanEmdeBoas.header_word_lt_summary_word {h : ℕ} (hh : h < 5) (a : ℕ) : h < summaryOffset + a

The entire header precedes every summary word.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.summary_end_le_span (d : ℕ) : summaryOffset + span d ≤ span (d + 1)

theorem Cslib.Algorithms.Lean.VanEmdeBoas.summary_word_lt_span (d : ℕ) {a : ℕ} (ha : a < span d) : summaryOffset + a < span (d + 1)

Every word of the summary is inside the parent record.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.cluster_end_le_span (d : ℕ) {i : ℕ} (hi : i < universeSize d) : clusterOffset d i + span d ≤ span (d + 1)

theorem Cslib.Algorithms.Lean.VanEmdeBoas.cluster_word_lt_span (d : ℕ) {i a : ℕ} (hi : i < universeSize d) (ha : a < span d) : clusterOffset d i + a < span (d + 1)

Every word of each valid cluster is inside the parent record.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.summary_end_le_clusterOffset (d i : ℕ) : summaryOffset + span d ≤ clusterOffset d i

The summary ends before every cluster starts.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.summary_word_lt_cluster_word (d i b : ℕ) {a : ℕ} (ha : a < span d) : summaryOffset + a < clusterOffset d i + b

Every summary word precedes every cluster word.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.cluster_end_le_clusterOffset (d : ℕ) {i j : ℕ} (hij : i < j) : clusterOffset d i + span d ≤ clusterOffset d j

Ordered clusters occupy nonoverlapping half-open intervals.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.cluster_word_lt_cluster_word (d : ℕ) {i j a : ℕ} (hij : i < j) (ha : a < span d) (b : ℕ) : clusterOffset d i + a < clusterOffset d j + b

Every word of an earlier cluster precedes every word of a later cluster.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.universeSize_mono {a b : ℕ} (hab : a ≤ b) : universeSize a ≤ universeSize b

Monotonicity of universeSize in the recursion depth.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.span_mono {a b : ℕ} (hab : a ≤ b) : span a ≤ span b

Monotonicity of span in the recursion depth.