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 space-constructable function ${\displaystyle f\in \Omega (\log(n))}$,

${\displaystyle {\mathsf {NSPACE}}\left(f\left(n\right)\right)\subseteq {\mathsf {DSPACE}}\left(f\left(n\right)^{2}\right).}$

In other words, if a nondeterministic Turing machine can solve a problem using ${\displaystyle f(n)}$ space, a 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 (as formalized in the unproven exponential time hypothesis), Savitch's theorem shows that it has a markedly more limited effect on space requirements.

The theorem can be relativized. That is, for any oracle, replacing every "Turing machine" with "oracle Turing machine" would still result in a theorem.