Space hierarchy theorem

TheoremThere is a PSPACE language outside L (space-hierarchy separation)#●ready to prove

There is a decision problem that belongs to PSPACE but not to the class \(\mathsf{L}\) of decision problems decidable in deterministic logarithmic space.

public theorem_wanted l_ne_pspace :
    ∃ L : MetaMathlibExt.ComplexityTheory.DecisionProblem, L ∈ PSPACE ∧ L ∉ LogSpace

Sources

• R. W. Stearns, J. Hartmanis, and P. M. Lewis II, "Hierarchies of memory limited computations" (1965); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009.

Uses 4

Statement usesDeterministic logarithmic space · Polynomial space for decision problems · Complexity classes · Decision problems

TheoremDeterministic space hierarchy: quadratic versus linear space#●ready to prove

There is a language \(L\) of bitstrings that lies in \(\mathrm{DSPACE}(n^2)\) but not in \(\mathrm{DSPACE}(n)\), the deterministic space classes of multi-tape Turing machines for the space bounds \(n \mapsto n^2\) and \(n \mapsto n\).

public theorem_wanted space_hierarchy :
    ∃ L : Set (List Bool), L ∈ Cslib.Turing.MultiTapeTM.DSPACE (fun n => n ^ 2) ∧
      L ∉ Cslib.Turing.MultiTapeTM.DSPACE (fun n => n)

Sources

• R. W. Stearns, J. Hartmanis, and P. M. Lewis II, "Hierarchies of memory limited computations", Proceedings of the Sixth Annual Symposium on Switching Circuit Theory and Logical Design (1965), 179-190.

Uses 1

Statement usesDeterministic space classes on multi-tape machines

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.