Deterministic Multi-Tape Turing Machines

Defines deterministic Turing machines with a read-only input tape, k work tapes and one write-only output tape. The tapes contain symbols from Option Symbol for a finite alphabet Symbol (where none is the blank symbol).

Design

The multi-tape Turing machine uses a read-only input tape, k work tapes and a write-only output tape. The input head can move freely on the input, but any move attempt beyond one cell outside the input results in no movement. The transition function can optionally output one symbol, which models the write-only output tape. Because of these restrictions, we ignore the input and output tapes for space usage of the machine. The space usage is defined as the total number of cells the work tape heads visited during execution.

Restricting the movement of the input head is not essential, but useful because it allows us to easily bound the number of possible configurations of a space-bounded machine. Most textbooks have this restriction.

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.

This definition is adapted from the one in [Papadimitriou94], chapter 2.3 including the sub-linear space modifications from chapter 2.5 with the following changes:

• We allow Turing machines to choose to not write on a tape. This is equivalent to writing the read symbol again but makes it easier to reason about the semantics.
• Our tapes are infinite in both directions instead of just to the right. This definition is equivalent (see [AroraBarak09], Claim 1.4). It saves us from having to add a "start marker" to the alphabet.
• We only have a single halting state. The different ways to halt (accepting, rejecting, etc) can be distinguished based on the output.
• The way to prevent the input head to move outside the input is enforced by the interpretation and not by a restriction on the transition function. The two definitions are equivalent, but not restricting the transition function makes it easier to define a universal machine.

Important Declarations

We define a number of structures and concepts related to multi-tape Turing machine computation:

• MultiTapeTM: the TM itself
• spaceUsed: the number of work tape cells touched by the heads until a certain step
• TransitionRelation: the transition relation from one configuration to the next
• HaltsAt: the run from a configuration halts at exactly a given step
• spaceUsed: the number of tape cells touched by work tape heads, our main space measure
• ComputesInTimeAndSpace: a proof that a specific TM computes an output from an input in a certain number of steps and using a certain number of tape cells
• ComputesFunInTimeAndSpace: a machine computes a function between specified encodings, respecting time and space bounds on each actual input.
• ComputableInTimeAndSpace: such a machine exists with binary alphabet and finitely many states.
• ComputableInTimeAndSpaceOfLength: the specialization to bounds on encoded input length.
• DecidableInTimeAndSpace: a proof that a TM decides a language within a certain time and space bound.

There are two ways to talk about the behaviour of a multi-tape Turing machine, and they are proven to be equivalent.

• MultiTapeTM.runFrom: the configuration reached after a given number of execution steps
• RelatesInSteps tm.TransitionRelation cfg cfg' t: a proof that tm transforms the configuration cfg into cfg' in exactly t steps

References

• [C. Papadimitriou, Computational Complexity][Papadimitriou94]
• [S. Arora, B. Barak, Computational Complexity: A Modern Approach][AroraBarak09]
• [M. Sipser, Introduction to the Theory of Computation][Sipser2013]

structure Turing.MultiTapeTM (k : ℕ) (Symbol : Type u_3) (State : Type u_4) : Type (max u_3 u_4)

A multi-tape Turing machine with k work tapes over the alphabet of Option Symbol (where none is the blank tape symbol). Note that it is not required that Symbol or State are finite to keep the definition more general. The restriction will be introduced once we start talking about computability by Turing machines in general.

• q₀ : State

  initial state

• tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : Action k Symbol State

  transition function, mapping a state, the current input symbol and a tuple of work head symbols to a movement for the input head, actions on the work tape, optionally a symbol to output and the successor state

Stepping a Turing Machine

This section defines the step function that lets the machine transition from one configuration to the next, and the configuration reached after a number of steps. Configurations themselves are defined in Cslib.Computability.Machines.Turing.MultiTape.Configuration.

def Turing.MultiTapeTM.step {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) : Cfg k Symbol State input

The step function corresponding to a MultiTapeTM.

Equations

• Turing.MultiTapeTM.step cfg = match cfg.state with | none => cfg | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg

theorem Turing.MultiTapeTM.step_apply_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) : step cfg = (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg

One step at a live state is the transition's action applied to the configuration.

def Turing.MultiTapeTM.outputSymbol {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) : Option Symbol

The symbol (optionally) output when executing one step starting from configuration cfg.

Equations

• Turing.MultiTapeTM.outputSymbol cfg = match cfg.state with | none => none | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).output

theorem Turing.MultiTapeTM.step_inputPos_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) : (step cfg).inputPos = moveInputPos cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputTape

The input head after a live step.

theorem Turing.MultiTapeTM.step_workTapes_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) (i : Fin k) : (step cfg).workTapes i = match (motive := Option (Option Symbol) → ℤ → Option Symbol) ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s

A work tape after a live step.

theorem Turing.MultiTapeTM.step_workTapePos_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) (i : Fin k) : (step cfg).workTapePos i = cfg.workTapePos i + ↑((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes i).2

A work tape head after a live step.

def Turing.MultiTapeTM.initCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} (input : List Symbol) : Cfg k Symbol State input

The initial configuration corresponding to an input string.

Equations

• Turing.MultiTapeTM.initCfg input = Turing.Cfg.init tm.q₀ input

@[simp]

theorem Turing.MultiTapeTM.step_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} (h : cfg.state = none) : step cfg = cfg

def Turing.MultiTapeTM.runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input

The configuration reached by running the Turing machine for t steps from cfg. If the Turing machine halts, it will stay at the halting configuration.

Equations

• Turing.MultiTapeTM.runFrom cfg t = Turing.MultiTapeTM.step^[t] cfg

theorem Turing.MultiTapeTM.runFrom_eq_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (runFrom cfg τ).state = none) : runFrom cfg t = runFrom cfg τ

Nothing changes after the machine has halted.

def Turing.MultiTapeTM.HaltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : Prop

The machine tm started in cfg halts at step t: it is halted after t steps and not halted after any smaller number of steps.

Equations

• tm.HaltsAt cfg t = ((Turing.MultiTapeTM.runFrom cfg t).Halted ∧ ∀ s < t, ¬(Turing.MultiTapeTM.runFrom cfg s).Halted)

theorem Turing.MultiTapeTM.HaltsAt.halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {t : ℕ} (h : tm.HaltsAt cfg t) : (runFrom cfg t).Halted

theorem Turing.MultiTapeTM.HaltsAt.not_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h : tm.HaltsAt cfg t) (hs : s < t) : ¬(runFrom cfg s).Halted

theorem Turing.MultiTapeTM.HaltsAt.le_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h : tm.HaltsAt cfg t) (hs : (runFrom cfg s).Halted) : t ≤ s

The halting step is the first step at which the machine is halted.

theorem Turing.MultiTapeTM.HaltsAt.unique {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h₁ : tm.HaltsAt cfg s) (h₂ : tm.HaltsAt cfg t) : s = t

The halting step is unique.

theorem Turing.MultiTapeTM.HaltsAt.runFrom_eq {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h : tm.HaltsAt cfg t) (hts : t ≤ s) : runFrom cfg s = runFrom cfg t

From the halting step on, the configuration does not change.

theorem Turing.MultiTapeTM.exists_haltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {t : ℕ} (hhalt : (runFrom cfg t).Halted) : ∃ u ≤ t, tm.HaltsAt cfg u

A run that is halted after t steps halts at some step u ≤ t.

theorem Turing.MultiTapeTM.existsUnique_haltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {t : ℕ} (hhalt : (runFrom cfg t).Halted) : ∃! u : ℕ, tm.HaltsAt cfg u

A run that is halted after some number of steps halts at exactly one step.

@[simp]

theorem Turing.MultiTapeTM.outputSymbol_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) : outputSymbol cfg = none

theorem Turing.MultiTapeTM.workTapePos_step_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (c : Cfg k Symbol State input) (i : Fin k) : |(step c).workTapePos i - c.workTapePos i| ≤ 1

The work-tape head moves by at most one cell in a single step.

Now we define space usage and add some helper lemmas.

def Turing.MultiTapeTM.visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ

The set of positions visited by the head of work tape i in the computation starting from configuration cfg up to step t.

Equations

• Turing.MultiTapeTM.visitedByTapeHead cfg t i = Finset.image (fun (n : Fin (t + 1)) => (Turing.MultiTapeTM.runFrom cfg ↑n).workTapePos i) Finset.univ

def Turing.MultiTapeTM.spaceUsedByTape {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ

The number of work tape cells touched by the head of tape i in the computation starting from configuration cfg up to step t.

Equations

• Turing.MultiTapeTM.spaceUsedByTape cfg t i = (Turing.MultiTapeTM.visitedByTapeHead cfg t i).card

def Turing.MultiTapeTM.spaceUsed {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ

The number of work tape cells touched by a computation starting from configuration cfg up to step t.

Equations

• Turing.MultiTapeTM.spaceUsed cfg t = ∑ i : Fin k, Turing.MultiTapeTM.spaceUsedByTape cfg t i

@[simp]

theorem Turing.MultiTapeTM.spaceUsed_zero_tapes_eq_zero {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) : spaceUsed cfg t = 0

A zero-tape Turing machine uses zero space.

theorem Turing.MultiTapeTM.spaceUsedByTape_le_spaceUsed {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : spaceUsedByTape cfg t i ≤ spaceUsed cfg t

Each tape's space usage is bounded by the total space used.

def Turing.MultiTapeTM.TransitionRelation {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (c₁ c₂ : Cfg k Symbol State input) : Prop

The TransitionRelation corresponding to a MultiTapeTM k Symbol is defined by the step function, which maps a configuration to its next configuration.

Equations

• Turing.MultiTapeTM.TransitionRelation c₁ c₂ = (Turing.MultiTapeTM.step c₁ = c₂)

@[simp]

theorem Turing.MultiTapeTM.step_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) : (step cfg).output = cfg.output ++ (outputSymbol cfg).toList

One step appends the symbol (optionally) emitted by that step to the output tape.

theorem Turing.MultiTapeTM.inputPos_runFrom_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : ↑(runFrom cfg t).inputPos ≤ ↑cfg.inputPos + t

In t steps the input head moves at most t positions to the right.

theorem Turing.MultiTapeTM.runFrom_output_eq_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (runFrom cfg τ).state = none) : (runFrom cfg t).output = (runFrom cfg τ).output

The output does not change after the machine has halted.

theorem Turing.MultiTapeTM.length_output_mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : Monotone fun (t : ℕ) => (runFrom cfg t).output.length

The output only grows during a run.

theorem Turing.MultiTapeTM.length_output_runFrom_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : (runFrom cfg t).output.length ≤ cfg.output.length + t

A machine emits at most one symbol per step.

def Turing.MultiTapeTM.ComputesInTimeAndSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop

A proof that the Turing machine tm on input input outputs output in at most t steps and uses exactly s space. Note that this does not require the alphabet or state set to be finite.

Equations

• One or more equations did not get rendered due to their size.

def Turing.MultiTapeTM.ComputesFunInTimeAndSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {α : Type u_3} {β : Type u_4} (tm : MultiTapeTM k Symbol State) (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) (t s : α → ℕ) : Prop

A machine computes f between the supplied encodings, with bounds depending on the input. The machine's alphabet and state type need not be finite.

Equations

• tm.ComputesFunInTimeAndSpace encIn encOut f t s = ∀ (a : α), ∃ t' ≤ t a, ∃ s' ≤ s a, tm.ComputesInTimeAndSpace (encIn a) (encOut (f a)) t' s'

def Turing.MultiTapeTM.ComputableInTimeAndSpace {α : Type u_3} {β : Type u_4} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : α → ℕ) : Prop

A function is computable within the input-indexed bounds by a machine with binary alphabet and finitely many states.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength {α : Type u_3} {β : Type u_4} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : ℕ → ℕ) : Prop

There exists a binary Turing machine with finitely many states that, for every input a, computes encOut (f a) from encIn a in at most t (encIn a).length steps, using at most s (encIn a).length work-tape cells.

Equations

• One or more equations did not get rendered due to their size.

theorem Turing.MultiTapeTM.ComputesFunInTimeAndSpace.mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {α : Type u_3} {β : Type u_4} {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol} {f : α → β} {t s t' s' : α → ℕ} (h : tm.ComputesFunInTimeAndSpace encIn encOut f t s) (ht : ∀ (a : α), t a ≤ t' a) (hs : ∀ (a : α), s a ≤ s' a) : tm.ComputesFunInTimeAndSpace encIn encOut f t' s'

Resource bounds can be weakened independently on every input.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.mono {α : Type u_3} {β : Type u_4} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s t' s' : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (ht : ∀ (a : α), t a ≤ t' a) (hs : ∀ (a : α), s a ≤ s' a) : ComputableInTimeAndSpace f encIn encOut t' s'

Computability is monotone in the resource bounds.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.length_encOut_le {α : Type u_3} {β : Type u_4} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (a : α) : (encOut (f a)).length ≤ t a

A machine emits at most one symbol per step, so the encoded result of a computation is no longer than its time bound. This is the only bound available on the length of an intermediate result: a machine can produce an output much longer than the space it uses.

noncomputable def Turing.MultiTapeTM.indicator {α : Type u_3} (L : Set α) : α → Bool

The Boolean indicator function of a set.

Equations

• Turing.MultiTapeTM.indicator L x = if x ∈ L then true else false

def Turing.MultiTapeTM.DecidableInTimeAndSpace {α : Type u_3} (L : Set α) (enc : α ↪ List Bool) (t s : α → ℕ) : Prop

A set is decidable within the given input-indexed bounds when its Boolean indicator is.

Equations

• One or more equations did not get rendered due to their size.

theorem Turing.MultiTapeTM.relatesInSteps_iff_runFrom_eq {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg₁ cfg₂ : Cfg k Symbol State input) (t : ℕ) : Relation.RelatesInSteps TransitionRelation cfg₁ cfg₂ t ↔ runFrom cfg₁ t = cfg₂

This lemma translates between the relational notion and the iterated step notion. The latter can be more convenient especially for deterministic machines as we have here.

theorem Turing.MultiTapeTM.not_halts_of_repeat_nonhalt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (h_not_halt : cfg.state ≠ none) (t : ℕ) (heq : runFrom cfg (t + 1) = cfg) (t' : ℕ) : (runFrom cfg t').state ≠ none

If a deterministic machine repeats a non-halting configuration, it never halts, because the sequence between the two configurations will loop forever. Note that this can be applied to two arbitrary and different time steps t and t + Δ using Function.iterate_add_apply.