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
• HaltsAt: the run from a configuration halts at exactly a given step
• spaceUsed: the number of tape cells visited by work tape heads, our main space measure
• 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.

Equations

• ntm.IsDeterministic = ∀ (q : State) (input : Option Symbol) (work : Fin k → Option Symbol), ∃! action : Turing.Action k Symbol State, ntm.Tr q input work action

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)

Equations

• Turing.instCoeOutMultiTapeTMMultiTapeNTM = { coe := Turing.MultiTapeTM.toMultiTapeNTM }

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.

Equations

• tm.tr q input work = Exists.choose ⋯

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

Equations

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

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

Equations

• Turing.MultiTapeTM.step cfg = Exists.choose ⋯

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

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.

Equations

• Turing.MultiTapeNTM.RunPath.ofDeterministic tm cfg t = { length := t, toFun := fun (n : Fin (t + 1)) => Turing.MultiTapeTM.step^[↑n] cfg, step := ⋯ }

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.

Equations

• Turing.MultiTapeNTM.ComputationPath.ofDeterministic tm input t = { toRunPath := Turing.MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) t, head_eq := ⋯ }

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.

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.

Equations

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

theorem Turing.MultiTapeTM.runFrom_succ {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : runFrom cfg (t + 1) = step (runFrom cfg t)

One more step of a run.

theorem Turing.MultiTapeTM.runFrom_add {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (m n : ℕ) : runFrom cfg (m + n) = runFrom (runFrom cfg m) n

A run splits at any intermediate step.

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

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.

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.

Equations

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

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.

Equations

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

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

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.

Equations

• tm.Computes input output = ∃ (u : ℕ), (Turing.MultiTapeTM.runFrom (tm.initCfg input) u).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg input) u).output = 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.

Equations

• tm.ComputesInTimeAndSpace input output t s = (tm.Computes input output ∧ tm.RunsInTime input t ∧ tm.RunsInSpace input s)

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.

Equations

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

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.

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

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

Equations

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

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.