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, a homomorphism of step relations (outCfgHom), so each run path of tm maps to a run path of the redirected machine.

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.

Equations

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

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.

Equations

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

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

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.

Equations

• tm.outCfgHom = ⋯.stepHom Turing.MultiTapeTM.outCfg ⋯ ⋯ ⋯

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