Deterministic space classes are closed under complement

A deterministic space-bounded decider is turned into a decider for the complement by running it, rewinding its output head to the verdict cell, and flipping the bit. The rewind only moves heads leftward or off the left marker, so it costs one extra cell of space. The machine and its space accounting are in Complexitylib.Classes.Containments.Internal.ComplementSpace.

Main results

• DSPACE_compl — DSPACE(S) is closed under complement whenever the constant 1 is O(S)
• PSPACE_compl — PSPACE is closed under complement

theorem Complexity.DSPACE_compl {L : Language} {S : ℕ → ℕ} (hone : BigO (fun (x : ℕ) => 1) S) (h : L ∈ DSPACE S) : Lᶜ ∈ DSPACE S

A space class with room for one more cell is closed under complement. If L ∈ DSPACE S and the constant function 1 is O(S), then Lᶜ ∈ DSPACE S: the complement machine uses space S + 1, and the extra cell is what the rewind to the verdict cell costs.

theorem Complexity.PSPACE_compl {L : Language} (h : L ∈ PSPACE) : Lᶜ ∈ PSPACE

PSPACE is closed under complement. The same machine runs, then rewinds its output head to the verdict cell and flips the bit; the rewind only moves heads leftward or off the left marker, so it costs one extra cell of space and no more.