Writing the output as a word on a work tape

The additions of cslib PR #1111 to Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToTape.

outputToWord tm runs tm with its output redirected to a new last work tape (Turing.MultiTapeTM.outputToTape), then moves the head of that tape back to cell 0 (Turing.MultiTapeTM.rewindWork). If tm computes output tidily (Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace), then outputToWord tm takes blank work tapes to blank work tapes, except that the last one holds output, and emits nothing.

Main definitions

• Turing.MultiTapeTM.outputToWord: the machine writing its output as a word on a work tape.

Main results

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.outputToWord: its specification.
• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.outputToWord_extendTapes: preserve unselected tapes while writing the output.
• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.outputToWord_onTape: the blank-tape case.

Rewinding the output tape

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

tm with its output written to a new last work tape, whose head is then moved back to cell 0.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.outputToWord {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) : tm.outputToWord.TransformsTapes (fun (inp : List Symbol) (ws : Fin (k + 1) → List Symbol) => inp = input ∧ ws = fun (x : Fin (k + 1)) => []) (fun (x : List Symbol) (x_1 ws' : Fin (k + 1) → List Symbol) (e : List Symbol) => ws' = Function.update (fun (x : Fin (k + 1)) => []) (Fin.last k) output ∧ e = []) (t + output.length + 2) (s + 2 * output.length + k + 4)

If tm computes output tidily, then outputToWord tm, started on blank work tapes, halts with output on its last work tape, every other work tape blank, and nothing emitted.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.outputToWord_extendTapes {k n : ℕ} {Symbol : Type u_3} {State : Type u_4} {machine : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (h : machine.ComputesTidilyInTimeAndSpace input output t s) (e : Fin (k + 1) ↪ Fin n) : (machine.outputToWord.extendTapes e).TransformsTapes (fun (inp : List Symbol) (ws : Fin n → List Symbol) => inp = input ∧ ∀ (j : Fin (k + 1)), ws (e j) = []) (fun (x : List Symbol) (ws ws' : Fin n → List Symbol) (emitted : List Symbol) => ws' = Function.update ws (e (Fin.last k)) output ∧ emitted = []) (t + output.length + 2) (s + 2 * output.length + k + 4 + (n - (k + 1)))

A tidy computation writes its output on the selected last tape, leaves its selected scratch tapes blank, and preserves all unselected words. All selected tapes must initially be blank.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.outputToWord_onTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s K : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) {e : Fin (k + 1) ↪ Fin K} {V : Fin K} (he : e (Fin.last k) = V) : (tm.outputToWord.extendTapes e).TransformsTapes (fun (inp : List Symbol) (ws : Fin K → List Symbol) => inp = input ∧ ws = fun (x : Fin K) => []) (fun (x : List Symbol) (x_1 ws' : Fin K → List Symbol) (em : List Symbol) => ws' = Function.update (fun (x : Fin K) => []) V output ∧ em = []) (t + output.length + 2) (s + 2 * output.length + k + 4 + (K - (k + 1)))

Write a tidy computation's output to a selected tape, leaving every other tape blank.