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 of the redirected machine mirror the corresponding step and run 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.

Equations

• Turing.MultiTapeTM.clampMove (some val) wflag m = m
• Turing.MultiTapeTM.clampMove none (some val) SignType.neg = SignType.zero
• Turing.MultiTapeTM.clampMove none (some val) m = m
• Turing.MultiTapeTM.clampMove none none SignType.pos = SignType.zero
• Turing.MultiTapeTM.clampMove none none m = m

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.

Equations

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

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.

Equations

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

@[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) (c : Cfg k Symbol State input) (outerInput : List Symbol) : step (inCfg mark c outerInput) = inCfg mark (step c) outerInput

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.

theorem Turing.MultiTapeTM.runFrom_inCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (mark : Symbol) (c : Cfg k Symbol State input) (outerInput : List Symbol) (n : ℕ) : runFrom (inCfg mark c outerInput) n = inCfg mark (runFrom c n) outerInput

The redirected run mirrors the original.

theorem Turing.MultiTapeTM.spaceUsed_inputFromTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (mark : Symbol) (c : Cfg k Symbol State input) (outerInput : List Symbol) (n : ℕ) : spaceUsed (inCfg mark c outerInput) n ≤ spaceUsed c n + 2 * (input.length + 2)

Space of the input-redirected machine. The k inner tapes visit exactly what the original does; 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).