94 Graph Theory — Basic
94.1 Overview
This module formalises the core data structures and the greedy selection loop underlying Kruskal’s minimum-spanning-tree algorithm. It defines weighted edges over \(n\) vertices, a union-find structure represented as a flat array of representatives, the edge-processing sweep that builds the spanning tree, and the top-level kruskal function. The two main correctness results show that every edge returned by the algorithm was present in the original input list.
94.2 Declarations
A weighted edge over \(n\) vertices is a structure with two endpoints \(u, v : \mathrm{Fin}\, n\) and a natural-number weight \(w : \mathbb {N}\).
The union-find state for \(n\) nodes is defined as a function \(\mathrm{Fin}\, n \to \mathbb {N}\) mapping each node to its current representative (component label).
\(\mathtt{init}\, n\) constructs the identity union-find on \(n\) nodes: every node \(i\) is its own representative, i.e. \(\mathtt{init}\, n\, (i) = i\).
\(\mathtt{find}\, \mathit{uf}\, i\) returns the representative of node \(i\) in the union-find state \(\mathit{uf}\), defined simply as \(\mathit{uf}(i)\).
\(\mathtt{merge}\, \mathit{uf}\, i\, j\) unifies the components of nodes \(i\) and \(j\) by reassigning every node whose representative equals \(\mathit{uf}(j)\) to instead carry the representative \(\mathit{uf}(i)\).
Consider the identity union-find on \(n\) nodes, in which every node is its own representative. For every node \(i \in \mathrm{Fin}\, n\), applying the find operation to this initial state returns the underlying numeric value of \(i\); that is, the representative of \(i\) is \(i\) itself.
Let \(\mathit{uf} \colon \mathrm{Fin}\, n \to \mathbb {N}\) be a union-find state on \(n\) nodes, and let \(i\) be one of its nodes. Then the representative of \(i\) returned by \(\mathrm{find}\) coincides with the direct evaluation of the state at \(i\); that is, \(\mathrm{find}(\mathit{uf}, i) = \mathit{uf}(i)\).
\(\mathtt{mergeAll}\, \mathit{uf}\, \mathit{es}\) folds a list of weighted edges \(\mathit{es}\) into the union-find \(\mathit{uf}\) by calling merge on each edge’s endpoints in sequence.
\(\mathtt{SamePartition}\, \mathit{uf}_1\, \mathit{uf}_2\) holds when two union-find states induce the same equivalence relation on nodes: for all \(i, j : \mathrm{Fin}\, n\), \(\mathit{uf}_1(i) = \mathit{uf}_1(j)\) if and only if \(\mathit{uf}_2(i) = \mathit{uf}_2(j)\).
\(\mathtt{processEdges}\, \mathit{es}\, \mathit{uf}\, \mathit{acc}\) scans the edge list \(\mathit{es}\) left-to-right: an edge \(e\) is added to the accumulator and its endpoints are merged whenever \(\mathit{uf}.\mathtt{find}\, e.u \ne \mathit{uf}.\mathtt{find}\, e.v\); otherwise \(e\) is skipped. The reversed accumulator is returned when the list is exhausted.
\(\mathtt{kruskal}\, n\, \mathit{edges}\) sorts the edge list by weight and then runs processEdges on the sorted list starting from the identity union-find, returning the selected spanning-tree edges.
Fix \(n\), and let \(\mathit{es}\) be a list of weighted edges over \(n\) vertices, let \(\mathit{uf}\) be a union-find state on \(n\) nodes, and let \(\mathit{acc}\) be an accumulator list of weighted edges. If a weighted edge \(e\) occurs in the output produced by running the edge-selection sweep on the edge list \(\mathit{es}\), the union-find state \(\mathit{uf}\), and the accumulator \(\mathit{acc}\), then \(e\) already occurs in the accumulator \(\mathit{acc}\) or \(e\) occurs in the edge list \(\mathit{es}\).
Fix \(n \in \mathbb {N}\) and a list of weighted edges over \(n\) vertices. Every edge returned by running Kruskal’s algorithm on this list occurs in the original list: if \(e\) belongs to the output of \(\mathtt{kruskal}\, n\, \mathit{edges}\), then \(e\) belongs to \(\mathit{edges}\).