The stack-loop machine: tape layout and phases

The machine of Turing.MultiTapeTM.ComputableInO.stackLoop has the kk work tapes shared by the machines it runs, followed by six named tapes: a flag tape for Turing.MultiTapeTM.onWords, the current value C, the halting flag F, the round input or output R, the pushed frames P and the stack S. The stack is kept as the framed words of its frames, top first, ending just before cell 0 of S, so that pushing writes to the left and popping erases from the left.

This file describes the configurations of the machine (StackLoopKernel.cfgS), the runs of its phases between them, one round, and the whole run.

Main definitions

• Turing.MultiTapeTM.StackLoopKernel.cfgS: the configurations of the machine.
• Turing.MultiTapeTM.StackLoopKernel.body: one round.
• Turing.MultiTapeTM.StackLoopKernel.stackLoopTM: the machine.
• Turing.MultiTapeTM.StackLoopKernel.roundTime, Turing.MultiTapeTM.StackLoopKernel.roundSpace: bounds on one round.

Main results

• Turing.MultiTapeTM.StackLoopKernel.transformsTapes_onWords_embed: onWords on embedded tapes, with every other tape arbitrary.
• Turing.MultiTapeTM.StackLoopKernel.runs_stackLoop: the run of the machine on a stack loop that halts with an empty stack.

Tape layout

@[reducible, inline]

abbrev Turing.MultiTapeTM.StackLoopKernel.nm {kk : ℕ} (j : Fin 6) : Fin (kk + 6)

The named tape j: 0 flag, 1 current value, 2 halting flag, 3 round word, 4 pushed frames, 5 stack.

def Turing.MultiTapeTM.StackLoopKernel.tapeWords {kk : ℕ} (c f r p s : List Bool) : Fin (kk + 6) → List Bool

The words on the tapes: the shared work tapes and the flag tape are blank.

def Turing.MultiTapeTM.StackLoopKernel.tapeOffs {kk : ℕ} (oc os : ℤ) : Fin (kk + 6) → ℤ

The offsets of the words: only the current value and the stack may be shifted.

def Turing.MultiTapeTM.StackLoopKernel.tapeHeads {kk : ℕ} (oc os hr hp : ℤ) : Fin (kk + 6) → ℤ

The heads: on the first cells of the words, except possibly on the round word and the pushed frames.

def Turing.MultiTapeTM.StackLoopKernel.cfgS {kk : ℕ} (input c f r p s : List Bool) (oc os hr hp : ℤ) (out : List Bool) : Cfg (kk + 6) Bool Unit input

A configuration of the stack-loop machine.

theorem Turing.MultiTapeTM.StackLoopKernel.tapeHeads_zero {kk : ℕ} (oc os : ℤ) : tapeHeads oc os 0 0 = tapeOffs oc os

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.tapeWords_castAdd {kk : ℕ} (c f r p s : List Bool) (i : Fin kk) : tapeWords c f r p s (Fin.castAdd 6 i) = []

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.tapeWords_nm {kk : ℕ} (c f r p s : List Bool) (j : Fin 6) : tapeWords c f r p s (nm j) = ![[], c, f, r, p, s] j

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.tapeOffs_castAdd {kk : ℕ} (oc os : ℤ) (i : Fin kk) : tapeOffs oc os (Fin.castAdd 6 i) = 0

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.tapeOffs_nm {kk : ℕ} (oc os : ℤ) (j : Fin 6) : tapeOffs oc os (nm j) = ![0, oc, 0, 0, 0, os] j

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.tapeHeads_castAdd {kk : ℕ} (oc os hr hp : ℤ) (i : Fin kk) : tapeHeads oc os hr hp (Fin.castAdd 6 i) = 0

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.tapeHeads_nm {kk : ℕ} (oc os hr hp : ℤ) (j : Fin 6) : tapeHeads oc os hr hp (nm j) = ![0, oc, 0, hr, hp, os] j

theorem Turing.MultiTapeTM.StackLoopKernel.cfgS_blank {kk : ℕ} {input : List Bool} (out : List Bool) : cfgS input [] [] [] [] [] 0 0 0 0 out = tapesCfg input (fun (x : Fin (kk + 6)) => []) 0 0 out

With every tape blank and every word at its start, a configuration of the stack-loop machine is a word configuration.

Embeddings of the phases

def Turing.MultiTapeTM.StackLoopKernel.owEmb {kk : ℕ} (v o : Fin 6) (hv : ↑v ≠ 0) (ho : ↑o ≠ 0) (hvo : ↑v ≠ ↑o) : Fin (kk + 1 + 2) ↪ Fin (kk + 6)

The tapes of Turing.MultiTapeTM.onWords with kk work tapes: the shared tapes, the output tape nm o, the input tape nm v and the flag tape nm 0.

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.owEmb_work {kk : ℕ} {v o : Fin 6} {hv : ↑v ≠ 0} {ho : ↑o ≠ 0} {hvo : ↑v ≠ ↑o} (i : Fin kk) : (owEmb v o hv ho hvo) (Fin.castAdd 2 i.castSucc) = Fin.castAdd 6 i

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.owEmb_out {kk : ℕ} {v o : Fin 6} {hv : ↑v ≠ 0} {ho : ↑o ≠ 0} {hvo : ↑v ≠ ↑o} : (owEmb v o hv ho hvo) (Fin.castAdd 2 (Fin.last kk)) = nm o

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.owEmb_in {kk : ℕ} {v o : Fin 6} {hv : ↑v ≠ 0} {ho : ↑o ≠ 0} {hvo : ↑v ≠ ↑o} : (owEmb v o hv ho hvo) (Fin.natAdd (kk + 1) 0) = nm v

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.owEmb_flag {kk : ℕ} {v o : Fin 6} {hv : ↑v ≠ 0} {ho : ↑o ≠ 0} {hvo : ↑v ≠ ↑o} : (owEmb v o hv ho hvo) (Fin.natAdd (kk + 1) 1) = nm 0

def Turing.MultiTapeTM.StackLoopKernel.initEmb {kk : ℕ} : Fin (kk + 1) ↪ Fin (kk + 6)

The tapes of Turing.MultiTapeTM.outputToWord with kk work tapes: the shared tapes and the current value.

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.initEmb_work {kk : ℕ} (i : Fin kk) : initEmb i.castSucc = Fin.castAdd 6 i

@[simp]

theorem Turing.MultiTapeTM.StackLoopKernel.initEmb_last {kk : ℕ} : initEmb (Fin.last kk) = nm 1

def Turing.MultiTapeTM.StackLoopKernel.pairEmb {kk : ℕ} (a b : Fin 6) (h : a ≠ b) : Fin 2 ↪ Fin (kk + 6)

Two named tapes, for a two-tape machine.

def Turing.MultiTapeTM.StackLoopKernel.copyEmb {kk : ℕ} : Fin (0 + 1 + 2) ↪ Fin (kk + 6)

The tapes of Turing.MultiTapeTM.copyWord: from the round word to the current value.

def Turing.MultiTapeTM.StackLoopKernel.emitEmb {kk : ℕ} : Fin (0 + 2) ↪ Fin (kk + 6)

The tapes of Turing.MultiTapeTM.emitWord: the current value.

Specifications on embedded tapes

theorem Turing.MultiTapeTM.StackLoopKernel.transformsTapes_onWords_embed {k K : ℕ} {Symbol : Type u_1} {S : Type u_2} {tm : MultiTapeTM k Symbol S} {x y : List Symbol} {t s : ℕ} (h : tm.TransformsTapes (fun (inp : List Symbol) (ws : Fin k → List Symbol) => inp = x ∧ ws = fun (x : Fin k) => []) (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e : List Symbol) => (ws' = fun (x : Fin k) => []) ∧ e = y) t s) (mark : Symbol) (e : Fin (k + 1 + 2) ↪ Fin K) : ((tm.onWords mark).extendTapes e).TransformsTapes (fun (x_1 : List Symbol) (ws : Fin K → List Symbol) => ws (e (Fin.natAdd (k + 1) 0)) = x ∧ ∀ (j : Fin (k + 1 + 2)), j ≠ Fin.natAdd (k + 1) 0 → ws (e j) = []) (fun (x : List Symbol) (ws ws' : Fin K → List Symbol) (em : List Symbol) => ws' = Function.update ws (e (Fin.castAdd 2 (Fin.last k))) y ∧ em = []) (t + y.length + 6) (s + 2 * x.length + 2 * y.length + 3 * k + 18 + (K - (k + 1 + 2)))

onWords on embedded tapes, with every other tape arbitrary: the input on the tape selected for the input of onWords, its other tapes blank.

Runs of the phases

noncomputable def Turing.MultiTapeTM.StackLoopKernel.clearM {kk : ℕ} (j : Fin 6) : MultiTapeTM (kk + 6) Bool (Unit ⊕ RewindWorkState)

The machine clearing the named tape j.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.copyM {kk : ℕ} : MultiTapeTM (kk + 6) Bool (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState)

Copying the round word to the blank current-value tape.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.emitM {kk : ℕ} : MultiTapeTM (kk + 6) Bool (MarkWorkState ⊕ (Unit ⊕ RewindState) ⊕ MarkWorkState)

Emitting the current value.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.wordsM {kk : ℕ} {S : Type u_1} (tm : MultiTapeTM kk Bool S) (v o : Fin 6) (hv : ↑v ≠ 0) (ho : ↑o ≠ 0) (hvo : ↑v ≠ ↑o) : MultiTapeTM (kk + 6) Bool (MarkWorkState ⊕ (S ⊕ RewindWorkState) ⊕ MarkWorkState)

Running a machine with kk work tapes on words, from the named tape v to the named tape o.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.initM {kk : ℕ} {S : Type u_1} (tm : MultiTapeTM kk Bool S) : MultiTapeTM (kk + 6) Bool (S ⊕ RewindWorkState)

The initialization: the machine reads the input and writes its output to the current-value tape.

Native phases

noncomputable def Turing.MultiTapeTM.StackLoopKernel.popM {kk : ℕ} : MultiTapeTM (kk + 6) Bool PopFrameState

Popping the stack to the round word.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.backRC {kk : ℕ} : MultiTapeTM (kk + 6) Bool CopyBackState

Moving the round word to the front of the current value.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.backPS {kk : ℕ} : MultiTapeTM (kk + 6) Bool CopyBackState

Moving the pushed frames to the front of the stack.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.eraseM {kk : ℕ} : MultiTapeTM (kk + 6) Bool EraseFrameState

Erasing the popped frame at the front of the current value.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.seekM {kk : ℕ} : MultiTapeTM (kk + 6) Bool Unit

Moving the head of the pushed frames to their end.

One round

noncomputable def Turing.MultiTapeTM.StackLoopKernel.haltM {kk : ℕ} {SH : Type u_1} (tH : MultiTapeTM kk Bool SH) : MultiTapeTM (kk + 6) Bool (MarkWorkState ⊕ (SH ⊕ RewindWorkState) ⊕ MarkWorkState)

The halting test, from the current value to the halting flag.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.pushM {kk : ℕ} {SP : Type u_1} (tP : MultiTapeTM kk Bool SP) : MultiTapeTM (kk + 6) Bool (MarkWorkState ⊕ (SP ⊕ RewindWorkState) ⊕ MarkWorkState)

The pushed frames of a round, from the current value.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.nextM {kk : ℕ} {SN : Type u_1} (tN : MultiTapeTM kk Bool SN) : MultiTapeTM (kk + 6) Bool (MarkWorkState ⊕ (SN ⊕ RewindWorkState) ⊕ MarkWorkState)

The next value of a round, from the current value to the round word.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.body {kk : ℕ} {SH : Type u_1} {SP : Type u_2} {SN : Type u_3} (tH : MultiTapeTM kk Bool SH) (tP : MultiTapeTM kk Bool SP) (tN : MultiTapeTM kk Bool SN) : MultiTapeTM (kk + 6) Bool ((Unit ⊕ RewindWorkState) ⊕ PopFrameState ⊕ CopyBackState ⊕ (MarkWorkState ⊕ (SP ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ (MarkWorkState ⊕ (SN ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ EraseFrameState ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ (Unit ⊕ RewindWorkState) ⊕ Unit ⊕ CopyBackState ⊕ MarkWorkState ⊕ (SH ⊕ RewindWorkState) ⊕ MarkWorkState)

One round: clear the halting flag, pop the stack to the front of the current value, compute the pushed frames and the next value, drop the popped frame, make the next value current, push the frames and test the next value.

The loop over a stack

def Turing.MultiTapeTM.StackLoopKernel.haltCond {kk : ℕ} : (Fin (kk + 6) → Option Bool) → Bool

The loop condition: the halting flag is false.

noncomputable def Turing.MultiTapeTM.StackLoopKernel.stackLoopTM {kk : ℕ} {SI : Type u_1} {SH : Type u_2} {SP : Type u_3} {SN : Type u_4} (tI : MultiTapeTM kk Bool SI) (tH : MultiTapeTM kk Bool SH) (tP : MultiTapeTM kk Bool SP) (tN : MultiTapeTM kk Bool SN) : MultiTapeTM (kk + 6) Bool ((SI ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ (SH ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ (((Unit ⊕ RewindWorkState) ⊕ PopFrameState ⊕ CopyBackState ⊕ (MarkWorkState ⊕ (SP ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ (MarkWorkState ⊕ (SN ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ EraseFrameState ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ (Unit ⊕ RewindWorkState) ⊕ Unit ⊕ CopyBackState ⊕ MarkWorkState ⊕ (SH ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit) ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ (Unit ⊕ RewindState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState)

The stack-loop machine: initialize the current value, test it, repeat rounds while the test fails, then emit the current value and clear the tapes.

@[reducible, inline]

abbrev Turing.MultiTapeTM.StackLoopKernel.zIn {α : Type u_1} {γ : Type u_2} (s : ℕ → α × List γ) (i : ℕ) : Option γ × α

The input of round i.

def Turing.MultiTapeTM.StackLoopKernel.roundTime {α : Type u_1} {γ : Type u_2} (encA : α ↪ List Bool) (encG : γ ↪ List Bool) (round : Option γ × α → List γ × α) (TH : α → ℕ) (TP TN : Option γ × α → ℕ) (s : ℕ → α × List γ) (i : ℕ) : ℕ

A bound on the time of round i.

def Turing.MultiTapeTM.StackLoopKernel.roundSpace {α : Type u_1} {γ : Type u_2} (encA : α ↪ List Bool) (encG : γ ↪ List Bool) (round : Option γ × α → List γ × α) (SH' : α → ℕ) (SP' SN' : Option γ × α → ℕ) (kk : ℕ) (s : ℕ → α × List γ) (i : ℕ) : ℕ

A bound on the space of round i.

theorem Turing.MultiTapeTM.StackLoopKernel.runs_stackLoop {kk : ℕ} {input : List Bool} {α : Type u_1} {γ : Type u_2} {encA : α ↪ List Bool} {encG : γ ↪ List Bool} {halt : α → Bool} {round : Option γ × α → List γ × α} {SI : Type u_3} {SH : Type u_4} {SP : Type u_5} {SN : Type u_6} {tI : MultiTapeTM kk Bool SI} {tH : MultiTapeTM kk Bool SH} {tP : MultiTapeTM kk Bool SP} {tN : MultiTapeTM kk Bool SN} {TH SH' : α → ℕ} {TP SP' TN SN' : Option γ × α → ℕ} (hH : ∀ (a : α), tH.TransformsTapes (fun (inp : List Bool) (ws : Fin kk → List Bool) => inp = encA a ∧ ws = fun (x : Fin kk) => []) (fun (x : List Bool) (x_1 ws' : Fin kk → List Bool) (e : List Bool) => (ws' = fun (x : Fin kk) => []) ∧ e = [halt a]) (TH a) (SH' a)) (hP : ∀ (z : Option γ × α), tP.TransformsTapes (fun (inp : List Bool) (ws : Fin kk → List Bool) => inp = frame ((encOption encG) z.1) ++ encA z.2 ∧ ws = fun (x : Fin kk) => []) (fun (x : List Bool) (x_1 ws' : Fin kk → List Bool) (e : List Bool) => (ws' = fun (x : Fin kk) => []) ∧ e = (encList encG) (round z).1) (TP z) (SP' z)) (hN : ∀ (z : Option γ × α), tN.TransformsTapes (fun (inp : List Bool) (ws : Fin kk → List Bool) => inp = frame ((encOption encG) z.1) ++ encA z.2 ∧ ws = fun (x : Fin kk) => []) (fun (x : List Bool) (x_1 ws' : Fin kk → List Bool) (e : List Bool) => (ws' = fun (x : Fin kk) => []) ∧ e = encA (round z).2) (TN z) (SN' z)) {tinit sinit : ℕ} (s : ℕ → α × List γ) (n : ℕ) (hI : tI.TransformsTapes (fun (inp : List Bool) (ws : Fin kk → List Bool) => inp = input ∧ ws = fun (x : Fin kk) => []) (fun (x : List Bool) (x_1 ws' : Fin kk → List Bool) (e : List Bool) => (ws' = fun (x : Fin kk) => []) ∧ e = encA (s 0).1) tinit sinit) (h0 : (s 0).2 = []) (hs : ∀ (i : ℕ), s (i + 1) = ((round (zIn s i)).2, (round (zIn s i)).1 ++ (s i).2.tail)) (hrun : ∀ i < n, halt (s i).1 = false) (hstop : halt (s n).1 = true) (hempty : (s n).2 = []) : (stackLoopTM tI tH tP tN).RunsBetween (cfgS input [] [] [] [] [] 0 0 0 0 []) (cfgS input [] [] [] [] [] 0 0 0 0 (encA (s n).1)) (tinit + TH (s 0).1 + ∑ i ∈ Finset.range n, (roundTime encA encG round TH TP TN s i + 1) + (encA (s 0).1).length + 5 * (encA (s n).1).length + 40) (sinit + SH' (s 0).1 + ∑ i ∈ Finset.range n, (roundSpace encA encG round SH' SP' SN' kk s i + (kk + 6)) + 4 * (encA (s 0).1).length + 3 * (encA (s n).1).length + 10 * kk + 100)

The run of the stack-loop machine. If s is the run of a stack loop from an initial value computed from the input with an empty stack, which halts after n rounds with an empty stack, then the machine computes the halting value, within the costs of the initialization, of the halting tests and of the rounds.