萨维奇定理

萨维奇定理（英語：Savitch's theorem）是计算复杂性理论中的一个定理，由沃尔特·萨维奇（英语：Walter Savitch）于1970年证明。定理的结论为对于任何函数${\displaystyle f(n)}$满足${\displaystyle f(n)\geq \log n}$，下列关系成立：

${\displaystyle {\text{NSPACE}}\left(f\left(n\right)\right)\subseteq {\text{DSPACE}}\left(\left(f\left(n\right)\right)^{2}\right).}$

亦即，如果一台非确定型图灵机能够利用${\displaystyle f(n)}$空间解决某个问题，那么一台确定型图灵机能够在至多${\displaystyle f^{2}(n)}$空间解决相同的问题。尽管非确定性的引入能够在时间上带来指数的提升，但是，这种引入对于空间而言作用有限。

萨维奇定理的证明是构造性的。证明过程为设计一个针对有向图连通性问题的算法（其它问题可以通过图灵机的格局图归约到此问题）。有向图连通问题可以简述为对于一个有向图和给定的两个顶点s和t，是否存在从s到t的有向路径。对于n个顶点，存在一个算法在${\displaystyle {\mbox{O}}\left((\log {n})^{2}\right)}$空间内解决这一问题。这一算法的基本思路是利用递归解决一个更一般化的问题：检查是否存在从s到t的一条至多包含k条边的有向路径，k是递归的输入参数。原始的有向图连通问题当${\displaystyle k=n}$时与此问题等价。为了测试是否存在一条从s到t的长度为k的有向边，可以测试是否存在一条从s到t的以u为中点的有向边。如果存在，那么对从s到u和从u到t递归此算法。

用伪代码表示如下（Python语法）：

def k-edge-path(s,t,k):
    if k == 0:
        return s == t
    else if k == 1:
        return (s,t) in edges
    else for u in vertices:
        if k-edge-path(s,u,⌊k/2⌋) and k-edge-path(u,t,⌈k/2⌉):
            return true
    return false

这一递归过程的递归深度为${\displaystyle O(\log n)}$层，每层需要${\displaystyle {\mbox{O}}(\log {n})}$位来存储该层的函数参数和局部变量。因此，算法的总空间复杂度为${\displaystyle {\mbox{O}}\left((\log {n})^{2}\right)}$。上述算法尽管是使用高级语言进行描述，然而，相同的算法使用图灵机实现时所需要的空间上界在渐近意义下是等同的。

由于有向图连通性问题为NL完全问题，因而任意NL中的语言都在复杂度类${\displaystyle {\text{DSPACE}}\left(\left(\log n\right)^{2}\right)}$中（这一复杂度类也常常被写作L²）.

从萨维奇定理可以得到许多重要的推论：

• PSPACE = NPSPACE
  • 得出这一结论因为多项式函数的平方仍然是一个多项式。尽管对于空间，确定性类与非确定性类相等，但是一般认为，对于时间的确定性类P和非确定性类NP，这种关系不成立，尽管这一假设尚是一个悬而未决的问题。
• NL ⊆ L²
  • 直接规定定理结论中的${\displaystyle f(n)=\log n}$即可。

• 空间层次定理

• Michael Sipser（英语：Michael Sipser）. Introduction to the Theory of Computation. PWS Publishing. 1997. ISBN 0-534-94728-X.  Section 8.1: Savitch's Theorem, pp.279–281.
• Christos Papadimitriou. Computational Complexity 1st edition. Addison Wesley. 1993. ISBN 0-201-53082-1.  引文格式1维护：冗余文本 (link) Pages 149–150 of section 7.3: The Reachability Method.
• W.J.Savitch, "Relationship between nondeterministic and deterministic tape classes", Journal of Computer and System Sciences, 4, pp 177–192, 1970

• Lance Fortnow, Foundations of Complexity, Lesson 18: Savitch's Theorem （页面存档备份，存于互联网档案馆）. 访问于2009年9月9日.
• Richard Lipton（英语：Richard Lipton）, Savitch’s Theorem （页面存档备份，存于互联网档案馆）. 这篇文章从历史的角度介绍了这一定理的证明是如何被发现的.