Reference · Algorithm guarantees

rainbow.algorithms.proofs.floyd-warshall

Algorithm guaranteessrc/rainbow/algorithms/proofs/floyd_warshall.clj1 definitions, 3 theorems

AHoF Floyd-Warshall all-pairs shortest paths -- the dynamic-programming relaxation through an intermediate node. Allowing paths to route through node k, the shortest i->j distance is the better of the current direct estimate and the detour i->k->j: cell direct dik dkj = min( direct, dik + dkj ) over exact-rational edge weights. Proved native and axiom-free: worked instances with direct 10 and detour 3 + 4 -- the cell relaxes to 7, and the worked certificates cell <= 10 and cell <= 3 + 4. The triple loop over (k, i, j) that fills the full distance matrix is an executable concern; what is proved here is the relaxation cell at this instance. That relaxation never worsens for all weights, and the correctness of Floyd-Warshall, are classical and not proved here. Requires nnrat/at-most, nnrat/add, 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.floyd-warshall` prints this classification.

floyd-warshall/cell :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

floyd-warshall/cell-relaxes :
  → floyd-warshall/cell 10 3 4 = 7

floyd-warshall/cell-below-direct :
  → floyd-warshall/cell 10 3 4 ≤ 10

floyd-warshall/cell-below-detour :
  → floyd-warshall/cell 10 3 4 ≤ 3 + 4