Reference · Algorithm guarantees

rainbow.algorithms.proofs.path-relaxation

Algorithm guaranteessrc/rainbow/algorithms/proofs/path_relaxation.clj1 definitions, 4 theorems

AHoF shortest-path edge relaxation (the core step of Bellman-Ford and Dijkstra): when a candidate path of cost `alt` reaches a node whose current best cost is `current`, the tentative distance is relaxed to the smaller of the two, relax current alt = nnrat-min current alt = if (current <= alt) then current else alt using the decidable rational order. Relaxation is designed to maintain the invariant that the relaxed distance is a lower bound of both inputs (relax c a <= c and relax c a <= a), and Dijkstra's optimality builds on it; neither is proved here in general. The graph, the edge weights, and the visit order are executable concerns; what is proved here is the relaxation operation and worked instances: relax 7 2 = 2, relax 2 5 = 2, relax 7 2 <= 7, and relax 7 2 <= 2. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all carried by the D63 checkpoint). Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.path-relaxation` prints this classification.

path/relax :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

path/relax-improves :
  → path/relax 7 2 = 2

path/relax-keeps-current :
  → path/relax 2 5 = 2

path/relax-below-current :
  → path/relax 7 2 ≤ 7

path/relax-below-alt :
  → path/relax 7 2 ≤ 2