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))}$,

${\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.^[1] 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.^[2]