形式陈述

若 $s(n)\ge\log n$$s(n)\ge \log n$ 是空间可构造函数，则

$$ \operatorname{NSPACE}(s(n)) \subseteq \operatorname{DSPACE}(s(n)^2). $$$$\mathrm{NSPACE}(s(n))\subseteq \mathrm{DSPACE}(s(n{)}^2).$$

证明把非确定机器的配置图可达性改写为递归谓词 $\operatorname{Reach}(u,v,\ell)$$\mathrm{Reach}(u,v,\ell )$：枚举中点 $m$$m$，递归检查 $u$$u$ 到 $m$$m$、$m$$m$ 到 $v$$v$ 是否各能在至多一半步数内到达。配置数至多 $2^{O(s)}$$2^{O(s)}$，递归深度 $O(s)$$O(s)$，每层保存 $O(s)$$O(s)$ 位配置和枚举状态，总空间 $O(s^2)$$O(s^2)$；时间通常指数级。

直觉

不保存整条非确定路径，而是用“是否存在中点”把长路径不断二分。深度优先复用递归空间，以巨大时间换取平方空间。

例子与边界

取 $s(n)=\log n$$s(n)=\log n$ 得 $\mathrm{NL}\subseteq\mathrm{DSPACE}(\log^2 n)$$\mathrm{NL}\subseteq \mathrm{DSPACE}({\log }^{2}n)$；对多项式空间取并，得到 $\mathrm{NPSPACE}=\mathrm{PSPACE}$$\mathrm{NPSPACE}=\mathrm{PSPACE}$。定理不推出 $\mathrm L=\mathrm{NL}$$\mathrm{L}=\mathrm{NL}$，因为 $\log^2 n$${\log }^{2}n$ 仍大于 $\log n$$\log n$；也没有给出相似的多项式时间去非确定化结论。

推论与应用

Savitch 定理说明空间非确定性的收益至多平方，并成为 PSPACE 闭合、完全问题和交替计算关系的基础。其递归可达算法也是“隐式指数图上用小空间搜索”的典型范式。

参考资料

• Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009，Ch. 4, Savitch theorem and configuration reachability。
• Michael Sipser, Introduction to the Theory of Computation, 3rd ed., Cengage, 2013，Ch. 8, Savitch theorem。