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.

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 [AroraBarak09]) 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][AroraBarak09]

def Turing.MultiTapeNTM.RunPath.visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {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.

Equations

• p.visitedByTapeHead i = Finset.image (fun (n : Fin (p.length + 1)) => (p.toFun n).workTapePos i) Finset.univ

def Turing.MultiTapeNTM.RunPath.spaceUsedByTape {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {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.

Equations

• p.spaceUsedByTape i = (p.visitedByTapeHead i).card

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

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

Equations

• p.space = ∑ i : Fin k, p.spaceUsedByTape i

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

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

Equations

• p.space = Turing.MultiTapeNTM.RunPath.space p.toRunPath

def Turing.MultiTapeNTM.RunsInSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (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.

Equations

• ntm.RunsInSpace input s = ∀ (p : ntm.ComputationPath input), p.space ≤ s

theorem Turing.MultiTapeNTM.RunsInSpace.mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {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_2} (ntm : MultiTapeNTM 0 Symbol State) (input : List Symbol) (s : ℕ) : ntm.RunsInSpace input s

A machine without work tapes satisfies every space bound.