Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.local-policy-search

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/local_policy_search.clj1 definitions, 3 theorems

AHoF D40 Local Policy Search: hill climbing in policy-parameter space. Each iteration perturbs the current policy, evaluates the neighbor, and keeps whichever policy scores higher (for a return/value to be maximized). The improvement step keeps the better of the incumbent and the neighbor value: improve incumbent neighbor = max(incumbent, neighbor) over the decidable rational order (improve is defined as that max). Proved native and axiom-free, as worked instances: improve(5, 7) = 7; and the worked certificates 5 <= improve(5, 7) and 7 <= improve(5, 7) (native nnrat/at-most). That the step never decreases the incumbent for all inputs, so that local search is an ascent, is the algorithm's classical property, not proved here. The perturbation and the policy evaluation are executable concerns. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 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-policy-search` prints this classification.

local-policy-search/improve :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

local-policy-search/improve-adopts-better :
  → knapsack/cell 5 7 = 7

local-policy-search/improve-above-incumbent :
  → 5 ≤ knapsack/cell 5 7

local-policy-search/improve-above-neighbor :
  → 7 ≤ knapsack/cell 5 7