The existing iterate-while machine and its fixed-machine run law

Machine programs, tape layouts and resource formulas are preserved from the original module.

The tapes

The machine

@[reducible, inline]

abbrev Turing.MultiTapeTM.IterateWhileRoundState (State : Type u_3) : Type u_3

The states of Turing.MultiTapeTM.iterateWhileRound.

@[reducible, inline]

abbrev Turing.MultiTapeTM.IterateWhileState (State : Type u_3) : Type u_3

The states of Turing.MultiTapeTM.iterateWhile.

noncomputable def Turing.MultiTapeTM.iterateWhile {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (mark : Symbol) : MultiTapeTM (k + 1 + 2) Symbol (IterateWhileState State)

tm, applied repeatedly while its result is non-empty, using mark to flag the left end of words: load the input to the next tape, repeat rounds until the next tape is empty, then output the current word and clear its tape.

The phases

Iterating a machine

theorem Turing.MultiTapeTM.computesTidily_iterateWhile {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {w : ℕ → List Symbol} {r t s l : ℕ} (h : ∀ n ≤ r, tm.ComputesTidilyInTimeAndSpace (w n) (w (n + 1)) t s) (hl : ∀ n ≤ r, (w n).length ≤ l) (hne : ∀ n < r, w (n + 1) ≠ []) (hnil : w (r + 1) = []) (mark : Symbol) : (tm.iterateWhile mark).ComputesTidilyInTimeAndSpace (w 0) (w r) ((r + 1) * (t + 10 * l + 24) + 8 * l + 17) (2 * (k + 3) * (s + 10 * l + 6 * k + 44) + 5 * l + 4 * k + 26)

If tm computes w (n + 1) from w n tidily within t steps and s cells for every n ≤ r, the words w n for n ≤ r have length at most l, and w (n + 1) is empty exactly for n = r, then tm.iterateWhile mark computes w r from w 0 tidily.