Running a tidy computation on work tapes

onWords tm mark reads its input as a word on one work tape and writes the output of tm as a word on another, leaving every other tape alone. It is tm with its output redirected to a new work tape (Turing.MultiTapeTM.outputToWord) and its input read from another new work tape (Turing.MultiTapeTM.inputFromWord).

Its k + 1 + 2 work tapes are the k work tapes of tm, the output work tape (Fin.last k).castAdd 2, the input work tape Fin.natAdd (k + 1) 0, and the flag tape of inputFromWord.

Main definitions

• Turing.MultiTapeTM.onWords: the composed machine.

Main results

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.onWords_extendTapes: run between two selected tapes with exact time and space overheads.

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.onWords: if tm computes output from input tidily, then onWords tm mark takes input on its input work tape to output on its output work tape.

• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.exists_onWords: a tidily computable function is computed by a machine that reads its input from one work tape and writes its output to another.

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

tm, with its output written to a new work tape and its input read from another, using mark to flag the left end of the input. The output work tape is (Fin.last k).castAdd 2, the input work tape Fin.natAdd (k + 1) 0.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.onWords {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (mark : Symbol) (h : tm.ComputesTidilyInTimeAndSpace input output t s) : (tm.onWords mark).TransformsTapes (fun (x : List Symbol) (ws : Fin (k + 1 + 2) → List Symbol) => ws = Function.update (fun (x : Fin (k + 1 + 2)) => []) (Fin.natAdd (k + 1) 0) input) (fun (x : List Symbol) (ws ws' : Fin (k + 1 + 2) → List Symbol) (emitted : List Symbol) => ws' = Function.update ws (Fin.castAdd 2 (Fin.last k)) output ∧ emitted = []) (t + output.length + 6) (s + 2 * input.length + 2 * output.length + 3 * k + 18)

If tm computes output from input tidily, then onWords tm mark, started with input on its input work tape and all other work tapes blank, halts with output on its output work tape, every other work tape unchanged, and nothing emitted.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.exists_onWords {α : Type u_3} {β : Type u_4} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableTidilyInTimeAndSpace f encIn encOut t s) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM (k + 1 + 2) Bool State) (i : Fin (k + 1 + 2)) (o : Fin (k + 1 + 2)), i ≠ o ∧ ∀ (a : α), tm.TransformsTapes (fun (x : List Bool) (ws : Fin (k + 1 + 2) → List Bool) => ws = Function.update (fun (x : Fin (k + 1 + 2)) => []) i (encIn a)) (fun (x : List Bool) (ws ws' : Fin (k + 1 + 2) → List Bool) (emitted : List Bool) => ws' = Function.update ws o (encOut (f a)) ∧ emitted = []) (t a + (encOut (f a)).length + 6) (s a + 2 * (encIn a).length + 2 * (encOut (f a)).length + 3 * k + 18)

A tidily computable function is computed by a machine with binary alphabet and finitely many states that reads its input from a work tape i and writes its output to a different work tape o, leaving every other work tape unchanged and emitting nothing.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.onWords_extendTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} (mark : Symbol) {input output : List Symbol} {t s K : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) {e : Fin (k + 1 + 2) ↪ Fin K} {V O : Fin K} (hi : e (Fin.natAdd (k + 1) 0) = V) (ho : e (Fin.castAdd 2 (Fin.last k)) = O) : ((tm.onWords mark).extendTapes e).TransformsTapes (fun (x : List Symbol) (ws : Fin K → List Symbol) => ws = Function.update (fun (x : Fin K) => []) V input) (fun (x : List Symbol) (ws ws' : Fin K → List Symbol) (em : List Symbol) => ws' = Function.update ws O output ∧ em = []) (t + output.length + 6) (s + 2 * input.length + 2 * output.length + 3 * k + 18 + (K - (k + 1 + 2)))

Run a tidy computation between two selected tapes, preserving the input and emitting nothing. The embedding ensures that the selected input and output tapes are distinct.