Base space complexity classes

This file defines the parametric space complexity classes DSPACE(S) and NSPACE(S), the building blocks from which polynomial and log-space classes are derived.

Work-tape head positions are bounded directly. The finite input region and its first trailing blank are free, while farther input-head travel is charged. The output verdict cell is free, while farther two-way output-head travel is also charged. This prevents either infinite named tape from becoming hidden workspace.

def Complexity.DSPACE (S : ℕ → ℕ) : Set Language

DSPACE(S) is the class of languages decidable by a deterministic TM using O(S(n)) auxiliary space under Cfg.WithinDecisionSpace.

Equations

• Complexity.DSPACE S = {L : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.TM k) (f : ℕ → ℕ), tm.DecidesInSpace L f ∧ Complexity.BigO f S}

def Complexity.NSPACE (S : ℕ → ℕ) : Set Language

NSPACE(S) is the class of languages decidable by a nondeterministic TM using O(S(n)) auxiliary space under Cfg.WithinDecisionSpace.

Equations

• Complexity.NSPACE S = {L : Complexity.Language | ∃ (k : ℕ) (tm : Complexity.NTM k) (f : ℕ → ℕ), tm.DecidesInSpace L f ∧ Complexity.BigO f S}