Chapter 24 - Single-Source Shortest Paths

Chapter 24 opens the shortest-path part of the CLRS graph track. It builds a finite weighted directed-graph model on top of the Chapter 22 style graph vocabulary and formalizes the Bellman-Ford algorithm: the relaxation dynamic program, the upper-bound property, realizability of estimates by actual walks, cycle removal under the no-negative-cycle hypothesis, exact correctness after |V| - 1 rounds, convergence, and the O(V·E) work bound.

Sections

• 24.1 The Bellman-Ford algorithm. Main declarations: CLRS.Chapter24.WeightedGraph, CLRS.Chapter24.WeightedGraph.walkWeight, CLRS.Chapter24.WeightedGraph.IsWalkFrom, CLRS.Chapter24.WeightedGraph.relaxDist, CLRS.Chapter24.WeightedGraph.relaxDist_le_walkWeight, CLRS.Chapter24.WeightedGraph.exists_walk_of_relaxDist, CLRS.Chapter24.WeightedGraph.NoNegCycle, CLRS.Chapter24.WeightedGraph.exists_simple_le, CLRS.Chapter24.WeightedGraph.IsShortestDist, CLRS.Chapter24.WeightedGraph.relaxDist_isShortestDist, CLRS.Chapter24.WeightedGraph.relaxDist_stabilizes, and CLRS.Chapter24.WeightedGraph.bellmanFordWork_le.

• 24.2 Single-source shortest paths in directed acyclic graphs. Main declarations: CLRS.Chapter24.WeightedGraph.IsTopoOrder, CLRS.Chapter24.WeightedGraph.isAcyclic_of_isTopoOrder, CLRS.Chapter24.WeightedGraph.relaxFrom, CLRS.Chapter24.WeightedGraph.dagRelax, CLRS.Chapter24.WeightedGraph.dagRelax_respects_edge, CLRS.Chapter24.WeightedGraph.dagRelax_isShortestDist, CLRS.Chapter24.WeightedGraph.sum_outdegree, and CLRS.Chapter24.WeightedGraph.dagSSSPWork_eq.

• 24.3 Dijkstra's algorithm. Main declarations: CLRS.Chapter24.WeightedGraph.Nonneg, CLRS.Chapter24.WeightedGraph.noNegCycle_of_nonneg, CLRS.Chapter24.WeightedGraph.walkWeight_nonneg, CLRS.Chapter24.WeightedGraph.exists_crossing, CLRS.Chapter24.WeightedGraph.dijkstra_extractMin_correct, CLRS.Chapter24.WeightedGraph.DijkstraState, CLRS.Chapter24.WeightedGraph.dijkstraInit, CLRS.Chapter24.WeightedGraph.dijkstraInit_invariant, CLRS.Chapter24.WeightedGraph.dijkstraStep_invariant, CLRS.Chapter24.WeightedGraph.dijkstraLoop, CLRS.Chapter24.WeightedGraph.dijkstraLoop_invariant, CLRS.Chapter24.WeightedGraph.dijkstraLoop_finish, CLRS.Chapter24.WeightedGraph.dijkstraLoop_correct, and CLRS.Chapter24.WeightedGraph.dijkstraWork_le_edge_log.

• 24.4 Difference constraints and shortest paths. Main declarations: CLRS.Chapter24.WeightedGraph.DiffConstraintSystem, CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.IsFeasible, CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.constraintGraph, CLRS.Chapter24.WeightedGraph.le_add_walkWeight_of_potential, CLRS.Chapter24.WeightedGraph.relaxDist_respects_edge, CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.noNegCycle_of_feasible, CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.feasible_of_noNegCycle, and CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.diffConstraint_feasible_iff_noNegCycle.

• 24.5 Proofs of shortest paths: the shortestDist distance function δ, the no-path property, the upper-bound property, and the triangle inequality (CLRS Lemmas 24.11-24.13). Main declarations: CLRS.Chapter24.WeightedGraph.shortestDist, CLRS.Chapter24.WeightedGraph.shortestDist_isShortestDist, CLRS.Chapter24.WeightedGraph.noPath_iff_top, CLRS.Chapter24.WeightedGraph.shortestDist_le_walkWeight, CLRS.Chapter24.WeightedGraph.IsWalkFrom.append_edge, and CLRS.Chapter24.WeightedGraph.shortestDist_triangleInequality.

Current Shape

Section 24.1 defines a WeightedGraph as a finite edge set plus a real weight function, defines walks and walk weights, and models Bellman-Ford as a synchronous relaxation dynamic program relaxDist valued in WithTop ℝ. It proves the upper-bound property (relaxDist_le_walkWeight), realizability of finite estimates by walks (exists_walk_of_relaxDist), the cycle-removal shortening lemma under NoNegCycle (exists_simple_le), and, as the headline, CLRS Theorem 24.4: after |V| - 1 rounds the estimates equal the single-source shortest-path distances δ(s, ·) characterized by IsShortestDist (relaxDist_isShortestDist), together with convergence (relaxDist_stabilizes) and the (|V| - 1)·|E| ≤ |V|·|E| = O(V·E) work bound (bellmanFordWork_le).

Section 24.3 adds Dijkstra's algorithm under nonnegative edge weights. It shows nonnegative weights imply NoNegCycle (so Section 24.1's δ applies), that a walk from a settled to an unsettled vertex crosses the settled frontier (exists_crossing), and proves CLRS Theorem 24.6, the greedy invariant (dijkstra_extractMin_correct): the unsettled vertex of minimum tentative distance already has the exact shortest-path distance. It also records the (|V| + |E|)·log|V| = O(E log V) binary-heap work decomposition (dijkstraWork_le_edge_log). The file defines an executable state/step/loop skeleton: dijkstraInit pre-settles the source with distance 0 and pre-relaxes its outgoing edges so that DijkstraInvariant holds from the start (dijkstraInit_invariant); one-step invariant preservation (dijkstraStep_invariant) lifts the invariant through dijkstraLoop (dijkstraLoop_invariant); and the end-to-end correctness theorem (dijkstraLoop_correct) proves that after |V| iterations every vertex has its exact shortest-path distance.

Section 24.2 formalizes CLRS's DAG-SHORTEST-PATHS. It restates the topological-order predicate over WeightedGraph.Adj (IsTopoOrder), shows a topological order forces acyclicity (isAcyclic_of_isTopoOrder), and models the algorithm as a fold of the single-vertex out-edge relaxation relaxFrom along the order (dagRelax). The headline is CLRS §24.2 correctness (dagRelax_isShortestDist): a single left-to-right pass already yields δ(s, ·) characterized by IsShortestDist, obtained from the per-edge upper bound (dagRelax_respects_edge) telescoped along walks plus realizability. The |V| + |E| = Θ(V + E) work count (sum_outdegree, dagSSSPWork_eq) records that each vertex and each edge is touched exactly once.

Section 24.4 formalizes the connection between difference constraints and shortest paths (CLRS §24.4). It defines a DiffConstraintSystem as a finite set of inequalities x_j ≤ x_i + b, builds the constraint graph (constraintGraph) as a WeightedGraph with a fresh source, proves the general potential-function lemma (le_add_walkWeight_of_potential) and the Bellman-Ford triangle inequality (relaxDist_respects_edge), and establishes CLRS Theorem 24.9 (diffConstraint_feasible_iff_noNegCycle): feasibility ↔ no negative-weight cycle, with the explicit Bellman-Ford solution x i = δ(s, i).

Deferred Work

• Per-edge relaxation ordering and mutable/RAM cost refinement of the abstract synchronous relaxation model.

The advertised Bellman-Ford correctness/work chain (Section 24.1), the DAG-shortest-paths correctness and Θ(V + E) work bound (Section 24.2), the Dijkstra greedy theorem, executable loop with end-to-end correctness, and abstract work bound (Section 24.3), and the difference-constraint feasibility characterisation (Section 24.4) are proved.