Nondeterministic space classes and their complements

Cslib.Complexity.NSPACE enc s consists of the problems that one finite-state binary nondeterministic multi-tape machine decides within space c₁ * s n + c₂, for constants c₁ and c₂, on instances whose encoding under enc has length n. As for Cslib.Complexity.NL, the space bound holds along every computation prefix, including rejecting branches; every branch halts, and on each input some finite time bounds all computation paths; the input tape is read-only and the output tape write-only. Cslib.Complexity.coNSPACE enc s consists of the complements of the problems in NSPACE enc s, under the same encoding.

The Immerman–Szelepcsényi theorem says that NSPACE(s) = coNSPACE(s) whenever log₂ n ≤ s n [Imm88] [Sze87] (Cslib.Complexity.NSPACE_eq_coNSPACE). No constructibility of s is assumed, following Immerman's remark after his Theorem 1: the standard space measure bounds every sequence of choices, so the space may be increased as needed. The complement machines come from Turing.MultiTapeNTM.exists_decidesInSpace_compl, which generalizes Erik Demaine's inductive-counting construction for logarithmic space.

Main definitions

• Cslib.Complexity.NSPACE: nondeterministic space classes.
• Cslib.Complexity.coNSPACE: their complements.

Main results

• Cslib.Complexity.NSPACE_mono_of_le_mul_add: NSPACE absorbs constant factors.
• Cslib.Complexity.NSPACE_mono, Cslib.Complexity.NSPACE_mono_of_eventually_le: monotonicity; only the eventual values of the bound matter.
• Cslib.Complexity.compl_mem_NSPACE_of_recognizesInSpace, Cslib.Complexity.compl_mem_NSPACE: closure under complement.
• Cslib.Complexity.mem_NSPACE_of_recognizesInSpace: recognizers and deciders give the same class.
• Cslib.Complexity.NSPACE_eq_coNSPACE: the Immerman–Szelepcsényi theorem.

References

• N. Immerman, Nondeterministic Space Is Closed under Complementation, Theorem 1
• R. Szelepcsényi, The Method of Forcing for Nondeterministic Automata
• M. Sipser, Introduction to the Theory of Computation, Section 8.6

def Cslib.Complexity.NSPACE {α : Type} (enc : α ↪ List Bool) (s : ℕ → ℕ) : Set (Set α)

The problems decided within space O(s n), that is c₁ * s n + c₂, by one finite-state binary nondeterministic machine, along every computation prefix and with every branch halting, on instances whose encoding under enc has length n.

def Cslib.Complexity.coNSPACE {α : Type} (enc : α ↪ List Bool) (s : ℕ → ℕ) : Set (Set α)

The complements of the problems in NSPACE enc s, with the same encoding.

theorem Cslib.Complexity.mem_coNSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} : A ∈ coNSPACE enc s ↔ Aᶜ ∈ NSPACE enc s

A problem belongs to coNSPACE exactly when its complement belongs to NSPACE.

theorem Cslib.Complexity.NSPACE_mono_of_le_mul_add {α : Type} {enc : α ↪ List Bool} {s₁ s₂ : ℕ → ℕ} {C : ℕ} (h : ∀ (n : ℕ), s₁ n ≤ C * s₂ n + C) : NSPACE enc s₁ ⊆ NSPACE enc s₂

NSPACE absorbs constant factors: a bound s₁ n ≤ C * s₂ n + C puts NSPACE enc s₁ inside NSPACE enc s₂.

theorem Cslib.Complexity.NSPACE_mono {α : Type} {enc : α ↪ List Bool} {s₁ s₂ : ℕ → ℕ} (h : ∀ (n : ℕ), s₁ n ≤ s₂ n) : NSPACE enc s₁ ⊆ NSPACE enc s₂

NSPACE is monotone in the space bound.

theorem Cslib.Complexity.NSPACE_mono_of_eventually_le {α : Type} {enc : α ↪ List Bool} {s₁ s₂ : ℕ → ℕ} (h : ∀ᶠ (n : ℕ) in Filter.atTop, s₁ n ≤ s₂ n) : NSPACE enc s₁ ⊆ NSPACE enc s₂

NSPACE only depends on the space bound eventually: the finitely many other values are absorbed by the additive constant.

theorem Cslib.Complexity.compl_mem_NSPACE_of_recognizesInSpace {α : Type} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} (hs : ∀ (n : ℕ), n.log2 ≤ s n) {k c₁ c₂ : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} (h : ntm.RecognizesInSpace enc A fun (a : α) => c₁ * s (enc a).length + c₂) : Aᶜ ∈ NSPACE enc s

The complement of a problem recognized within space O(s) is decided within space O(s), every branch halting, when log₂ n ≤ s n. The recognizer's branches may run forever.

theorem Cslib.Complexity.compl_mem_NSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} (hs : ∀ (n : ℕ), n.log2 ≤ s n) (h : A ∈ NSPACE enc s) : Aᶜ ∈ NSPACE enc s

Nondeterministic space is closed under complement, when log₂ n ≤ s n.

theorem Cslib.Complexity.mem_NSPACE_of_recognizesInSpace {α : Type} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} (hs : ∀ (n : ℕ), n.log2 ≤ s n) {k c₁ c₂ : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} (h : ntm.RecognizesInSpace enc A fun (a : α) => c₁ * s (enc a).length + c₂) : A ∈ NSPACE enc s

A recognizer within space O(s) gives a decider, every branch halting, when log₂ n ≤ s n. Its branches may run forever.

theorem Cslib.Complexity.compl_mem_NSPACE_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} (hs : ∀ (n : ℕ), n.log2 ≤ s n) : Aᶜ ∈ NSPACE enc s ↔ A ∈ NSPACE enc s

Complementation preserves membership in nondeterministic space.

theorem Cslib.Complexity.NSPACE_eq_coNSPACE {α : Type} {enc : α ↪ List Bool} {s : ℕ → ℕ} (hs : ∀ (n : ℕ), n.log2 ≤ s n) : NSPACE enc s = coNSPACE enc s

The Immerman–Szelepcsényi theorem: NSPACE(s) = coNSPACE(s) for every bound with log₂ n ≤ s n, constructible or not Immerman, Theorem 1, for the library's native machines and arbitrary injective instance encodings.