Skip to content

Time and space classes on multi-tape machines

14 fully proved

Uniform bounds

DefinitionTime-bounded multi-tape machine#✓fully proved

A deterministic Turing machine \(M\) with \(k\) work tapes is time bounded by \(t : \mathbb{N} \to \mathbb{N}\) when, for every input word \(w\), every computation path of \(M\) on \(w\) with at least \(t(|w|)\) steps ends in a halted configuration, where \(|w|\) is the length of \(w\).

def TimeBoundedBy (tm : MultiTapeTM k Symbol State) (t : ℕ → ℕ) : Prop :=
  ∀ w, tm.RunsInTime w (t w.length)
Used by 6
Used byPolynomial-space decider runs in exponential time · PSPACE is contained in EXP · Time classes are contained in space classes · Uniform time bounds give uniform space bounds · DSPACE over codes · DTIME over codes

DefinitionSpace-bounded multi-tape machine#✓fully proved

A deterministic Turing machine \(M\) with \(k\) work tapes is space bounded by \(s : \mathbb{N} \to \mathbb{N}\) when, for every input word \(w\), every computation path of \(M\) on \(w\) visits at most \(s(|w|)\) work-tape cells, counting the cells visited on each work tape and summing over the tapes, where \(|w|\) is the length of \(w\).

def SpaceBoundedBy (tm : MultiTapeTM k Symbol State) (s : ℕ → ℕ) : Prop :=
  ∀ w, tm.RunsInSpace w (s w.length)
Used by 6
Used byPolynomial-space decider runs in exponential time · PSPACE is contained in EXP · Time classes are contained in space classes · Uniform time bounds give uniform space bounds · DSPACE over codes · DTIME over codes

TheoremTime bounds space on one input#✓fully proved

Let \(M\) be a deterministic Turing machine with \(k\) work tapes, let \(w\) be an input word and let \(T \in \mathbb{N}\). If \(M\) runs in time \(T\) on \(w\), that is, every computation path of \(M\) on \(w\) with at least \(T\) steps ends in a halted configuration, then \(M\) runs in space \(k(T + 1)\) on \(w\): every computation path of \(M\) on \(w\) visits at most \(k(T + 1)\) work-tape cells, counting the cells visited on each work tape and summing over the tapes.

theorem runsInSpace_of_runsInTime {tm : MultiTapeTM k Symbol State} {w : List Symbol} {T : ℕ}
    (h : tm.RunsInTime w T) : tm.RunsInSpace w (k * (T + 1))
Uses 1 · Used by 1
Proof usesA time bound forces halting
Used byUniform time bounds give uniform space bounds

TheoremUniform time bounds give uniform space bounds#✓fully proved

Let \(M\) be a deterministic Turing machine with \(k\) work tapes and let \(t : \mathbb{N} \to \mathbb{N}\). If \(M\) is time bounded by \(t\), then \(M\) is space bounded by the function \(n \mapsto k(t(n) + 1)\).

theorem TimeBoundedBy.spaceBoundedBy {tm : MultiTapeTM k Symbol State} {t : ℕ → ℕ}
    (h : TimeBoundedBy tm t) : SpaceBoundedBy tm fun n ↦ k * (t n + 1)
Uses 3 · Used by 1
Statement usesSpace-bounded multi-tape machine · Time-bounded multi-tape machine
Proof usesTime bounds space on one input
Used byTime classes are contained in space classes

Deciding languages

DefinitionA multi-tape machine deciding a language#✓fully proved

A deterministic multi-tape Turing machine over the Boolean alphabet decides a language \(L\) of Boolean strings when, on every input \(w\), it eventually halts with output the one-bit string \([\mathrm{true}]\) if \(w \in L\) and \([\mathrm{false}]\) if \(w \notin L\).

def Decides (tm : MultiTapeTM k Bool State) (L : Set (List Bool)) : Prop :=
  ∀ w, tm.Computes w [MultiTapeTM.indicator L w]
Used by 9
Used byPolynomial-space decider runs in exponential time · PSPACE is contained in EXP · Decidability within time and space bounds, unfolded · Time classes are contained in space classes · Relabelling preserves deciding a language · Deciding by a code is finite-state decidability · Decidability over codes · DSPACE over codes · DTIME over codes

TheoremDecidability within time and space bounds, unfolded#✓fully proved

Let \(L\) be a language of Boolean strings and let \(t\) and \(s\) assign a natural number to every Boolean string. Then \(L\) is decidable within time \(t\) and space \(s\) in CSLib's sense, with the identity encoding of inputs, if and only if there are a number \(k\), a finite type of states and a deterministic Turing machine with \(k\) work tapes over the Boolean alphabet that decides \(L\) and, on every input \(w\), runs in time \(t(w)\) (every computation path of at least \(t(w)\) steps ends in a halted configuration) and in space \(s(w)\) (every computation path visits at most \(s(w)\) work-tape cells, summed over the work tapes).

theorem decidableInTimeAndSpace_iff {L : Set (List Bool)} {t s : List Bool → ℕ} :
    MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl _) t s ↔
      ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State),
        Decides tm L ∧ (∀ w, tm.RunsInTime w (t w)) ∧ ∀ w, tm.RunsInSpace w (s w)
Uses 1 · Used by 4
Statement usesA multi-tape machine deciding a language
Used byPSPACE is contained in EXP · Time classes are contained in space classes · Deciding by a code is finite-state decidability · Decidability over codes

Deterministic time and space classes

DefinitionDeterministic time classes on multi-tape machines#✓fully proved

For \(t : \mathbb{N} \to \mathbb{N}\), \(\mathrm{DTIME}(t)\) is the set of languages \(L\) of Boolean strings for which there are constants \(c_1, c_2 \in \mathbb{N}\), a function \(s : \mathbb{N} \to \mathbb{N}\) and a deterministic multi-tape Turing machine with Boolean tape alphabet and finitely many states such that, on every input \(w\) of length \(n\), the machine halts with the one-bit output \([\mathrm{true}]\) if \(w \in L\) and \([\mathrm{false}]\) otherwise, runs in time \(c_1 t(n) + c_2\) (every computation path of at least \(c_1 t(n) + c_2\) steps ends in a halted configuration) and runs in space \(s(n)\) (every computation path visits at most \(s(n)\) work-tape cells, summed over the work tapes).

def DTIME (t : ℕ → ℕ) : Set (Set (List Bool)) :=
  {L | ∃ c₁ c₂ : ℕ, ∃ s : ℕ → ℕ, MultiTapeTM.DecidableInTimeAndSpace L
    (Function.Embedding.refl _) (fun w ↦ c₁ * t w.length + c₂) (fun w ↦ s w.length)}
Used by 9
Used byPSPACE is contained in EXP · Deterministic time classes are monotone up to affine changes of the bound · Time classes are contained in space classes · Polynomial time on multi-tape machines · P is contained in PSPACE · The class E · The class EXP · Deterministic time hierarchy: quadratic versus linear time · DTIME over codes

DefinitionDeterministic space classes on multi-tape machines#✓fully proved

For \(s : \mathbb{N} \to \mathbb{N}\), \(\mathrm{DSPACE}(s)\) is the set of languages \(L\) of Boolean strings for which there are constants \(c_1, c_2 \in \mathbb{N}\), a function \(t : \mathbb{N} \to \mathbb{N}\) and a deterministic multi-tape Turing machine with Boolean tape alphabet and finitely many states such that, on every input \(w\) of length \(n\), the machine halts with the one-bit output \([\mathrm{true}]\) if \(w \in L\) and \([\mathrm{false}]\) otherwise, runs in time \(t(n)\) (every computation path of at least \(t(n)\) steps ends in a halted configuration) and runs in space \(c_1 s(n) + c_2\) (every computation path visits at most \(c_1 s(n) + c_2\) work-tape cells, summed over the work tapes).

def DSPACE (s : ℕ → ℕ) : Set (Set (List Bool)) :=
  {L | ∃ c₁ c₂ : ℕ, ∃ t : ℕ → ℕ, MultiTapeTM.DecidableInTimeAndSpace L
    (Function.Embedding.refl _) (fun w ↦ t w.length) (fun w ↦ c₁ * s w.length + c₂)}
Used by 9
Used byPSPACE is contained in EXP · Deterministic space classes are monotone up to affine changes of the bound · Time classes are contained in space classes · P is contained in PSPACE · Polynomial space on multi-tape machines · The class EXPSPACE · Deterministic logarithmic space · Deterministic space hierarchy: quadratic versus linear space · DSPACE over codes

TheoremDeterministic time classes are monotone up to affine changes of the bound#✓fully proved

Let \(t_1, t_2 : \mathbb{N} \to \mathbb{N}\) and \(a, b \in \mathbb{N}\) satisfy \(t_1(n) \le a \, t_2(n) + b\) for every \(n \in \mathbb{N}\). Then \(\mathrm{DTIME}(t_1) \subseteq \mathrm{DTIME}(t_2)\).

theorem DTIME_mono {t₁ t₂ : ℕ → ℕ} (a b : ℕ) (h : ∀ n, t₁ n ≤ a * t₂ n + b) :
    DTIME t₁ ⊆ DTIME t₂
Uses 1
Statement usesDeterministic time classes on multi-tape machines

TheoremDeterministic space classes are monotone up to affine changes of the bound#✓fully proved

Let \(s_1, s_2 : \mathbb{N} \to \mathbb{N}\) and \(a, b \in \mathbb{N}\) satisfy \(s_1(n) \le a \, s_2(n) + b\) for every \(n \in \mathbb{N}\). Then \(\mathrm{DSPACE}(s_1) \subseteq \mathrm{DSPACE}(s_2)\).

theorem DSPACE_mono {s₁ s₂ : ℕ → ℕ} (a b : ℕ) (h : ∀ n, s₁ n ≤ a * s₂ n + b) :
    DSPACE s₁ ⊆ DSPACE s₂
Uses 1
Statement usesDeterministic space classes on multi-tape machines

TheoremTime classes are contained in space classes#✓fully proved

For every \(t : \mathbb{N} \to \mathbb{N}\), \(\mathrm{DTIME}(t) \subseteq \mathrm{DSPACE}(t)\).

theorem DTIME_subset_DSPACE (t : ℕ → ℕ) : DTIME t ⊆ DSPACE t
Uses 7 · Used by 1
Statement usesDeterministic space classes on multi-tape machines · Deterministic time classes on multi-tape machines
Proof usesA multi-tape machine deciding a language · Space-bounded multi-tape machine · Time-bounded multi-tape machine · Uniform time bounds give uniform space bounds · Decidability within time and space bounds, unfolded
Used byP is contained in PSPACE

DefinitionPolynomial time on multi-tape machines#✓fully proved

\(\mathrm{P}\) is the set of languages of Boolean strings that lie in \(\mathrm{DTIME}(n \mapsto n^d)\) for some \(d \in \mathbb{N}\).

def P : Set (Set (List Bool)) := ⋃ d, DTIME (· ^ d)
Uses 1 · Used by 1
Statement usesDeterministic time classes on multi-tape machines
Used byP is contained in PSPACE

DefinitionPolynomial space on multi-tape machines#✓fully proved

\(\mathrm{PSPACE}\) is the set of languages of Boolean strings that lie in \(\mathrm{DSPACE}(n \mapsto n^d)\) for some \(d \in \mathbb{N}\).

def PSPACE : Set (Set (List Bool)) := ⋃ d, DSPACE (· ^ d)
Uses 1 · Used by 2
Statement usesDeterministic space classes on multi-tape machines
Used byP is contained in PSPACE · Polynomial space for decision problems

TheoremP is contained in PSPACE#✓fully proved

On the deterministic multi-tape model, \(\mathrm{P} \subseteq \mathrm{PSPACE}\).

theorem P_subset_PSPACE : P ⊆ PSPACE
Uses 5
Statement usesPolynomial time on multi-tape machines · Polynomial space on multi-tape machines
Proof usesDeterministic space classes on multi-tape machines · Deterministic time classes on multi-tape machines · Time classes are contained in space classes

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.