Native nondeterministic space complementation

Inductive counting constructs a new finite-state nondeterministic multi-tape machine for the complement of the language recognized by a machine within space c₁ * s n + c₂, for any bound s with Nat.log2 n ≤ s n. The construction first counts the input length, then scans compact configuration graphs of growing radices with the small-register controller, and compiles its binary choices and read-only input queries to native instructions. The radix grows only after a certified overflow, so no constructibility of s is needed [Imm88].

The output machine halts on every branch and obeys an every-prefix work-space bound. The source need only recognize its language: its branches may run forever. Input and write-only output are uncharged, exactly as in the existing native RunsInSpace convention.

Main results

• Turing.MultiTapeNTM.exists_decidesInSpace_compl: a native recognizer within space c₁ * s n + c₂ has an all-branches-halting native complement decider within space c * (s n + 1).

References

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

theorem Turing.MultiTapeNTM.exists_decidesInSpace_compl {α State : Type} {k c₁ c₂ : ℕ} [Finite State] {ntm : MultiTapeNTM k Bool State} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} (hA : ntm.RecognizesInSpace enc A fun (a : α) => c₁ * s (enc a).length + c₂) (hs : ∀ (n : ℕ), n.log2 ≤ s n) : ∃ (k' : ℕ) (State' : Type) (_ : Finite State') (ntm' : MultiTapeNTM k' Bool State') (c : ℕ), ntm'.DecidesInSpace enc Aᶜ fun (a : α) => c * (s (enc a).length + 1)

Immerman–Szelepcsényi, with native machines. Every language recognized within space c₁ * s n + c₂, for a bound with Nat.log2 n ≤ s n, has a complement decider within space c * (s n + 1) whose every branch halts. Both the input encoding and the original all-prefix work-space convention are preserved, and s need not be constructible [Imm88].