PSPACE ⊆ EXP — proof internals

⚠️ Unreviewed by Bolton

A space-bounded machine has only exponentially many configurations, and a deterministic run visits each at most once before halting, so its halting time is bounded by that count. The machine is unchanged: only the time bound is new.

The counting needs one invariant the space predicate does not state. Cfg.WithinDecisionSpace bounds head positions, not tape contents; but a head that never leaves [0, S] can never write outside it, so every cell beyond the window still holds its initial blank. Windowed records that, and Windowed.step propagates it.

theorem Complexity.Windowed.step {k : ℕ} {tm : TM k} {x : List Bool} {S : ℕ} {c c' : Cfg k tm.Q} (hw : Windowed x S c) (hstep : tm.step c = some c') (hspace : c.WithinDecisionSpace x.length S) : Windowed x S c'

A step of a machine whose heads stay inside the window preserves the invariant.

Counting the configurations inside the window

A halting deterministic run is short

The deterministic iteration TM.runCfg and its algebra come from Complexitylib.Classes.P.Cobham.Internal.Simulate, where the Cobham simulation already needed them.

theorem Complexity.TM.reaches_runCfg {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) (n : ℕ) : tm.reaches c (tm.runCfg c n)

Every configuration of a run is reachable.

theorem Complexity.TM.runCfg_periodic {k : ℕ} (tm : TM k) (c₀ : Cfg k tm.Q) {i d : ℕ} (h : tm.runCfg c₀ i = tm.runCfg c₀ (i + d)) (r : ℕ) : tm.runCfg c₀ (i + r) = tm.runCfg c₀ (i + d + r)

Once a configuration repeats, the run is periodic from that point on.

theorem Complexity.TM.repeat_contradiction {k : ℕ} (tm : TM k) (c₀ : Cfg k tm.Q) {t : ℕ} (hmin : ∀ s < t, ¬tm.halted (tm.runCfg c₀ s)) (hhalt : tm.halted (tm.runCfg c₀ t)) {a b : ℕ} (hb : b ≤ t) (hlt : a < b) (hab : tm.runCfg c₀ a = tm.runCfg c₀ b) : False

A repeat before the first halt is impossible: periodicity would pull a halted configuration back before time t.

theorem Complexity.TM.runCfg_injective_before_halt {k : ℕ} (tm : TM k) (c₀ : Cfg k tm.Q) {t : ℕ} (hmin : ∀ s < t, ¬tm.halted (tm.runCfg c₀ s)) (hhalt : tm.halted (tm.runCfg c₀ t)) : Function.Injective fun (i : Fin (t + 1)) => tm.runCfg c₀ ↑i

Before the first halt, the configurations of a deterministic run are pairwise distinct.

From a space bound to a time bound

theorem Complexity.TM.exists_reachesIn {k : ℕ} {tm : TM k} {c c' : Cfg k tm.Q} (h : tm.reaches c c') : ∃ (t : ℕ), tm.reachesIn t c c'

Reachability gives a step count.

theorem Complexity.TM.reachesIn_runCfg {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) (t : ℕ) : (∀ s < t, ¬tm.halted (tm.runCfg c s)) → tm.reachesIn t c (tm.runCfg c t)

Before the first halt, the run is a genuine reachesIn run.

theorem Complexity.TM.windowed_runCfg {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInSpace L f) (x : List Bool) (n : ℕ) : Windowed x (f x.length) (tm.runCfg (tm.initCfg x) n)

Every configuration of a run from the initial configuration is windowed.

def Complexity.TM.spaceTimeBound {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : ℕ

The exponential configuration bound of a space-f machine.

Equations

• tm.spaceTimeBound f n = Fintype.card tm.Q * ((n + f n + 2) * (((f n + 1) * 4 ^ (f n + 1)) ^ k * ((f n + 2) * 4 ^ (f n + 2))))

theorem Complexity.TM.halt_time_le {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInSpace L f) (x : List Bool) {t : ℕ} (hmin : ∀ s < t, ¬tm.halted (tm.runCfg (tm.initCfg x) s)) (hhalt : tm.halted (tm.runCfg (tm.initCfg x) t)) : t < tm.spaceTimeBound f x.length

A space-bounded machine halts within its configuration count.

theorem Complexity.TM.spaceTimeBound_le_two_pow {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : tm.spaceTimeBound f n ≤ 2 ^ (Fintype.card tm.Q + (n + f n + 2) + 3 * k * (f n + 1) + 3 * (f n + 2))

The configuration count is at most exponential in the space bound.

noncomputable def Complexity.TM.boundExp {k : ℕ} (tm : TM k) (p : Polynomial ℕ) : Polynomial ℕ

A polynomial dominating the exponent of the configuration count.

Equations

• tm.boundExp p = Polynomial.C (Fintype.card tm.Q) + (Polynomial.X + p + Polynomial.C 2) + Polynomial.C (3 * k) * (p + 1) + Polynomial.C 3 * (p + Polynomial.C 2)

theorem Complexity.TM.spaceTimeBound_le_two_pow_poly {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (p : Polynomial ℕ) (hf : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) (n : ℕ) : tm.spaceTimeBound f n ≤ 2 ^ Polynomial.eval n (tm.boundExp p)

The configuration count is at most 2 to a polynomial.

The time bound

theorem Complexity.TM.decidesInTime_of_decidesInSpace {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInSpace L f) : tm.DecidesInTime L (tm.spaceTimeBound f)

A space-bounded decider is a time-bounded decider, with no change of machine: the run halts by the time it would have to repeat a configuration.

theorem Complexity.TM.eval_le_pow_succ (q : Polynomial ℕ) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Polynomial.eval n q ≤ n ^ (q.natDegree + 1)

A polynomial is eventually dominated by the next power.

theorem Complexity.TM.spaceTimeBound_bigO {k : ℕ} {tm : TM k} {f : ℕ → ℕ} {m : ℕ} (hf : BigO f fun (x : ℕ) => x ^ m) : ∃ (j : ℕ), BigO (tm.spaceTimeBound f) fun (n : ℕ) => 2 ^ n ^ j

The configuration count is exponential.

theorem Complexity.PSPACE_subset_EXP_internal : PSPACE ⊆ EXP

PSPACE ⊆ EXP. A polynomial-space decider halts within its configuration count, which is exponential, so the same machine is an exponential-time decider.