形式陈述

若 $s_1,s_2$$s_1,s_2$ 是空间可构造函数，且 $s_1(n)=o(s_2(n))$$s_1(n)=o(s_2(n))$、$s_2(n)\ge\log n$$s_2(n)\ge \log n$，则 $\mathrm{DSPACE}(s_1)\subsetneq\mathrm{DSPACE}(s_2)$$\mathrm{DSPACE}(s_1)⊊\mathrm{DSPACE}(s_2)$。常见表述还要求比例差足以容纳通用模拟和对角化。证明构造一台在 $s_2$$s_2$ 空间内模拟第 $i$$i$ 台小空间机器并翻转其答案的机器；空间可构造性用于精确划出可用带区。非确定空间也有相应层级版本。

直觉

给机器更多可构造工作空间确实会增加可判定能力：新机器可以列举所有较小空间程序，并在与自身编号对应的输入上故意不同。

例子与边界

由定理可得 $L\subsetneq PSPACE$$L⊊PSPACE$，因为对数空间远小于某个多项式空间界；更精确地存在语言位于 $\mathrm{DSPACE}(n)$$\mathrm{DSPACE}(n)$ 而不在 $\mathrm{DSPACE}(\log n)$$\mathrm{DSPACE}(\log n)$。定理不能直接证明具体自然问题的分离，只保证某个对角语言存在。若空间函数不可构造，机器未必能知道何时越界，对角化可能失效。Big-O 类之间必须有渐近间隙，不能从同阶函数推出严格包含。

推论与应用

空间层级定理证明空间复杂性不是人为记账：随着内存上界增长，语言类严格扩张，并为 L、PSPACE 及更高空间类提供无条件分离。

参考资料

• Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009，Chs. 1–8。
• Michael Sipser, Introduction to the Theory of Computation, 3rd ed., Cengage, 2013，Chs. 0–10。