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

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_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) (c : Cfg k Symbol State input) : step (outCfg c) = outCfg (step c)

The redirection is a step-semiconjugation.

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

The redirected run mirrors the original.

theorem Turing.MultiTapeTM.step_outputToTape_withOutput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg (k + 1) Symbol State input) (out : List Symbol) : step (c.withOutput out) = (step c).withOutput out

outputToTape tm never writes the real output, so replacing it commutes with a step.

theorem Turing.MultiTapeTM.runFrom_outputToTape_withOutput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg (k + 1) Symbol State input) (out : List Symbol) (n : ℕ) : runFrom (c.withOutput out) n = (runFrom c n).withOutput out

The redirected run commutes with the real output already present.

theorem Turing.MultiTapeTM.spaceUsed_outputToTape_withOutput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg (k + 1) Symbol State input) (out : List Symbol) (u : ℕ) : spaceUsed (c.withOutput out) u = spaceUsed c u

outputToTape's space does not depend on the real output already present.

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.spaceUsed_outputToTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) (u : ℕ) : spaceUsed (outCfg c) u ≤ spaceUsed c u + ((runFrom c u).output.length + 1)

Space of the output-redirected machine. The k inner tapes visit exactly what the original does, and the frontier head only walks between the initial and the final length of the output, so the redirection costs at most the final output length plus one.