Immerman–Szelepcsényi 定理

非确定性天然适合证明“存在路径”，而补问题“没有路径”似乎需要记住整个可达集合。定理的突破是给分层可达集合计数，并让错误计数无法产生接受分支；通过逐层验证精确数量，可把全称式的不可达声明改造成可逐项核验的非确定性证书，在极小空间内证实不可达。它表明空间受限非确定性对补运算比时间受限情形更对称。

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

对有 $N$ 个编号顶点的有向图，设 $R_i$ 是从 $s$ 在至多 $i$ 步内可达的集合。关键子程序不是猜一个“不在”的标记，而是使用已经正确的计数 $c_i=|R_i|$：按编号遍历全部顶点 $u$，每个顶点选择“列入”或“略过”；列入时必须逐步猜出并核验一条从 $s$ 到 $u$、长度至多 $i$ 的路径。只保存当前路径点和步数，不保存整条路径。最后要求列入总数恰为 $c_i$，否则拒绝这一分支。

通过检查的列举没有假阳性，又因计数精确而不可能漏掉 $R_i$ 中的顶点。因此在列举时同时记录“是否有 $u=v$ 或边 $u\to v$”，就准确决定 $v\in R_{i+1}$，包括原来已可达的顶点。对每个 $v$ 重新执行这次认证列举，累计肯定答案得到 $c_{i+1}$。从 $c_0=1$ 起归纳，每条未拒绝分支都保持计数正确；选择所有真实可达点及其见证路径，至少有一条分支能通过。

算到 $c_{N-1}$ 后再作一次认证列举，只有没有列入目标 $t$ 时才接受。索引 $i,u,v$、已知计数、当前计数及路径核验区总共只需 $O(\log N)$ 位，所有循环都有显式有限界。若 $t$ 可达，任何通过的列举都包含它；若不可达，正确列举提供接受分支。将这套程序用于非确定机器的隐式配置图时，取初始配置为起点，再添加唯一的新目标 $t_{\ast }$，并从每个接受配置向 $t_{\ast }$ 加一条边。于是 $t_{\ast }$ 可达当且仅当机器存在接受计算，不要求接受配置本来就唯一。增广图仍只有 $N=2^{O(s(n))}$ 个顶点，$\log N=O(s(n))$；合法配置、普通一步转移以及通往 $t_{\ast }$ 的接受状态检查都能在 $O(s(n))$ 空间内完成。对这个目标运行不可达性程序，才得到机器语言的补。这说明精确计数如何防止假不可达证书，而不把非确定猜测当作免费的全称检查。

简单地“猜 $t$ 不可达”没有可验证内容，枚举某些路径也不能证明没有遗漏。定理需要 $s(n)\ge \log n$ 以保存顶点索引和计数，并推广为 $NSPACE(s(n))=coNSPACE(s(n))$，不只是一条 NL 特例。

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

它直接给出 非确定对数空间类理路复杂度类 NLComplexity class NL · Nondeterministic logspace可在非确定性对数空间内判定的语言类。 的补封闭性，即 $\mathrm{NL}=\mathrm{coNL}$，并以 STCON理路STCON 的 NL 完全性NL-completeness of STCON · Directed reachability is NL-complete有向图可达性在确定性对数空间多一归约下是 NL 完全问题。 的补问题为核心。与 Savitch 定理理路Savitch 定理Savitch's theorem通过配置可达性的中点递归与工作区复用，把非确定空间 s 确定化为平方空间。 的确定化上界不同，这里保留非确定空间而完成补封闭；它也说明 非确定空间类理路非确定性空间复杂性类Nondeterministic space class · NSPACE由非确定性图灵机在给定空间界内判定的语言集合。 的结构不能照搬 NP 与 coNP 的直觉。