Containments between time and space classes

TheoremFirst halting time is below the configuration-core bound#✓fully proved

The first halting time is smaller than the canonical bound on reachable cores.

theorem haltTime_lt_coreBound [Fintype Symbol] [Fintype State] {s T : ℕ}
    (hs : ∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s)
    (hT : tm.HaltsAt (tm.initCfg input) T) :
    T < (input.length + 2) * storageBound Symbol State k s

Used by 1

Used byHalting space-bounded runs obey the core-count time bound

TheoremHalting space-bounded runs obey the core-count time bound#✓fully proved

A halting, space-bounded run has an actual step bound.

theorem runsInTime_coreBound [Fintype Symbol] [Fintype State] {s : ℕ}
    (hs : ∀ t, tm.spaceUsed (tm.initCfg input) t ≤ s)
    (hh : ∃ t, (tm.runFrom (tm.initCfg input) t).Halted) :
    tm.RunsInTime input ((input.length + 2) * storageBound Symbol State k s)

Uses 2 · Used by 1

Proof usesFirst halting time is below the configuration-core bound · Halting persists along a run

Used byExponential time bound from a space bound and halting

TheoremExponential time bound from a space bound and halting#✓fully proved

Exponential time from a visited-cell space bound and a halting run.

theorem runsInTime_exponential_of_space [Fintype Symbol] [Fintype State] {s : ℕ}
    (hs : tm.RunsInSpace input s)
    (hh : ∃ t, (tm.runFrom (tm.initCfg input) t).Halted) :
    tm.RunsInTime input ((input.length + 2) * storageBoundBase Symbol State k *
      2 ^ (storageBoundExp Symbol k * s))

Uses 1 · Used by 1

Proof usesHalting space-bounded runs obey the core-count time bound

Used byUniform constants for the exponential time-from-space bound

TheoremUniform constants for the exponential time-from-space bound#✓fully proved

One pair of constants works for every input of the fixed machine.

theorem exists_exponential_time_bound [Finite Symbol] [Finite State]
    (tm : MultiTapeTM k Symbol State) :
    ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ), tm.RunsInSpace input s →
      (∃ t, (tm.runFrom (tm.initCfg input) t).Halted) →
      tm.RunsInTime input ((input.length + 2) * a * 2 ^ (c * s))

Uses 1 · Used by 1

Proof usesExponential time bound from a space bound and halting

Used byPolynomial-space decider runs in exponential time

TheoremPolynomial-space decider runs in exponential time#✓fully proved

The same finite polynomial-space decider has an exponential time bound. All constants precede every input. Halting comes from Decides, not space.

theorem SpaceBoundedBy.exists_exponential_timeBoundedBy
    {k : ℕ} {State : Type*} [Finite State]
    {tm : MultiTapeTM k Bool State} {L : Set (List Bool)} {c₁ c₂ d : ℕ}
    (hs : SpaceBoundedBy tm (fun n => c₁ * n ^ d + c₂))
    (hd : Decides tm L) :
    ∃ D A B : ℕ, TimeBoundedBy tm (fun n => A * 2 ^ (n ^ D) + B)

Uses 4 · Used by 1

Statement usesA multi-tape machine deciding a language · Space-bounded multi-tape machine · Time-bounded multi-tape machine

Proof usesUniform constants for the exponential time-from-space bound

Used byPSPACE is contained in EXP

TheoremPSPACE is contained in EXP#✓fully proved

Every canonical polynomial-space language is in exponential time, using its original finite multi-tape decider.

theorem pspace_subset_exp : PSPACE ⊆ EXP

Sources

• S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009, Chapter 4 (Space complexity).

Uses 12

Statement usesThe class EXP · Polynomial space for decision problems · Complexity classes · Decision problems

Proof usesLanguage of a decision problem · Deterministic space classes on multi-tape machines · Deterministic time classes on multi-tape machines · A multi-tape machine deciding a language · Space-bounded multi-tape machine · Polynomial-space decider runs in exponential time · Time-bounded multi-tape machine · Decidability within time and space bounds, unfolded

TheoremNEXP is contained in EXPSPACE#●ready to prove

Every decision problem in NEXP, the class of nondeterministic exponential time, also belongs to EXPSPACE, the class of deterministic exponential space.

public theorem_wanted nexp_subset_expspace :
    NEXP ⊆ EXPSPACE

Sources

• S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009 (NEXP ⊆ EXPSPACE by exhaustive simulation).

Uses 4

Statement usesThe class EXPSPACE · The complexity class NEXP · Complexity classes · Decision problems

TheoremNL is contained in P#●ready to prove

Every decision problem in NL, the class of nondeterministic logarithmic space, also belongs to P, the class of decision problems computable in deterministic polynomial time.

public theorem_wanted nl_subset_p :
    NL ⊆ MetaMathlibExt.ComplexityTheory.P

Sources

• S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 4.14 (NL ⊆ P); C. H. Papadimitriou, Computational Complexity, 1994.

Uses 4

Statement usesThe complexity class NL · Complexity classes · Decision problems · The complexity class P

TheoremNP is contained in PSPACE#●ready to prove

Every decision problem in NP also belongs to PSPACE, the class of decision problems decidable in polynomial space.

public theorem_wanted np_subset_pspace :
    MetaMathlibExt.ComplexityTheory.NP ⊆ PSPACE

Sources

• S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009, Theorem 4.14 (NP ⊆ PSPACE); C. H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994, Theorem 7.2.

Uses 4

Statement usesPolynomial space for decision problems · Complexity classes · Decision problems · The complexity class NP

6 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.