Documentation

Complexity.Computability.Complexity.Classes.Space.Basic

Deterministic space classes #

Cslib.Complexity.DSPACE enc s consists of the problems that some machine with a binary alphabet and finitely many states decides within space c₁ * s n + c₂, for constants c₁ and c₂, on instances whose encoding under enc has length n. Space counts visited work-tape cells; the input tape is read-only and the output tape write-only. The time bound may depend on the input length, with no prescribed growth rate. By configuration counting this is equivalent to allowing any halting time bound (Cslib.Complexity.mem_DSPACE_iff).

The definition follows the shape proposed in cslib pull request #767, for encoded instances. The concrete classes expose their DSPACE characterizations in Classes.LogSpace and Classes.Space.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.DSPACE {α : Type u_1} (enc : α ↪ List Bool) (s : ℕ → ℕ) :
Set (Set α)

The problems decidable within space O(s n), that is c₁ * s n + c₂ for constants c₁ and c₂, on instances whose encoding under enc has length n, by a machine with a binary alphabet and finitely many states, within some time bound of n Sipser, Definition 8.2.

Instances For
    source
    theorem Cslib.Complexity.mem_DSPACE_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} :
    A ∈ DSPACE enc s ↔ ∃ (c₁ : ℕ) (c₂ : ℕ) (t : α → ℕ), Turing.MultiTapeTM.DecidableInTimeAndSpace A enc t fun (a : α) => c₁ * s (enc a).length + c₂

    Membership in DSPACE asks for no particular time bound: a machine that halts within the space bound halts within the number of its configurations, a function of the length of the encoded instance (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_time_of_length).

    source
    theorem Cslib.Complexity.DSPACE_mono {α : Type u_1} {enc : α ↪ List Bool} {s₁ s₂ : ℕ → ℕ} (h : ∀ (n : ℕ), s₁ n ≤ s₂ n) :
    DSPACE enc s₁ ⊆ DSPACE enc s₂

    DSPACE is monotone in the space bound.

    source
    theorem Cslib.Complexity.DSPACE_mono_of_eventually_le {α : Type u_1} {enc : α ↪ List Bool} {s₁ s₂ : ℕ → ℕ} (h : ∀ᶠ (n : ℕ) in Filter.atTop, s₁ n ≤ s₂ n) :
    DSPACE enc s₁ ⊆ DSPACE enc s₂

    DSPACE only depends on the space bound eventually: the finitely many other values are absorbed by the additive constant.

    source
    theorem Cslib.Complexity.DSPACE_subset_of_le_mul_add {α : Type u_1} {enc : α ↪ List Bool} {s₁ s₂ : ℕ → ℕ} (c d : ℕ) (h : ∀ (n : ℕ), s₁ n ≤ c * s₂ n + d) :
    DSPACE enc s₁ ⊆ DSPACE enc s₂

    DSPACE depends on the space bound only up to a constant factor and an additive constant.