Redirecting the output to a work tape

outputToTape tm behaves like tm, except that whatever tm would append to the write-only output tape is written on a fresh work tape instead, whose head always stands at the write frontier.

Since the output is append-only, the frontier position is a function of the configuration — the length of the output so far — so the redirected machine mirrors the original through the configuration map outCfg. 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.

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

tm, with its output writes redirected onto a fresh last work tape, whose head always stands at the write frontier.

def Turing.MultiTapeTM.outCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : Cfg (k + 1) Symbol State input

A configuration of tm, as the redirected machine sees it: the output so far sits on the last work tape with the head at its end, and the real output is empty.

@[simp]

theorem Turing.MultiTapeTM.outCfg_inputSymbol {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : (outCfg c).inputSymbol = c.inputSymbol

@[simp]

theorem Turing.MultiTapeTM.outCfg_workTapes_last {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : (outCfg c).workTapes (Fin.last k) = tapeOfList c.output

@[simp]

theorem Turing.MultiTapeTM.outCfg_workTapes_castSucc {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (j : Fin k) : (outCfg c).workTapes j.castSucc = c.workTapes j

@[simp]

theorem Turing.MultiTapeTM.outCfg_workTapePos_last {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : (outCfg c).workTapePos (Fin.last k) = ↑c.output.length

@[simp]

theorem Turing.MultiTapeTM.outCfg_workTapePos_castSucc {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (j : Fin k) : (outCfg c).workTapePos j.castSucc = c.workTapePos j

@[simp]

theorem Turing.MultiTapeTM.outCfg_workTapeSymbols_castSucc {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) (j : Fin k) : (outCfg c).workTapeSymbols j.castSucc = c.workTapeSymbols j

theorem Turing.MultiTapeTM.step_outCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) : Function.Semiconj outCfg step step

The redirection is a step-semiconjugation.

noncomputable def Turing.MultiTapeTM.outCfgHom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) : (tm.stepRel input).Hom (tm.outputToTape.stepRel input)

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

@[simp]

theorem Turing.MultiTapeTM.outCfgHom_apply {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) : tm.outCfgHom c = outCfg c

theorem Turing.MultiTapeTM.initCfg_outputToTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) : tm.outputToTape.initCfg input = outCfg (tm.initCfg input)

The initial configuration of the redirected machine is the original's through outCfg.

theorem Turing.MultiTapeTM.space_map_outCfgHom_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (p : tm.RunPath input) : (p.map tm.outCfgHom).space ≤ p.space + ((RelSeries.last p).output.length + 1)

Space of the output-redirected path. The k inner tapes visit exactly what the original path visits, and the frontier head only walks up to the final length of the output, so the redirection costs at most the final output length plus one.