Reference · Graph algorithms

rainbow.algorithms.proofs.graph.walk-shorten

Graph algorithmssrc/rainbow/algorithms/proofs/graph/walk_shorten.clj0 definitions, 4 theorems

CYCLE REMOVAL: without negative closed walks, every walk over n nodes can be replaced by one of FEWER THAN n arcs with the same ends that is no longer: signed/walk-shorten : no-negative-cycles n W -> forall k x, (forall t <= k, x t < n) -> exists k', k' < n /\ exists y, (forall t <= k', y t < n) /\ y 0 = x 0 /\ y k' = x k /\ walk-length (y, k') <= walk-length (x, k) Proof by strong induction on a length bound K. A walk of fewer than n arcs is kept. A walk of k >= n arcs visits x 0 .. x n, n + 1 nodes below n, so nat/pigeonhole gives a < b <= n with x a = x b. With b = (e + 1) + a and k = c + b, signed/walk-cut-length cuts the cycle. The cut walk has c + a < k arcs, the same ends and no greater length, and the induction hypothesis finishes it. This is what makes n - 1 Bellman-Ford rounds enough.

Depends onalgorithms.proofs.graph.walk-cycle-cutmath.nat.pigeonhole

nat/at-most-successor-cancel-local :
  (a b : ℕ)
  (h : data/succ a ≤ data/succ b)
  → a ≤ b

nat/walk-cut-shorter :
  (c a e : ℕ)
  → data/succ (algebra/nat-add c a) ≤ algebra/nat-add c (algebra/nat-add (data/succ e) a)

signed/walk-shorten-bounded :
  (n : ℕ) (W : ℕ → ℕ → ℚ)
  (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 => W (z t) (z (data/succ t))) d)
  (K k : ℕ)
  (hk : k ≤ K)
  (x : ℕ → ℕ) (hin : ∀ (t : ℕ), ∀ (ht : t ≤ k), nat/strict-below (x t) n)
  → proposition/existence ℕ (fun k2 => proposition/conjunction (nat/strict-below k2 n) (proposition/existence (ℕ → ℕ) (fun y => proposition/conjunction (∀ (t : ℕ), ∀ (ht : t ≤ k2), nat/strict-below (y t) n) (proposition/conjunction (y 0 = x 0) (proposition/conjunction (y k2 = x k) (signed/expr-sum-value (fun t => W (y t) (y (data/succ t))) k2 ≤ value))))))
  where value := signed/expr-sum-value (fun t => W (x t) (x (data/succ t))) k

signed/walk-shorten :
  (n : ℕ) (W : ℕ → ℕ → ℚ)
  (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 => W (z t) (z (data/succ t))) d)
  (k : ℕ) (x : ℕ → ℕ) (hin : ∀ (t : ℕ), ∀ (ht : t ≤ k), nat/strict-below (x t) n)
  → proposition/existence ℕ (fun k2 => proposition/conjunction (nat/strict-below k2 n) (proposition/existence (ℕ → ℕ) (fun y => proposition/conjunction (∀ (t : ℕ), ∀ (ht : t ≤ k2), nat/strict-below (y t) n) (proposition/conjunction (y 0 = x 0) (proposition/conjunction (y k2 = x k) (signed/expr-sum-value (fun t => W (y t) (y (data/succ t))) k2 ≤ value))))))
  where value := signed/expr-sum-value (fun t => W (x t) (x (data/succ t))) k