Documentation

Complexitylib.Models.TuringMachine.Registers.Probe

symProbeTM: read the input symbol at a register-indexed position #

symProbeTM f r q walks the input head to the cell indexed by register r (lockstep over r's marks), reads the symbol s there, adds (f s).val ≤ 3 marks to register q, and restores everything: the input head returns to cell 1, r is untouched, q becomes regTape (d + (f s)).

This is the reduction emitter's only input-reading machine: the start clauses of the tableau pin the input cells, so their symbol digits are read off the input tape position by position.

source
inductive Complexity.TM.ProbePhase :
Type

Control states of symProbeTM: walk out to the probed cell (pre, walk), rewind the input and register r carrying the read digit k (backI k, backR k), scan to the end of q and append k marks (scanQ k), then rewind q and park (backQ, park, done).

Instances For
    source
    def Complexity.TM.instDecidableEqProbePhase.decEq (x✝ x✝¹ : ProbePhase) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.TM.instDecidableEqProbePhase :
      DecidableEq ProbePhase
      Equations
      source
      @[implicit_reducible]
      instance Complexity.TM.instFintypeProbePhase :
      Fintype ProbePhase

      ProbePhase is a finite type (17 states), as required for TM state sets.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.TM.symProbeTM {n : ℕ} (f : Γ → Fin 4) (r q : Fin n) :
      TM n

      Probe the input at the position held by r and add f-of-the-symbol to q. All tapes restored except q.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.TM.symProbeTM_hoareTime {n : ℕ} (f : Γ → Fin 4) (r q : Fin n) (hrq : r ≠ q) (pos d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hhead : inp₀.head = 1) (hwf : inp₀.cells 0 = Γ.start) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hr : work₀ r = regTape pos) (hq : work₀ q = regTape d) :
        (symProbeTM f r q).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ q (regTape (d + ↑(f (inp₀.cells pos))))) ys) (3 * pos + 2 * d + 20)

        symProbeTM Hoare specification. Reads the input symbol at the position held by register r and adds its f-index to register q; the input (parked at cell 1), the register r, and every other tape are restored exactly.