PSPACE is closed under complement

⚠️ Unreviewed by Bolton

TM.complementTM already flips a decider's verdict, and TM.complementTM_decidesInTime accounts for its time. The space account is what PH ⊆ PSPACE needs, and it is not immediate: the space predicate constrains every reachable configuration, so it is not enough to know where the machine ends up — one has to know that no configuration along the way strays outside the window.

The complement machine has three phases. In the first it simulates the source machine, so every configuration it meets is an embedded reachable configuration of that machine and inherits its bound. In the other two it idles every tape except the output, whose head it walks left to the marker and then one cell right. The one lemma that makes the accounting work is that an idle move on a tape carrying its left marker sends the head to max head 1 — it bounces off cell 0 and otherwise stands still — so no head can drift outward however long the rewind takes. One extra cell therefore covers the whole construction.

The head-bounce lemmas it uses are shared with the loop combinator and live in Complexitylib.Models.TuringMachine.Combinators.Internal.IdleHeads.

Main definitions

• TM.CompInv — the invariant carried along a run of the complement machine

Main results

• TM.complement_head_bound — after the simulation, no head passes max head 1
• TM.complementTM_withinDecisionSpace — every reachable configuration stays in the window
• TM.complementTM_decidesInSpace — the complement is decided in space S + 1
• DSPACE_compl — a space class with room for one more cell is closed under complement
• PSPACE_compl — PSPACE is closed under complement

theorem Complexity.TM.complement_head_bound {n : ℕ} (tm : TM n) {c c' : Cfg n tm.complementTM.Q} (hnotsim : ∀ (q : tm.Q), c.state = Sum.inl q → q = tm.qhalt) (hstep : tm.complementTM.step c = some c') (hinp : c.input.StartInvariant) (hwork : ∀ (i : Fin n), (c.work i).StartInvariant) (hout : c.output.StartInvariant) : c'.input.head ≤ max c.input.head 1 ∧ (∀ (i : Fin n), (c'.work i).head ≤ max (c.work i).head 1) ∧ c'.output.head ≤ max c.output.head 1

After the simulation, the complement machine never grows a head beyond max head 1. Every phase idles the input and work tapes, and moves the output head right only when it is sitting on the left marker.

theorem Complexity.TM.complement_state_of_step {n : ℕ} (tm : TM n) {c c' : Cfg n tm.complementTM.Q} (hnotsim : ∀ (q : tm.Q), c.state = Sum.inl q → q = tm.qhalt) (hstep : tm.complementTM.step c = some c') : ∃ (ph : ComplementPhase), c'.state = Sum.inr ph

After the simulation phase the machine never returns to it.

def Complexity.TM.CompInv {n : ℕ} (tm : TM n) (x : List Bool) (s : ℕ) (c : Cfg n tm.complementTM.Q) : Prop

The invariant carried along a run of the complement machine: every tape keeps its left marker, the simulation phase only ever holds an embedded reachable configuration of the source machine, and every later phase respects the space bound with one cell to spare.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.CompInv.step {n : ℕ} {tm : TM n} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c c' : Cfg n tm.complementTM.Q} (hinv : tm.CompInv x (S x.length) c) (hstep : tm.complementTM.step c = some c') : tm.CompInv x (S x.length) c'

The invariant is preserved by a step.

theorem Complexity.TM.CompInv.init {n : ℕ} (tm : TM n) (x : List Bool) (s : ℕ) : tm.CompInv x s (tm.complementTM.initCfg x)

The invariant holds at the start of the run.

theorem Complexity.TM.CompInv.reaches {n : ℕ} {tm : TM n} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c : Cfg n tm.complementTM.Q} (h : tm.complementTM.reaches (tm.complementTM.initCfg x) c) : tm.CompInv x (S x.length) c

The invariant holds at every reachable configuration.

theorem Complexity.TM.complementTM_withinDecisionSpace {n : ℕ} {tm : TM n} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (x : List Bool) {c : Cfg n tm.complementTM.Q} (h : tm.complementTM.reaches (tm.complementTM.initCfg x) c) : c.WithinDecisionSpace x.length (S x.length + 1)

The complement machine respects the space bound with one cell to spare.

theorem Complexity.TM.complementTM_decidesInSpace {n : ℕ} {tm : TM n} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) : tm.complementTM.DecidesInSpace Lᶜ fun (m : ℕ) => S m + 1

The complement machine decides the complement, in one more cell of space.

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. The one 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.