Runs between configurations with shifted words

Turing.MultiTapeTM.TransformsTapes describes machines that start and halt with every word at the start of its tape and every head on the first cell of its word. Some machines keep a word at a drifting position, for example a stack that grows to the left. This file describes runs between arbitrary configurations and transports specifications to configurations whose words sit anywhere.

Turing.Cfg.shift δ moves the contents and the head of every work tape i by δ i cells. Machines are translation invariant (Turing.MultiTapeTM.runFrom_shift), so a run from a shifted configuration is the shifted run. Turing.tapesCfg input ws o h out is the configuration whose tape i holds the word ws i from cell o i on, with its head at cell h i; a wordsCfg configuration shifted by δ is tapesCfg input ws δ δ out.

Turing.MultiTapeTM.RunsBetween tm c c' t s says that tm, started in its initial state on the tapes of c, has halted on the tapes of c' after t steps, using at most s cells. Such runs compose sequentially, embed into machines with more tapes, follow from TransformsTapes specifications at any shift, and accumulate along the loop Turing.MultiTapeTM.whileCond.

Main definitions

• Turing.Cfg.shift, Turing.tapesCfg: shifted configurations.
• Turing.MultiTapeTM.RunsBetween: a run between two configurations within bounds.

Main results

• Turing.MultiTapeTM.runFrom_shift, Turing.MultiTapeTM.space_shift: translation invariance.
• Turing.MultiTapeTM.RunsBetween.seq, .extendTapes, .of_transformsTapes: composition.
• Turing.MultiTapeTM.runsBetween_whileCond: loops, with the costs of the rounds adding up.

def Turing.Cfg.shift {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (δ : Fin k → ℤ) (c : Cfg k Symbol State input) : Cfg k Symbol State input

The configuration with the contents and the head of every work tape i moved by δ i cells to the right.

@[simp]

theorem Turing.Cfg.shift_withState {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (δ : Fin k → ℤ) (c : Cfg k Symbol State input) {State' : Type u_3} (q : Option State') : (shift δ c).withState q = shift δ (c.withState q)

def Turing.tapesCfg {k : ℕ} {Symbol : Type u_1} (input : List Symbol) (ws : Fin k → List Symbol) (o h : Fin k → ℤ) (out : List Symbol) : Cfg k Symbol Unit input

The configuration whose work tape i holds the word ws i from cell o i on, with its head at cell h i, the input head at the start of the input and the output out. Its state is irrelevant for Turing.MultiTapeTM.RunsBetween.

@[simp]

theorem Turing.tapesCfg_workTapes {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (o h : Fin k → ℤ) (out : List Symbol) (i : Fin k) (z : ℤ) : (tapesCfg input ws o h out).workTapes i z = tapeOfList (ws i) (z - o i)

@[simp]

theorem Turing.tapesCfg_workTapePos {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (o h : Fin k → ℤ) (out : List Symbol) : (tapesCfg input ws o h out).workTapePos = h

theorem Turing.tapesCfg_workTapeSymbols {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (o h : Fin k → ℤ) (out : List Symbol) (i : Fin k) : (tapesCfg input ws o h out).workTapeSymbols i = tapeOfList (ws i) (h i - o i)

The symbol under the head of a tape of a tapesCfg configuration.

theorem Turing.tapesCfg_workTapeSymbols_self {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (o : Fin k → ℤ) (out : List Symbol) (i : Fin k) : (tapesCfg input ws o o out).workTapeSymbols i = (ws i).head?

With every head on the first cell of its word, the scanned symbols are the first letters.

theorem Turing.shift_tapesCfg {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (o h δ : Fin k → ℤ) (out : List Symbol) : Cfg.shift δ (tapesCfg input ws o h out) = tapesCfg input ws (fun (i : Fin k) => o i + δ i) (fun (i : Fin k) => h i + δ i) out

theorem Turing.tapesCfg_zero_withState {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (ws : Fin k → List Symbol) (out : List Symbol) (q : Option State) : (tapesCfg input ws 0 0 out).withState q = wordsCfg input q ws out

theorem Turing.wordsCfg_shift {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (ws : Fin k → List Symbol) (δ : Fin k → ℤ) (out : List Symbol) (q : Option State) : Cfg.shift δ (wordsCfg input q ws out) = (tapesCfg input ws δ δ out).withState q

A wordsCfg configuration, shifted.

Translation invariance

theorem Turing.MultiTapeTM.step_shift {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (δ : Fin k → ℤ) (c : Cfg k Symbol State input) : step (Cfg.shift δ c) = Cfg.shift δ (step c)

One step of a machine commutes with shifting the work tapes.

theorem Turing.MultiTapeTM.runFrom_shift {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (δ : Fin k → ℤ) (c : Cfg k Symbol State input) (t : ℕ) : runFrom (Cfg.shift δ c) t = Cfg.shift δ (runFrom c t)

Translation invariance. The run from a shifted configuration is the shifted run.

theorem Turing.MultiTapeTM.space_shift {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (δ : Fin k → ℤ) (c : Cfg k Symbol State input) (t : ℕ) : (MultiTapeNTM.RunPath.ofDeterministic tm (Cfg.shift δ c) t).space = (MultiTapeNTM.RunPath.ofDeterministic tm c t).space

A shifted run visits as many cells as the run.

Runs between configurations

def Turing.MultiTapeTM.RunsBetween {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c c' : Cfg k Symbol Unit input) (t s : ℕ) : Prop

RunsBetween tm c c' t s: started in its initial state on the tapes, heads and output of c, the machine has halted after t steps on those of c', having visited at most s cells. The states of c and c' are ignored.

theorem Turing.MultiTapeTM.RunsBetween.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {c c' : Cfg k Symbol Unit input} {t s t' s' : ℕ} (h : tm.RunsBetween c c' t s) (ht : t ≤ t') (hs : s ≤ s') : tm.RunsBetween c c' t' s'

Larger bounds: a halted machine stays where it is.

theorem Turing.MultiTapeTM.RunsBetween.of_runFrom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {c c' : Cfg k Symbol Unit input} {t : ℕ} (h : runFrom (c.withState (some tm.q₀)) t = c'.withState none) : tm.RunsBetween c c' t (k * (t + 1))

A run to a halted configuration: its space is at most one cell per tape and configuration.

theorem Turing.MultiTapeTM.RunsBetween.shift {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {c c' : Cfg k Symbol Unit input} {t s : ℕ} (h : tm.RunsBetween c c' t s) (δ : Fin k → ℤ) : tm.RunsBetween (Cfg.shift δ c) (Cfg.shift δ c') t s

A run between shifted configurations.

theorem Turing.MultiTapeTM.RunsBetween.seq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {c c' : Cfg k Symbol Unit input} {t s : ℕ} {State₁ : Type u_3} {tm₁ : MultiTapeTM k Symbol State₁} {c'' : Cfg k Symbol Unit input} {t₁ s₁ : ℕ} (h₀ : tm.RunsBetween c c' t s) (h₁ : tm₁.RunsBetween c' c'' t₁ s₁) : (tm.seq tm₁).RunsBetween c c'' (t + t₁) (s + s₁)

Sequential composition.

theorem Turing.MultiTapeTM.RunsBetween.extendTapes {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t s : ℕ} (e : Fin k ↪ Fin k') {c : Cfg k' Symbol Unit input} {d : Cfg k Symbol Unit input} (h : tm.RunsBetween (viewCfg e c) d t s) : (tm.extendTapes e).RunsBetween c (embed e d c.workTapes c.workTapePos) t (s + (k' - k))

A run on the tapes selected by an embedding. The other tapes are left alone; each costs one cell.

theorem Turing.MultiTapeTM.RunsBetween.of_transformsTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} (h : tm.TransformsTapes P Q t s) {ws : Fin k → List Symbol} (hP : P input ws) (δ : Fin k → ℤ) (out : List Symbol) : ∃ (ws' : Fin k → List Symbol) (e : List Symbol), Q input ws ws' e ∧ tm.RunsBetween (tapesCfg input ws δ δ out) (tapesCfg input ws' δ δ (out ++ e)) t s

A TransformsTapes specification, read as runs between shifted word configurations.

theorem Turing.MultiTapeTM.RunsBetween.of_transformsTapes_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {P : List Symbol → (Fin k → List Symbol) → Prop} {ws ws' : Fin k → List Symbol} {e : List Symbol} (h : tm.TransformsTapes P (fun (x : List Symbol) (x_1 ws'' : Fin k → List Symbol) (e' : List Symbol) => ws'' = ws' ∧ e' = e) t s) (hP : P input ws) (δ : Fin k → ℤ) (out : List Symbol) : tm.RunsBetween (tapesCfg input ws δ δ out) (tapesCfg input ws' δ δ (out ++ e)) t s

A TransformsTapes specification whose postcondition determines the words and the emitted word, read as a run between shifted word configurations.

@[simp]

theorem Turing.MultiTapeTM.viewCfg_tapesCfg {k k' : ℕ} {Symbol : Type u_1} {input : List Symbol} (e : Fin k ↪ Fin k') (ws : Fin k' → List Symbol) (o h : Fin k' → ℤ) (out : List Symbol) : viewCfg e (tapesCfg input ws o h out) = tapesCfg input (fun (j : Fin k) => ws (e j)) (fun (j : Fin k) => o (e j)) (fun (j : Fin k) => h (e j)) out

Viewing the tapes of a tapesCfg configuration through an embedding.

theorem Turing.MultiTapeTM.embed_tapesCfg {k k' : ℕ} {Symbol : Type u_1} {input : List Symbol} (e : Fin k ↪ Fin k') {v : Fin k → List Symbol} {ov hv : Fin k → ℤ} {ws ws' : Fin k' → List Symbol} {o h o' h' : Fin k' → ℤ} {out : List Symbol} (hsel : ∀ (j : Fin k), ws' (e j) = v j ∧ o' (e j) = ov j ∧ h' (e j) = hv j) (hother : ∀ l ∉ Set.range ⇑e, ws' l = ws l ∧ o' l = o l ∧ h' l = h l) : embed e (tapesCfg input v ov hv out) (tapesCfg input ws o h out).workTapes (tapesCfg input ws o h out).workTapePos = tapesCfg input ws' o' h' out

Placing a tapesCfg configuration on the tapes selected by an embedding, the other tapes of another one.

theorem Turing.MultiTapeTM.step_tapesCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {q : State} {ws ws' : Fin k → List Symbol} {o h o' h' : Fin k → ℤ} {out : List Symbol} {a : Action k Symbol State} (ha : (tm.tr q (tapesCfg input ws o h out).inputSymbol fun (i : Fin k) => tapeOfList (ws i) (h i - o i)) = a) (hin : a.inputTape = 0) (hout : a.output = none) (htape : ∀ (i : Fin k), (match (motive := Option (Option Symbol) → ℤ → Option Symbol) (a.workTapes i).1 with | none => fun (z : ℤ) => tapeOfList (ws i) (z - o i) | some s => Function.update (fun (z : ℤ) => tapeOfList (ws i) (z - o i)) (h i) s) = fun (z : ℤ) => tapeOfList (ws' i) (z - o' i)) (hhead : ∀ (i : Fin k), h i + ↑(a.workTapes i).2 = h' i) : step ((tapesCfg input ws o h out).withState (some q)) = (tapesCfg input ws' o' h' out).withState a.state

One step from a tapesCfg configuration, for an action that keeps the input head and emits nothing: each tape is written and moved as the action says.

Loops

theorem Turing.MultiTapeTM.runsBetween_whileCond {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {c : Option Symbol → (Fin k → Option Symbol) → Bool} {tm : MultiTapeTM k Symbol State} (cfg : ℕ → Cfg k Symbol Unit input) (n : ℕ) (t s : ℕ → ℕ) (hround : ∀ i < n, c (cfg i).inputSymbol (cfg i).workTapeSymbols = true ∧ tm.RunsBetween (cfg i) (cfg (i + 1)) (t i) (s i)) (hstop : c (cfg n).inputSymbol (cfg n).workTapeSymbols = false) : (whileCond c tm).RunsBetween (cfg 0) (cfg n) (∑ i ∈ Finset.range n, (t i + 1) + 1) (∑ i ∈ Finset.range n, (s i + k) + 2 * k)

Loops. If c holds at the configurations cfg i for i < n, from each of which tm runs to cfg (i + 1), and fails at cfg n, then whileCond c tm runs from cfg 0 to cfg n. The times of the rounds add up, with one step per round to read the condition.