Reference · Graph algorithms

rainbow.algorithms.proofs.graph.bellman-ford-convergence-upper

Graph algorithmssrc/rainbow/algorithms/proofs/graph/bellman_ford_convergence_upper.clj0 definitions, 1 theorems

BELLMAN-FORD CONVERGENCE, UPPER HALF (second half, part (U)). Label rounds L(t, v) on nodes v < n with arc weights W(u, v) relax at every round: round t := forall j < n, L(t+1, j) <= L(t, j) /\ forall i < n, L(t+1, j) <= L(t, i) + W(i, j) (exactly the bound half of signed/bford-round-reading, so a chain of accepted Bellman-Ford round stores gives it). Then after r rounds no walk of at most r arcs beats the label at its end: signed/bford-labels-below-walks : forall n W L r, (forall t < r, round t) -> forall k x, k <= r -> (forall t <= k, x t < n) -> L(r, x k) <= L(0, x 0) + walk-length(x, k) where a walk is a node sequence x 0 .. x k and walk-length(x, k) = signed/expr-sum-value (fun t. W(x t, x (t+1))) k. With L(0, .) = (0, M, ..., M) this is: after r rounds, d_r(v) is at most the length of every walk of at most r arcs from the source. The other half (R), that d_r(v) is ATTAINED by such a walk, uses the attainment part of the reading. Proof by induction on r. If the walk has k <= r arcs, the previous round's bound plus L(r+1, .) <= L(r, .) closes it. If k = r + 1, the prefix walk of r arcs gives L(r, x r) <= L(0, x 0) + walk-length(x, r), and round r's arc bound at (x r, x (r+1)) adds the last arc. walk-length(x, r+1) is walk-length(x, r) + W(x r, x (r+1)) by definition.

Depends onmath.rational.signed.one-hot-selectsmath.nat.divmodmath.rational.signed.add-associative

signed/bford-labels-below-walks :
  (n : ℕ) (W L : ℕ → ℕ → ℚ) (r : ℕ)
  (hr : ∀ (t : ℕ), ∀ (ht : nat/strict-below t r), ∀ (j : ℕ), ∀ (hj : nat/strict-below j n), proposition/conjunction (L (data/succ t) j ≤ L t j) (∀ (i : ℕ), ∀ (hi : nat/strict-below i n), L (data/succ t) j ≤ L t i + W i j))
  (k : ℕ) (x : ℕ → ℕ)
  (hk : k ≤ r)
  (x₁ : ∀ (t : ℕ), ∀ (ht : t ≤ k), nat/strict-below (x t) n)
  → L r (x k) ≤ L 0 (x 0) + signed/expr-sum-value (fun t => W (x t) (x (data/succ t))) k