Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.christofides

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

AHoF Christofides Algorithm: the best-known polynomial APPROXIMATION for the metric Travelling Salesman Problem. It builds a minimum spanning tree, adds a minimum-weight perfect matching on the ODD-degree vertices (making all degrees even), forms an Eulerian circuit, and shortcuts repeated vertices (valid by the triangle inequality). Its classical guarantee (not proved here) is that the produced tour costs at most 3/2 times the optimal. A tour is accepted as within-bound when within-bound? tour-cost approximation-bound = decide (tour-cost <= approximation-bound) where approximation-bound = (3/2) * optimal-cost, over exact-rational costs. Proved native and axiom-free: the within-bound test, and worked instances with optimal cost 10 and bound 15 -- a tour of cost 13 is accepted; the certificate 13 <= 15 as a native nnrat/at-most; and a tour of cost 17 is not accepted. The MST, matching, Euler tour, and shortcut steps are executable; what is proved is the bound decision at these instances, not the 3/2 approximation guarantee. Requires nnrat/at-most, audit/decide-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.christofides` prints this classification.

christofides/within-bound? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

christofides/tour-within-guarantee :
  → ce-fal/elite? 13 15 = data/true

christofides/tour-at-most-bound :
  → 13 ≤ 15

christofides/tour-over-bound-rejected :
  → ce-fal/elite? 17 15 = data/false