12 Verified depth-first search
The pebble game of section 13 keeps an orientation of the edges it has accepted, with pebbles on the vertices. To bring a pebble to a vertex \(u\), it looks for a directed path from \(u\) to a vertex that has a free pebble, and it reverses the arcs of that path (definition 13.9). Lee and Streinu find such a path by depth-first search [ LS08 , § 3 ] . In this section we define a search of this kind and prove it correct.
The search works with any relation \(R\) on a finite set \(V\), given by a list of out-neighbours at each vertex, and with any predicate \(P\) on \(V\). Started at a vertex \(v\), it follows walks from \(v\) along \(R\) depth first, trying the out-neighbours of a vertex in the order of its list. It marks each vertex it enters and never enters a marked vertex again, and it stops at the first vertex that satisfies \(P\). It then returns that vertex together with the walk from \(v\) to it. If it finds no such vertex, it fails. The section uses nothing from the earlier sections.
We first define directed walks (definition 12.1) and the search (definition 12.2). We then prove that the search is sound and complete (theorem 12.4): a returned walk is simple and ends at a vertex satisfying \(P\), and the search fails only if no vertex reachable from \(v\) satisfies \(P\). In section 12.1 we compute the set of vertices reachable from \(v\), by running the search once for each vertex. The pebble game uses this set when it rejects an edge (definition 13.12).
Let \(R\) be a relation on a set \(V\), whose elements we call vertices. A directed \(R\)-walk from \(u\) to \(w\) is a sequence \(u = v_0, v_1, \ldots , v_m = w\) of vertices, with \(m \ge 0\), such that \((v_{i-1}, v_i) \in R\) for \(1 \le i \le m\). Its length is \(m\). The walk is simple if \(v_0, \ldots , v_m\) are distinct.
We say that \(w\) is reachable from \(u\) along \(R\) if \((u, w)\) lies in the reflexive-transitive closure of \(R\), that is, if there is a directed \(R\)-walk from \(u\) to \(w\).
We define the search with an arbitrary set of vertices marked at the start, since we prove its correctness by induction over all such sets.
Let \(V\) be a finite set, and let each vertex \(a \in V\) have a list \(N^+(a)\) of vertices, its out-neighbours. Let \(R\) be the relation with \((a, b) \in R\) when \(b\) appears in \(N^+(a)\), and let \(P\) be a predicate on \(V\). For a set \(S \subseteq V\) of marked vertices and a vertex \(x\), the search for \(P\) from \(x\) with \(S\) marked returns a set \(S' \supseteq S\) of marked vertices, together with either a vertex \(w\) and a walk from \(x\) to \(w\), or a failure. It runs as follows.
If \(x \in S\), the search fails, with \(S' = S\).
Otherwise, if \(P(x)\) holds, it returns \(x\) and the walk of length \(0\) at \(x\), with \(S' = S\).
Otherwise, let \(y_1, \ldots , y_k\) be the out-neighbours of \(x\) in the order of \(N^+(x)\), and let \(S_0 = S \cup \{ x\} \). For \(i = 1, \ldots , k\) in turn, it runs the search for \(P\) from \(y_i\) with \(S_{i-1}\) marked. If this search returns a vertex \(w\) and a walk \(p\) from \(y_i\) to \(w\), it stops, and returns \(w\), the walk from \(x\) that steps to \(y_i\) and follows \(p\), and the set that this search returned. If it fails, with the set \(S_i\), the search goes on to \(y_{i+1}\). If all \(k\) of these searches fail, the search fails, with \(S' = S_k\).
The search for \(P\) from \(v\) is the case \(S = \varnothing \) and \(x = v\), without its set \(S'\).
The out-neighbours are given as lists, not as finite sets, so that the search can be computed. A finite set has no preferred order of its elements, and mathlib lists them by a choice that cannot be computed; the search would inherit that choice. The marked set can be a finite set, since the search only tests whether a vertex lies in it and never lists its elements. For these tests the formal search assumes that equality of vertices can be decided, and it takes \(P\) as a function from \(V\) to \(\{ \mathrm{true}, \mathrm{false}\} \).
The search terminates, since each search started in step 3 starts with a set that contains \(S \cup \{ x\} \), so with fewer unmarked vertices than the search that starts it, and \(V\) is finite. A vertex that the search enters is marked, it stays marked for the rest of the search, and the search does not enter a marked vertex again. So the search from \(v\) enters each vertex at most once, and starts at most one search for each entry of each list \(N^+(a)\).
Let \(V\), \(R\) and \(P\) be as in definition 12.2, and let \(v \in V\).
(Soundness) If the search for \(P\) from \(v\) returns a vertex \(w\) and a walk \(p\), then \(p\) is a simple directed \(R\)-walk from \(v\) to \(w\), and \(P(w)\) holds.
(Completeness) If some vertex reachable from \(v\) along \(R\) satisfies \(P\), then the search for \(P\) from \(v\) does not fail.
For each part we prove a statement about the search for \(P\) from \(x\) with \(S\) marked, for every set \(S\) and vertex \(x\), by induction on the number of unmarked vertices. The part follows from the case \(S = \varnothing \) and \(x = v\).
For soundness we show more: if the search for \(P\) from \(x\) with \(S\) marked returns \(w\) and \(p\), then \(P(w)\) holds, \(p\) is simple, and no vertex of \(p\) lies in \(S\). If the search returns in step 2, then \(w = x\), \(P(x)\) holds, \(x \notin S\), and \(p\) has the single vertex \(x\). Otherwise it returns in step 3, and \(p\) steps from \(x\) to an out-neighbour \(y_i\) and then follows a walk \(p'\), which the search from \(y_i\) with \(S_{i-1}\) marked returned. By induction, \(P(w)\) holds, \(p'\) is simple, and no vertex of \(p'\) lies in \(S_{i-1}\), which contains \(S \cup \{ x\} \). Since \(x \notin S\), the walk \(p\) is simple and avoids \(S\).
For completeness we show: if the search for \(P\) from \(x\) with \(S\) marked fails, with the set \(S'\), then \(x \in S'\), and every vertex of \(S' \setminus S\) fails \(P\) and has all its out-neighbours in \(S'\). If \(x \in S\), then \(S' = S\), which contains \(x\). If \(P(x)\) holds, the search does not fail. So let \(x \notin S\), and let \(P(x)\) fail. Then the searches from \(y_1, \ldots , y_k\) in step 3 all fail, with sets \(S_0 \subseteq S_1 \subseteq \cdots \subseteq S_k = S'\). By induction, \(y_i \in S_i \subseteq S'\), and every vertex of \(S_i \setminus S_{i-1}\) fails \(P\) and has all its out-neighbours in \(S_i \subseteq S'\). Since \(S_0 = S \cup \{ x\} \), a vertex of \(S' \setminus S\) is either \(x\), which fails \(P\) and whose out-neighbours are \(y_1, \ldots , y_k\), or a vertex of \(S_i \setminus S_{i-1}\) for some \(i\). And \(x \in S_0 \subseteq S'\).
This gives completeness. If the search for \(P\) from \(v\) fails, with the set \(S'\), then \(v \in S'\), and every vertex of \(S'\) fails \(P\) and has all its out-neighbours in \(S'\), since nothing was marked at the start. By induction on the length of a directed \(R\)-walk from \(v\), every vertex reachable from \(v\) lies in \(S'\), so none satisfies \(P\).
12.1 Reachability regions
Lee and Streinu call the set of vertices reachable from a vertex \(v\) its reachability region, and write it \(\mathrm{Reach}(v)\) [ LS08 , § 4 ] . When the pebble game rejects an edge \(uv\), its witness is the union of the reachability regions of \(u\) and \(v\) (definition 13.12). We compute the reachability region of \(v\) by running the search from \(v\) once for each vertex \(w\), with the predicate that holds at \(w\) alone. Since the search can be computed, so can the region.
Let \(V\) and \(R\) be as in definition 12.2, and let \(v \in V\). For \(w \in V\), let \(P_w\) be the predicate that holds at \(w\) and nowhere else. The reachability region \(\mathrm{Reach}_R(v)\) is the set of vertices \(w \in V\) for which the search for \(P_w\) from \(v\) does not fail.
Let \(V\) and \(R\) be as in definition 12.2, and let \(v, w \in V\). Then \(w \in \mathrm{Reach}_R(v)\) if and only if \(w\) is reachable from \(v\) along \(R\).
Suppose that \(w \in \mathrm{Reach}_R(v)\). Then the search for \(P_w\) from \(v\) returns a vertex \(w'\) and a walk. By part (1) of theorem 12.4, \(P_w(w')\) holds, so \(w' = w\), and the walk is a directed \(R\)-walk from \(v\) to \(w\). Hence \(w\) is reachable from \(v\).
Conversely, suppose that \(w\) is reachable from \(v\). Then \(w\) is a vertex reachable from \(v\) that satisfies \(P_w\). By part (2) of theorem 12.4, the search for \(P_w\) from \(v\) does not fail, so \(w \in \mathrm{Reach}_R(v)\).