Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.fibonacci-search

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

AHoF O8 worked Fibonacci Search reduction step over exact rationals, reusing the shared bracket-reduction lemma (rainbow.algorithms.proofs.golden-section-search, linesearch/*). Fibonacci and Golden Section Search share the same ITERATE loop and differ only in probe-point placement; here the Fibonacci probes evaluate to 3/8 (left) and 5/8 (right). Since the left value 3/8 is at most the right value 5/8, the left sub-interval is kept and the retained interior value is 3/8; swapping the probes keeps the right sub-interval and still retains 3/8. This second catalog row is discharged entirely by the reused general lemma -- a demonstration of lemma leverage. 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.fibonacci-search` prints this classification.

Depends onalgorithms.proofs.golden-section-search

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

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

ahof-o8/keeps-left :
  → ce-is/elite? ahof-o8/left-value ahof-o8/right-value = data/true

ahof-o8/retains-min-left :
  → astar-fal/expand-value ahof-o8/left-value ahof-o8/right-value = 3/8

ahof-o8/keeps-right-when-swapped :
  → ce-is/elite? ahof-o8/right-value ahof-o8/left-value = data/false

ahof-o8/retains-min-right :
  → astar-fal/expand-value ahof-o8/right-value ahof-o8/left-value = 3/8

ahof-o8/fibonacci-search :
  → proposition/conjunction (elite? = data/true) (value = 3/8)
  where elite? := ce-is/elite? ahof-o8/left-value ahof-o8/right-value
  where value := astar-fal/expand-value ahof-o8/left-value ahof-o8/right-value