Documentation

Complexity.Computability.Machines.Turing.MultiTape.Combinators.Reverse

The input-reversal machine #

A two-state machine without work tapes that outputs the reversal of its input word tidily in 2 * input.length + 2 steps and zero work-tape space.

In its initial state false, Turing.MultiTapeTM.reverseInput scans the input from left to right without emitting anything until it reaches the right boundary blank at position input.length + 1, where it steps one cell left onto position input.length and enters state true. In state true it walks left across the input, emitting each symbol as it passes, until it reaches the left boundary blank at position 0, where it steps one cell right back to the initial head position 1 and halts.

Main definitions #

Main results #

source
def Turing.MultiTapeTM.reverseInput (Symbol : Type u_2) :
MultiTapeTM 0 Symbol Bool

The input-reversal machine: two states (Bool) and no work tapes. State false scans right to the blank after the input and steps left into state true; state true walks left emitting each input symbol until the blank before the input, then steps right to position 1 and halts.

Instances For
    source
    def Turing.MultiTapeTM.ReverseInput.cfg {Symbol : Type u_1} (input : List Symbol) (q : Option Bool) (pos : Fin (input.length + 2)) (tapes : Fin 0 → ℤ → Option Symbol) (heads : Fin 0 → ℤ) (out : List Symbol) :
    Cfg 0 Symbol Bool input

    Configuration of reverseInput in state q with the input head at pos and output out. input is explicit because it only occurs in the type.

    Instances For
      source
      theorem Turing.MultiTapeTM.ReverseInput.runFrom_full {Symbol : Type u_1} (input : List Symbol) (tapes : Fin 0 → ℤ → Option Symbol) (heads : Fin 0 → ℤ) (out : List Symbol) :
      runFrom (cfg input (some (reverseInput Symbol).q₀) 1 tapes heads out) (2 * input.length + 2) = cfg input none 1 tapes heads (out ++ input.reverse)

      Complete run from the initial state at position 1 with arbitrary prior output prefix out: after 2 * input.length + 2 steps, reverseInput halts at position 1 with output out ++ input.reverse.

      source
      theorem Turing.MultiTapeTM.ReverseInput.computesInTimeAndSpace {Symbol : Type u_1} (input : List Symbol) :
      (reverseInput Symbol).ComputesInTimeAndSpace input input.reverse (2 * input.length + 2) 0

      reverseInput computes input.reverse in 2 * input.length + 2 steps and zero space.

      source
      theorem Turing.MultiTapeTM.ReverseInput.computesTidily {Symbol : Type u_1} (input : List Symbol) :
      (reverseInput Symbol).ComputesTidilyInTimeAndSpace input input.reverse (2 * input.length + 2) 0

      reverseInput computes input.reverse tidily in 2 * input.length + 2 steps and zero work-tape space, preserving any ambient output prefix.

      source
      theorem Turing.MultiTapeTM.computableTidilyInTimeAndSpace_reverse {α : Type u_2} {β : Type u_3} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (hf : ∀ (a : α), encOut (f a) = (encIn a).reverse) :
      ComputableTidilyInTimeAndSpace f encIn encOut (fun (a : α) => 2 * (encIn a).length + 2) fun (x : α) => 0

      Any function whose encoding reverses the encoded input is tidily computable in 2 * (encIn a).length + 2 steps and zero work-tape space.