Documentation

CslibFrontier.Computability.Complexity.Classes.TimeSpace.Basic

Simultaneous time and space classes #

Cslib.Complexity.TISP enc t s consists of the problems that one machine with a binary alphabet and finitely many states decides within time c₁ * t n + c₂ and, simultaneously, within space c₁ * s n + c₂, for constants c₁ and c₂, on instances whose encoding under enc has length n Arora and Barak, Section 5.4. The model is the one of DTIME and DSPACE: the input tape is read-only, the output tape write-only, and space counts visited work-tape cells, so sublinear space bounds are meaningful.

Since a machine visits at most one new cell per step, time bounds space, and TISP enc t t is DTIME enc t (Cslib.Complexity.TISP_self_eq_DTIME).

Main definitions #

Main results #

References #

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

The problems decidable by one machine within time O(t n) and space O(s n) simultaneously, that is within time c₁ * t n + c₂ and space c₁ * s n + c₂ for constants c₁ and c₂, on instances whose encoding under enc has length n, with a binary alphabet and finitely many states. Space counts visited work-tape cells.

Instances For
    source
    theorem Cslib.Complexity.mem_TISP_iff_computableInO {α : Type} {enc : α ↪ List Bool} {A : Set α} {t s : ℕ → ℕ} :
    A ∈ TISP enc t s ↔ Turing.MultiTapeTM.ComputableInO (Turing.MultiTapeTM.indicator A) enc Turing.MultiTapeTM.encBool (fun (a : α) => t (enc a).length) fun (a : α) => s (enc a).length

    Membership in TISP is computability of the indicator within the charged bounds O(t n) and O(s n).

    source
    theorem Cslib.Complexity.setOf_mem_TISP_of_computableInO {α : Type} {enc : α ↪ List Bool} {f : α → Bool} {T S : α → ℕ} {t s : ℕ → ℕ} (h : Turing.MultiTapeTM.ComputableInO f enc Turing.MultiTapeTM.encBool T S) (hT : ∀ (a : α), T a ≤ t (enc a).length) (hS : ∀ (a : α), S a ≤ s (enc a).length) :
    {a : α | f a = true} ∈ TISP enc t s

    A Boolean function computable within time O(T a) and space O(S a) decides its true set within any bounds t and s of the length of the encoded instance above T and S.

    source
    theorem Cslib.Complexity.TISP_mono_of_le_mul_add {α : Type} {enc : α ↪ List Bool} {t₁ t₂ s₁ s₂ : ℕ → ℕ} {C : ℕ} (ht : ∀ (n : ℕ), t₁ n ≤ C * t₂ n + C) (hs : ∀ (n : ℕ), s₁ n ≤ C * s₂ n + C) :
    TISP enc t₁ s₁ ⊆ TISP enc t₂ s₂

    TISP depends on both bounds only up to a constant factor and an additive constant.

    source
    theorem Cslib.Complexity.TISP_mono {α : Type} {enc : α ↪ List Bool} {t₁ t₂ s₁ s₂ : ℕ → ℕ} (ht : ∀ (n : ℕ), t₁ n ≤ t₂ n) (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) :
    TISP enc t₁ s₁ ⊆ TISP enc t₂ s₂

    TISP is monotone in both bounds.

    source
    theorem Cslib.Complexity.TISP_subset_DTIME {α : Type} {enc : α ↪ List Bool} {t s : ℕ → ℕ} :
    TISP enc t s ⊆ DTIME enc t

    Forgetting the space bound.

    source
    theorem Cslib.Complexity.TISP_subset_DSPACE {α : Type} {enc : α ↪ List Bool} {t s : ℕ → ℕ} :
    TISP enc t s ⊆ DSPACE enc s

    Forgetting the time bound.

    source
    theorem Cslib.Complexity.DTIME_subset_TISP {α : Type} {enc : α ↪ List Bool} {t : ℕ → ℕ} :
    DTIME enc t ⊆ TISP enc t t

    A machine running within time O(t n) also runs within space O(t n).

    source
    theorem Cslib.Complexity.TISP_self_eq_DTIME {α : Type} {enc : α ↪ List Bool} {t : ℕ → ℕ} :
    TISP enc t t = DTIME enc t

    With equal bounds, simultaneous time and space is deterministic time.

    source
    theorem Cslib.Complexity.compl_mem_TISP {α : Type} {enc : α ↪ List Bool} {A : Set α} {t s : ℕ → ℕ} (h : A ∈ TISP enc t s) :
    Aᶜ ∈ TISP enc t s

    TISP is closed under complement: negate the output.

    source
    theorem Cslib.Complexity.compl_mem_DTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} (h : A ∈ DTIME enc t) :
    Aᶜ ∈ DTIME enc t

    DTIME is closed under complement: negate the output.

    source
    theorem Cslib.Complexity.compl_mem_DSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} {s : ℕ → ℕ} (h : A ∈ DSPACE enc s) :
    Aᶜ ∈ DSPACE enc s

    DSPACE is closed under complement: negate the output.