Documentation

MIPRE.TM.MultiInput.OneInputEquiv

One-input machines are exactly CSLib's multi-tape machines #

The multi-input model of MIPRE.TM.MultiInput.Deterministic specializes, at input arity one, to the vendored CSLib model Turing.MultiTapeTM — exactly, not just up to simulation. This file provides the two machine translations

shows they are mutually inverse, and proves that along the configuration correspondence MultiInputTM.cfgEquiv they preserve step, configs, outputString, spaceUsed, and ComputesInTimeAndSpace on the nose (Milestone A acceptance criteria, planning/tm-infrastructure.md).

Throughout, a one-input tuple is written fun _ : Fin 1 => input (never ![input]), so that the dependent input-head positions transport definitionally.

source
def Turing.MultiInputTM.toCSLib {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (M : MultiInputTM 1 w Symbol State) :
MultiTapeTM w Symbol State

Reinterpret a one-input machine as a CSLib multi-tape machine.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Turing.MultiInputTM.ofCSLib {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (N : MultiTapeTM w Symbol State) :
    MultiInputTM 1 w Symbol State

    Reinterpret a CSLib multi-tape machine as a one-input machine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Turing.MultiInputTM.toCSLib_ofCSLib {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (N : MultiTapeTM w Symbol State) :
      (ofCSLib N).toCSLib = N

      Round trip on CSLib machines: toCSLib undoes ofCSLib.

      source
      @[simp]
      theorem Turing.MultiInputTM.ofCSLib_toCSLib {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (M : MultiInputTM 1 w Symbol State) :
      ofCSLib M.toCSLib = M

      Round trip on one-input machines: ofCSLib undoes toCSLib.

      source
      def Turing.MultiInputTM.cfgEquiv {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) :
      MultiTapeTM.Cfg w Symbol State input ≃ Cfg 1 w Symbol State fun (x : Fin 1) => input

      Configurations of a CSLib machine on input correspond exactly to configurations of a one-input machine on the tuple fun _ => input.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Turing.MultiInputTM.cfgEquiv_state {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : MultiTapeTM.Cfg w Symbol State input) :
        ((cfgEquiv input) c).state = c.state
        source
        @[simp]
        theorem Turing.MultiInputTM.cfgEquiv_inputPos {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : MultiTapeTM.Cfg w Symbol State input) (j : Fin 1) :
        ((cfgEquiv input) c).inputPos j = c.inputPos
        source
        @[simp]
        theorem Turing.MultiInputTM.cfgEquiv_workTapes {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : MultiTapeTM.Cfg w Symbol State input) :
        ((cfgEquiv input) c).workTapes = c.workTapes
        source
        @[simp]
        theorem Turing.MultiInputTM.cfgEquiv_workTapePos {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : MultiTapeTM.Cfg w Symbol State input) :
        ((cfgEquiv input) c).workTapePos = c.workTapePos
        source
        @[simp]
        theorem Turing.MultiInputTM.cfgEquiv_symm_state {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : Cfg 1 w Symbol State fun (x : Fin 1) => input) :
        ((cfgEquiv input).symm c).state = c.state