Space hierarchy theorem

Remarks

The proof is a diagonalization. A machine $D$, on input $w$, marks off $f(\abs{w})$ cells and simulates the machine encoded by $w$ on $w$ within that space. It then answers the opposite. A machine using space $o(f(n))$ is simulated within the bound on long enough inputs, so it cannot decide the same language as $D$. Richard Stearns, Juris Hartmanis and Philip Lewis proved the theorem in 1965.

Consequences: $\mathrm{L} \subsetneq \mathrm{PSPACE}$, where L is the class L and PSPACE is the class PSPACE. By Savitch's theorem, NL lies in $\mathrm{DSPACE}((\log n)^2)$, so also $\mathrm{NL} \subsetneq \mathrm{PSPACE}$. The space-constructibility hypothesis is needed: without it, the Borodin gap theorem gives functions $f$ with $\mathrm{DSPACE}(f(n)) = \mathrm{DSPACE}(2^{f(n)})$.

Going deeper

For a student

The space hierarchy is tighter than the time hierarchy, because simulating a machine costs only a constant factor in space but a logarithmic factor in time. It is one of the few unconditional separations of complexity classes. It shows that at least one of the inclusions $\mathrm{L} \subseteq \mathrm{P} \subseteq \mathrm{NP} \subseteq \mathrm{PSPACE}$ is strict, though it does not say which.