Reference · Graph algorithms

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

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

FLOYD-WARSHALL, ATTAINMENT HALF (second half, part (R)). Tables D(t, i, j) on nodes < n with pivots P(t) < n, where every round's entries are ATTAINED (kept, or through the pivot: the attainment part of signed/fwround-reading): round t := 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) Then every entry after r rounds is the length of an actual walk, measured with the initial table as arc weights: signed/fw-entries-attained : (forall t < r, P t < n /\ round t) -> forall i j < n, exists k x, (forall t <= k, x t < n) /\ x 0 = i /\ x k = j /\ D(r, i, j) ~ walk-length(D 0, x, k) Base: the one-arc walk i, j. A kept entry keeps its walk. A pivot entry concatenates the walks i -> p and p -> j (signed/walk-concat), and the lengths add.

Depends onalgorithms.proofs.graph.walk-concatalgorithms.proofs.graph.walk-shorten

signed/fw-entries-attained :
  (n : ℕ) (D : ℕ → ℕ → ℕ → ℚ) (P : ℕ → ℕ) (r : ℕ)
  (hr : ∀ (t : ℕ), ∀ (ht : nat/strict-below t r), proposition/conjunction (nat/strict-below (P t) n) (∀ (i : ℕ), ∀ (hi : nat/strict-below i n), ∀ (j : ℕ), ∀ (hj : nat/strict-below j n), proposition/disjunction (D (data/succ t) i j = D t i j) (D (data/succ t) i j = D t i (P t) + D t (P t) j)))
  (i : ℕ) (hi : nat/strict-below i n) (j : ℕ) (hj : nat/strict-below j n)
  → proposition/existence ℕ (fun k => proposition/existence (ℕ → ℕ) (fun x => proposition/conjunction (∀ (t : ℕ), ∀ (ht : t ≤ k), nat/strict-below (x t) n) (proposition/conjunction (x 0 = i) (proposition/conjunction (x k = j) (D r i j = signed/expr-sum-value (fun t => (fun u => fun v => D 0 u v) (x t) (x (data/succ t))) k)))))