查看“︁萨维奇定理”︁的源代码

'''萨维奇定理'''（{{Lang-en|Savitch's theorem}}）是[[计算复杂性理论]]中的一个[[定理]]，由{{le|沃尔特·萨维奇|Walter Savitch}}于1970年证明。定理的结论为对于任何函数<math>f(n)</math>满足<math>f(n)\geq \log n</math>，下列关系成立：
  
:<math>\text{NSPACE}\left(f\left(n\right)\right) \subseteq \text{DSPACE}\left(\left(f\left(n\right)\right)^2\right).</math>

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

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

用[[伪代码]]表示如下（[[Python]]语法）：
<syntaxhighlight lang="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
</syntaxhighlight>
这一递归过程的递归深度为<math>O(\log n)</math>层，每层需要<math>\mbox{O}(\log{n})</math>位来存储该层的函数参数和局部变量。因此，算法的总空间复杂度为<math>\mbox{O}\left((\log{n})^2\right)</math>。上述算法尽管是使用[[高级语言]]进行描述，然而，相同的算法使用[[图灵机]]实现时所需要的空间上界在渐近意义下是等同的。

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

== 推论 ==
从萨维奇定理可以得到许多重要的推论：
* [[PSPACE]] = [[NPSPACE]]
** 得出这一结论因为多项式函数的平方仍然是一个多项式。尽管对于空间，确定性类与非确定性类相等，但是一般认为，对于时间的确定性类[[P (复杂度)|P]]和非确定性类[[NP (复杂度)|NP]]，这种关系不成立，尽管这一假设尚是一个[[P/NP问题|悬而未决的问题]]。
* [[NL (复杂度)|NL]] ⊆ [[L (复杂度)|L]]<sup>2</sup>
** 直接规定定理结论中的<math>f(n)= \log n</math>即可。

== 参见 ==
* [[空间层次定理]]

== 参考资料 ==
* {{cite book|author = {{le|Michael Sipser}} | year = 1997 | title = Introduction to the Theory of Computation |url = https://archive.org/details/introductiontoth00sips| publisher = PWS Publishing | isbn = 0-534-94728-X}} Section 8.1: Savitch's Theorem, pp.279–281.
* {{cite book|author = [[赫里斯托斯·帕帕季米特里乌|Christos Papadimitriou]] | year = 1993 | title = Computational Complexity | publisher = Addison Wesley | edition = 1st edition | isbn = 0-201-53082-1}} 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, ''[http://blog.computationalcomplexity.org/2003/05/foundations-of-complexity-lesson-18.html Foundations of Complexity, Lesson 18: Savitch's Theorem] {{Wayback|url=http://blog.computationalcomplexity.org/2003/05/foundations-of-complexity-lesson-18.html |date=20090518112319 }}''. 访问于2009年9月9日.
* {{le|Richard Lipton}}, ''[http://rjlipton.wordpress.com/2009/04/05/savitchs-theorem/ Savitch’s Theorem] {{Wayback|url=http://rjlipton.wordpress.com/2009/04/05/savitchs-theorem/ |date=20090408071348 }}''. 这篇文章从历史的角度介绍了这一定理的证明是如何被发现的.

[[Category:计算复杂性理论]]
[[Category:数学定理|S]]
[[Category:結構複雜度理論]]