Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bisection

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/bisection.clj3 definitions, 4 theorems

AHoF O12 worked bisection bracket search over exact rationals. Starting from the bracket [0, 1], the probe midpoint is 1/2; keeping the lower half narrows to [0, 1/2], whose probe midpoint is 1/4 -- the interval and probe both halve. Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.bisection` prints this classification.

ahof-o12/first-midpoint :
  → ℚ≥0

ahof-o12/lower-bracket :
  → data/Product ℚ≥0 ℚ≥0

ahof-o12/second-midpoint :
  → ℚ≥0

ahof-o12/first-midpoint-is-half :
  → ahof-o12/first-midpoint = nnrat/half

ahof-o12/narrows-to-lower-half :
  → search/bisection-narrow data/true 0 1 = data/pair ℚ≥0 ℚ≥0 0 (search/bracket-midpoint 0 1)

ahof-o12/second-midpoint-is-quarter :
  → ahof-o12/second-midpoint = nnrat/quarter

ahof-o12/bisection :
  → proposition/conjunction (ahof-o12/first-midpoint = nnrat/half) (conjunction)
  where conjunction := proposition/conjunction (search/bisection-narrow data/true 0 1 = data/pair ℚ≥0 ℚ≥0 0 (search/bracket-midpoint 0 1)) (ahof-o12/second-midpoint = nnrat/quarter)