Class membership as an explicit polynomial bound

⚠️ Unreviewed by Bolton

Membership in PSPACE is stated asymptotically: some space function that is O(n^k). A machine under construction needs the opposite — a concrete polynomial it can be checked against, and a way to hand that polynomial back as a PSPACE membership when it is done. The two theorems here are that exchange, in both directions, and every space-bounded construction in this folder passes through them.

Main results

• exists_poly_window_of_mem_PSPACE — a PSPACE language with an explicit polynomial window
• mem_PSPACE_of_polyWindow — and the converse
• mem_P_of_polyTime — the time-domain counterpart, for P

theorem Complexity.exists_poly_window_of_mem_PSPACE {L : Language} (h : L ∈ PSPACE) : ∃ (k : ℕ) (tm : TM k) (q : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k tm.Q), tm.reaches (tm.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length q)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k tm.Q), tm.reaches (tm.initCfg x) c' ∧ tm.halted c' ∧ (x ∈ L → c'.output.cells 1 = Γ.one) ∧ (x ∉ L → c'.output.cells 1 = Γ.zero)

A PSPACE language comes with an explicit polynomial window. Membership in PSPACE only gives an asymptotic bound on some space function; a machine has to be handed a concrete polynomial, since the window it must respect is a function of the input length it can evaluate.

theorem Complexity.mem_PSPACE_of_polyWindow {L : Language} {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (hwin : ∀ (x : List Bool) (c' : Cfg k tm.Q), tm.reaches (tm.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length q)) (hdec : ∀ (x : List Bool), ∃ (c' : Cfg k tm.Q), tm.reaches (tm.initCfg x) c' ∧ tm.halted c' ∧ (x ∈ L → c'.output.cells 1 = Γ.one) ∧ (x ∉ L → c'.output.cells 1 = Γ.zero)) : L ∈ PSPACE

A machine with an explicit polynomial window decides a PSPACE language. The exact converse: together the two say that membership in PSPACE is the existence of a machine keeping a polynomial window, with no asymptotics left to manage.

theorem Complexity.mem_P_of_polyTime {L : Language} {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (hdec : tm.DecidesInTime L fun (n : ℕ) => Polynomial.eval n q) : L ∈ P

A machine with an explicit polynomial time bound decides a P language. The time-domain counterpart of mem_PSPACE_of_polyWindow: a construction hands back a concrete Polynomial ℕ and gets the class membership, with the asymptotics discharged here.