Savitch's theorem

In computational complexity theory, Savitch's theorem, proved by Walter Savitch in 1970, states that for any function "f"("n") ≥ log("n")

:NSPACE(f(n)) ⊆ DSPACE(f²(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 the space. 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.

Proof

The proof of the theorem 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 log("n")² space for "n" vertices. Then, it builds a DSPACE machine which runs the algorithm on the computation tree of the corresponding NSPACE machine to determine whether there is a path from the start node to the accept node, and accepts if and only if this is so. As STCON is NL-complete, this demonstrates that all languages in NL are also in L².

Corollaries

Some important corollaries of the theorem include:
* PSPACE = NPSPACE
** This follows directly from the fact that the square of a polynomial function is still a polynomial function. It is believed that a similar relationship does not exist between the polynomial time complexity classes, P and NP, although this is still an open question.
* NL ⊆ L²
** A direct result of the construction of the proof.

References

* Section 8.1: Savitch's Theorem, pp.279–281.
* Pages 149–150 of section 7.3: The Reachability Method.
* W.J.Savitch, "Relationship between nondeterministic and deterministic tape classes", J.CSS, 4, pp 177-192, 1970