Chapter 25 - All-Pairs Shortest Paths

Chapter 25 generalises the single-source shortest-path machinery of Chapter 24 to the all-pairs setting: compute the shortest-path distance for every ordered pair of vertices. The chapter formalises three main families of algorithms:

1. Repeated squaring of the min-plus matrix product (Section 25.1, this section).

2. The Floyd-Warshall algorithm (Section 25.2).

3. Johnson's sparse-graph algorithm (Section 25.3).

Sections

• 25.1 All-pairs shortest paths model and repeated-squaring DP. Main declarations: CLRS.Chapter24.WeightedGraph.weightMatrix, CLRS.Chapter24.WeightedGraph.minPlusMul, CLRS.Chapter24.WeightedGraph.extendShortestPaths, CLRS.Chapter24.WeightedGraph.L, CLRS.Chapter24.WeightedGraph.fasterAPSP, CLRS.Chapter24.WeightedGraph.lemma_25_1, CLRS.Chapter24.WeightedGraph.L_sq_eq_minPlusMul (Lemma 25.2), CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_L, CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_shortestDist, CLRS.Chapter24.WeightedGraph.minPlusMulCost, CLRS.Chapter24.WeightedGraph.fasterAPSPCost, CLRS.Chapter24.WeightedGraph.fasterAPSPCost_le_n_cubed_log (O(V³ log V)), and CLRS.Chapter24.WeightedGraph.fasterAPSPCost_le_n_four.

• 25.2 Floyd-Warshall (Section_25_2_Floyd_Warshall). Main declarations: CLRS.Chapter24.WeightedGraph.fwStep, CLRS.Chapter24.WeightedGraph.D, CLRS.Chapter24.WeightedGraph.floydWarshall, CLRS.Chapter24.WeightedGraph.floydWarshall_O_cubed.

• 25.3 Johnson's algorithm (Section_25_3_Johnsons_Algorithm). Main declarations: CLRS.Chapter24.WeightedGraph.johnsonAugmentedGraph, CLRS.Chapter24.WeightedGraph.reweightedGraph, CLRS.Chapter24.WeightedGraph.reweightedWalkWeight_eq, CLRS.Chapter24.WeightedGraph.reweightedWeight_nonneg, CLRS.Chapter24.WeightedGraph.johnsonCost_eq (O(V² log V + V E log V)), and CLRS.Chapter24.WeightedGraph.johnsonCost_le.

Current Shape

Section 25.1 defines the edge-weight matrix W, the min-plus matrix product A ◁ B, and the inductive sequence L^(m) of shortest-path weights using at most m edges. It then defines FASTER-APSP as repeated squaring (via Function.iterate) and proves:

• Lemma 25.1: L^(m+1)_ij = min_k (L^m_ik + w_kj).

• Lemma 25.2 (squaring identity): L^(2m) = L^m ◁ L^m.

• Under no negative-weight cycles, L^m = L^{|V|-1} for all m ≥ |V|-1.

• fasterAPSP = L^{|V|-1} = δ, the all-pairs shortest-path matrix (fasterAPSP_eq_shortestDist).

Section 25.2 defines the Floyd-Warshall DP recurrence D and the floydWarshall algorithm, and proves its correctness (Lemma 25.7, Theorem 25.8, CLRS Theorem 25.3). The predecessor matrix Pi, path reconstruction fwReconstructPath (walk validity and weight equality), and the negative-cycle detection diagonal test are all complete.

Section 25.3 defines Johnson's augmented graph and reweighted graph, constructs the Bellman-Ford potential h(v) = δ(none, some v), proves the triangle inequality h(v) ≤ h(u) + w(u, v), proves reweighted edge-weight nonnegativity, packages the end-to-end Johnson correctness theorem johnsonDist_isShortestDist (CLRS Theorem 25.5), and records the O(V² log V + V E log V) binary-heap work bound (johnsonCost_eq / johnsonCost_le).

Running-time layer

All three algorithms now carry explicit, reader-facing running-time theorems bound to their real executable constructions:

• Section 25.1: minPlusMulCost / fasterAPSPCost bound to the actual graph G and iteration count numSquarings; fasterAPSPCost_le_n_cubed_log proves the O(V³ log V) repeated-squaring bound, with the trivial O(V⁴) corollary fasterAPSPCost_le_n_four.

• Section 25.2: fwStepCost / floydWarshallCost count the actual D recurrence over Finset.univ.toList, and floydWarshall_O_cubed proves the exact O(V³) bound.

• Section 25.3: johnsonAugmentedGraph_edges_card proves the augmented graph has |V| + |E| edges; johnsonCost_eq / johnsonCost_le prove the O(V² log V + V E log V) binary-heap bound.

Deferred Work

• Lower-level RAM / mutable-array machine-arithmetic accounting for the cost models; the reader-facing asymptotic bounds above are proved, and concrete word-level constants remain an optional refinement.