Tape transformations with the input head anywhere

A Turing.MultiTapeTM.TransformsTapes specification starts and ends with the input head on the first symbol of the input. A machine that reads its input once, from left to right, keeps a cursor there instead: its input head stays where the last round left it. TransformsTapesAt is the same specification format with the position of the input head as part of the precondition and the postcondition.

A machine that never needs the input is run with its input head frozen (freezeInput): then every TransformsTapes specification of it holds at any position of the input head (Turing.MultiTapeTM.TransformsTapes.freezeInput).

Main definitions

• Turing.MultiTapeTM.wordsCfgAt: Turing.wordsCfg with the input head anywhere.
• Turing.MultiTapeTM.TransformsTapesAt: the specification format.
• Turing.MultiTapeTM.freezeInput: a machine run on a blank input, with its input head fixed.

Main results

• Turing.MultiTapeTM.transformsTapesAt_seq: sequential composition.
• Turing.MultiTapeTM.TransformsTapesAt.seq_eq: composition with normalized cursor, tape and emitted-word equalities.
• Turing.MultiTapeTM.TransformsTapes.freezeInput: a specification of tm gives one of tm.freezeInput at any position of the input head, which it keeps.
• Turing.MultiTapeTM.transformsTapesAt_rewindInput: rewinding the input head.

def Turing.MultiTapeTM.wordsCfgAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input

The configuration whose work tape i holds the word ws i with its head at the start, with the input head at position p, in state q with output out.

@[simp]

theorem Turing.MultiTapeTM.wordsCfgAt_state {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfgAt input p q ws out).state = q

@[simp]

theorem Turing.MultiTapeTM.wordsCfgAt_workTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (i : Fin k) (a✝ : ℤ) : (wordsCfgAt input p q ws out).workTapes i a✝ = tapeOfList (ws i) a✝

@[simp]

theorem Turing.MultiTapeTM.wordsCfgAt_inputPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfgAt input p q ws out).inputPos = p

@[simp]

theorem Turing.MultiTapeTM.wordsCfgAt_workTapePos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (x✝ : Fin k) : (wordsCfgAt input p q ws out).workTapePos x✝ = 0

@[simp]

theorem Turing.MultiTapeTM.wordsCfgAt_output {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfgAt input p q ws out).output = out

@[simp]

theorem Turing.MultiTapeTM.wordsCfgAt_one {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : wordsCfgAt input 1 q ws out = wordsCfg input q ws out

@[simp]

theorem Turing.MultiTapeTM.withState_wordsCfgAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {State' : Type u_5} (input : List Symbol) (p : Fin (input.length + 2)) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (q' : Option State') : (wordsCfgAt input p q ws out).withState q' = wordsCfgAt input p q' ws out

def Turing.MultiTapeTM.TransformsTapesAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (P : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Prop) (Q : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop) (t s : ℕ) : Prop

TransformsTapesAt tm P Q t s: started in its initial state with the input head at position p and on tapes holding words ws with P input p ws, the machine is halted after t steps with the input head at a position p', on tapes holding words ws', having appended emitted to the output, with Q input p ws p' ws' emitted, and having used at most s work-tape cells.

theorem Turing.MultiTapeTM.TransformsTapesAt.imp {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P P' : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Prop} {Q Q' : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop} {t s t' s' : ℕ} (h : tm.TransformsTapesAt P Q t s) (hP : ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol), P' input p ws → P input p ws) (hQ : ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol), P' input p ws → Q input p ws p' ws' e → Q' input p ws p' ws' e) (ht : t ≤ t') (hs : s ≤ s') : tm.TransformsTapesAt P' Q' t' s'

A stronger precondition, a weaker postcondition and larger bounds.

theorem Turing.MultiTapeTM.TransformsTapes.transformsTapesAt {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 : ℕ} (h : tm.TransformsTapes P Q t s) : tm.TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => p = 1 ∧ P input ws) (fun (input : List Symbol) (x : Fin (input.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => p' = 1 ∧ Q input ws ws' e) t s

A TransformsTapes specification is a TransformsTapesAt specification with the input head at the start before and after.

theorem Turing.MultiTapeTM.TransformsTapesAt.transformsTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Prop} {Q : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapesAt P Q t s) (hQ : ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol), Q input p ws p' ws' e → p' = 1) : tm.TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => P input 1 ws) (fun (input : List Symbol) (ws ws' : Fin k → List Symbol) (e : List Symbol) => Q input 1 ws 1 ws' e) t s

A TransformsTapesAt specification from and to the start of the input is a TransformsTapes specification.

theorem Turing.MultiTapeTM.transformsTapesAt_seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {P₀ P₁ : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Prop} {Q₀ Q₁ : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop} {t₀ s₀ t₁ s₁ : ℕ} (h₀ : tm₀.TransformsTapesAt P₀ Q₀ t₀ s₀) (h₁ : tm₁.TransformsTapesAt P₁ Q₁ t₁ s₁) (hmid : ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol), P₀ input p ws → Q₀ input p ws p' ws' e → P₁ input p' ws') : (tm₀.seq tm₁).TransformsTapesAt P₀ (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (p'' : Fin (input.length + 2)) (ws'' : Fin k → List Symbol) (e : List Symbol) => ∃ (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e₀ : List Symbol) (e₁ : List Symbol), Q₀ input p ws p' ws' e₀ ∧ Q₁ input p' ws' p'' ws'' e₁ ∧ e = e₀ ++ e₁) (t₀ + t₁) (s₀ + s₁)

Sequential composition. If the postcondition of the first specification implies the precondition of the second, the composed machine performs the two one after the other.

theorem Turing.MultiTapeTM.TransformsTapesAt.seq_eq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {P : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Prop} {R : List Symbol → Prop} {p₁ p₂ : ℕ} {ws₁ ws₂ : Fin k → List Symbol} {e₀ e₁ : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} (h₀ : tm₀.TransformsTapesAt P (fun (input : List Symbol) (x : Fin (input.length + 2)) (x_1 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => R input ∧ ↑p' = p₁ ∧ ws' = ws₁ ∧ e = e₀) t₀ s₀) (h₁ : tm₁.TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => R input ∧ ↑p = p₁ ∧ ws = ws₁) (fun (input : List Symbol) (x : Fin (input.length + 2)) (x_1 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => R input ∧ ↑p' = p₂ ∧ ws' = ws₂ ∧ e = e₁) t₁ s₁) : (tm₀.seq tm₁).TransformsTapesAt P (fun (input : List Symbol) (x : Fin (input.length + 2)) (x_1 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => R input ∧ ↑p' = p₂ ∧ ws' = ws₂ ∧ e = e₀ ++ e₁) (t₀ + t₁) (s₀ + s₁)

Sequential composition with normalized cursor, tape and emitted-word equalities.

theorem Turing.MultiTapeTM.TransformsTapes.transformsTapesAt_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {x e : List Symbol} {ws₀ ws₁ : Fin k → List Symbol} {t s : ℕ} (h : tm.TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => input = x ∧ ws = ws₀) (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e' : List Symbol) => ws' = ws₁ ∧ e' = e) t s) : tm.TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => input = x ∧ ↑p = 1 ∧ ws = ws₀) (fun (input : List Symbol) (x_1 : Fin (input.length + 2)) (x_2 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e' : List Symbol) => input = x ∧ ↑p' = 1 ∧ ws' = ws₁ ∧ e' = e) t s

A fixed-input tape transformation, with its cursor equalities normalized.

Freezing the input head

noncomputable def Turing.MultiTapeTM.freezeInput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol State

tm, run as if on a blank input: it reads a blank on the input tape and never moves its input head.

def Turing.MultiTapeTM.FreezeInput.atPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (p : Fin (input.length + 2)) (c : Cfg k Symbol State []) : Cfg k Symbol State input

A configuration on the empty input, with the input head placed at p on input.

theorem Turing.MultiTapeTM.FreezeInput.step_atPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : Fin (input.length + 2)) (c : Cfg k Symbol State []) : step (atPos p c) = atPos p (step c)

theorem Turing.MultiTapeTM.FreezeInput.runFrom_atPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : Fin (input.length + 2)) (c : Cfg k Symbol State []) (n : ℕ) : runFrom (atPos p c) n = atPos p (runFrom c n)

theorem Turing.MultiTapeTM.TransformsTapes.freezeInput {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 : ℕ} (h : tm.TransformsTapes P Q t s) : tm.freezeInput.TransformsTapesAt (fun (x : List Symbol) (x_1 : Fin (x.length + 2)) (ws : Fin k → List Symbol) => P [] ws) (fun (x : List Symbol) (p : Fin (x.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (x.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => p' = p ∧ Q [] ws ws' e) t s

A specification of tm on the empty input is a specification of tm.freezeInput at any position of the input head, which it keeps.

theorem Turing.MultiTapeTM.TransformsTapes.freezeInput_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {ws₀ ws₁ : Fin k → List Symbol} {e : List Symbol} {t s : ℕ} (h : tm.TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws = ws₀) (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e' : List Symbol) => ws' = ws₁ ∧ e' = e) t s) (x : List Symbol) (p : ℕ) : tm.freezeInput.TransformsTapesAt (fun (input : List Symbol) (p' : Fin (input.length + 2)) (ws : Fin k → List Symbol) => input = x ∧ ↑p' = p ∧ ws = ws₀) (fun (input : List Symbol) (x_1 : Fin (input.length + 2)) (x_2 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e' : List Symbol) => input = x ∧ ↑p' = p ∧ ws' = ws₁ ∧ e' = e) t s

A fixed tape transformation at an unchanged cursor, with normalized equalities.

Rewinding the input head

noncomputable def Turing.MultiTapeTM.rewindInputOn (k : ℕ) (Symbol : Type u_5) : MultiTapeTM k Symbol RewindState

rewindInput on a machine with k work tapes.

theorem Turing.MultiTapeTM.transformsTapesAt_rewindInput {k : ℕ} {Symbol : Type u_1} (x : List Symbol) : (rewindInputOn k Symbol).TransformsTapesAt (fun (input : List Symbol) (x_1 : Fin (input.length + 2)) (x_2 : Fin k → List Symbol) => input = x) (fun (x : List Symbol) (x_1 : Fin (x.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (x.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => p' = 1 ∧ ws' = ws ∧ e = []) (x.length + 2) k

rewindInputOn k Symbol moves the input head from anywhere on the input x back to its start and changes nothing else.

@[reducible, inline]

abbrev Turing.MultiTapeTM.TransformsWordsAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (x : List Symbol) (p p' : ℕ) (ws ws' : Fin k → List Symbol) (e : List Symbol) (t s : ℕ) : Prop

TransformsWordsAt tm x p p' ws ws' e t s: on the input x with the input head at the position p, the machine tm takes the words ws to the words ws' emitting e, with the input head ending at p', within t steps and s work-tape cells.

theorem Turing.MultiTapeTM.TransformsTapesAt.wordsAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Prop} {Q : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapesAt P Q t s) {x : List Symbol} {p p' : ℕ} {ws ws' : Fin k → List Symbol} {e : List Symbol} (hP : ∀ (q : Fin (x.length + 2)), ↑q = p → P x q ws) (hQ : ∀ (q q' : Fin (x.length + 2)) (v : Fin k → List Symbol) (e' : List Symbol), ↑q = p → Q x q ws q' v e' → ↑q' = p' ∧ v = ws' ∧ e' = e) : tm.TransformsWordsAt x p p' ws ws' e t s

A specification read on given words, on the input x with the input head at p.

theorem Turing.MultiTapeTM.TransformsWords.freezeInput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {ws ws' : Fin k → List Symbol} {e : List Symbol} {t s : ℕ} (h : tm.TransformsWords ws ws' e t s) (x : List Symbol) (p : ℕ) : tm.freezeInput.TransformsWordsAt x p p ws ws' e t s

A specification given by equations, with the input head fixed.

theorem Turing.MultiTapeTM.TransformsWordsAt.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {x : List Symbol} {p p' : ℕ} {ws ws' : Fin k → List Symbol} {e : List Symbol} {t s t' s' : ℕ} (h : tm.TransformsWordsAt x p p' ws ws' e t s) (ht : t ≤ t') (hs : s ≤ s') : tm.TransformsWordsAt x p p' ws ws' e t' s'

theorem Turing.MultiTapeTM.TransformsWordsAt.congr {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {x : List Symbol} {p p' p₂ p₂' : ℕ} {ws ws' ws₂ ws₂' : Fin k → List Symbol} {e e₂ : List Symbol} {t s : ℕ} (h : tm.TransformsWordsAt x p p' ws ws' e t s) (hp : p₂ = p) (hp' : p' = p₂') (hws : ws₂ = ws) (hws' : ws' = ws₂') (he : e = e₂) : tm.TransformsWordsAt x p₂ p₂' ws₂ ws₂' e₂ t s

Other spellings of the positions, the words and the emitted word.

theorem Turing.MultiTapeTM.TransformsWordsAt.seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_3} {State₁ : Type u_4} {x : List Symbol} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {p₀ p₁ p₂ : ℕ} {ws₀ ws₁ ws₂ : Fin k → List Symbol} {e₀ e₁ : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} (h₀ : tm₀.TransformsWordsAt x p₀ p₁ ws₀ ws₁ e₀ t₀ s₀) (h₁ : tm₁.TransformsWordsAt x p₁ p₂ ws₁ ws₂ e₁ t₁ s₁) : (tm₀.seq tm₁).TransformsWordsAt x p₀ p₂ ws₀ ws₂ (e₀ ++ e₁) (t₀ + t₁) (s₀ + s₁)

Sequential composition: the position and the words left by the first machine are those the second one starts on, and the emitted words are concatenated.