Space usage of multi-tape Turing machines

Defines the space used by a run path of a multi-tape Turing machine. Space usage counts the positions visited by each work-tape head along the path and sums over the tapes.

MultiTapeNTM.RunPath.InWindow says that every head of a run path stays within the window [-s, s], which bounds the space of the path.

MultiTapeNTM.RunPath.space_map_le bounds the space of a run path mapped by RunPath.map through the head positions of the original path.

Design

The input tape is read-only with bounded head movement, and the output tape is write-only, so we ignore both for space usage. A work-tape cell is visited when its head occupies that position in any configuration of the path, including the initial and final configurations. Each cell counts once, regardless of repeated visits.

Instead of considering the cells visited by the work tape heads, some textbooks (including [AB09]) only consider the number of cells that contain a non-blank symbol at some point in the execution or the number of cells written to. This allows work tape heads to freely move at no cost as long as they do not write. It is important to note that this causes DSPACE(1) to include DSPACE(log log n), a class that contains e.g. the non-regular language {0^n 1^n | n ∈ ℕ} (it is accepted by a TM that writes a single marker on the work tape and then counts the number of symbols by work tape head movement without writing). Defining space usage via "cells visited" thus yields the more fine-grained "complexity world" in which DSPACE(1) is exactly the class of regular languages.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Turing.window (s : ℕ) : Finset ℤ

The window [-s, s] of tape positions allotted to a tape that uses s cells.

theorem Turing.mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s

@[simp]

theorem Turing.card_window (s : ℕ) : (window s).card = 2 * s + 1

def Turing.MultiTapeNTM.RunPath.visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (i : Fin k) : Finset ℤ

The set of positions visited by the head of work tape i along a run path.

def Turing.MultiTapeNTM.RunPath.spaceUsedByTape {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (i : Fin k) : ℕ

The number of positions visited by the head of work tape i along a run path.

def Turing.MultiTapeNTM.RunPath.space {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) : ℕ

The number of work tape cells visited along a run path.

theorem Turing.MultiTapeNTM.RunPath.spaceUsedByTape_le_card {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) {i : Fin k} {S : Finset ℤ} (h : ∀ c ∈ p, c.workTapePos i ∈ S) : p.spaceUsedByTape i ≤ S.card

A set containing every position of a head along a path bounds the space used by its tape.

theorem Turing.MultiTapeNTM.RunPath.space_le_sum_card {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) {S : Fin k → Finset ℤ} (h : ∀ c ∈ p, ∀ (i : Fin k), c.workTapePos i ∈ S i) : p.space ≤ ∑ i : Fin k, (S i).card

Sets containing every position of the heads along a path bound its space by their total size.

theorem Turing.MultiTapeNTM.RunPath.space_le_of_subset {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {p q : ntm.RunPath input} (h : ∀ c ∈ q, c ∈ p) : q.space ≤ p.space

A path whose configurations all lie on another path visits no more cells.

Windows

def Turing.MultiTapeNTM.RunPath.InWindow {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (s : ℕ) : Prop

Every head stays within the window [-s, s] along the path.

theorem Turing.MultiTapeNTM.RunPath.InWindow.space_le {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {p : ntm.RunPath input} {s : ℕ} (h : p.InWindow s) : p.space ≤ k * (2 * s + 1)

A path whose heads stay within [-s, s] visits at most 2 * s + 1 cells on each tape.

theorem Turing.MultiTapeNTM.RunPath.InWindow.smash {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {p q : ntm.RunPath input} {h : RelSeries.last p = RelSeries.head q} {s : ℕ} (hp : p.InWindow s) (hq : q.InWindow s) : InWindow (RelSeries.smash p q h) s

Joining two paths whose heads stay within [-s, s] keeps them there.

Mapped paths

theorem Turing.MultiTapeNTM.RunPath.visitedByTapeHead_map {k k' : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input input' : List Symbol} {ntm : MultiTapeNTM k Symbol State} {ntm' : MultiTapeNTM k' Symbol State'} (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.stepRel input')) {i : Fin k} {i' : Fin k'} (h : ∀ c ∈ p, (f c).workTapePos i' = c.workTapePos i) : (p.map f).visitedByTapeHead i' = p.visitedByTapeHead i

If the head of tape i' of a mapped path follows the head of tape i of the source path, the two tapes visit the same cells.

theorem Turing.MultiTapeNTM.RunPath.space_map_le {k k' : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input input' : List Symbol} {ntm : MultiTapeNTM k Symbol State} {ntm' : MultiTapeNTM k' Symbol State'} (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.stepRel input')) (e : Fin k ↪ Fin k') (window : Fin k' → Finset ℤ) (hfollow : ∀ c ∈ p, ∀ (j : Fin k), (f c).workTapePos (e j) = c.workTapePos j) (hwindow : ∀ c ∈ p, ∀ l ∉ Set.range ⇑e, (f c).workTapePos l ∈ window l) : (p.map f).space ≤ p.space + ∑ l ∈ (Finset.map e Finset.univ)ᶜ, (window l).card

Space of a mapped path. If tape e j of the mapped path follows tape j of p, and every other tape l stays in window l, the mapped path uses the space of p plus the cells of window l for every other tape l.

def Turing.MultiTapeNTM.ComputationPath.space {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.ComputationPath input) : ℕ

The number of work tape cells visited along a computation path.

def Turing.MultiTapeNTM.RunsInSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_3} (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) (s : ℕ) : Prop

Every computation prefix on input visits at most s work-tape cells, regardless of its outcome.

theorem Turing.MultiTapeNTM.RunsInSpace.mono {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {s s' : ℕ} (h : ntm.RunsInSpace input s) (hs : s ≤ s') : ntm.RunsInSpace input s'

A space bound can be increased.

@[simp]

theorem Turing.MultiTapeNTM.runsInSpace_zero_tapes {State : Type u_1} {Symbol : Type u_3} (ntm : MultiTapeNTM 0 Symbol State) (input : List Symbol) (s : ℕ) : ntm.RunsInSpace input s

A machine without work tapes satisfies every space bound.