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
        source
        theorem Turing.MultiInputTM.cfgEquiv_inputSymbol {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).inputSymbol j = c.inputSymbol

        The input symbol read is preserved by the configuration correspondence.

        source
        theorem Turing.MultiInputTM.cfgEquiv_inputSymbols {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : MultiTapeTM.Cfg w Symbol State input) :
        ((cfgEquiv input) c).inputSymbols = fun (x : Fin 1) => c.inputSymbol

        The tuple of input symbols of a transported configuration.

        source
        theorem Turing.MultiInputTM.cfgEquiv_workTapeSymbols {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (c : MultiTapeTM.Cfg w Symbol State input) :
        ((cfgEquiv input) c).workTapeSymbols = c.workTapeSymbols

        The work symbols read are preserved by the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_step {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (M : MultiInputTM 1 w Symbol State) (c : MultiTapeTM.Cfg w Symbol State input) :
        (cfgEquiv input) (MultiTapeTM.step c) = step ((cfgEquiv input) c)

        The step functions agree along the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_configs {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (M : MultiInputTM 1 w Symbol State) (c : MultiTapeTM.Cfg w Symbol State input) (t : ℕ) :
        (cfgEquiv input) (MultiTapeTM.configs c t) = configs ((cfgEquiv input) c) t

        The step-indexed runs agree along the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_outputSymbol {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (M : MultiInputTM 1 w Symbol State) (c : MultiTapeTM.Cfg w Symbol State input) :
        MultiTapeTM.outputSymbol c = outputSymbol ((cfgEquiv input) c)

        The emitted symbols agree along the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_outputString {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (M : MultiInputTM 1 w Symbol State) (c : MultiTapeTM.Cfg w Symbol State input) (t : ℕ) :
        M.toCSLib.outputString c t = M.outputString ((cfgEquiv input) c) t

        The output strings agree along the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_visitedByTapeHead {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (M : MultiInputTM 1 w Symbol State) (c : MultiTapeTM.Cfg w Symbol State input) (t : ℕ) (d : Fin w) :
        MultiTapeTM.visitedByTapeHead c t d = visitedByTapeHead ((cfgEquiv input) c) t d

        The visited work-tape cells agree along the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_spaceUsed {w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (M : MultiInputTM 1 w Symbol State) (c : MultiTapeTM.Cfg w Symbol State input) (t : ℕ) :
        MultiTapeTM.spaceUsed c t = spaceUsed ((cfgEquiv input) c) t

        The space usage agrees along the configuration correspondence.

        source
        theorem Turing.MultiInputTM.toCSLib_initCfg {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (M : MultiInputTM 1 w Symbol State) (input : List Symbol) :
        (cfgEquiv input) (MultiTapeTM.initCfg input) = initCfg fun (x : Fin 1) => input

        The initial configurations correspond.

        source
        theorem Turing.MultiInputTM.toCSLib_computesInTimeAndSpace {w : ℕ} {State : Type u_1} {Symbol : Type u_2} (M : MultiInputTM 1 w Symbol State) (input output : List Symbol) (t s : ℕ) :
        M.toCSLib.ComputesInTimeAndSpace input output t s ↔ M.ComputesInTimeAndSpace (fun (x : Fin 1) => input) output t s

        A one-input machine and its CSLib avatar compute the same input/output/time/space quadruples.