RMQ

Stream: CSLib

[Li Xuanji]

Hello, I've formalized a data structure (commonly called a "sparse table") that solves the RMQ problem, which is to find the minimum value in a sub-array of an array. I wonder if this is suitable for CSLib.

Generally, preprocessing is needed on the input data; a data structure solves RMQ in <p, q> if the preprocessing time is p and the query time is q. Wikipedia has a summary of the different approaches.

• Naive approach (no preprocessing): <O(1), O(n)>
• Naively precompute all answers: <O(n^3), O(1)>
• Precompute all answers using dynamic programming: <O(n^2), O(1)>
• Sparse table (this formalization): <O(n log n), O(1)>
• Optimal solution: <O(n), O(1)>, e.g. Fischer and Heun

There also exist easier solutions in <O(n log log n), O(1)> and <O(1), O(log n)> (both mentioned in the Wikipedia article), which could be intermediate targets to formalize before the optimal ones.

My choice for stating that a data structure solves RMQ was to package the data structure, functions, and proofs into a structure, and use TimeM annotations for the time complexity:

/-
A structure for stating that `α` and some associated (TimeM-annotated) functions is a solution to the RMQ problem.
- `make` : preprocess an array of values `a`, returning an `α`
- `query` : query `α` for the minimum value in a subarray of `a`
- `correct` : the result is the same as the naive implementation
- `make_time`, `query_time` : the time complexity of `make` and `query`, as a function of `|a|`
- `make_time_bound`, `query_time_bound` : proofs of the time complexity bounds
-/
class RMQSolution (α : Type) where
  make : Array ℕ → TimeM α
  query : α → ℕ → ℕ → TimeM ℕ
  correct (a : Array ℕ) (l r : ℕ) (h : l ≤ r) (hr : r < a.size) :
    (⟪query ⟪make a⟫ l r⟫) = rmqNaive a l r
  make_time : ℕ → ℕ
  make_time_bound : ∀ a : Array ℕ, (make a).time ≤ make_time a.size
  query_time : ℕ → ℕ
  query_time_bound : ∀ a : Array ℕ, ∀ l r : ℕ, (query ⟪make a⟫ l r).time ≤ query_time a.size

instance : RMQSolution SparseTable where
  make := SparseTable.make
  query := SparseTable.query
  correct := correct
  make_time n := n * Nat.log 2 n
  make_time_bound := SparseTable.make_time
  query_time _ := 1
  query_time_bound := fun _ l r => by simp [SparseTable.query_time]

[Shreyas Srinivas]

This is the kind of formalisation I would prefer to see in Prog instead of TimeM, because it starts to reach the threshold where review complexity goes up since you are using custom tick sizes

[Shreyas Srinivas]

And this is just the beginning.