In computational complexity theory, the Immerman–Szelepcsényi theorem states that nondeterministic space complexity classes are closed under complementation. It was proven independently by Neil Immerman and Róbert Szelepcsényi in 1987, for which they shared the 1995 Gödel Prize. In its general form the theorem states that NSPACE = co-NSPACE for any function s ≥ log n. The result is equivalently stated as NL = co-NL; although this is the special case when s = log n, it implies the general theorem by a standard padding argument. The result solved the second LBA problem. In other words, if a nondeterministic machine can solve a problem, another machine with the same resource bounds can solve its complement problem in the same asymptotic amount of space. No similar result is known for the time complexity classes, and indeed it is conjectured that NP is not equal toco-NP. The principle used to prove the theorem has become known as inductive counting. It has also been used to prove other theorems in computational complexity, including the closure of LOGCFL under complementation and the existence of error-free randomized logspace algorithms for USTCON.
Proof sketch
The theorem can be proven by showing how to translate any nondeterministic Turing machineM into another nondeterministic Turing machine that solves the complementary decision problem under O of the same space constraints, plus a constant number of pointers and counters, which needs only a logarithmic amount of space. The idea is to simulate all the configurations of M, and to check if any configuration is accepting. This can be done in NSPACE of the same magnitude, but needs also a constant number of pointers and counters to keep track of the configurations. If no configuration is accepting, the simulating Turing machine accepts the input; thus it accepts if and only if M has no accepting path. This idea is elaborated in what follows for logarithmic NSPACE ; generalization to larger NSPACE is straightforward, but can also be proven by padding. The states of M can be thought of as the vertices of a directed graph, and the transitions of M can be thought of as edges in this graph. M accepts an input string whenever there exists a path in this graph from the vertex that represents the starting state to a special vertex that represents any accepting state. In this way, the existence of an accepting nondeterministic computation for M can be seen as a version of the -connectivity problem, for implicit graphs rather than graphs given explicitly as an explicitly-represented input graph. In this graphical view, the goal of the proof is to find a nondeterministic logspace algorithm that accepts only when there does not exist a path from to in the same implicit graph. An algorithm that solves this non-reachability problem can be based on the principle of counting, for each number from 1 to , the number of vertices reachable from by paths of length at most. If, at any stage of the algorithm, the correct value of is known for some value of, then it is possible to test whether a given vertex is reachable from by paths of length at most, using the following subroutine:
If, return true
Initialize a counter to 0
For each vertex in the implicit graph, repeat the following steps:
*Nondeterministically search for a path of length at most from to
*If a path to is found, increment and test whether there exists an edge from to
If, halt the algorithm and reject the input. Otherwise, return true if an edge from to was found, and false otherwise.
When used within a larger nondeterministic algorithm, the only accepting computations of the algorithm can be ones in which the subroutine finds paths to all the reachable vertices and computes the correct answer, so this subroutine can be used as if it were deterministic. With it in hand, the algorithm for testing non-reachability of t from s can be expressed by the following steps:
Initialize to 0 and to 1
Repeat the following steps times:
* // =#vertices reachable within steps
*Initialize a counter to 0
*For each vertex test whether is reachable from within steps, and if so increment
*Increment and set to
Test whether is reachable from within steps, and reject the input if it is.
Otherwise, if equals, accept the input.
The algorithm only needs to maintain representations of a constant number of counters and vertices in its memory, so it uses logarithmic space. By applying this algorithm to the implicit graph constructed from a given nondeterministic machine M, one obtains a nondeterministic machine for the complementary language to the one accepted by M.
Logspace hierarchy
As a corollary, in the same article, Immerman proved that, using descriptive complexity's equality between NL and FO, the logarithmic hierarchy, i.e. the languages decided by an alternating Turing machine in logarithmic space with a bounded number of alternation, is the same class as NL.