Reference · Algorithm guarantees

rainbow.algorithms.proofs.bisection

Algorithm guaranteessrc/rainbow/algorithms/proofs/bisection.clj2 definitions, 3 theorems

Bisection bracket search over exact nonnegative rationals. The probe point of a bracket [lo, hi] is its midpoint (lo + hi) / 2; narrowing keeps the lower or upper half depending on a pluggable test, exactly halving the interval. All bracket methods share this ITERATE loop and differ only in the probe point (AHoF O12, the simplest instance). Scope (measured by the kernel): this module has 3 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.bisection` prints this classification.

search/bracket-midpoint :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

search/bisection-narrow :
  (x₁ : data/Bool) (x₂ x₃ : ℚ≥0)
  → data/Product ℚ≥0 ℚ≥0

search/bracket-midpoint-unfold :
  (lo hi : ℚ≥0)
  → search/bracket-midpoint lo hi = (lo + hi) · nnrat/half

search/narrow-keeps-lower :
  (lo hi : ℚ≥0)
  (keep : data/true = data/true)
  → search/bisection-narrow data/true lo hi = data/pair ℚ≥0 ℚ≥0 lo (search/bracket-midpoint lo hi)

search/narrow-keeps-upper :
  (lo hi : ℚ≥0)
  (reject : data/false = data/false)
  → search/bisection-narrow data/false lo hi = data/pair ℚ≥0 ℚ≥0 (search/bracket-midpoint lo hi) hi