Savitch's theorem

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

${\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.^[3] 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.^[4]

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