Reference · Algorithm guarantees

rainbow.algorithms.proofs.fibonacci

Algorithm guaranteessrc/rainbow/algorithms/proofs/fibonacci.clj2 definitions, 4 theorems

AHoF Fibonacci numbers -- the linear recurrence behind Fibonacci search (the derivative-free line-search that places probes at Fibonacci ratios) and a canonical dynamic-programming example. Computed in one pass by recursion on n carrying the adjacent pair (fib n, fib (n+1)): fib-pair 0 = (0, 1) fib-pair (succ n) = (snd p, fst p + snd p) where p = fib-pair n fib n = fst (fib-pair n) so fib n is produced in linear time with exact naturals (no double recursion, no memo table). Proved native and axiom-free: the pair carries adjacent Fibonacci numbers, and worked values reduce by reflexivity (fib 0 = 0, fib 1 = 1, fib 7 = 13). The Fibonacci-ratio probe placement of the search is an executable concern; what is proved here is the recurrence and worked values. Requires nat, nat addition (algebra/nat-add), and the product type (data/Product, data/pair, product/first, product/second) -- all in D63. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 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.fibonacci` prints this classification.

fibonacci/pair :
  (x₁ : ℕ)
  → data/Product ℕ ℕ

fibonacci/fib :
  (x₁ : ℕ)
  → ℕ

fibonacci/pair-step-unfold :
  (n : ℕ)
  → fibonacci/pair (data/succ n) = data/pair ℕ ℕ (product/second ℕ ℕ (fibonacci/pair n)) (add)
  where add := algebra/nat-add (product/first ℕ ℕ (fibonacci/pair n)) (product/second ℕ ℕ (fibonacci/pair n))

fibonacci/fib-zero :
  → fibonacci/fib 0 = 0

fibonacci/fib-one :
  → fibonacci/fib 1 = 1

fibonacci/fib-seven :
  → fibonacci/fib 7 = 13