Reading the input from a work tape

inputFromTape tm behaves like tm, except that it reads its input from a work tape — the virtual input tape — instead of the real one, which it never touches. The virtual input head lives at cell p - 1 when the simulated input head is at position p, so the word cells 0, …, len - 1 are the input positions 1, …, len and the two boundary positions read the blanks at cells -1 and len.

The one thing a blank cell cannot tell the machine is which boundary it is at — and it must know, because the input head clamps there. This ambiguity is resolved by tracking a boundary classification. A second fresh work tape, the flag tape, moves in lockstep with the virtual input head and carries a single non-blank mark at cell -1, so the left boundary is recognised by reading the flag. Reading blank on both the virtual input tape and the flag tape means the right boundary.

The configuration map inCfg places the simulated input on the virtual input tape, places the marker on the flag tape, and leaves the real input tape unused. The main lemmas show that one step and an entire run path of the redirected machine mirror the corresponding step and run path of tm.

def Turing.MultiTapeTM.clampMove {Symbol : Type u_1} (wvip wflag : Option Symbol) (m : SignType) : SignType

The clamped move of the virtual input head: at the left boundary (blank under the virtual head, flag marked) left moves are blocked, at the right boundary (blank on both) right moves are.

noncomputable def Turing.MultiTapeTM.inputFromTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + 2) Symbol State

tm, reading its input from the virtual input tape Fin.natAdd k 0, with the flag tape Fin.natAdd k 1 marking the cell left of the input. The real input tape is never read and never moved.

def Turing.MultiTapeTM.inCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (mark : Symbol) {input : List Symbol} (c : Cfg k Symbol State input) (outerInput : List Symbol) : Cfg (k + 2) Symbol State outerInput

A configuration of tm on input, as the redirecting machine sees it, over an arbitrary ambient input: input sits on the virtual input tape with the head at cell inputPos - 1, the flag tape carries its mark at -1 with its head in lockstep, and the ambient input head rests at 1.

@[simp]

theorem Turing.MultiTapeTM.inCfg_inputPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) : (inCfg mark c outerInput).inputPos = 1

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapes_castAdd {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) (j : Fin k) : (inCfg mark c outerInput).workTapes (Fin.castAdd 2 j) = c.workTapes j

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapes_vip {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) : (inCfg mark c outerInput).workTapes (Fin.natAdd k 0) = tapeOfList input

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapes_flag {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) : (inCfg mark c outerInput).workTapes (Fin.natAdd k 1) = Function.update (fun (x : ℤ) => none) (-1) (some mark)

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapePos_castAdd {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) (j : Fin k) : (inCfg mark c outerInput).workTapePos (Fin.castAdd 2 j) = c.workTapePos j

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapePos_natAdd {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) (i : Fin 2) : (inCfg mark c outerInput).workTapePos (Fin.natAdd k i) = ↑↑c.inputPos - 1

The virtual input head and the flag head both stand at cell inputPos - 1.

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapeSymbols_castAdd {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) (j : Fin k) : (inCfg mark c outerInput).workTapeSymbols (Fin.castAdd 2 j) = c.workTapeSymbols j

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapeSymbols_vip {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) : (inCfg mark c outerInput).workTapeSymbols (Fin.natAdd k 0) = c.inputSymbol

The virtual input head reads exactly what the simulated input head reads: the word cells are the input positions, the two boundary cells are blank.

@[simp]

theorem Turing.MultiTapeTM.inCfg_workTapeSymbols_flag {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {mark : Symbol} {input outerInput : List Symbol} (c : Cfg k Symbol State input) : (inCfg mark c outerInput).workTapeSymbols (Fin.natAdd k 1) = if ↑c.inputPos = 0 then some mark else none

The flag head reads the mark exactly at the left boundary.

theorem Turing.MultiTapeTM.val_moveInputPos_sub_one_eq_clampMove {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (mark : Symbol) (c : Cfg k Symbol State input) (m : SignType) : ↑↑(moveInputPos c.inputPos m) - 1 = ↑↑c.inputPos - 1 + ↑(clampMove c.inputSymbol (if ↑c.inputPos = 0 then some mark else none) m)

The clamped move of the virtual input head tracks the simulated input head exactly.

theorem Turing.MultiTapeTM.step_inCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (mark : Symbol) (outerInput : List Symbol) : Function.Semiconj (fun (x : Cfg k Symbol State input) => inCfg mark x outerInput) step step

The redirection is a step-semiconjugation. One step of the machine reading its input from the virtual tape mirrors one step of the original, under the embedding inCfg.

noncomputable def Turing.MultiTapeTM.inCfgHom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (mark : Symbol) (outerInput : List Symbol) : (tm.stepRel input).Hom (tm.inputFromTape.stepRel outerInput)

The redirection preserves steps, so it maps run paths of tm to run paths of the redirected machine.

@[simp]

theorem Turing.MultiTapeTM.inCfgHom_apply {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (mark : Symbol) (outerInput : List Symbol) (x✝ : Cfg k Symbol State input) : (tm.inCfgHom mark outerInput) x✝ = inCfg mark x✝ outerInput

theorem Turing.MultiTapeTM.space_map_inCfgHom_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (mark : Symbol) (outerInput : List Symbol) (p : tm.RunPath input) : (p.map (tm.inCfgHom mark outerInput)).space ≤ p.space + 2 * (input.length + 2)

Space of the input-redirected path. The k inner tapes visit exactly what the original path visits; the two extra tapes (virtual input, flag) each move only with the simulated input head, which stays within [-1, input.length], so they add at most 2 * (input.length + 2).