Tape transformations as runs

Turing.MultiTapeTM.TransformsTapes asks for a run path to the halted normal form within the time and space bounds. Since a deterministic machine stays where it halted, this is the same as asking that the run of exactly t steps ends in the normal form, using at most s cells: the form in which Christian Reitwiessner's branch crei/tidy-universal states and proves its specifications.

Main results

• Turing.MultiTapeTM.runFrom_nop_withState: nop halts in one step from any configuration and changes nothing else.
• Turing.MultiTapeTM.transformsTapes_iff_runFrom: a tape transformation, read on runs.

theorem Turing.MultiTapeTM.runFrom_nop_withState {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (C : Cfg k Symbol State input) : runFrom (C.withState (some ())) 1 = C.withState none

nop halts in one step from any configuration and changes nothing else.

theorem Turing.MultiTapeTM.transformsTapes_iff_runFrom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t s : ℕ} : tm.TransformsTapes P Q t s ↔ ∀ (input : List Symbol) (ws : Fin k → List Symbol) (out : List Symbol), P input ws → ∃ (ws' : Fin k → List Symbol) (emitted : List Symbol), runFrom (wordsCfg input (some tm.q₀) ws out) t = wordsCfg input none ws' (out ++ emitted) ∧ Q input ws ws' emitted ∧ space (wordsCfg input (some tm.q₀) ws out) t ≤ s

A tape transformation, read on runs. TransformsTapes tm P Q t s holds exactly when, on words ws satisfying P, the run of t steps ends in the halted normal form, holding words ws' and having emitted emitted with Q input ws ws' emitted, and uses at most s cells.