Reference · Graph algorithms

rainbow.algorithms.proofs.graph.floyd-warshall-convergence-upper

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

FLOYD-WARSHALL INVARIANT, UPPER HALF (part (U)). Tables D(t, i, j) over nodes < n with pivots P t < n relax at every round: round t := P t < n /\ forall i j < n, D(t+1, i, j) <= D(t, i, j) /\ D(t+1, i, j) <= D(t, i, P t) + D(t, P t, j) With arc weights W = D 0 and no negative closed walk, after t rounds no walk of >= 1 arc whose INTERMEDIATE nodes are all pivots of earlier rounds beats the entry at its ends: signed/fw-entries-below-walks : no-negative-cycles n (D 0) -> (forall s < t, round s) -> forall k x, 0 < k -> (forall s <= k, x s < n) -> (forall s, 0 < s -> s < k -> exists u < t, x s = P u) -> D(t, x 0, x k) <= walk-length(D 0, x, k) Base: no pivots means no intermediates, so the walk is one arc and D(0) is its length. Step to the new pivot p = P t: if no intermediate is p, every intermediate is an earlier pivot. Otherwise take the FIRST and LAST intermediate visits a <= b of p (nat/least-witness, nat/greatest-witness). The prefix 0..a and the suffix b..k avoid p as an intermediate, so the induction hypothesis bounds them by D(t, x 0, p) and D(t, p, x k). The middle a..b is a closed walk, so it is >= 0. The round's pivot bound closes it. The lengths split as in signed/walk-cut-length.

Depends onalgorithms.proofs.graph.floyd-warshall-convergence-attainedmath.nat.extremal-index

signed/fw-entries-below-walks :
  (n : ℕ) (D : ℕ → ℕ → ℕ → ℚ) (P : ℕ → ℕ)
  (hneg : ∀ (z : ℕ → ℕ), ∀ (d : ℕ), ∀ (hz : ∀ (t : ℕ), ∀ (ht : t ≤ d), nat/strict-below (z t) n), ∀ (hc : z d = z 0), 0 ≤ signed/expr-sum-value (fun t => (fun u => fun v => D 0 u v) (z t) (z (data/succ t))) d)
  (t : ℕ)
  (hr : ∀ (s : ℕ), ∀ (hs : nat/strict-below s t), proposition/conjunction (nat/strict-below (P s) n) (∀ (i : ℕ), ∀ (hi : nat/strict-below i n), ∀ (j : ℕ), ∀ (hj : nat/strict-below j n), proposition/conjunction (D (data/succ s) i j ≤ D s i j) (D (data/succ s) i j ≤ D s i (P s) + D s (P s) j)))
  (k : ℕ) (x : ℕ → ℕ) (hk0 : nat/strict-below 0 k)
  (hin : ∀ (t₁ : ℕ), ∀ (ht : t₁ ≤ k), nat/strict-below (x t₁) n)
  (hint : ∀ (s : ℕ), ∀ (hs0 : nat/strict-below 0 s), ∀ (hsk : nat/strict-below s k), proposition/existence ℕ (fun u => proposition/conjunction (nat/strict-below u t) (x s = P u)))
  → D t (x 0) (x k) ≤ signed/expr-sum-value (fun t₁ => (fun u => fun v => D 0 u v) (x t₁) (x (data/succ t₁))) k