Documentation

Complexity.Computability.Machines.Turing.MultiTape.Run

Facts about runs of multi-tape machines #

Small facts about configurations and runs that are not specific to any construction: the input symbol under the head as a list lookup, the input head move on natural-number positions, the contents of a work tape after an action as a case distinction, the distance a work head can travel, and the initial configuration as a configuration of words.

Main definitions #

Main results #

The input tape #

source
def Turing.inputAt {Symbol : Type u_1} (x : List Symbol) (j : ℕ) :
Option Symbol

The symbol at position j of an input tape holding x: positions 0 and x.length + 1 are the blank end cells, and position j + 1 holds x[j].

Instances For
    source
    theorem Turing.Cfg.inputSymbol_eq_inputAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) :
    cfg.inputSymbol = inputAt input ↑cfg.inputPos
    source
    def Turing.moveInputPosNat (n j : ℕ) (d : SignType) :
    ℕ

    The input head position after a move d from position j, on an input of length n: the head is clamped to 0, …, n + 1. This is Turing.moveInputPos on positions as natural numbers.

    Instances For
      source
      theorem Turing.val_moveInputPos_eq_moveInputPosNat {n : ℕ} (pos : Fin (n + 2)) (d : SignType) :
      ↑(moveInputPos pos d) = moveInputPosNat n (↑pos) d
      source
      theorem Turing.le_add_one_of_moveInputPosNat_eq {n j j' : ℕ} {d : SignType} (hj' : j' < n + 2) (h : moveInputPosNat n j' d = j) :
      j - 1 ≤ j' ∧ j' ≤ j + 1

      A position on the input tape is reached by one move only from a neighbouring position.

      Work tapes #

      source
      theorem Turing.Action.apply_workTapes_eq_ite {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (a : Action k Symbol State) {input : List Symbol} (cfg : Cfg k Symbol State input) (i : Fin k) (z : ℤ) :
      (a.apply cfg).workTapes i z = if z = cfg.workTapePos i then (a.workTapes i).1.getD (cfg.workTapes i z) else cfg.workTapes i z

      The contents of a work tape after applying an action: the written symbol under the head, if the action writes one, and the old contents elsewhere.

      source
      theorem Turing.MultiTapeTM.abs_workTapePos_runFrom_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} (x : List Symbol) (t : ℕ) (i : Fin k) :
      |(runFrom (tm.initCfg x) t).workTapePos i| ≤ ↑t

      After t steps from the initial configuration, a work head is within t cells of the origin.

      source
      theorem Turing.MultiTapeTM.initCfg_eq_wordsCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} (input : List Symbol) :
      tm.initCfg input = wordsCfg input (some tm.q₀) (fun (x : Fin k) => []) []

      The initial configuration is the configuration with the input and blank work tapes.

      source
      theorem Turing.MultiTapeTM.runPath_last_eq_runFrom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.RunPath input) :
      RelSeries.last p = runFrom (RelSeries.head p) p.time

      A path of a deterministic machine ends where the run from its head does.

      source
      theorem Turing.MultiTapeTM.runFrom_eq_of_runPath {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {p : tm.RunPath input} (hp : (RelSeries.last p).Halted) {t : ℕ} (ht : p.time ≤ t) :
      runFrom (RelSeries.head p) t = RelSeries.last p

      A path of a deterministic machine to a halted configuration gives the run from its head at any later step.

      source
      theorem Turing.MultiTapeTM.space_le_of_runsInSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {s : ℕ} (h : tm.RunsInSpace input s) (t : ℕ) :
      space (tm.initCfg input) t ≤ s

      A deterministic machine satisfying the shared space bound s uses at most s cells in every prefix of its run.

      source
      theorem Turing.MultiTapeTM.runsInSpace_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {s : ℕ} :
      tm.RunsInSpace input s ↔ ∀ (t : ℕ), space (tm.initCfg input) t ≤ s

      A deterministic machine satisfies the shared space bound s exactly when every prefix of its run uses at most s cells.

      source
      theorem Turing.MultiTapeTM.ComputesInTimeAndSpace.runFrom_of_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {x out : List Symbol} {t s J : ℕ} (h : tm.ComputesInTimeAndSpace x out t s) (hJ : t ≤ J) :
      (runFrom (tm.initCfg x) J).Halted ∧ (runFrom (tm.initCfg x) J).output = out

      A machine that computes out within time t has halted with output out after any number of steps from t on.

      source
      @[simp]
      theorem Turing.MultiTapeNTM.RunPath.last_ofDeterministic {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) :
      RelSeries.last (ofDeterministic tm cfg t) = MultiTapeTM.runFrom cfg t

      The path of the first t steps from cfg ends where the run does.