Step machines, on words

A machine that carries the state of a step machine on tape V, behind two cells that record the symbol under the input head. Each round records that symbol with peekInput, emits with E and computes the next state with Nm (frozenRound), writes the move of the input head to tape M with Mm and moves the input head there, and writes to tape C with Cm whether another round follows. The input head stays where the step machine has it between the rounds.

Main definitions

• Turing.MultiTapeTM.stepRound: one round.
• Turing.MultiTapeTM.stepTM: the rounds, between the initial state and the final clean-up.

Main results

• Turing.MultiTapeTM.transformsTapesAt_stepRound: the specification of a round.
• Turing.MultiTapeTM.computesTidily_stepTM: the rounds compute tidily.

def Turing.MultiTapeTM.slot : List Bool

The two cells in front of the state on tape V, before the symbol under the input head is recorded in them.

noncomputable def Turing.MultiTapeTM.stepRound {K : ℕ} {SE : Type u_2} {SN : Type u_3} {SM : Type u_4} {SC : Type u_5} (E : MultiTapeTM K Bool SE) (Nm : MultiTapeTM K Bool SN) (Mm : MultiTapeTM K Bool SM) (Cm : MultiTapeTM K Bool SC) (V N F C M : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : MultiTapeTM K Bool ((Unit ⊕ RewindWorkState) ⊕ PeekState ⊕ (SE ⊕ SN ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState) ⊕ SM ⊕ Unit ⊕ (Unit ⊕ RewindWorkState) ⊕ SC)

One round: clear the flag tape C, record the symbol under the input head on tape V, emit with E and compute the next state with Nm, write the move to tape M with Mm, move the input head, clear tape M and write the flag with Cm.

def Turing.MultiTapeTM.stepTapes {K : ℕ} (V C : Fin K) (w c : List Bool) : Fin K → List Bool

The tapes between two rounds: the state w on tape V behind the two cells of slot, and the flag c on tape C.

def Turing.MultiTapeTM.stepRoundTime (lc lu lv lm tE tN tM tC : ℕ) : ℕ

The time of a round, in the lengths of the old flag lc, of the word lu that the parts read, of the new state lv and of the move lm, and the times of the parts.

def Turing.MultiTapeTM.stepRoundSpace (K lc lu lv lm sE sN sM sC : ℕ) : ℕ

The space of a round, as stepRoundTime, on K tapes.

theorem Turing.MultiTapeTM.transformsTapesAt_stepRound {K : ℕ} {SE : Type u_2} {SN : Type u_3} {SM : Type u_4} {SC : Type u_5} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {Mm : MultiTapeTM K Bool SM} {Cm : MultiTapeTM K Bool SC} {V N F C M : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (hVC : V ≠ C) (hVM : V ≠ M) (x : List Bool) (p : Fin (x.length + 2)) {w w' c c' e m : List Bool} {tE sE tN sN tM sM tC sC : ℕ} (hE : E.TransformsTapes (fun (x_1 : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (peekWord (inputSymbolAt x p) ++ w)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = e) tE sE) (hN : Nm.TransformsTapes (fun (x_1 : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (peekWord (inputSymbolAt x p) ++ w)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws N (slot ++ w') ∧ em = []) tN sN) (hM : Mm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (slot ++ w')) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws M m ∧ em = []) tM sM) (hC : Cm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (slot ++ w')) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws C c' ∧ em = []) tC sC) : (E.stepRound Nm Mm Cm V N F C M hVN hVF hNF).TransformsTapesAt (fun (input : List Bool) (p₀ : Fin (input.length + 2)) (ws : Fin K → List Bool) => input = x ∧ ↑p₀ = ↑p ∧ ws = stepTapes V C w c) (fun (input : List Bool) (x_1 : Fin (input.length + 2)) (x_2 : Fin K → List Bool) (p' : Fin (input.length + 2)) (ws' : Fin K → List Bool) (em : List Bool) => input = x ∧ ↑p' = ↑(moveInputPos p (moveOfCell m.head?)) ∧ ws' = stepTapes V C w' c' ∧ em = e) (stepRoundTime c.length (peekWord (inputSymbolAt x p) ++ w).length (slot ++ w').length m.length tE tN tM tC) (stepRoundSpace K c.length (peekWord (inputSymbolAt x p) ++ w).length (slot ++ w').length m.length sE sN sM sC)

A round. If, from the state w behind the symbol a under the input head, E emits e and Nm computes the next state w', and from w' Mm writes the move m and Cm the flag c', then a round takes the state w and any flag to w' and the flag c', emitting e, and moves the input head by m.

noncomputable def Turing.MultiTapeTM.stepTM {K : ℕ} {SI : Type u_1} {SE : Type u_2} {SN : Type u_3} {SM : Type u_4} {SC : Type u_5} (I : MultiTapeTM K Bool SI) (E : MultiTapeTM K Bool SE) (Nm : MultiTapeTM K Bool SN) (Mm : MultiTapeTM K Bool SM) (Cm : MultiTapeTM K Bool SC) (V N F C M : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : MultiTapeTM K Bool ((SI ⊕ SC) ⊕ RepeatUntilBlankState ((Unit ⊕ RewindWorkState) ⊕ PeekState ⊕ (SE ⊕ SN ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState) ⊕ SM ⊕ Unit ⊕ (Unit ⊕ RewindWorkState) ⊕ SC) ⊕ (Unit ⊕ RewindWorkState) ⊕ RewindState)

The step machine on words: write the initial state with I and the flag with Cm, run rounds while the flag is not blank, then clear tape V and rewind the input.

theorem Turing.MultiTapeTM.computesTidily_stepTM {K : ℕ} {SI : Type u_1} {SE : Type u_2} {SN : Type u_3} {SM : Type u_4} {SC : Type u_5} {I : MultiTapeTM K Bool SI} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {Mm : MultiTapeTM K Bool SM} {Cm : MultiTapeTM K Bool SC} {V N F C M : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (hVC : V ≠ C) (hVM : V ≠ M) (x : List Bool) (rounds : ℕ) (ws es ms cs : ℕ → List Bool) (ps : ℕ → Fin (x.length + 2)) (hp₀ : ps 0 = 1) (hps : ∀ n < rounds, ps (n + 1) = moveInputPos (ps n) (moveOfCell (ms n).head?)) (hcs : ∀ n < rounds, cs n ≠ []) (hlast : cs rounds = []) {tI sI sR : ℕ} {tE sE tN sN tM sM tC sC : ℕ → ℕ} (hI : I.TransformsTapes (fun (inp : List Bool) (ws : Fin K → List Bool) => inp = x ∧ ws = fun (x : Fin K) => []) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update (fun (x : Fin K) => []) V (slot ++ ws 0) ∧ em = []) tI sI) (hE : ∀ n < rounds, E.TransformsTapes (fun (x_1 : List Bool) (v : Fin K → List Bool) => v = Function.update (fun (x : Fin K) => []) V (peekWord (inputSymbolAt x (ps n)) ++ ws n)) (fun (x : List Bool) (v v' : Fin K → List Bool) (em : List Bool) => v' = v ∧ em = es n) (tE n) (sE n)) (hN : ∀ n < rounds, Nm.TransformsTapes (fun (x_1 : List Bool) (v : Fin K → List Bool) => v = Function.update (fun (x : Fin K) => []) V (peekWord (inputSymbolAt x (ps n)) ++ ws n)) (fun (x : List Bool) (v v' : Fin K → List Bool) (em : List Bool) => v' = Function.update v N (slot ++ ws (n + 1)) ∧ em = []) (tN n) (sN n)) (hM : ∀ n < rounds, Mm.TransformsTapes (fun (x : List Bool) (v : Fin K → List Bool) => v = Function.update (fun (x : Fin K) => []) V (slot ++ ws (n + 1))) (fun (x : List Bool) (v v' : Fin K → List Bool) (em : List Bool) => v' = Function.update v M (ms n) ∧ em = []) (tM n) (sM n)) (hC : ∀ n ≤ rounds, Cm.TransformsTapes (fun (x : List Bool) (v : Fin K → List Bool) => v = Function.update (fun (x : Fin K) => []) V (slot ++ ws n)) (fun (x : List Bool) (v v' : Fin K → List Bool) (em : List Bool) => v' = Function.update v C (cs n) ∧ em = []) (tC n) (sC n)) (hsR : ∀ n < rounds, stepRoundSpace K (cs n).length (peekWord (inputSymbolAt x (ps n)) ++ ws n).length (slot ++ ws (n + 1)).length (ms n).length (sE n) (sN n) (sM n) (sC (n + 1)) ≤ sR) : (I.stepTM E Nm Mm Cm V N F C M hVN hVF hNF).ComputesTidilyInTimeAndSpace x (List.map es (List.range rounds)).flatten (tI + tC 0 + (∑ n ∈ Finset.range rounds, (stepRoundTime (cs n).length (peekWord (inputSymbolAt x (ps n)) ++ ws n).length (slot ++ ws (n + 1)).length (ms n).length (tE n) (tN n) (tM n) (tC (n + 1)) + 1) + 1 + (3 * ((slot ++ ws rounds).length + 1) + (x.length + 2)))) (sI + sC 0 + (2 * K * sR + K + ((slot ++ ws rounds).length + 1 + K + K)))

The step machine on words. If I writes the initial state ws 0 and, for every round n, from the state ws n behind the symbol under the input head at ps n, E emits es n and Nm computes the next state, from which Mm writes the move ms n that takes the input head to ps (n + 1), and Cm writes from every state ws n a flag cs n that is blank exactly after the last round rounds, then stepTM emits the words es n, tidily.