Simulation of SingleTapeTM by MultiTapeTM

This file simulates any single-tape Turing machine (Cslib.Turing.SingleTapeTM Symbol) on a 1-work-tape multi-tape Turing machine (Turing.MultiTapeTM 1 Symbol ...) in three sequential phases:

1. copyInputToWork: copy the read-only input x onto work tape 0 and rewind work tape 0 to cell 0 in 2 * x.length + 4 steps (reusing InputReader.appendOne).
2. runOnWork: execute the single-tape transitions of tm directly on work tape 0. By BiTape.Represents.step, n steps of tm correspond to n steps of runOnWork tm.
3. emitWork: starting from the final head position on work tape 0, walk right and emit each non-blank symbol to the output tape until the first blank cell, taking y.length + 1 steps when the final tape represents BiTape.mk₁ y.

Main definitions

• Turing.MultiTapeTM.copyInputToWork: copy the input tape to work tape 0 and rewind to 0.
• Turing.MultiTapeTM.runOnWork: run a SingleTapeTM on work tape 0.
• Turing.MultiTapeTM.emitWork: emit the word on work tape 0 to the output tape until blank.
• Turing.MultiTapeTM.ofSingleTapeTM: the composed 3-phase MultiTapeTM 1 Symbol simulating a SingleTapeTM Symbol.

Main results

• Turing.MultiTapeTM.computesInTimeAndSpace_ofSingleTapeTM: if tm.OutputsWithinTime x y t, then ofSingleTapeTM tm computes y from x in 2 * x.length + 4 + (t + (y.length + 1)) steps (and in 3 * x.length + 2 * t + 6 steps).
• Turing.MultiTapeTM.computes_ofSingleTapeTM: if tm.Outputs x y, then (ofSingleTapeTM tm).Computes x y.
• Cslib.Turing.SingleTapeTM.TimeComputable.computableInTimeAndSpace: transfers SingleTapeTM.TimeComputable to MultiTapeTM.ComputableInTimeAndSpace.
• Cslib.Turing.SingleTapeTM.PolyTimeComputable.computableTidilyInPolyTime: transfers SingleTapeTM.PolyTimeComputable to MultiTapeTM.ComputableTidilyInPolyTime.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation

Phase 1: Copy input to work tape 0 and rewind

def Turing.MultiTapeTM.copyReader (Symbol : Type u_1) : InputReader Symbol Unit

The InputReader that copies every input symbol verbatim.

@[simp]

theorem Turing.MultiTapeTM.copyReader_q₀ (Symbol : Type u_1) : (copyReader Symbol).q₀ = ()

@[simp]

theorem Turing.MultiTapeTM.copyReader_read (Symbol : Type u_1) (w : List Symbol) : (copyReader Symbol).read () w = (w, w.length)

@[reducible, inline]

abbrev Turing.MultiTapeTM.CopyInputState : Type

State type of copyInputToWork.

noncomputable def Turing.MultiTapeTM.copyInputToWork (Symbol : Type u_1) : MultiTapeTM 1 Symbol CopyInputState

Phase 1 machine: copies the input tape onto work tape 0 and rewinds work tape 0 to cell 0.

theorem Turing.MultiTapeTM.runFrom_copyInputToWork {Symbol : Type} (x : List Symbol) : ∃ (p' : Fin (x.length + 2)), runFrom ((copyInputToWork Symbol).initCfg x) (2 * x.length + 4) = { state := none, inputPos := p', workTapes := fun (x_1 : Fin 1) => tapeOfList x, workTapePos := fun (x : Fin 1) => 0, output := [] }

theorem Turing.MultiTapeTM.represents_tapeOfList {Symbol : Type} (xs : List Symbol) : (Cslib.Turing.BiTape.mk₁ xs).Represents (tapeOfList xs) 0

BiTape.mk₁ xs represents tapeOfList xs with head at 0.

Phase 2: Run SingleTapeTM transitions on work tape 0

def Turing.MultiTapeTM.dirToSign : Option Dir → SignType

Convert an optional Turing.Dir to a SignType head movement.

theorem Turing.MultiTapeTM.biTape_step_dirToSign {Symbol : Type} (t : Cslib.Turing.BiTape Symbol) (wr : Option Symbol) (dir : Option Dir) : t.step (some wr, dirToSign dir) = (t.write wr).optionMove dir

def Turing.MultiTapeTM.runOnWork {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) : MultiTapeTM 1 Symbol tm.State

Phase 2 machine: executes the transitions of tm : SingleTapeTM Symbol on work tape 0, leaving the input head and output tape untouched.

structure Turing.MultiTapeTM.SimRel {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) {input : List Symbol} (scfg : tm.Cfg) (mcfg : Cfg 1 Symbol tm.State input) : Prop

Simulation relation between a SingleTapeTM configuration and a 1-work-tape MultiTapeTM configuration.

• state : mcfg.state = scfg.state
• work : scfg.BiTape.Represents (mcfg.workTapes 0) (mcfg.workTapePos 0)

theorem Turing.MultiTapeTM.SimRel.step {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {tm : Cslib.Turing.SingleTapeTM Symbol} {input : List Symbol} {scfg scfg' : tm.Cfg} {mcfg : Cfg 1 Symbol tm.State input} (hsim : SimRel tm scfg mcfg) (hstep : tm.TransitionRelation scfg scfg') : SimRel tm scfg' (MultiTapeTM.step mcfg) ∧ (MultiTapeTM.step mcfg).output = mcfg.output

theorem Turing.MultiTapeTM.SimRel.runFrom_of_relatesInSteps {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {tm : Cslib.Turing.SingleTapeTM Symbol} {input : List Symbol} {scfg₁ scfg₂ : tm.Cfg} {mcfg₁ : Cfg 1 Symbol tm.State input} {n : ℕ} (hsim : SimRel tm scfg₁ mcfg₁) (hrel : Relation.RelatesInSteps tm.TransitionRelation scfg₁ scfg₂ n) : SimRel tm scfg₂ (runFrom mcfg₁ n) ∧ (runFrom mcfg₁ n).output = mcfg₁.output

theorem Turing.MultiTapeTM.runFrom_runOnWork_of_outputsWithinTime {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) {input x y : List Symbol} {t : ℕ} {mcfg : Cfg 1 Symbol tm.State input} (hstate : mcfg.state = some tm.q₀) (hwork : (Cslib.Turing.BiTape.mk₁ x).Represents (mcfg.workTapes 0) (mcfg.workTapePos 0)) (hout : tm.OutputsWithinTime x y t) : (runFrom mcfg t).state = none ∧ (Cslib.Turing.BiTape.mk₁ y).Represents ((runFrom mcfg t).workTapes 0) ((runFrom mcfg t).workTapePos 0) ∧ (runFrom mcfg t).output = mcfg.output

Phase 3: Emit work tape 0 until blank

def Turing.MultiTapeTM.emitWork (Symbol : Type u_1) : MultiTapeTM 1 Symbol Unit

Phase 3 machine: walks right along work tape 0, emitting each symbol to the output tape, and halts on the first blank cell.

theorem Turing.MultiTapeTM.EmitWork.runFrom_walk {Symbol : Type} {input : List Symbol} {inpos : Fin (input.length + 2)} {y : List Symbol} {contents : ℤ → Option Symbol} {head : ℤ} (hrep : (Cslib.Turing.BiTape.mk₁ y).Represents contents head) (out : List Symbol) (n : ℕ) (hn : n ≤ y.length) : runFrom { state := some (), inputPos := inpos, workTapes := fun (x : Fin 1) => contents, workTapePos := fun (x : Fin 1) => head, output := out } n = { state := some (), inputPos := inpos, workTapes := fun (x : Fin 1) => contents, workTapePos := fun (x : Fin 1) => head + ↑n, output := out ++ List.take n y }

theorem Turing.MultiTapeTM.runFrom_emitWork {Symbol : Type} {input y : List Symbol} (mcfg : Cfg 1 Symbol Unit input) (hstate : mcfg.state = some ()) (hrep : (Cslib.Turing.BiTape.mk₁ y).Represents (mcfg.workTapes 0) (mcfg.workTapePos 0)) : (runFrom mcfg (y.length + 1)).state = none ∧ (runFrom mcfg (y.length + 1)).output = mcfg.output ++ y

Composed 3-phase SingleTapeTM simulator

@[reducible, inline]

abbrev Turing.MultiTapeTM.OfSingleTapeState {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) : Type

State type of ofSingleTapeTM tm.

noncomputable def Turing.MultiTapeTM.ofSingleTapeTM {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) : MultiTapeTM 1 Symbol (OfSingleTapeState tm)

Simulate a SingleTapeTM Symbol on a 1-work-tape MultiTapeTM: copy input to work tape 0, run tm on work tape 0, and emit work tape 0 to output.

theorem Turing.MultiTapeTM.runFrom_ofSingleTapeTM_of_outputsWithinTime {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) {x y : List Symbol} {t : ℕ} (h : tm.OutputsWithinTime x y t) : have T := 2 * x.length + 4 + (t + (y.length + 1)); (runFrom ((ofSingleTapeTM tm).initCfg x) T).Halted ∧ (runFrom ((ofSingleTapeTM tm).initCfg x) T).output = y

theorem Turing.MultiTapeTM.computesInTimeAndSpace_ofSingleTapeTM {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) {x y : List Symbol} {t : ℕ} (h : tm.OutputsWithinTime x y t) : have T := 2 * x.length + 4 + (t + (y.length + 1)); (ofSingleTapeTM tm).ComputesInTimeAndSpace x y T (T + 1)

If tm.OutputsWithinTime x y t, then ofSingleTapeTM tm computes y from x in 2 * x.length + 4 + (t + (y.length + 1)) steps.

theorem Turing.MultiTapeTM.computesInTimeAndSpace_ofSingleTapeTM_of_input {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) {x y : List Symbol} {t : ℕ} (h : tm.OutputsWithinTime x y t) : have T := 3 * x.length + 2 * t + 6; (ofSingleTapeTM tm).ComputesInTimeAndSpace x y T (T + 1)

Input-only time bound for ofSingleTapeTM tm: since y.length ≤ max 1 x.length + t, 3 * x.length + 2 * t + 6 steps always suffice.

theorem Turing.MultiTapeTM.computes_ofSingleTapeTM {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : Cslib.Turing.SingleTapeTM Symbol) {x y : List Symbol} (h : tm.Outputs x y) : (ofSingleTapeTM tm).Computes x y

If tm.Outputs x y, then (ofSingleTapeTM tm).Computes x y.

theorem Turing.MultiTapeTM.computesInTimeAndSpace_ofTM0 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] [DecidableEq Λ] (M : TM0.Machine (Option Symbol) Λ) (S : Finset Λ) (hs : TM0.Supports M ↑S) {x y : List Symbol} {t : ℕ} {q_f : Λ} (hreach : Relation.RelatesWithinSteps (fun (a b : TM0.Cfg (Option Symbol) Λ) => b ∈ TM0.step M a) (TM0.init (List.map some x)) { q := q_f, Tape := Cslib.Turing.BiTape.equivTape (Cslib.Turing.BiTape.mk₁ y) } t) (hhalt : TM0.step M { q := q_f, Tape := Cslib.Turing.BiTape.equivTape (Cslib.Turing.BiTape.mk₁ y) } = none) : have T := 2 * x.length + 4 + (t + 1 + (y.length + 1)); (ofSingleTapeTM (Cslib.Turing.SingleTapeTM.ofTM0 M S hs)).ComputesInTimeAndSpace x y T (T + 1)

Any Mathlib TM0.Machine supported on S is simulated on a 1-work-tape MultiTapeTM in 2 * x.length + 4 + ((t + 1) + (y.length + 1)) steps.

theorem Turing.MultiTapeTM.computes_ofTM0 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] [DecidableEq Λ] (M : TM0.Machine (Option Symbol) Λ) (S : Finset Λ) (hs : TM0.Supports M ↑S) {x y : List Symbol} {q_f : Λ} (h : { q := q_f, Tape := Cslib.Turing.BiTape.equivTape (Cslib.Turing.BiTape.mk₁ y) } ∈ StateTransition.eval (TM0.step M) (TM0.init (List.map some x))) : (ofSingleTapeTM (Cslib.Turing.SingleTapeTM.ofTM0 M S hs)).Computes x y

Any Mathlib TM0.Machine supported on S is simulated on a 1-work-tape MultiTapeTM.

theorem Cslib.Turing.SingleTapeTM.TimeComputable.computesFunInTimeAndSpace {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {α : Type u_1} {β : Type u_2} {f : List Symbol → List Symbol} (hf : TimeComputable f) (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (g : α → β) (hfg : ∀ (a : α), f (encIn a) = encOut (g a)) : (Turing.MultiTapeTM.ofSingleTapeTM hf.tm).ComputesFunInTimeAndSpace encIn encOut g (fun (a : α) => 3 * (encIn a).length + 2 * hf.timeBound (encIn a).length + 6) fun (a : α) => 3 * (encIn a).length + 2 * hf.timeBound (encIn a).length + 7

A SingleTapeTM.TimeComputable function is computed by ofSingleTapeTM hf.tm in 3 * n + 2 * hf.timeBound n + 6 steps.

theorem Cslib.Turing.SingleTapeTM.TimeComputable.computableInTimeAndSpace {α : Type u_1} {β : Type u_2} {f : List Bool → List Bool} (hf : TimeComputable f) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (g : α → β) (hfg : ∀ (a : α), f (encIn a) = encOut (g a)) : Turing.MultiTapeTM.ComputableInTimeAndSpace g encIn encOut (fun (a : α) => 3 * (encIn a).length + 2 * hf.timeBound (encIn a).length + 6) fun (a : α) => 3 * (encIn a).length + 2 * hf.timeBound (encIn a).length + 7

A SingleTapeTM.TimeComputable function over Bool gives MultiTapeTM.ComputableInTimeAndSpace.

theorem Cslib.Turing.SingleTapeTM.PolyTimeComputable.computableTidilyInPolyTime {α : Type u_1} {β : Type u_2} {f : List Bool → List Bool} (hf : PolyTimeComputable f) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (g : α → β) (hfg : ∀ (a : α), f (encIn a) = encOut (g a)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime g encIn encOut

A SingleTapeTM.PolyTimeComputable function over Bool is tidily computable in polynomial time on a multi-tape Turing machine (MultiTapeTM.ComputableTidilyInPolyTime).

theorem Cslib.Turing.SingleTapeTM.PolyTimeComputable.computableTidilyInPolyTime_id {f : List Bool → List Bool} (hf : PolyTimeComputable f) : Turing.MultiTapeTM.ComputableTidilyInPolyTime f (Function.Embedding.refl (List Bool)) (Function.Embedding.refl (List Bool))

Special case of PolyTimeComputable.computableTidilyInPolyTime for f : List Bool → List Bool under the identity encoding.