Documentation

Complexity.Computability.Machines.Turing.MultiTape.Universal.Space

The simulation in the space of the simulated machine #

A zipper holds a cell only at a position its head has visited, and the visited positions of a head that moves by at most one cell per step form an interval around 0. So the configuration of the simulation after j steps takes space linear in the number of visited cells, times the size of a symbol, plus the length of the input head in binary (Turing.MultiTapeTM.Universal.length_eCfg_le_space). For the description of a machine, the visited cells are those of the machine (Turing.MultiTapeTM.Universal.simSpace_desc).

Main definitions #

Main results #

Zippers within the visited positions #

A step on a single work tape #

Visited positions #

source
def Turing.MultiTapeTM.Universal.run (d : Desc) (x : List ℕ) (j : ℕ) :
SCfg

The configuration of the simulation after j steps.

Instances For
    source
    def Turing.MultiTapeTM.Universal.headAt (d : Desc) (x : List ℕ) (j i : ℕ) :
    ℤ

    The head of work tape i after j steps.

    Instances For
      source
      def Turing.MultiTapeTM.Universal.visited (d : Desc) (x : List ℕ) (j i : ℕ) :
      Finset ℤ

      The positions visited by the head of work tape i up to step j.

      Instances For
        source
        def Turing.MultiTapeTM.Universal.simSpace (d : Desc) (x : List ℕ) (j : ℕ) :
        ℕ

        The number of work-tape cells visited by the simulation up to step j.

        Instances For

          The size of the configuration #

          source
          theorem Turing.MultiTapeTM.Universal.length_eCfg_le_space (d : Desc) (x : List ℕ) (j : ℕ) :
          (eCfg (run d x j)).length ≤ 2 * descLen d + 3 + 2 * (encNat (x.length + 1)).length + 1 + 3 * (2 * descLen d + 5) * 2 * simSpace d x j + d.tapes

          The size of the configuration after j steps, in the number of visited cells: linear in the visited cells and the number of work tapes, times the size of a symbol, plus the length of the position of the input head in binary.

          Descriptions of machines #

          source
          theorem Turing.MultiTapeTM.Universal.simSpace_desc {k : ℕ} {Symbol State : Type} [Fintype State] [Fintype Symbol] (eS : State ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol State) (x : List Symbol) (j : ℕ) :
          simSpace (desc eS eY tm) (List.map (⇑eY) x) j = space (tm.initCfg x) j

          The space of the simulation of the description of a machine is the space of the machine.