Complementary nondeterministic logarithmic space

coNL enc consists of the complements of problems in the native machine class NL enc. It uses exactly the same encoding, every-prefix work-space measure and all-branches halting convention as NL.

NL is the nondeterministic space class of the bound Nat.log2 (Cslib.Complexity.NL_eq_NSPACE), so the Immerman–Szelepcsényi theorem for nondeterministic space (Cslib.Complexity.NSPACE_eq_coNSPACE) gives NL = coNL. Its source machine may even be a recognizer with nonterminating branches; the constructed machine halts on every branch.

Main definitions

• Cslib.Complexity.coNL: complements of nondeterministic logarithmic-space problems.

Main results

• Cslib.Complexity.mem_coNL: membership is membership of the complement in NL.
• Cslib.Complexity.compl_mem_coNL_iff: the corresponding double-complement equivalence.
• Cslib.Complexity.NL_eq_NSPACE: NL is NSPACE(log₂ n).
• Cslib.Complexity.compl_mem_NL: native nondeterministic logarithmic-space complement closure.
• Cslib.Complexity.NL_eq_coNL: the Immerman–Szelepcsényi theorem.
• Cslib.Complexity.mem_NL_of_recognizesInSpace: recognizers and deciders give the same class.

References

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

def Cslib.Complexity.coNL {α : Type} (enc : α ↪ List Bool) : Set (Set α)

The problems whose complements belong to native nondeterministic logarithmic space Sipser, Section 8.6.

theorem Cslib.Complexity.mem_coNL {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ coNL enc ↔ Aᶜ ∈ NL enc

A problem belongs to coNL exactly when its complement belongs to NL.

theorem Cslib.Complexity.compl_mem_coNL_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} : Aᶜ ∈ coNL enc ↔ A ∈ NL enc

Complementing a problem in NL gives a problem in coNL, and conversely.

theorem Cslib.Complexity.NL_eq_NSPACE {α : Type} {enc : α ↪ List Bool} : NL enc = NSPACE enc Nat.log2

NL is NSPACE(log₂ n): the bounds c * (log₂ n + 1) and c₁ * log₂ n + c₂ give the same problems.

theorem Cslib.Complexity.compl_mem_NL {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ NL enc) : Aᶜ ∈ NL enc

Native nondeterministic logarithmic space is closed under complement. The constructed machine halts on every branch and obeys the same input/output space convention.

theorem Cslib.Complexity.compl_mem_NL_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} : Aᶜ ∈ NL enc ↔ A ∈ NL enc

Complementation preserves membership in native nondeterministic logarithmic space.

theorem Cslib.Complexity.NL_eq_coNL {α : Type} {enc : α ↪ List Bool} : NL enc = coNL enc

NL = coNL, the Immerman–Szelepcsényi theorem for the library's native machines and arbitrary injective instance encodings: the case s = log₂ of Cslib.Complexity.NSPACE_eq_coNSPACE.

theorem Cslib.Complexity.mem_NL_of_recognizesInSpace {α : Type} {enc : α ↪ List Bool} {A : Set α} {k c : ℕ} {State : Type} [Finite State] {ntm : Turing.MultiTapeNTM k Bool State} (h : ntm.RecognizesInSpace enc A fun (a : α) => c * ((enc a).length.log2 + 1)) : A ∈ NL enc

A logarithmic-space recognizer, even with nonterminating branches, recognizes a problem decidable within logarithmic space with every branch halting.