Chapter 22 - Elementary Graph Algorithms

Chapter 22 introduces the finite-graph model used by the rest of the graph algorithm track. The current development proves CLRS BFS shortest-distance and predecessor-tree correctness, establishes the DFS color/timestamp/white-path theory needed by later graph algorithms, proves both Kahn and DFS topological sort correct for DAGs, and proves full functional correctness of Kosaraju's SCC algorithm.

The model intentionally mirrors the edge-list style used by CLRS pseudocode: a finite vertex set plus an adjacency function gives a directed graph, and an undirected graph is obtained by requiring symmetric adjacency.

Sections

• 22.1 Representing graphs. Main definitions: CLRS.Chapter22.Graph, CLRS.Chapter22.Graph.Adj, CLRS.Chapter22.Graph.IsWalk, CLRS.Chapter22.Graph.IsPath, CLRS.Chapter22.Graph.IsCycle, CLRS.Chapter22.Graph.Reachable, CLRS.Chapter22.Graph.ConnectedComponent, CLRS.Chapter22.Graph.reachable_refl, CLRS.Chapter22.Graph.reachable_trans, and CLRS.Chapter22.Graph.reachable_adj.

• 22.2 Breadth-first search. Main declarations: CLRS.Chapter22.Graph.bfsAux, CLRS.Chapter22.Graph.bfs, CLRS.Chapter22.Graph.BFSInvariant, CLRS.Chapter22.Graph.bfsInvariant_step, CLRS.Chapter22.Graph.bfsAux_sound, CLRS.Chapter22.Graph.bfs_sound, CLRS.Chapter22.Graph.bfs_complete, CLRS.Chapter22.Graph.bfsState, CLRS.Chapter22.Graph.bfsState_distance_eq_some_iff, CLRS.Chapter22.Graph.bfsState_isBFSPredecessorTree, and CLRS.Chapter22.Graph.bfsState_correct.

• 22.3 Depth-first search. Main declarations: CLRS.Chapter22.Graph.DFSState, CLRS.Chapter22.Graph.dfsVisit, CLRS.Chapter22.Graph.dfs, CLRS.Chapter22.Graph.dfsVisit_blackens_u, CLRS.Chapter22.Graph.dfsVisit_preserves_black, CLRS.Chapter22.Graph.dfsVisit_no_new_gray, CLRS.Chapter22.Graph.dfs_all_black, CLRS.Chapter22.Graph.dfsVisit_blackens_iff_whiteReachable, CLRS.Chapter22.Graph.dfs_parenthesis, CLRS.Chapter22.Graph.dfs_intervals_not_cross, CLRS.Chapter22.Graph.IsDFSAncestor_reachable, CLRS.Chapter22.Graph.intervalNestedInside_dfs_iff_ancestor, CLRS.Chapter22.Graph.DFSEdgeKind, CLRS.Chapter22.Graph.dfs_edge_classification_unique, CLRS.Chapter22.Graph.dfs_tree_or_forward_edge_iff_timestamps, CLRS.Chapter22.Graph.dfs_back_edge_iff_timestamps, CLRS.Chapter22.Graph.dfs_cross_edge_iff_timestamps, CLRS.Chapter22.Graph.dfs_undirected_edge_tree_or_back, and CLRS.Chapter22.Graph.exists_discovery_state.

• 22.4 Topological sort. Main declarations: CLRS.Chapter22.Graph.IsDAG, CLRS.Chapter22.Graph.indegree, CLRS.Chapter22.Graph.IsTopologicalOrder, CLRS.Chapter22.Graph.topologicalSort, CLRS.Chapter22.Graph.topologicalSort_isTopologicalOrder, CLRS.Chapter22.Graph.dfs_finish_time_decreases_on_dag_edge, CLRS.Chapter22.Graph.dfsTopologicalSort, and CLRS.Chapter22.Graph.dfsTopologicalSort_isTopologicalOrder.

• 22.5 Strongly connected components. Main declarations: CLRS.Chapter22.Graph.transpose, CLRS.Chapter22.Graph.StronglyConnected, CLRS.Chapter22.Graph.IsSCC, CLRS.Chapter22.Graph.IsSCCPartition, CLRS.Chapter22.Graph.dfsFromListCollect, CLRS.Chapter22.Graph.kosarajuComponents, CLRS.Chapter22.Graph.scc_finish_time_order, CLRS.Chapter22.Graph.scc_finish_order, CLRS.Chapter22.Graph.kosarajuComponents_eq_sccs, CLRS.Chapter22.Graph.kosarajuComponents_subset, CLRS.Chapter22.Graph.kosarajuComponents_pairwise_disjoint, CLRS.Chapter22.Graph.kosarajuComponents_cover, and CLRS.Chapter22.Graph.kosarajuComponents_isSCCPartition.

Supporting proof modules

The DFS proof is split by responsibility so downstream developments can import only the layer they need. On the reader site, these implementation layers are nested under Section 22.3 rather than presented as separate CLRS sections:

• Section_22_3_DFS.S1_WhitePath develops finite white reachability and proves that a sufficiently fuelled visit blackens exactly the white-reachable set.

• Section_22_3_DFS.S2_Intervals develops timestamp, discovery-state, ancestor, and parent-edge infrastructure and proves the DFS parenthesis theorem plus the nesting-to-ancestor direction.

• Section_22_3_DFS.S3_Bridge connects local discovery states to the final DFS timestamps used by the SCC proof.

• Section_22_3_DFS.S4_SCC packages maximum-finish and first-discovery facts.

• Section_22_3_DFS.S5_EdgeClassification proves the unique tree/back/forward/cross classification, its CLRS timestamp characterizations, and the undirected tree-or-back theorem.

• Section_22_5_Strongly_Connected_Components.MergeSortCongr records a comparison congruence helper for decreasing-finish-time sorting.

Current Shape

Section 22.1 establishes the public graph vocabulary. Section 22.2 proves that BFS is sound and complete for reachability, that its distance labels are exact unweighted shortest-path lengths, and that its parent pointers form a rooted predecessor tree over exactly the reachable vertices. Section 22.3 gives a functional DFS model, proves its global color and timestamp invariants, proves the white-path characterization used by the SCC development, and proves that final DFS timestamp intervals are disjoint or nested and that strict nesting is equivalent to proper ancestry in the final parent forest; every graph edge is then uniquely classified as tree, back, forward, or cross. Section 22.4 implements both Kahn's algorithm and CLRS's decreasing-DFS-finish-time algorithm, and proves that each returns a valid topological order for every DAG. Section 22.5 proves the SCC finish-time ordering, proves that each component collected by Kosaraju is strongly connected and maximal, and concludes that the returned components form an SCC partition of the vertex set.

Deferred Work

• Algorithm-cost refinements: explicit work measures for the fuelled and classically selected functional implementations.

All advertised Chapter 22 algorithm-correctness chains are complete. The remaining work is executable-cost refinement rather than a functional correctness gap.