Reference · Algorithm guarantees

rainbow.algorithms.proofs.local-search

Algorithm guaranteessrc/rainbow/algorithms/proofs/local_search.clj2 definitions, 5 theorems

Bounded local (hill-climbing) search over a finite candidate set with exact rational objectives. A best-neighbor step delegates to the proven finite rational argmax: it picks the candidate maximizing the objective, keeping the current point as the fallback. Because the current point is itself a candidate, each step never decreases the objective -- the hill-climbing guarantee. The candidate/objective pair is a pluggable strategy (AHoF D40 DELEGATE).

search/nnrat-best-neighbor.{u} :
  (Theta : Type u) (candidates : Finset Theta) (current : Theta)
  (evaluate : Theta → ℚ≥0)
  → Theta

search/nnrat-hill-climb.{u} :
  (Theta : Type u) (candidates : Finset Theta) (evaluate : Theta → ℚ≥0) (x₁ : ℕ)
  (x₂ : Theta)
  → Theta

search/nnrat-best-neighbor-is-candidate.{u} :
  (Theta : Type u) (candidates : Finset Theta) (current : Theta)
  (evaluate : Theta → ℚ≥0)
  (current-member : current ∈ candidates)
  → search/nnrat-best-neighbor Theta candidates current evaluate ∈ candidates

search/nnrat-best-neighbor-improves.{u} :
  (Theta : Type u) (candidates : Finset Theta) (current : Theta)
  (evaluate : Theta → ℚ≥0)
  (current-member : current ∈ candidates)
  → evaluate current ≤ evaluate (search/nnrat-best-neighbor Theta candidates current evaluate)

search/nnrat-hill-climb-zero.{u} :
  (Theta : Type u) (candidates : Finset Theta) (evaluate : Theta → ℚ≥0)
  (initial : Theta)
  → search/nnrat-hill-climb Theta candidates evaluate 0 initial = initial

search/nnrat-hill-climb-successor.{u} :
  (Theta : Type u) (candidates : Finset Theta) (evaluate : Theta → ℚ≥0) (steps : ℕ)
  (initial : Theta)
  → climb (data/succ steps) initial = (fun x₁ => fun previous => search/nnrat-best-neighbor Theta candidates previous evaluate) steps (climb steps initial)
  where climb := search/nnrat-hill-climb Theta candidates evaluate

search/nnrat-best-neighbor-transfer.{u} :
  (Theta : Type u) (candidates : Finset Theta) (evaluate : Theta → ℚ≥0) (left : Theta)
  (left-member : left ∈ candidates)
  (right : Theta)
  (right-member : right ∈ candidates)
  → proposition/conjunction (evaluate left ≤ evaluate (neighbor₁)) (evaluate right ≤ evaluate (neighbor))
  where neighbor := search/nnrat-best-neighbor Theta candidates right evaluate
  where neighbor₁ := search/nnrat-best-neighbor Theta candidates left evaluate