136 Graph Theory — Exchange

136.1 Overview

This module develops the exchange argument underlying the correctness of Kruskal’s algorithm: if an edge \(e\) joins two components that are already connected by some spanning edge list, then one of the edges of that list may be swapped out for \(e\) without losing any reachability. The argument is given both in the reachability formulation and in the union–find formulation, together with a lemma that removes a redundant edge from a candidate set without increasing its total weight.

136.2 Declarations

Lemma 136.1 Exchanging the head edge for a new edge

✓

Let \(\mathit{base}, \mathit{rest}\) be edge lists on \(n\) vertices and let \(g, e\) be edges. Suppose that in \(\mathit{base} \mathbin {+\! \! +} \mathit{rest}\) the vertex \(e.u\) reaches \(g.u\) and \(g.v\) reaches \(e.v\). Then every pair \(a, b\) that is reachable in \(\mathit{base} \mathbin {+\! \! +} (g :: \mathit{rest})\) is also reachable in \(\mathit{base} \mathbin {+\! \! +} \mathit{rest} \mathbin {+\! \! +} [e]\); that is, \(g\) may be replaced by \(e\) without losing connectivity.

Lemma 136.2 Exchanging the head edge, reversed orientation

✓

The same exchange statement with the endpoints of \(g\) taken in the opposite order: if in \(\mathit{base} \mathbin {+\! \! +} \mathit{rest}\) the vertex \(e.u\) reaches \(g.v\) and \(g.u\) reaches \(e.v\), then every pair reachable in \(\mathit{base} \mathbin {+\! \! +} (g :: \mathit{rest})\) is reachable in \(\mathit{base} \mathbin {+\! \! +} \mathit{rest} \mathbin {+\! \! +} [e]\).

Lemma 136.3 Exchange argument over a base edge list

✓

Let \(\mathit{base}, S\) be edge lists and let \(e\) be an edge with \(e.u \neq e.v\) whose endpoints are connected in \(\mathit{base} \mathbin {+\! \! +} S\) but not in \(\mathit{base}\) alone. Then there exists an edge \(f \in S\) such that every pair \(a, b\) reachable in \(\mathit{base} \mathbin {+\! \! +} S\) remains reachable in \(\mathit{base} \mathbin {+\! \! +} (S \setminus \{ f\} ) \mathbin {+\! \! +} [e]\), where \(S \setminus \{ f\} \) denotes \(\mathtt{S.erase}\, f\).

Lemma 136.4 Union–find form of the exchange argument

✓

Let \(\mathit{uf}\) be a union–find state whose classes are exactly the reachability classes of an edge list \(\mathit{base}\), i.e. \(\mathit{uf}\, a = \mathit{uf}\, b\) iff \(a\) and \(b\) are reachable in \(\mathit{base}\). If merging all edges of \(S\) into \(\mathit{uf}\) identifies \(e.u\) and \(e.v\) while \(\mathit{uf}\) itself keeps them apart, then there is an edge \(f \in S\) such that \((\mathit{uf}.\mathtt{merge}\, e.u\, e.v).\mathtt{mergeAll}\, (S \setminus \{ f\} )\) induces the same partition as \(\mathit{uf}.\mathtt{mergeAll}\, S\).

Lemma 136.5 Removing a redundant edge from a candidate set

✓

Let \(\mathit{uf}\) be a union–find state, \(e\) an edge, and \(\mathit{rest}, S\) edge lists with every element of \(S\) lying in \(e :: \mathit{rest}\), such that \(\mathit{uf}.\mathtt{mergeAll}\, S\) and \(\mathit{uf}.\mathtt{mergeAll}\, \mathit{rest}\) induce the same partition. If \(e\) is redundant for \(\mathit{uf}\), i.e. \(\mathit{uf}\, e.u = \mathit{uf}\, e.v\), then there exists a list \(S'\) all of whose edges lie in \(\mathit{rest}\), such that \(\mathit{uf}.\mathtt{mergeAll}\, S'\) induces the same partition as \(\mathit{uf}.\mathtt{mergeAll}\, \mathit{rest}\) and \(\mathtt{totalWeight}\, S' \leq \mathtt{totalWeight}\, S\).