Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.local-search

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

AHoF D40 worked bounded local (hill-climbing) policy search. Three candidate policies {0,1,2} scored 1/4, 3/4, 1/2 by an exact rational objective. From the current policy 0 the best-neighbor step selects policy 1 (the maximizer), which is admissible and never decreases the objective (1/4 <= 3/4). The candidate membership proofs reuse the finite range machinery. 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.local-search` prints this classification.

ahof-d40/candidates :
  → Finset ℕ

ahof-d40/objective :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d40/best-is-one :
  → search/nnrat-best-neighbor ℕ ahof-d40/candidates 0 ahof-d40/objective = 1

ahof-d40/admissible :
  → search/nnrat-best-neighbor ℕ ahof-d40/candidates 0 ahof-d40/objective ∈ ahof-d40/candidates

ahof-d40/improvement :
  → ahof-d40/objective 0 ≤ ahof-d40/objective (search/nnrat-best-neighbor ℕ ahof-d40/candidates 0 ahof-d40/objective)

ahof-d40/hill-climb-recurrence :
  → proposition/conjunction (climb = 0) (∀ (steps : ℕ), search/nnrat-hill-climb ℕ ahof-d40/candidates ahof-d40/objective (data/succ steps) 0 = (fun x₂ => fun previous => neighbor previous ahof-d40/objective) steps (search/nnrat-hill-climb ℕ ahof-d40/candidates ahof-d40/objective steps 0))
  where climb := search/nnrat-hill-climb ℕ ahof-d40/candidates ahof-d40/objective 0 0
  where neighbor := search/nnrat-best-neighbor ℕ ahof-d40/candidates

ahof-d40/local-search :
  → proposition/conjunction (neighbor ∈ ahof-d40/candidates) (proposition/conjunction (ahof-d40/objective 0 ≤ ahof-d40/objective (neighbor)) (proposition/conjunction (climb = 0) (∀ (steps : ℕ), search/nnrat-hill-climb ℕ ahof-d40/candidates ahof-d40/objective (data/succ steps) 0 = (fun x₈ => fun previous => search/nnrat-best-neighbor ℕ ahof-d40/candidates previous ahof-d40/objective) steps (search/nnrat-hill-climb ℕ ahof-d40/candidates ahof-d40/objective steps 0))))
  where climb := search/nnrat-hill-climb ℕ ahof-d40/candidates ahof-d40/objective 0 0
  where neighbor := search/nnrat-best-neighbor ℕ ahof-d40/candidates 0 ahof-d40/objective