Documentation

Complexity.Computability.Machines.Turing.MultiTape.Plumbing.InputHead

Reading and moving the input head #

Two machines with one work tape that leave the input head where a two-way computation needs it: peekInput writes the symbol under the input head into the first two cells of the word on its work tape, without moving the input head, and moveInput moves the input head by the move written at the start of the word on its work tape.

Main definitions #

Main results #

source
theorem Turing.MultiTapeTM.TransformsTapesAt.tapeEmb {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM 1 Symbol State} {P : (input : List Symbol) → Fin (input.length + 2) → (Fin 1 → List Symbol) → Prop} {Q : (input : List Symbol) → Fin (input.length + 2) → (Fin 1 → List Symbol) → Fin (input.length + 2) → (Fin 1 → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapesAt P Q t s) (i : Fin k) :
(tm.extendTapes (MultiTapeTM.tapeEmb i)).TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => P input p fun (x : Fin 1) => ws i) (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (emitted : List Symbol) => ∃ (v : Fin 1 → List Symbol), Q input p (fun (x : Fin 1) => ws i) p' v emitted ∧ ws' = Function.update ws i (v 0)) t (s + (k - 1))

A one-tape specification on tape i, for a machine that may move the input head.

Reading the symbol under the input head #

source
def Turing.MultiTapeTM.peekWord (a : Option Bool) :
List Bool

The word that records the symbol a under the input head: whether it is a symbol, and the symbol.

Instances For
    source
    inductive Turing.MultiTapeTM.PeekState :
    Type

    The states of peekInput: before writing the first and the second cell.

    Instances For
      source
      instance Turing.MultiTapeTM.instFinitePeekState :
      Finite PeekState
      source
      def Turing.MultiTapeTM.peekInput :
      MultiTapeTM 1 Bool PeekState

      Writes peekWord of the symbol under the input head into the first two cells of its work tape, moving the input head nowhere.

      Instances For
        source
        theorem Turing.MultiTapeTM.transformsTapesAt_peekInput :
        peekInput.TransformsTapesAt (fun (x : List Bool) (x_1 : Fin (x.length + 2)) (ws : Fin 1 → List Bool) => 2 ≤ (ws 0).length) (fun (input : List Bool) (p : Fin (input.length + 2)) (ws : Fin 1 → List Bool) (p' : Fin (input.length + 2)) (ws' : Fin 1 → List Bool) (e : List Bool) => p' = p ∧ ws' 0 = peekWord (inputSymbolAt input p) ++ List.drop 2 (ws 0) ∧ e = []) 2 2

        Reading the symbol under the input head: peekInput replaces the first two cells of the word on its tape by peekWord of the symbol under the input head, which it does not move.

        Moving the input head #

        source
        def Turing.MultiTapeTM.moveOfCell :
        Option Bool → SignType

        The move written as the first cell of a word: none, to the left, or to the right.

        Instances For
          source
          def Turing.MultiTapeTM.moveInput :
          MultiTapeTM 1 Bool Unit

          Moves the input head by moveOfCell of the cell under its work-tape head, in one step.

          Instances For
            source
            theorem Turing.MultiTapeTM.transformsTapesAt_moveInput :
            moveInput.TransformsTapesAt (fun (x : List Bool) (x_1 : Fin (x.length + 2)) (x_2 : Fin 1 → List Bool) => True) (fun (x : List Bool) (p : Fin (x.length + 2)) (ws : Fin 1 → List Bool) (p' : Fin (x.length + 2)) (ws' : Fin 1 → List Bool) (e : List Bool) => p' = moveInputPos p (moveOfCell (ws 0).head?) ∧ ws' = ws ∧ e = []) 1 1

            Moving the input head: moveInput moves the input head by the move at the start of the word on its tape, and changes nothing else.