Deterministic Multi-Tape Turing Machines

A deterministic Turing machine is a nondeterministic machine whose transition relation has exactly one action for every combination of state and symbols read. From the transition relation it derives a transition function tr and a function step which maps each configuration to its unique successor configuration (a halted configuration maps to itself).

The design choices for configurations and actions are documented in Cslib.Computability.Machines.Turing.MultiTape.Configuration.

Important Declarations

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

• MultiTapeNTM.IsDeterministic: the transition relation relates every state and tuple of read symbols to exactly one action
• MultiTapeTM: the TM itself
• tr, ofTr: the derived transition function and construction from a function
• step, runFrom: the successor configuration and iteration of this function
• MultiTapeNTM.RunPath.ofDeterministic, MultiTapeNTM.ComputationPath.ofDeterministic: paths of a given length from an arbitrary or initial configuration
• space: the space of the path of the first t steps from a configuration
• Computes: the machine halts with the given output on an input
• ComputesInTimeAndSpace: the machine produces an output within the shared resource bounds
• ComputesFunInTimeAndSpace: function computation with the shared time and space bounds
• 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.

def Turing.MultiTapeNTM.IsDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) : Prop

Every state and tuple of read symbols is related to exactly one action by ntm's transition relation.

structure Turing.MultiTapeTM (k : ℕ) (Symbol : Type u_3) (State : Type u_4) extends Turing.MultiTapeNTM k Symbol State : 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
• Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) (action : Action k Symbol State) : Prop
• deterministic : self.IsDeterministic

  Every state and tuple of read symbols is related to exactly one action by the transition relation.

@[instance_reducible]

instance Turing.instCoeOutMultiTapeTMMultiTapeNTM {k : ℕ} {State : Type u_1} {Symbol : Type u_2} : CoeOut (MultiTapeTM k Symbol State) (MultiTapeNTM k Symbol State)

noncomputable def Turing.MultiTapeTM.tr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : Action k Symbol State

The unique action related to the given state and read symbols by Tr.

@[simp]

theorem Turing.MultiTapeTM.tr_iff {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {q : State} {input : Option Symbol} {work : Fin k → Option Symbol} {action : Action k Symbol State} : tm.Tr q input work action ↔ tm.tr q input work = action

Tr relates a state and read symbols to an action exactly when tr returns that action.

def Turing.MultiTapeTM.ofTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) : MultiTapeTM k Symbol State

Construct a deterministic machine from an initial state and transition function.

@[simp]

theorem Turing.MultiTapeTM.q₀_ofTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) : (ofTr q₀ tr).q₀ = q₀

The initial state of ofTr is the supplied one.

@[simp]

theorem Turing.MultiTapeTM.tr_ofTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : (ofTr q₀ tr).tr q input work = tr q input work

Extracting the transition of ofTr recovers the supplied function.

Stepping a Turing Machine

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

noncomputable 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 unique successor configuration related to cfg by the inherited step relation.

@[simp]

theorem Turing.MultiTapeTM.step_iff {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ step c = c'

Step relates c to c' exactly when step c = c'.

theorem Turing.MultiTapeTM.step_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

A running configuration takes the action selected by the transition function.

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.

@[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.stepHom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : Cfg k Symbol State input → Cfg k' Symbol State' input') (h : Function.Semiconj f step step) : (tm.stepRel input).Hom (tm'.stepRel input')

A configuration map semiconjugating the step functions is a homomorphism of the step relations, so it maps run paths with RelSeries.map.

def Turing.MultiTapeTM.runningStepHom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : Cfg k Symbol State input → Cfg k' Symbol State' input') (h : ∀ (c : Cfg k Symbol State input), ¬c.Halted → step (f c) = f (step c)) : (tm.runningStepRel input).Hom (tm'.stepRel input')

A configuration map commuting with the step functions on running configurations is a homomorphism from the running steps of tm to the steps of tm'.

@[simp]

theorem Turing.MultiTapeTM.runningStepHom_apply {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : Cfg k Symbol State input → Cfg k' Symbol State' input') (h : ∀ (c : Cfg k Symbol State input), ¬c.Halted → step (f c) = f (step c)) (a✝ : Cfg k Symbol State input) : (runningStepHom f h) a✝ = f a✝

noncomputable def Turing.MultiTapeNTM.RunPath.ofDeterministic {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.RunPath input

The path of the first t steps from cfg.

theorem Turing.MultiTapeNTM.RunPath.eq_ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.RunPath input) : p = ofDeterministic tm (RelSeries.head p) p.time

Every deterministic run path is the canonical path from its head for its duration.

noncomputable def Turing.MultiTapeNTM.ComputationPath.ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : tm.ComputationPath input

The path of the first t steps on input, starting at the initial configuration.

theorem Turing.MultiTapeNTM.ComputationPath.eq_ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.ComputationPath input) : p = ofDeterministic tm input p.time

Every deterministic computation path is the canonical path for its duration.

theorem Turing.MultiTapeNTM.RunPath.map_ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : (tm.stepRel input).Hom (tm'.stepRel input')) (cfg : Cfg k Symbol State input) (t : ℕ) : (ofDeterministic tm cfg t).map f = ofDeterministic tm' (f cfg) t

A step-preserving map sends the path of t steps from cfg to the path of t steps from the image of cfg.

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

theorem Turing.MultiTapeTM.runPath_apply_eq_runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.RunPath input) (i : Fin (p.length + 1)) : p.toFun i = runFrom (RelSeries.head p) ↑i

Every path of a deterministic machine follows its iterated step function.

theorem Turing.MultiTapeTM.computationPath_last_eq_runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.ComputationPath input) : p.last = runFrom (tm.initCfg input) p.time

A deterministic computation ends at the corresponding iterate.

theorem Turing.MultiTapeTM.runFrom_map {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : (tm.stepRel input).Hom (tm'.stepRel input')) (cfg : Cfg k Symbol State input) (t : ℕ) : runFrom (f cfg) t = f (runFrom cfg t)

Running from the image of a configuration under a step-preserving map reaches the image of the original run.

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.

theorem Turing.MultiTapeTM.runsInTime_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {t : ℕ} (h : (runFrom (tm.initCfg input) t).Halted) : tm.RunsInTime input t

A deterministic machine halted after t steps satisfies the shared time bound.

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.

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

noncomputable 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 visited by the head of tape i in the computation starting from configuration cfg up to step t.

@[reducible, inline]

noncomputable abbrev Turing.MultiTapeTM.space {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 visited in the first t steps from cfg: the space of the path of these steps.

@[simp]

theorem Turing.MultiTapeTM.space_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) : space cfg t = 0

A zero-tape Turing machine uses zero space.

theorem Turing.MultiTapeTM.spaceUsedByTape_le_space {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 ≤ space cfg t

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

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.

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

The machine eventually halts on input with the given output.

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

The machine computes output from input within the shared time and space bounds.

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

The machine computes f relative to given encodings within the given time and space bounds.

theorem Turing.MultiTapeTM.ComputesFunInTimeAndSpace.mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {α : Type u_3} {β : Type u_4} {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.

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

Computability by a deterministic machine with a binary tape alphabet and finitely many states, within the supplied input-indexed bounds.

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

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.

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

The Boolean indicator function of a set.

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 computable in those bounds.

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.