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 [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.

This definition is adapted from the one in [Pap94], 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 [AB09], 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
• Cfg: the configuration of a TM: the internal state, the work tape contents and head positions
• 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
• 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
• ComputableInTimeAndSpace: a proof that there is a multi-tape TM that computes a function (on strings) respecting a time and space bound in the 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.configs: a sequence of configurations by execution step
• 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
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation

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

The output of the transition function.

• inputMove : SignType

  The movement (attempt) of the input head.

• workActions : Fin k → Option (Option Symbol) × SignType

  Actions on the work tapes: optionally a symbol to write and the head movement.

• outS : Option Symbol

  An optional symbol to output.

• q' : Option State

  The successor state or none to halt.

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 BiTape 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) : TransitionOut 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

Configurations of a Turing Machine

This section defines the configurations of a Turing machine, the step function that lets the machine transition from one configuration to the next, the resulting sequence of configurations and the initial configuration.

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

The configurations of a Turing machine is relative to the input of the machine and consist of:

• an Optional state (or none for the halting state),
• the position of the input head (shifted by one),
• the contents of the work tape,
• the positions of the work tape heads.

• state : Option State

  the state of the TM (or none for the halting state)

• inputPos : Fin (input.length + 2)

  the position of the input head, shifted by one

• workTapes : Fin k → ℤ → Option Symbol

  the work tapes

• workTapePos : Fin k → ℤ

  the positions of the heads on the work tapes

theorem Turing.MultiTapeTM.Cfg.ext {k : ℕ} {Symbol : Type u_3} {State : Type u_4} {input : List Symbol} {x y : Cfg k Symbol State input} (state : x.state = y.state) (inputPos : x.inputPos = y.inputPos) (workTapes : x.workTapes = y.workTapes) (workTapePos : x.workTapePos = y.workTapePos) : x = y

theorem Turing.MultiTapeTM.Cfg.ext_iff {k : ℕ} {Symbol : Type u_3} {State : Type u_4} {input : List Symbol} {x y : Cfg k Symbol State input} : x = y ↔ x.state = y.state ∧ x.inputPos = y.inputPos ∧ x.workTapes = y.workTapes ∧ x.workTapePos = y.workTapePos

@[instance_reducible]

instance Turing.MultiTapeTM.instInhabitedCfg {a✝ : ℕ} {a✝¹ : Type u_3} {a✝² : Type u_4} {a✝³ : List a✝¹} : Inhabited (Cfg a✝ a✝¹ a✝² a✝³)

Equations

• Turing.MultiTapeTM.instInhabitedCfg = { default := Turing.MultiTapeTM.instInhabitedCfg.default }

def Turing.MultiTapeTM.moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2)

Attempt to move the input tape head. The machine can only read one empty cell outside of the input, any attempted movement beyond that results in no movement.

The addition is performed in ℤ before clamping. Performing it in Fin (n + 2) would wrap an outward boundary move to the opposite end of the input.

Equations

• Turing.MultiTapeTM.moveInputPos pos m = if h : (↑↑pos + ↑m).toNat < n + 2 then ⟨(↑↑pos + ↑m).toNat, h⟩ else ⟨n + 1, ⋯⟩

@[simp]

theorem Turing.MultiTapeTM.moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) : moveInputPos pos 0 = pos

@[simp]

theorem Turing.MultiTapeTM.moveInputPos_leftBoundary {n : ℕ} : moveInputPos 0 (-1) = 0

@[simp]

theorem Turing.MultiTapeTM.moveInputPos_rightBoundary {n : ℕ} : moveInputPos ⟨n + 1, ⋯⟩ 1 = ⟨n + 1, ⋯⟩

theorem Turing.MultiTapeTM.moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) : moveInputPos p SignType.neg = ⟨↑p - 1, ⋯⟩

A left move away from the left input boundary decrements the native input position.

theorem Turing.MultiTapeTM.moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : ↑p ≠ n + 1) : moveInputPos p SignType.pos = ⟨↑p + 1, ⋯⟩

A right move away from the right input boundary increments the native input position.

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

The symbol currently under the input tape head.

Equations

• cfg.inputSymbol = if h₁ : cfg.inputPos = 0 then none else if h₂ : ↑cfg.inputPos = input.length + 1 then none else some input[↑cfg.inputPos - 1]

@[simp]

theorem Turing.MultiTapeTM.inputSymbolInner {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {cfg : Cfg k Symbol State input} (p : ℕ) (h₁ : ↑cfg.inputPos = 1 + p) (h₂ : p < input.length) : cfg.inputSymbol = some input[p]

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

The symbol read by work tape i.

Equations

• cfg.workTapeSymbols i = cfg.workTapes i (cfg.workTapePos i)

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

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

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).outS

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 = { state := some tm.q₀, inputPos := 1, workTapes := fun (x : Fin k) (x_1 : ℤ) => none, workTapePos := fun (x : Fin k) => 0 }

def Turing.MultiTapeTM.configs {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 sequence of configurations of the Turing machine starting from cfg. If the Turing machine halts, it will stay at the halting configuration.

Equations

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

@[simp]

theorem Turing.MultiTapeTM.iter_step_eq_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} {n : ℕ} (h_halt : cfg.state = none) : step^[n] cfg = cfg

Any number of steps run from a halting configuration results in the same configuration.

@[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.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 = (List.map (fun (t' : ℕ) => (Turing.MultiTapeTM.configs cfg t').workTapePos i) (List.range (t + 1))).toFinset.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 {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 ≤ t + 1

The number of cells touched by a single work tape grows by at most one each step.

theorem Turing.MultiTapeTM.spaceUsed_linear {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : spaceUsed cfg t ≤ k * t + k

The space used by a computation is bounded linearly by the number of steps.

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₂)

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

The string output by the Turing machine tm starting in configuration cfg₀, executing for t steps. It is the concatenation of the symbols (optionally) emitted at each of the first t steps.

Equations

• tm.outputString cfg₀ t = List.flatMap (fun (t' : ℕ) => (Turing.MultiTapeTM.outputSymbol (Turing.MultiTapeTM.configs cfg₀ t')).toList) (List.range t)

theorem Turing.MultiTapeTM.outputString_succ {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : tm.outputString cfg (t + 1) = tm.outputString cfg t ++ (outputSymbol (configs cfg t)).toList

The output produced in t + 1 steps is the output produced in t steps followed by the symbol (optionally) emitted at step t.

theorem Turing.MultiTapeTM.outputString_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (h_halt : cfg.state = none) (t : ℕ) : tm.outputString cfg t = []

From a halting configuration, a TM does not output anything.

theorem Turing.MultiTapeTM.outputString_add_eq_append {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t₁ t₂ : ℕ) : tm.outputString cfg (t₁ + t₂) = tm.outputString cfg t₁ ++ tm.outputString (configs cfg t₁) t₂

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} (tm : MultiTapeTM k Symbol State) {IOSymbol : Type u_3} (f : List IOSymbol → List IOSymbol) (toMachineSymbol : IOSymbol ↪ Symbol) (t s : ℕ → ℕ) : Prop

A proof that the Turing machine tm computes the function f such that on all inputs of length n it uses at most t n steps and s n space. It assumes an embedding function from the input/output alphabet into the machine alphabet. 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.ComputableInTimeAndSpace {IOSymbol : Type u_3} (f : List IOSymbol → List IOSymbol) (t s : ℕ → ℕ) : Prop

The main definition of complexity of multi-tape Turing machines: A proof that the function f is computable by some multi-tape Turing machine tm (with finite work alphabet and finite state set) via an alphabet embedding function toMachineSymbol, such that on all inputs of length n, tm uses at most t n steps and at most s n space.

Equations

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

noncomputable def Turing.MultiTapeTM.indicator {Symbol : Type u_3} [Inhabited Symbol] (L : Language Symbol) : List Symbol → List Symbol

The indicator function of a language.

Equations

• Turing.MultiTapeTM.indicator L x✝ = if x✝ ∈ L then [default] else []

def Turing.MultiTapeTM.DecidableInTimeAndSpace {IOSymbol : Type} [Inhabited IOSymbol] (L : Language IOSymbol) (t s : ℕ → ℕ) : Prop

A language is decidable in time t and space s if and only if its indicator function is computable in time t and space s.

Equations

• Turing.MultiTapeTM.DecidableInTimeAndSpace L t s = Turing.MultiTapeTM.ComputableInTimeAndSpace (Turing.MultiTapeTM.indicator L) t s

theorem Turing.MultiTapeTM.relatesInSteps_iff_configs_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 ↔ configs 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.

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

The Turing machine tm halts after exactly t steps on input input if its state is none at step t and non-none at step t - 1. Note that every Turing machine hast to perform at least one step to halt.

Equations

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

theorem Turing.MultiTapeTM.halting_step_unique {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {t₁ t₂ : ℕ} (h_halts₁ : tm.haltsAtStep input t₁ = true) (h_halts₂ : tm.haltsAtStep input t₂ = true) : t₁ = t₂

If a Turing machine halts, the time step is uniquely determined.