All-pairs shortest paths by min-plus products

DefinitionShortest path weight with at most \(r\) edges#✓fully proved

Let \(w\) be an \(n \times n\) matrix of weights in \(\mathbb{Z} \cup \{\infty\}\) on the vertices \(\{0, \dots, n-1\}\), let \(r\) be a natural number, let \(i\) and \(j\) be vertices, and let \(d \in \mathbb{Z} \cup \{\infty\}\). A weighted path from \(i\) to \(j\) is a nonempty list \(p\) of vertices that starts at \(i\), ends at \(j\) and has finite weight on each pair of consecutive vertices; its number of edges is its length minus one, and its weight \(w(p)\) is the sum of the weights of its edges. Then \(d\) is the shortest weight of a path from \(i\) to \(j\) with at most \(r\) edges when \(d \le w(p)\) for every weighted path \(p\) from \(i\) to \(j\) with at most \(r\) edges, and either \(d = \infty\) or \(d = w(p)\) for some weighted path \(p\) from \(i\) to \(j\) with at most \(r\) edges.

Paths may repeat vertices; no absence-of-negative-cycles hypothesis is needed.

@[expose] public def IsEdgeBoundedShortestPathWeight {n : Nat}
    (weight : Matrix (Fin n) (Fin n) (WithTop Int))
    (r : Nat) (i j : Fin n) (distance : WithTop Int) : Prop :=
  (∀ path, IsWeightedPath weight i j path → path.length - 1 ≤ r →
    distance ≤ pathWeight weight path) ∧
  (distance = ⊤ ∨ ∃ path, IsWeightedPath weight i j path ∧
    path.length - 1 ≤ r ∧ pathWeight weight path = distance)

Uses 2 · Used by 7

Statement usesFinite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix

Used byFASTER-APSP computes shortest-path weights · FASTER-APSP computes edge-bounded shortest-path weights · Characterization of the shortest path weight with at most \(r\) edges · One min-plus multiplication extends shortest paths by one edge · Min-plus matrix powers give shortest path weights with at most \(r\) edges · SLOW-APSP computes shortest-path weights · Bounded-edge shortest weights from SLOW-APSP

TheoremCharacterization of the shortest path weight with at most \(r\) edges#✓fully proved

Let \(w\) be an \(n \times n\) matrix of weights in \(\mathbb{Z} \cup \{\infty\}\) on the vertices \(\{0, \dots, n-1\}\), let \(r\) be a natural number, let \(i\) and \(j\) be vertices, and let \(d \in \mathbb{Z} \cup \{\infty\}\). For a weighted path \(p\), write \(w(p)\) for its weight. Then \(d\) is the shortest weight of a path from \(i\) to \(j\) with at most \(r\) edges if and only if \(d \le w(p)\) for every weighted path \(p\) from \(i\) to \(j\) with at most \(r\) edges, and either \(d = \infty\) or \(d = w(p)\) for some weighted path \(p\) from \(i\) to \(j\) with at most \(r\) edges.

public theorem isEdgeBoundedShortestPathWeight_iff {n : Nat}
    (weight : Matrix (Fin n) (Fin n) (WithTop Int))
    (r : Nat) (i j : Fin n) (distance : WithTop Int) :
    IsEdgeBoundedShortestPathWeight weight r i j distance ↔
      (∀ path, IsWeightedPath weight i j path → path.length - 1 ≤ r →
        distance ≤ pathWeight weight path) ∧
      (distance = ⊤ ∨ ∃ path, IsWeightedPath weight i j path ∧
        path.length - 1 ≤ r ∧ pathWeight weight path = distance)

Uses 3

Statement usesShortest path weight with at most \(r\) edges · Finite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix

TheoremEntries of the min-plus matrix accumulator#✓fully proved

Let \(A\), \(B\) and \(C\) be \(n \times n\) matrices with entries in \(\mathbb{Z} \cup \{\infty\}\), viewed in the min-plus semiring. For all \(i, j \in \{0, \dots, n-1\}\), the entry \((i, j)\) of the matrix returned by the matrix accumulator on \(A\), \(B\) and the accumulator \(C\) equals \(\min\bigl(C_{ij}, \min_{k} (A_{ik} + B_{kj})\bigr)\), where \(k\) ranges over \(\{0, \dots, n-1\}\).

public theorem matrixAccumulate_minPlus_apply {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (MinTropical (WithTop Int)) n) n)
    (i j : Fin n) :
    MinTropical.untrop (((matrixAccumulate A B C).ret.get i).get j) =
      min (MinTropical.untrop ((C.get i).get j))
        (Finset.univ.inf fun k : Fin n =>
          MinTropical.untrop ((A.get i).get k) +
            MinTropical.untrop ((B.get k).get j))

Uses 2 · Used by 1

Statement usesSquare matrix accumulation

Proof usesSquare matrix accumulation computes \(C + AB\)

Used byOne min-plus multiplication extends shortest paths by one edge

TheoremOne min-plus multiplication extends shortest paths by one edge#✓fully proved

Let \(A\) and \(B\) be \(n \times n\) matrices with entries in \(\mathbb{Z} \cup \{\infty\}\), viewed in the min-plus semiring, and let \(r\) be a natural number. Suppose that \(B_{jj} = 0\) for every \(j\), and that for all \(i\) and \(j\) the entry \(A_{ij}\) is the shortest weight of a path from \(i\) to \(j\) with at most \(r\) edges for the weight matrix \(B\). Then for all \(i\) and \(j\), the entry \((i, j)\) of the matrix returned by the matrix accumulator on \(A\), \(B\) and the accumulator whose entries are all \(\infty\) is the shortest weight of a path from \(i\) to \(j\) with at most \(r + 1\) edges for the weight matrix \(B\).

Paths may repeat vertices and edge weights may be negative.

public theorem matrixAccumulate_edgeBounded {n r : Nat}
    (A B : _root_.Vector (_root_.Vector (MinTropical (WithTop Int)) n) n)
    (hdiag : ∀ j : Fin n, MinTropical.untrop ((B.get j).get j) = 0)
    (hprevious : ∀ i j : Fin n,
      FloydWarshall.IsEdgeBoundedShortestPathWeight
        (Matrix.of fun x y => MinTropical.untrop ((B.get x).get y))
        r i j (MinTropical.untrop ((A.get i).get j)))
    (i j : Fin n) :
    FloydWarshall.IsEdgeBoundedShortestPathWeight
      (Matrix.of fun x y => MinTropical.untrop ((B.get x).get y))
      (r + 1) i j
      (MinTropical.untrop (((matrixAccumulate A B
        (Vector.replicate n (Vector.replicate n 0))).ret.get i).get j))

Uses 5 · Used by 1

Statement usesShortest path weight with at most \(r\) edges · Square matrix accumulation

Proof usesFinite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix · Entries of the min-plus matrix accumulator

Used byMin-plus matrix powers give shortest path weights with at most \(r\) edges

TheoremMin-plus matrix powers give shortest path weights with at most \(r\) edges#✓fully proved

Let \(W\) be an \(n \times n\) matrix with entries in \(\mathbb{Z} \cup \{\infty\}\), viewed in the min-plus semiring, with \(W_{ii} = 0\) for every \(i\). Then for every natural number \(r\) and all \(i\) and \(j\), the entry \((W^r)_{ij}\) of the \(r\)-th min-plus power of \(W\) is the shortest weight of a path from \(i\) to \(j\) with at most \(r\) edges for the weight matrix \(W\).

Paths may repeat vertices.

public theorem matrix_pow_edgeBounded {n : Nat}
    (W : Matrix (Fin n) (Fin n) (MinTropical (WithTop Int)))
    (hdiag : ∀ i : Fin n, MinTropical.untrop (W i i) = 0)
    (r : Nat) (i j : Fin n) :
    FloydWarshall.IsEdgeBoundedShortestPathWeight
      (Matrix.of fun x y => MinTropical.untrop (W x y)) r i j
      (MinTropical.untrop ((W ^ r) i j))

Uses 6 · Used by 2

Statement usesShortest path weight with at most \(r\) edges

Proof usesFinite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix · Square matrix accumulation · One min-plus multiplication extends shortest paths by one edge · Square matrix accumulation computes \(C + AB\)

Used byFASTER-APSP computes edge-bounded shortest-path weights · Bounded-edge shortest weights from SLOW-APSP

DefinitionCounted copy of a square matrix#✓fully proved

Given an \(n \times n\) matrix \(A\) (a vector of \(n\) rows, each a vector of \(n\) entries), this computation returns the matrix whose \((i, j)\) entry is \(A_{ij}\), traversing the entries row by row and charging a cost of \((1, (0, 0))\) for each entry, that is, one logical assignment in the first cost coordinate and nothing in the other two.

@[nospecialize] public def copyCells {α : Type*} {n : Nat}
    (input : Vector (Vector α n) n) :
    TimeM (Nat × (Nat × Nat)) (Vector (Vector α n) n) :=
  Vector.ofFnM fun i => Vector.ofFnM fun j => do
    TimeM.tick (1, (0, 0))
    pure ((input.get i).get j)

Used by 8

Used byThe counted matrix copy returns its input · Cost of the counted matrix copy · FASTER-APSP · FASTER-APSP returns a power of the input matrix · Operation counts of FASTER-APSP · Slow all-pairs shortest paths (SLOW-APSP) · SLOW-APSP returns a min-plus matrix power · Exact operation counts of SLOW-APSP

TheoremThe counted matrix copy returns its input#✓fully proved

For every \(n \times n\) matrix \(A\) with entries in any type, the value returned by the counted copy of \(A\) is \(A\) itself.

public theorem copyCells_ret {α : Type*} {n : Nat} (input : Vector (Vector α n) n) :
    (copyCells input).ret = input

Uses 1 · Used by 4

Statement usesCounted copy of a square matrix

Used byFASTER-APSP returns a power of the input matrix · Operation counts of FASTER-APSP · SLOW-APSP returns a min-plus matrix power · Exact operation counts of SLOW-APSP

TheoremCost of the counted matrix copy#✓fully proved

For every \(n \times n\) matrix \(A\) with entries in any type, the counted copy of \(A\) has total cost \((n^2, (0, 0))\): exactly \(n^2\) logical assignments in the first cost coordinate and zero in the other two.

public theorem copyCells_time {α : Type*} {n : Nat} (input : Vector (Vector α n) n) :
    (copyCells input).time = (n ^ 2, (0, 0))

Uses 1 · Used by 2

Statement usesCounted copy of a square matrix

Used byOperation counts of FASTER-APSP · Exact operation counts of SLOW-APSP

DefinitionCounted zero initialization of a square matrix#✓fully proved

For a type \(\alpha\) with a zero element and a natural number \(n\), this computation returns the \(n \times n\) matrix over \(\alpha\) all of whose entries are \(0\), producing the entries row by row and charging a cost of \((1, (0, 0))\) for each entry, that is, one logical assignment in the first cost coordinate and nothing in the other two.

@[nospecialize] public def fillCells {α : Type*} [Zero α] (n : Nat) :
    TimeM (Nat × (Nat × Nat)) (Vector (Vector α n) n) :=
  Vector.ofFnM fun (_ : Fin n) => Vector.ofFnM fun (_ : Fin n) => do
    TimeM.tick (1, (0, 0))
    pure 0

Used by 8

Used byFASTER-APSP · FASTER-APSP returns a power of the input matrix · Operation counts of FASTER-APSP · The counted zero initialization returns the zero matrix · Cost of the counted zero initialization · Slow all-pairs shortest paths (SLOW-APSP) · SLOW-APSP returns a min-plus matrix power · Exact operation counts of SLOW-APSP

TheoremThe counted zero initialization returns the zero matrix#✓fully proved

For every type \(\alpha\) with a zero element and every natural number \(n\), the counted zero initialization of size \(n\) over \(\alpha\) returns the \(n \times n\) matrix all of whose entries are \(0\).

public theorem fillCells_ret {α : Type*} [Zero α] (n : Nat) :
    (fillCells (α := α) n).ret = Vector.replicate n (Vector.replicate n 0)

Uses 1 · Used by 3

Statement usesCounted zero initialization of a square matrix

Used byFASTER-APSP returns a power of the input matrix · SLOW-APSP returns a min-plus matrix power · Exact operation counts of SLOW-APSP

TheoremCost of the counted zero initialization#✓fully proved

For every type \(\alpha\) with a zero element and every natural number \(n\), the counted zero initialization of size \(n\) over \(\alpha\) has total cost \((n^2, (0, 0))\): exactly \(n^2\) logical assignments in the first cost coordinate and zero in the other two.

public theorem fillCells_time {α : Type*} [Zero α] (n : Nat) :
    (fillCells (α := α) n).time = (n ^ 2, (0, 0))

Uses 1 · Used by 2

Statement usesCounted zero initialization of a square matrix

Used byOperation counts of FASTER-APSP · Exact operation counts of SLOW-APSP

DefinitionFASTER-APSP#✓fully proved

Let \(W\) be an \(n \times n\) matrix over a type with addition, multiplication and zero. FASTER-APSP copies \(W\) into a matrix \(L\) and sets \(r = 1\). While \(r < n - 1\), it fills a new \(n \times n\) matrix \(M\) with zeros, sets each entry to \(M_{ij} = 0 + L_{i0} L_{0j} + \dots + L_{i,n-1} L_{n-1,j}\) (adding the terms from left to right), copies \(M\) into \(L\) and doubles \(r\). It returns the final \(L\). The run also records three counts: one assignment for each matrix cell copied or filled with zero, and one scalar addition and one scalar multiplication for each term added to an entry of \(M\).

@[nospecialize] public def fasterAPSP {α : Type u} [Add α] [Mul α] [Zero α]
    {n : Nat} (W : Vector (Vector α n) n) :
    TimeM (Nat × (Nat × Nat)) (Vector (Vector α n) n) := do
  let saved ← copyCells W
  squareLoop 1 (by decide) saved

Uses 3 · Used by 5

Statement usesCounted copy of a square matrix · Counted zero initialization of a square matrix · Square matrix accumulation

Used byFASTER-APSP computes shortest-path weights · FASTER-APSP computes edge-bounded shortest-path weights · FASTER-APSP returns a power of the input matrix · Operation counts of FASTER-APSP · Asymptotic operation count of FASTER-APSP

TheoremFASTER-APSP returns a power of the input matrix#✓fully proved

Let \(\alpha\) be a semiring, let \(W\) be an \(n \times n\) matrix over \(\alpha\), and let \(k = \lceil \log_2 (n - 1) \rceil\) be the least natural number with \(n - 1 \le 2^k\) (so \(k = 0\) when \(n \le 2\)). The matrix returned by FASTER-APSP on \(W\) is the matrix power \(W^{2^k}\), with products computed in \(\alpha\).

public theorem fasterAPSP_ret {α : Type u} [Semiring α] {n : Nat}
    (W : Vector (Vector α n) n) :
    Matrix.of (fun i j => ((fasterAPSP W).ret.get i).get j) =
      Matrix.of (fun i j => (W.get i).get j) ^ (2 ^ Nat.clog 2 (n - 1))

Uses 7 · Used by 1

Statement usesFASTER-APSP

Proof usesCounted copy of a square matrix · The counted matrix copy returns its input · Counted zero initialization of a square matrix · The counted zero initialization returns the zero matrix · Square matrix accumulation · Square matrix accumulation computes \(C + AB\)

Used byFASTER-APSP computes edge-bounded shortest-path weights

TheoremOperation counts of FASTER-APSP#✓fully proved

Let \(\alpha\) be a type with addition, multiplication and zero, let \(W\) be an \(n \times n\) matrix over \(\alpha\), and let \(k = \lceil \log_2 (n - 1) \rceil\) be the least natural number with \(n - 1 \le 2^k\). On input \(W\), FASTER-APSP performs exactly \(n^2 + 2 k n^2\) copy and fill assignments, \(k n^3\) scalar additions and \(k n^3\) scalar multiplications.

Assignments count the matrix cells copied or filled with zero; the accumulator vector updates inside the matrix multiplications are not counted.

public theorem fasterAPSP_time {α : Type u} [Add α] [Mul α] [Zero α] {n : Nat}
    (W : Vector (Vector α n) n) :
    (fasterAPSP W).time =
      (n ^ 2 + 2 * Nat.clog 2 (n - 1) * n ^ 2,
        (Nat.clog 2 (n - 1) * n ^ 3, Nat.clog 2 (n - 1) * n ^ 3))

Uses 8 · Used by 1

Statement usesFASTER-APSP

Proof usesCounted copy of a square matrix · The counted matrix copy returns its input · Cost of the counted matrix copy · Counted zero initialization of a square matrix · Cost of the counted zero initialization · Square matrix accumulation · Operation count of square matrix accumulation

Used byAsymptotic operation count of FASTER-APSP

TheoremAsymptotic operation count of FASTER-APSP#✓fully proved

Let \(\alpha\) be a type with addition, multiplication and zero, and for each \(n\) let \(W_n\) be an \(n \times n\) matrix over \(\alpha\). The total number of copy and fill assignments, scalar additions and scalar multiplications that FASTER-APSP performs on \(W_n\) is \(\Theta(n^3 \log n)\) as \(n \to \infty\).

public theorem fasterAPSP_time_isTheta {α : Type u} [Add α] [Mul α] [Zero α]
    (W : (n : Nat) → Vector (Vector α n) n) :
    Asymptotics.IsTheta Filter.atTop
      (fun n => ((fasterAPSP (W n)).time.1 +
        (fasterAPSP (W n)).time.2.1 + (fasterAPSP (W n)).time.2.2 : ℝ))
      (fun n => (n : ℝ) ^ 3 * Real.log (n : ℝ))

Uses 2

Statement usesFASTER-APSP

Proof usesOperation counts of FASTER-APSP

DefinitionSlow all-pairs shortest paths (SLOW-APSP)#✓fully proved

Let \(W\) and \(L^{(0)}\) be \(n \times n\) matrices over the min-plus semiring on \(\mathbb{Z} \cup \{\infty\}\), in which addition is \(\min\) and multiplication is \(+\). SLOW-APSP copies \(L^{(0)}\) cell by cell and then runs \(\max(n - 1, 0)\) phases. Phase \(r\) fills a fresh \(n \times n\) matrix \(M\) with \(\infty\), then for each triple \((i, j, k)\) in increasing \(i\)-\(j\)-\(k\) order sets \(M_{ij} \leftarrow \min(M_{ij}, L^{(r-1)}_{ik} + W_{kj})\), and finally copies \(M\) cell by cell to give \(L^{(r)}\); the result is \(L^{(n-1)}\). The cost is a triple of natural numbers: the first coordinate counts one assignment for each cell copied or filled, and the second and third coordinates count one scalar addition and one scalar minimum for each update \(M_{ij} \leftarrow \min(M_{ij}, L^{(r-1)}_{ik} + W_{kj})\).

Accumulator updates inside the loop are not charged as assignments.

@[no_expose] public def slowAPSP {n : Nat}
    (W L0 : _root_.Vector (_root_.Vector (MinTropical (WithTop Int)) n) n) :
    TimeM (Nat × (Nat × Nat))
      (_root_.Vector (_root_.Vector (MinTropical (WithTop Int)) n) n) := do
  let saved ← copyCells L0
  runPhases W (n - 1) saved

Uses 3 · Used by 6

Statement usesCounted copy of a square matrix · Counted zero initialization of a square matrix · Square matrix accumulation

Used byFASTER-APSP computes shortest-path weights · SLOW-APSP computes shortest-path weights · Bounded-edge shortest weights from SLOW-APSP · SLOW-APSP returns a min-plus matrix power · Exact operation counts of SLOW-APSP · SLOW-APSP takes quartic time

TheoremSLOW-APSP returns a min-plus matrix power#✓fully proved

For \(n \times n\) matrices \(W\) and \(L^{(0)}\) over the min-plus semiring on \(\mathbb{Z} \cup \{\infty\}\), in which addition is \(\min\) and multiplication is \(+\), the matrix returned by SLOW-APSP on \(W\) and \(L^{(0)}\) equals the min-plus matrix product \(L^{(0)} W^{n-1}\).

public theorem slowAPSP_ret {n : Nat}
    (W L0 : _root_.Vector
      (_root_.Vector (MinTropical (WithTop Int)) n) n) :
    Matrix.of (fun i j => ((slowAPSP W L0).ret.get i).get j) =
      Matrix.of (fun i j => (L0.get i).get j) *
        Matrix.of (fun i j => (W.get i).get j) ^ (n - 1)

Uses 7 · Used by 1

Statement usesSlow all-pairs shortest paths (SLOW-APSP)

Proof usesCounted copy of a square matrix · The counted matrix copy returns its input · Counted zero initialization of a square matrix · The counted zero initialization returns the zero matrix · Square matrix accumulation · Square matrix accumulation computes \(C + AB\)

Used byBounded-edge shortest weights from SLOW-APSP

TheoremBounded-edge shortest weights from SLOW-APSP#✓fully proved

Let \(W\) and \(L^{(0)}\) be \(n \times n\) matrices over the min-plus semiring on \(\mathbb{Z} \cup \{\infty\}\), and let \(w_{xy}\) be the underlying value in \(\mathbb{Z} \cup \{\infty\}\) of \(W_{xy}\). Suppose that \(w_{ii} = 0\) for every \(i\) and that the underlying value of \(L^{(0)}_{ij}\) is \(0\) if \(i = j\) and \(\infty\) otherwise. Then for all \(i, j \in \{0, \dots, n-1\}\), the underlying value \(d\) of the \((i, j)\) entry of the matrix returned by SLOW-APSP on \(W\) and \(L^{(0)}\) is at most the weight of every path from \(i\) to \(j\) with at most \(n - 1\) edges, and \(d\) is either \(\infty\) or the weight of such a path. Here a path from \(i\) to \(j\) is a nonempty sequence of vertices that starts at \(i\), ends at \(j\) and has \(w_{xy} \ne \infty\) for each pair of consecutive vertices \(x, y\); vertices may repeat, its number of edges is its number of vertices minus one, and its weight is the sum of these \(w_{xy}\).

public theorem slowAPSP_edgeBounded {n : Nat}
    (W L0 : _root_.Vector (_root_.Vector (MinTropical (WithTop Int)) n) n)
    (hdiag : ∀ i : Fin n, MinTropical.untrop ((W.get i).get i) = 0)
    (hinit : ∀ i j : Fin n,
      MinTropical.untrop ((L0.get i).get j) = if i = j then 0 else ⊤)
    (i j : Fin n) :
    FloydWarshall.IsEdgeBoundedShortestPathWeight
      (Matrix.of fun x y => MinTropical.untrop ((W.get x).get y))
      (n - 1) i j
      (MinTropical.untrop (((slowAPSP W L0).ret.get i).get j))

Uses 4 · Used by 2

Statement usesShortest path weight with at most \(r\) edges · Slow all-pairs shortest paths (SLOW-APSP)

Proof usesMin-plus matrix powers give shortest path weights with at most \(r\) edges · SLOW-APSP returns a min-plus matrix power

Used byFASTER-APSP computes shortest-path weights · SLOW-APSP computes shortest-path weights

TheoremSLOW-APSP computes shortest-path weights#✓fully proved

Let \(W\) and \(L^{(0)}\) be \(n \times n\) matrices over the min-plus semiring on \(\mathbb{Z} \cup \{\infty\}\), and let \(w_{xy}\) be the underlying value in \(\mathbb{Z} \cup \{\infty\}\) of \(W_{xy}\). Suppose that \(w_{ii} = 0\) for every \(i\), that the underlying value of \(L^{(0)}_{ij}\) is \(0\) if \(i = j\) and \(\infty\) otherwise, and that \(w\) has no negative cycle. Then for all \(i, j \in \{0, \dots, n-1\}\), the underlying value \(d\) of the \((i, j)\) entry of the matrix returned by SLOW-APSP on \(W\) and \(L^{(0)}\) is at most the weight of every path from \(i\) to \(j\), and \(d\) is either \(\infty\) or the weight of some path from \(i\) to \(j\). Here a path from \(i\) to \(j\) is a nonempty sequence of vertices that starts at \(i\), ends at \(j\) and has \(w_{xy} \ne \infty\) for each pair of consecutive vertices \(x, y\); its weight is the sum of these \(w_{xy}\). A negative cycle is a path from a vertex to itself with at least two vertices, negative weight, and no repeated vertex once its last vertex is removed.

public theorem slowAPSP_distance_spec {n : Nat}
    (W L0 : _root_.Vector (_root_.Vector (MinTropical (WithTop Int)) n) n)
    (hdiag : ∀ i : Fin n, MinTropical.untrop ((W.get i).get i) = 0)
    (hinit : ∀ i j : Fin n,
      MinTropical.untrop ((L0.get i).get j) = if i = j then 0 else ⊤)
    (hNoCycle : FloydWarshall.NoNegativeCycle
      (Matrix.of fun x y => MinTropical.untrop ((W.get x).get y)))
    (i j : Fin n) :
    FloydWarshall.IsStageShortestPathWeight
      (Matrix.of fun x y => MinTropical.untrop ((W.get x).get y))
      n i j
      (MinTropical.untrop (((slowAPSP W L0).ret.get i).get j))

Uses 10 · Used by 1

Statement usesStage-\(k\) shortest-path weight · Weight matrices without negative cycles · Slow all-pairs shortest paths (SLOW-APSP)

Proof usesMatrices with a negative cycle · Intermediate vertices below a bound · Shortest path weight with at most \(r\) edges · Negative cycles · Finite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix · Bounded-edge shortest weights from SLOW-APSP

Used byFASTER-APSP computes shortest-path weights

TheoremExact operation counts of SLOW-APSP#✓fully proved

For all \(n \times n\) matrices \(W\) and \(L^{(0)}\) over the min-plus semiring on \(\mathbb{Z} \cup \{\infty\}\), the cost of SLOW-APSP on \(W\) and \(L^{(0)}\) is the triple \((n^2 + 2(n-1)n^2,\ (n-1)n^3,\ (n-1)n^3)\) of cell assignments (copies and fills), scalar additions and scalar minimums, where \(n - 1\) means \(\max(n - 1, 0)\).

The assignment count excludes the accumulator updates inside the min-plus accumulation loop.

public theorem slowAPSP_time {n : Nat}
    (W L0 : _root_.Vector
      (_root_.Vector (MinTropical (WithTop Int)) n) n) :
    (slowAPSP W L0).time =
      (n ^ 2 + 2 * (n - 1) * n ^ 2,
        ((n - 1) * n ^ 3, (n - 1) * n ^ 3))

Uses 9 · Used by 1

Statement usesSlow all-pairs shortest paths (SLOW-APSP)

Proof usesCounted copy of a square matrix · The counted matrix copy returns its input · Cost of the counted matrix copy · Counted zero initialization of a square matrix · The counted zero initialization returns the zero matrix · Cost of the counted zero initialization · Square matrix accumulation · Operation count of square matrix accumulation

Used bySLOW-APSP takes quartic time

TheoremSLOW-APSP takes quartic time#✓fully proved

For any choice, for each \(n\), of \(n \times n\) matrices \(W_n\) and \(L^{(0)}_n\) over the min-plus semiring on \(\mathbb{Z} \cup \{\infty\}\), the total cost of SLOW-APSP on \(W_n\) and \(L^{(0)}_n\), that is the number of cell assignments (copies and fills) plus the number of scalar additions plus the number of scalar minimums, is \(\Theta(n^4)\) as \(n \to \infty\).

public theorem slowAPSP_time_isTheta
    (W L0 : (n : Nat) →
      _root_.Vector
        (_root_.Vector (MinTropical (WithTop Int)) n) n) :
    Asymptotics.IsTheta Filter.atTop
      (fun n => ((slowAPSP (W n) (L0 n)).time.1 +
        (slowAPSP (W n) (L0 n)).time.2.1 +
        (slowAPSP (W n) (L0 n)).time.2.2 : ℝ))
      (fun n => (n : ℝ) ^ 4)

Uses 2

Statement usesSlow all-pairs shortest paths (SLOW-APSP)

Proof usesExact operation counts of SLOW-APSP

TheoremFASTER-APSP computes edge-bounded shortest-path weights#✓fully proved

Let \(W\) be an \(n \times n\) matrix with entries in \(\mathbb{Z} \cup \{\infty\}\), read as edge weights of a directed graph on the vertices \(0, \dots, n - 1\) (weight \(\infty\) meaning no edge), with \(W_{ii} = 0\) for every \(i\), and let \(k = \lceil \log_2 (n - 1) \rceil\) be the least natural number with \(n - 1 \le 2^k\). Run FASTER-APSP on \(W\) over the min-plus semiring, whose addition is \(\min\) and whose multiplication is \(+\). Then for all vertices \(i\) and \(j\), the returned entry \(d\) at \((i, j)\) is at most the weight of every path from \(i\) to \(j\) with at most \(2^k\) edges, all of finite weight, and either \(d = \infty\) or \(d\) is the weight of such a path. Paths are nonempty vertex sequences and may repeat vertices; no assumption on negative cycles is made.

public theorem fasterAPSP_edgeBounded {n : Nat}
    (W : Vector (Vector (MinTropical (WithTop Int)) n) n)
    (hdiag : ∀ i : Fin n, MinTropical.untrop ((W.get i).get i) = 0)
    (i j : Fin n) :
    FloydWarshall.IsEdgeBoundedShortestPathWeight
      (Matrix.of fun x y => MinTropical.untrop ((W.get x).get y))
      (2 ^ Nat.clog 2 (n - 1)) i j
      (MinTropical.untrop (((fasterAPSP W).ret.get i).get j))

Uses 4 · Used by 1

Statement usesShortest path weight with at most \(r\) edges · FASTER-APSP

Proof usesFASTER-APSP returns a power of the input matrix · Min-plus matrix powers give shortest path weights with at most \(r\) edges

Used byFASTER-APSP computes shortest-path weights

TheoremFASTER-APSP computes shortest-path weights#✓fully proved

Let \(W\) be an \(n \times n\) matrix with entries in \(\mathbb{Z} \cup \{\infty\}\), read as edge weights of a directed graph on the vertices \(0, \dots, n - 1\) (weight \(\infty\) meaning no edge), such that \(W_{ii} = 0\) for every \(i\) and \(W\) has no negative cycle. Run FASTER-APSP on \(W\) over the min-plus semiring, whose addition is \(\min\) and whose multiplication is \(+\). Then for all vertices \(i\) and \(j\), the returned entry \(d\) at \((i, j)\) is the shortest-path weight from \(i\) to \(j\): \(d\) is at most the weight of every path from \(i\) to \(j\) all of whose edges have finite weight, and either \(d = \infty\) or \(d\) is the weight of such a path. Paths are nonempty vertex sequences and may repeat vertices.

public theorem fasterAPSP_distance_spec {n : Nat}
    (W : Vector (Vector (MinTropical (WithTop Int)) n) n)
    (hdiag : ∀ i : Fin n, MinTropical.untrop ((W.get i).get i) = 0)
    (hNoCycle : FloydWarshall.NoNegativeCycle
      (Matrix.of fun x y => MinTropical.untrop ((W.get x).get y)))
    (i j : Fin n) :
    FloydWarshall.IsStageShortestPathWeight
      (Matrix.of fun x y => MinTropical.untrop ((W.get x).get y)) n i j
      (MinTropical.untrop (((fasterAPSP W).ret.get i).get j))

Uses 11

Statement usesStage-\(k\) shortest-path weight · Weight matrices without negative cycles · FASTER-APSP

Proof usesIntermediate vertices below a bound · Shortest path weight with at most \(r\) edges · Finite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix · FASTER-APSP computes edge-bounded shortest-path weights · Slow all-pairs shortest paths (SLOW-APSP) · SLOW-APSP computes shortest-path weights · Bounded-edge shortest weights from SLOW-APSP

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.