Documentation

Complexity.Computability.Machines.Turing.MultiTape.Plumbing.InputFromTape

Reading the input from a word on a work tape #

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

inputFromWord M mark reads the input from a word on the virtual input tape, with blank work tapes around it. It runs three machines in sequence:

  1. markFlag k (some mark) writes mark to cell -1 of the flag tape;
  2. inputFromTape M runs M on the virtual input tape;
  3. markFlag k none erases the mark again.

Main definitions #

Main results #

Setting and erasing the flag #

source
noncomputable def Turing.MultiTapeTM.markFlag {Symbol : Type u_1} (k : ℕ) (write : Option Symbol) :
MultiTapeTM (k + 2) Symbol MarkWorkState

markWork write placed on the flag tape, the last of k + 2 work tapes: it writes write to the cell left of the head of that tape.

Instances For
    source
    noncomputable def Turing.MultiTapeTM.inputFromWord {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : MultiTapeTM k Symbol State) (mark : Symbol) :
    MultiTapeTM (k + 2) Symbol (MarkWorkState ⊕ State ⊕ MarkWorkState)

    M, reading its input from a word on the virtual input tape Fin.natAdd k 0, with mark written to cell -1 of the flag tape, the last work tape, before and erased after.

    Instances For
      source
      theorem Turing.MultiTapeTM.inCfg_wordsCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (mark : Symbol) {w : List Symbol} (q : Option State) (ws : Fin k → List Symbol) (o outer : List Symbol) :
      inCfg mark (wordsCfg w q ws o) outer = { state := q, inputPos := 1, workTapes := Fin.append (fun (j : Fin k) => tapeOfList (ws j)) ![tapeOfList w, Function.update (fun (x : ℤ) => none) (-1) (some mark)], workTapePos := fun (x : Fin (k + 2)) => 0, output := o }

      Turing.MultiTapeTM.inCfg of a wordsCfg configuration: the input w on the virtual input tape, mark at cell -1 of the flag tape, every head at cell 0.

      source
      theorem Turing.MultiTapeTM.transformsTapes_inputFromWord {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (mark : Symbol) {M : MultiTapeTM k Symbol State} {w e : List Symbol} {ws₀ ws₁ : Fin k → List Symbol} {t s : ℕ} (hM : ∃ (p : M.RunPath w), RelSeries.head p = wordsCfg w (some M.q₀) ws₀ [] ∧ RelSeries.last p = wordsCfg w none ws₁ e ∧ p.time ≤ t ∧ p.space ≤ s) :
      (M.inputFromWord mark).TransformsTapes (fun (x : List Symbol) (ws : Fin (k + 2) → List Symbol) => ws = Fin.append ws₀ ![w, []]) (fun (x : List Symbol) (x_1 ws' : Fin (k + 2) → List Symbol) (em : List Symbol) => ws' = Fin.append ws₁ ![w, []] ∧ em = e) (t + 4) (s + 2 * w.length + 2 * k + 12)

      If M, run on the input w with work tapes ws₀, has a run path of at most t steps and s cells to the halting configuration with work tapes ws₁, every head back at its start, having emitted e, then inputFromWord M mark takes the work tapes Fin.append ws₀ ![w, []] to Fin.append ws₁ ![w, []] and emits e.

      source
      theorem Turing.MultiTapeTM.transformsTapes_inputFromWord_of_runFrom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (mark : Symbol) {M : MultiTapeTM k Symbol State} {w e : List Symbol} {ws₀ ws₁ : Fin k → List Symbol} {t s : ℕ} (hrun : runFrom (wordsCfg w (some M.q₀) ws₀ []) t = wordsCfg w none ws₁ e) (hspace : space (wordsCfg w (some M.q₀) ws₀ []) t ≤ s) :
      (M.inputFromWord mark).TransformsTapes (fun (x : List Symbol) (ws : Fin (k + 2) → List Symbol) => ws = Fin.append ws₀ ![w, []]) (fun (x : List Symbol) (x_1 ws' : Fin (k + 2) → List Symbol) (em : List Symbol) => ws' = Fin.append ws₁ ![w, []] ∧ em = e) (t + 4) (s + 2 * w.length + 2 * k + 12)

      If M, run on the input w with work tapes ws₀, halts after t steps with work tapes ws₁ and every head back at its start, having emitted e, then inputFromWord M mark takes the work tapes Fin.append ws₀ ![w, []] to Fin.append ws₁ ![w, []] and emits e.

      source
      theorem Turing.MultiTapeTM.append_nil_eq_update {Symbol : Type u_1} {k : ℕ} (w : List Symbol) :
      Fin.append (fun (x : Fin k) => []) ![w, []] = Function.update (fun (x : Fin (k + (Nat.succ 0).succ)) => []) (Fin.natAdd k 0) w

      The work tapes in which inputFromWord starts and halts, for a tidy machine.

      source
      theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.inputFromWord {Symbol : Type u_1} {State : Type u_2} {k : ℕ} {tm : MultiTapeTM k Symbol State} (mark : Symbol) {w y : List Symbol} {t s : ℕ} (h : tm.ComputesTidilyInTimeAndSpace w y t s) :
      (tm.inputFromWord mark).TransformsTapes (fun (x : List Symbol) (ws : Fin (k + 2) → List Symbol) => True ∧ ws = Function.update (fun (x : Fin (k + 2)) => []) (Fin.natAdd k 0) w) (fun (x : List Symbol) (ws ws' : Fin (k + 2) → List Symbol) (em : List Symbol) => ws' = Function.update ws (Fin.natAdd k 0) w ∧ em = y) (t + 4) (s + 2 * (w.length + 2) + 2 * k + 8)

      A tidy machine run on the word on a work tape, emitting what it computes.

      source
      theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.inputFromWord_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 + 2) ↪ Fin K} {V : Fin K} (he : e (Fin.natAdd k 0) = V) :
      ((tm.inputFromWord 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' = ws ∧ em = output) (t + 4) (s + 2 * (input.length + 2) + 2 * k + 8 + (K - (k + 2)))

      Run a tidy computation on a selected input tape, preserving it and emitting the output.