Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.tabu-search

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

AHoF Tabu Search: a local-search metaheuristic that escapes local optima by ALWAYS moving to the best neighbor -- even a worsening one -- while a short-term memory (the TABU LIST) forbids reversing recent moves, preventing cycling. A candidate move is allowed exactly when it is NOT currently tabu: move-allowed? move-is-tabu? = NOT move-is-tabu? over booleans. Proved native and axiom-free: the allowed-move test as the boolean negation of the tabu status (via logic/if-data over Bool); that a non-tabu move is allowed; and that a tabu move is forbidden -- unless it would improve on the best solution ever seen (the aspiration criterion, an override handled by the caller). The neighborhood evaluation, tabu-list tenure, and best-so-far tracking are executable; what is proved is the tabu-membership move decision. Requires data/Bool, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 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.tabu-search` prints this classification.

tabu-search/move-allowed? :
  (x₁ : data/Bool)
  → data/Bool

tabu-search/non-tabu-move-allowed :
  → fuzzing/flip data/false = data/true

tabu-search/tabu-move-forbidden :
  → fuzzing/flip data/true = data/false