Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OneWorkTape

Hand-stepped runs of machines with one work tape #

Scaffolding for verifying small machines with one work tape step by step, as in Turing.MultiTapeTM.ZipTransducer.toTM and Turing.MultiTapeTM.TakeDropUnary.toTM. A configuration is written as cfgAt w st p tape h o with the input head at p (clamped to the input), and a run segment Seg tm S c c' t records that tm reaches c' from c within t steps while its work head stays in S. Segments compose, so a bound on the cells used by a whole run follows from the bounds of its phases.

Main definitions #

Main results #

source
theorem Turing.moveInputPosNat_one {n j : ℕ} (hj : j ≤ n) :
moveInputPosNat n j 1 = j + 1

Moving right from a position before the right end cell.

source
theorem Turing.moveInputPosNat_zero {n j : ℕ} (hj : j ≤ n + 1) :
moveInputPosNat n j 0 = j

Not moving.

source
theorem Turing.moveInputPosNat_neg_one {n j : ℕ} (hj : j ≤ n + 1) :
moveInputPosNat n j (-1) = j - 1

Moving left from a position on the input tape.

Configurations #

source
def Turing.MultiTapeTM.OneWorkTape.cfgAt {Symbol : Type u_1} {State : Type u_2} (w : List Symbol) (st : Option State) (p : ℕ) (tape : ℤ → Option Symbol) (h : ℤ) (o : List Symbol) :
Cfg 1 Symbol State w

The configuration in state st with the input head at p (clamped to the input), the work tape tape with its head at h, and the output o.

Instances For
    source
    theorem Turing.MultiTapeTM.OneWorkTape.step_cfgAt {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {tm : MultiTapeTM 1 Symbol State} {f : State → Option Symbol → Option Symbol → Action 1 Symbol State} (htr : ∀ (s : State) (x y : Option Symbol), (tm.tr s x fun (x : Fin 1) => y) = f s x y) (s : State) (p : ℕ) (tape : ℤ → Option Symbol) (h : ℤ) (o : List Symbol) :
    step (cfgAt w (some s) p tape h o) = cfgAt w (f s (inputAt w (min p (w.length + 1))) (tape h)).state (moveInputPosNat w.length (min p (w.length + 1)) (f s (inputAt w (min p (w.length + 1))) (tape h)).inputTape) (match (motive := Option (Option Symbol) → ℤ → Option Symbol) ((f s (inputAt w (min p (w.length + 1))) (tape h)).workTapes 0).1 with | none => tape | some x => Function.update tape h x) (h + ↑((f s (inputAt w (min p (w.length + 1))) (tape h)).workTapes 0).2) (o ++ (f s (inputAt w (min p (w.length + 1))) (tape h)).output.toList)

    One step of a machine with one work tape, read off a transition function f on the input symbol and the work-tape symbol.

    source
    theorem Turing.MultiTapeTM.OneWorkTape.cfgAt_congr {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {st : Option State} {p p' : ℕ} {tape : ℤ → Option Symbol} {h h' : ℤ} {o : List Symbol} (hp : min p (w.length + 1) = min p' (w.length + 1)) (hh : h = h') :
    cfgAt w st p tape h o = cfgAt w st p' tape h' o

    Configurations agree when their clamped input positions and their work heads do.

    source
    @[simp]
    theorem Turing.MultiTapeTM.OneWorkTape.cfgAt_workTapePos {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} (st : Option State) (p : ℕ) (tape : ℤ → Option Symbol) (h : ℤ) (o : List Symbol) :
    (cfgAt w st p tape h o).workTapePos 0 = h

    The work head of cfgAt.

    source
    @[reducible, inline]
    abbrev Turing.MultiTapeTM.OneWorkTape.cells (n : ℕ) :
    Finset ℤ

    The cells -1, …, n: the left end marker cell and a word of length n.

    Instances For
      source
      theorem Turing.MultiTapeTM.OneWorkTape.cfgAt_mem_cells {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {n : ℕ} {st : Option State} {p : ℕ} {tape : ℤ → Option Symbol} {h : ℤ} {o : List Symbol} (h₀ : -1 ≤ h) (h₁ : h ≤ ↑n) :
      (cfgAt w st p tape h o).workTapePos 0 ∈ cells n

      A work head between -1 and n is in cells n.

      Runs through a set of work-head positions #

      source
      def Turing.MultiTapeTM.OneWorkTape.Seg {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} (tm : MultiTapeTM 1 Symbol State) (S : Finset ℤ) (c c' : Cfg 1 Symbol State w) (t : ℕ) :
      Prop

      From c, tm reaches c' within t steps, its work head staying in S.

      Instances For
        source
        theorem Turing.MultiTapeTM.OneWorkTape.Seg.refl {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {tm : MultiTapeTM 1 Symbol State} {S : Finset ℤ} {c : Cfg 1 Symbol State w} (hc : c.workTapePos 0 ∈ S) :
        Seg tm S c c 0

        The empty segment.

        source
        theorem Turing.MultiTapeTM.OneWorkTape.Seg.single {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {tm : MultiTapeTM 1 Symbol State} {S : Finset ℤ} {c c' : Cfg 1 Symbol State w} (hc : c.workTapePos 0 ∈ S) (h : step c = c') (hc' : c'.workTapePos 0 ∈ S) :
        Seg tm S c c' 1

        A segment of one step.

        source
        theorem Turing.MultiTapeTM.OneWorkTape.Seg.trans {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {tm : MultiTapeTM 1 Symbol State} {S : Finset ℤ} {c c' c'' : Cfg 1 Symbol State w} {t t' : ℕ} (h₁ : Seg tm S c c' t) (h₂ : Seg tm S c' c'' t') :
        Seg tm S c c'' (t + t')

        Consecutive segments compose, adding their times.

        source
        theorem Turing.MultiTapeTM.OneWorkTape.Seg.mono {Symbol : Type u_1} {State : Type u_2} {w : List Symbol} {tm : MultiTapeTM 1 Symbol State} {S : Finset ℤ} {c c' : Cfg 1 Symbol State w} {t t' : ℕ} (h : Seg tm S c c' t) (ht : t ≤ t') :
        Seg tm S c c' t'

        A segment within t steps is within any larger number of steps.