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 formula_1, In other words, if a nondeterministic Turing machine can solve a problem using formula_3 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, this theorem shows that it has a markedly more limited effect on space requirements. Proof. The proof relies on an algorithm for STCON, the problem  of determining whether there is a path between two vertices in a directed graph, which runs in formula_4 space for formula_5 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 s-t" path, by recursively searching for paths of half the length from "s" to "u" and "u" to "t". Using pseudocode (in Python syntax) we can express this algorithm as follows: def k_edge_path(s, t, k) -> bool: This search calls itself to a recursion depth of formula_6 levels, each of which requires formula_6 bits to store the function arguments and local variables at that level: "k" and all vertices ("s", "t", "u") require formula_6 bits each. The total auxiliary space complexity is thus formula_4. Although described above in the form of a program  in a high-level language, the same algorithm may be implemented with the same asymptotic space bound on a Turing machine. To see why this algorithm implies the theorem, consider the following. For any language formula_10, there is a Turing machine formula_11 which decides formula_12 in space formula_3. Assume w.l.o.g. the alphabet is a binary alphabet formula_14 (viz. formula_15). For any input word formula_16, there is a directed graph formula_17 whose vertices are the configurations of formula_11 when running on the input formula_19. There may be "infinitely many" such configurations; e.g. when formula_11 keeps writing a symbol on the tape  and moving the head to the right in a loop, ad infinitum. The configurations then grow arbitrarily large. However, we know that at most formula_21 space is needed to decide whether formula_22, so we only care about configurations of size at most formula_21; call any such configuration "admissible". There are finitely many admissible configurations; namely formula_24. Therefore, the induced subgraph formula_25 of formula_17 containing (exactly) the admissible configurations has formula_24 vertices. For each input formula_28, formula_25 has a path from the starting configuration to an accepting configuration if and only if formula_22. Thus by deciding connectivity in formula_25, we can  decide membership of formula_19 in formula_12. By the above algorithm this can be done deterministically in space formula_34; hence formula_12 is in formula_36. Since this holds for all formula_37 and all formula_38, we get the statement of the theorem: Corollaries. Some important corollaries of the theorem include: