Reference · Graph algorithms

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

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

BELLMAN-FORD CONVERGENCE, ATTAINMENT HALF (second half, part (R)). If every round's new label is ATTAINED, i.e. equal to the old label or to some L(t, i) + W(i, j) (the attainment half of signed/bford-round-reading), then every label after r rounds is the start label of some node plus the length of a walk of at most r arcs from it: signed/bford-labels-attained : forall n W L r, (forall t < r, attained t) -> forall v < n, exists k, k <= r /\ exists x, (forall t <= k, x t < n) /\ x k = v /\ L(r, v) ~ L(0, x 0) + walk-length(x, k) With (U) (signed/bford-labels-below-walks) this is the exact r-round semantics: d_r(v) = min over walks x of at most r arcs ending at v of d_0(x 0) + walk-length(x, k). Proof by induction on r. A kept label reuses the previous round's walk. A label attained through the arc (i, v) extends i's walk by v: ext x k v = fun t. if t <= k then x t else v (by nat/decide-at-most). The extended walk agrees with x below k + 1, so its first k arcs have the same length (signed/expr-sum-value-congruence-below), and its last arc is W(i, v).

Depends onalgorithms.proofs.graph.bellman-ford-convergence-uppermath.rational.signed.decide-completeness

signed/bford-labels-attained :
  (n : ℕ) (W L : ℕ → ℕ → ℚ) (r : ℕ)
  (ha : ∀ (t : ℕ), ∀ (ht : nat/strict-below t r), ∀ (j : ℕ), ∀ (hj : nat/strict-below j n), proposition/disjunction (L (data/succ t) j = L t j) (proposition/existence ℕ (fun i => proposition/conjunction (nat/strict-below i n) (L (data/succ t) j = L t i + W i j))))
  (v : ℕ) (hv : nat/strict-below v n)
  → proposition/existence ℕ (fun k => proposition/conjunction (k ≤ r) (proposition/existence (ℕ → ℕ) (fun x => proposition/conjunction (∀ (t : ℕ), ∀ (ht : t ≤ k), nat/strict-below (x t) n) (proposition/conjunction (x k = v) (L r v = L 0 (x 0) + signed/expr-sum-value (fun t => W (x t) (x (data/succ t))) k)))))