Savitch's theorem

In computational complexity theory, Savitch's theorem, proved by Walter Savitch in 1970, gives a relationship between deterministic and non-deterministic space complexity. It states that for any function ${\displaystyle f\in \Omega (\log(n))}$,

In other words, if a nondeterministic Turing machine can solve a problem using f(n) space, an ordinary deterministic Turing machine can solve the same problem in the square of that space bound. Although it seems that nondeterminism may produce exponential gains in time, this theorem shows that it has a markedly more limited effect on space requirements.

There is a proof of the theorem that 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 ${\displaystyle O\left((\log n)^{2}\right)}$ 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. Using pseudocode (with syntax closely resembling Python) we can express this algorithm as follows:

...
Wikipedia