Savitch's Theorem - Proof

Proof

There is a proof of the theorem which is constructive: it demonstrates an algorithm for STCON, the problem of determining whether there is a path between two vertices in a directed graph, which runs in space for n vertices. The basic idea of the algorithm is to solve recursively a somewhat more general problem, testing the existence of a path from a vertex s to another vertex t that uses at most k edges, where k is a parameter that is given as input to the recursive algorithm; STCON may be solved from this problem by setting k to n. To test for a k-edge path from s to t, one may test whether each vertex u may be the midpoint of the path, by recursively searching for paths of half the length from s to u and u to t. In pseudocode:

def k_edge_path(s, t, k): if k == 0: return s == t else if k == 1: return s == t or (s, t) in edges else: for u in vertices: if k_edge_path(s, u, floor(k / 2)) and k_edge_path(u, t, ceil(k / 2)): return true return false

This search calls itself to a recursion depth of O(log n) levels, each of which requires O(log n) bits to store the function arguments and local variables at that level, so the total space used by the algorithm is . Although described above in the form of a program in a high-level language, the same algorithm may be implemented with the same asymptotic space bound on a Turing machine. As STCON is NL-complete, this demonstrates that all languages in NL are also in the complexity class, which is often abbreviated as L2.