Immerman-Szelepcsényi定理

这个定理可以通过演示如何在当程序执行次数n趋近于无穷大时的空间复杂度前提下，将任意非确定性图灵机“M”转换成在相同空间复杂度约束下，尝试解决互补决策问题的，带有恒定数量的指针和计数器的另外一个非确定性图灵机这一过程来得到证明其仅需要对数级的空间。

证明的具体过程是通过模拟非确定性图灵机“M”的所有配置，并检测其任意配置是否可以被识别确认。这个证明过程可以在相同量级的NSPACE中完成，但同样是需要恒定数量的指针和计数器来跟踪标记其配置。如果没有配置被识别确认，正进行模拟的图灵机接收输入内容；因此，当且仅当非确定性图灵机“M”没有可进行识别确认的路径时，它才开始进行接收。这一想法在接下来的对数级别NSPACE (NL)算法中得到了详细描述；虽然推广到更大量级的NSPACE后定理表达式变得简单直白，但仍可以通过引入填充参数来得到证明。

非确定性图灵机M的运行状态(通过其磁头在输入磁带上的位置和log级别空间的内存储器的配置来定义)可以被认为是有向图的顶点，非确定性图灵机M的转换可以被认为是该有向图中的边。每当图中存在从表示起始状态的顶点s到表示任何识别确认状态的特殊顶点t的路径时，M接收输入字符串。以这种方式，对于非确定性图灵机M而言判断是否存在非确定性识别计算的问题，可以被看做为一种在隐式图中而不是明确指明输入图像的显性图内是否存在从顶点s到顶点t的路径的问题。在这个可视化视图中，证明的目标是找到一个logspace类型的非确定性算法，该算法当且仅当在同一隐式图中不存在从顶点s到t的路径时才接收输入内容。

解决这种不可达路径问题的算法可以基于计数的原理:对于从1到n(隐式图的顺序编号)的每个数i，从顶点s出发，其可到达的r个顶点中路径长度最大为i。在算法的运行期间，如果已知r的值为某一数值i，则可以使用以下子程序来测试在给定某一顶点v前提下是否可以从顶点s出发通过长度最多为i + 1的路径到达:

1. 如果v = s，返回结果true
2. 将计数器c初始化为0
3. 对于隐式图中的每个顶点u，重复以下步骤:
   • 非确定性地搜索一条从s到u的路径，其路径长度最大为i
   • 如果搜索到一条满足条件的路径，计数器c=c+1，并尝试搜索一条从u到v的边
4. 如果c ≠ r，停止算法并拒绝输入。如果c = r，当存在一条从u到v的边时返回结果true，否则返回结果false。

当在较大的非确定性算法中使用时，该算法唯一可接受的内容是子程序找到所有可到达顶点的路径并计算出正确答案，因此该子程序在实际运行过程中可以表现得像是带有确定性特征。有了该算法后，测试顶点s是否不可到达顶点t的算法可以通过以下步骤来实现：

1. 将i初始化为0，r初始化为1
2. 重复以下步骤n-2次:
   • //令r = 路径长度i内可到达的顶点数量
   • 将计数器d初始化为0
   • 对于每个顶点v，测试从顶点s出发到达任意顶点v的路径长度是否可以≤ i + 1，如果满足条件，d=d+1
   • i=i+1并令r=d
3. 测试从顶点s出发到达顶点t的路径长度是否可以≤ i + 1，如果满足条件，则拒绝输入。
4. 否则，如果i + 1=n，接受输入。

该算法只需要在其内存中保证存储连续增长的计数器和顶点，因此它仅使用对数级别的空间。通过将该算法应用于由给定的非确定性机器M构造的隐式图中，可以获得与该机器所接受的语言互补的非确定性机器。

作为Immerman–Szelepcsényi定理的一个推论，在同一篇文章中，Immerman利用NL和FO(传递闭包)之间的可描述性复杂度等式，证明了对数级别空间层次，即在对数级别空间中由交替次数受限的交替式图灵机决定的语言，和NL是同一类别。