形式陈述

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

$$\mathrm{NSPACE}(s(n))=\mathrm{coNSPACE}(s(n)).$$

取 $s(n)=\log n$ 即得

$$\mathrm{NL}=\mathrm{coNL}.$$

证明的核心是归纳计数：在配置图中逐层计算从起点可达的配置数；一旦某层的精确计数得到认证，就能非确定性地证明目标配置没有来自上一层可达集合的边，从而认证“不可达”。计数器与当前配置都只需 $O(s(n))$ 空间。

直觉

非确定性通常容易证明“存在一条路径”，却不容易证明“不存在路径”。定理通过给整个可达集合计数，把全称式的不可达声明改造成可逐项核验的非确定性证书。

例子与边界

有向 $s$–$t$ 不可达性因此属于 NL，尽管直接交换可达性算法的接受、拒绝状态并不正确。定理证明的是空间类的补闭包，不推出 $\mathrm{L}=\mathrm{NL}$，也没有对应的已知结论 $\mathrm{NP}=\mathrm{coNP}$。

推论与应用

NL 完全问题的补问题仍是 NL 完全问题；在低空间归约下，可达性与不可达性可以在同一复杂度类内相互使用。该定理也补齐了 Savitch 定理只给出确定性平方空间模拟、未给出同空间补闭包的一侧。

参考资料

• Neil Immerman, “Nondeterministic Space is Closed Under Complementation,” SIAM Journal on Computing 17(5), 1988，pp. 935–938。
• Róbert Szelepcsényi, “The Method of Forced Enumeration for Nondeterministic Automata,” Acta Informatica 26, 1988，pp. 279–284。