Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.golden-section-search

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/golden_section_search.clj2 definitions, 5 theorems

AHoF O9 worked Golden Section Search reduction step over exact rationals. Two interior probe values are compared. When the left value 1/2 is at most the right value 3/4, the left sub-interval is kept and the retained minimum is 1/2. When the probe values are swapped (3/4 on the left, 1/2 on the right) the right sub-interval is kept and the retained minimum is still 1/2 -- in both orientations of this pair the search retains the smaller interior value. Proved native and axiom-free. Scope (measured by the kernel): this module has 5 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.golden-section-search` prints this classification.

Depends onalgorithms.proofs.golden-section-search

ahof-o9/left-value :
  → ℚ≥0

ahof-o9/right-value :
  → ℚ≥0

ahof-o9/keeps-left :
  → ce-is/elite? ahof-d63/rate ahof-d25/value-a = data/true

ahof-o9/retains-min-left :
  → astar-fal/expand-value ahof-d63/rate ahof-d25/value-a = 1/2

ahof-o9/keeps-right-when-swapped :
  → ce-is/elite? ahof-d25/value-a ahof-d63/rate = data/false

ahof-o9/retains-min-right :
  → astar-fal/expand-value ahof-d25/value-a ahof-d63/rate = 1/2

ahof-o9/golden-section :
  → proposition/conjunction (elite? = data/true) (value = 1/2)
  where elite? := ce-is/elite? ahof-d63/rate ahof-d25/value-a
  where value := astar-fal/expand-value ahof-d63/rate ahof-d25/value-a