2 Graph Algorithms
2.1 Traversal
2.1.1 Breadth-first search
Throughout, \(G\) is a simple directed graph whose vertex set \(V(G)\) is finite and given as data, and whose arc membership is decidable. Undirected graphs are searched through their symmetric orientation (Definition 1.3.2), so one search serves both kinds of graph.
Let \(s \in V(G)\). The layers of breadth-first search from \(s\) are the sets
where \(N^+(L)\) denotes the set of out-neighbours of the vertices of \(L\). The set of vertices visited within \(k\) rounds is \(V_k = L_0 \cup \dots \cup L_k\). When \(s \notin V(G)\) every layer is empty. In Lean the search is a state \((V_k, L_k)\) iterated \(k\) times from \((\{ s\} , \{ s\} )\), so that the definition reduces and decide can evaluate it.
Every vertex of \(L_k\) is the endpoint of a walk of length \(k\) from \(s\).
By induction on \(k\): a vertex of \(L_{k+1}\) is an out-neighbour of a vertex of \(L_k\), and appending that arc to the walk given by the induction hypothesis yields a walk of length \(k + 1\).
The endpoint of a walk of length \(\ell \) from \(s\) lies in \(V_\ell \).
By induction on the walk. The key step is that the out-neighbours of a vertex of \(V_k\) lie in \(V_{k+1}\): such a vertex lies in some \(L_j\) with \(j \le k\), and its out-neighbours are either already in \(V_j\) or in \(L_{j+1}\).
If \(L_k \neq \emptyset \) then \(k {\lt} |V(G)|\). Hence the search from \(s\) has exhausted every layer after \(|V(G)|\) rounds.
An empty layer is followed by an empty layer, so \(L_0, \dots , L_k\) are all non-empty. They are pairwise disjoint subsets of \(V(G)\), so \(k + 1 \le |V_k| \le |V(G)|\).
For every vertex \(v\) and every \(k \in {\mathbb N}\),
Let \(v \in L_k\). Soundness gives \(\operatorname{dist}(s, v) \le k\). For the reverse inequality there is nothing to show when \(k = 0\); when \(k = j + 1\), a walk from \(s\) to \(v\) of length at most \(j\) would place \(v\) in \(V_j\) by completeness, whereas \(L_{j+1}\) avoids \(V_j\) by construction, so \(\operatorname{dist}(s, v) {\gt} j\), i.e. \(\operatorname{dist}(s, v) \ge k\). Conversely, if \(\operatorname{dist}(s, v) = k\) then a shortest walk places \(v \in V_k\), so \(v \in L_j\) for some \(j \le k\), and the first part gives \(j = k\).
The set \(V_{|V(G)|}\) is exactly the set of vertices reachable from \(s\), and the least \(k {\lt} |V(G)|\) with \(v \in L_k\) (or \(\infty \) if there is none) is exactly \(\operatorname{dist}(s, v)\).
Soundness gives one inclusion and one inequality; completeness together with the termination bound gives the other.