Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.tsp-nearest-neighbor

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

AHoF Nearest-Neighbor TSP heuristic: build a tour of the Travelling Salesman Problem by starting at a city and repeatedly travelling to the NEAREST unvisited city, returning to the start at the end. It is a fast constructive heuristic (not optimal, but a common baseline and warm-start for local search). At each step it selects the closer of two candidate unvisited cities: nearer-city da na db nb = if da <= db then na else nb (return the id of the smaller-distance city), over exact-rational distances. Proved native and axiom-free: the nearest-city selection; a worked choice of the nearer city; and the certificate that the visited city's distance is at most the alternative's (native nnrat/at-most) -- a worked instance of the greedy nearest-neighbor invariant, not a proof of it for all distances. The distance matrix and the visited-set bookkeeping are executable; what is proved is the nearest-unvisited-city selection. Requires nat, audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (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.tsp-nearest-neighbor` prints this classification.

tsp-nn/nearer-city :
  (x₁ : ℚ≥0) (x₂ : ℕ) (x₃ : ℚ≥0) (x₄ : ℕ)
  → ℕ

tsp-nn/visits-nearest :
  → kmeans/assign 3 2 8 5 = 2

tsp-nn/visits-second-when-nearer :
  → kmeans/assign 9 2 4 5 = 5

tsp-nn/visited-is-nearest :
  → 3 ≤ 8