Iterating a function while its result is non-empty

tm.iterateWhile mark applies tm to its input, then to the result, and so on, until tm produces the empty word, and then outputs the last word before the empty one. tm is applied at least once, so if it maps the input itself to the empty word, the output is the input. The computation need not terminate.

The machine keeps the current word on one work tape and the next one on another. A round copies the next word to the current tape (Turing.MultiTapeTM.copyWord) and computes the new next word from it with tm. Rounds are repeated by Turing.MultiTapeTM.repeatUntilBlank until the next word is empty.

Main definitions

• Turing.MultiTapeTM.iterateWhile: the iterating machine.

Main results

• Turing.MultiTapeTM.computesTidily_iterateWhile: if tm computes w (n + 1) from w n tidily for every n ≤ r, and w (n + 1) is empty exactly for n = r, then tm.iterateWhile mark computes w r from w 0 tidily.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterateWhile: if f is tidily computable, so is a ↦ f^[r a] a, where r a is the least n such that f^[n + 1] a has the empty encoding.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength.iterateWhile: the same, with bounds on the number of rounds and on the lengths of all intermediate values in terms of the length of the input.

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.

Iterating a computable function

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterateWhile {α : Type u_3} {f : α → α} {enc : α ↪ List Bool} {t s r : α → ℕ} (hf : ComputableTidilyInTimeAndSpace f enc enc t s) (hr : ∀ (a : α), IsLeast {n : ℕ | enc (f^[n + 1] a) = []} (r a)) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (a : α) => f^[r a] a) enc enc (fun (a : α) => (r a + 1) * (((Finset.Iic (r a)).sup fun (n : ℕ) => t (f^[n] a)) + c * (((Finset.Iic (r a)).sup fun (n : ℕ) => (enc (f^[n] a)).length) + 1))) fun (a : α) => c * ((((Finset.Iic (r a)).sup fun (n : ℕ) => s (f^[n] a)) + (Finset.Iic (r a)).sup fun (n : ℕ) => (enc (f^[n] a)).length) + 1)

If f is tidily computable, so is a ↦ f^[r a] a, where r a is the least n such that f^[n + 1] a has the empty encoding. Each of the r a + 1 rounds costs at most the largest time of f on the values f^[n] a for n ≤ r a plus a term linear in their longest encoding; the space is linear in the largest space of f on these values and their longest encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength.iterateWhile {α : Type u_3} {f : α → α} {enc : α ↪ List Bool} {t s l ρ : ℕ → ℕ} {r : α → ℕ} (ht : Monotone t) (hs : Monotone s) (hf : ComputableTidilyInTimeAndSpaceOfLength f enc enc t s) (hr : ∀ (a : α), IsLeast {n : ℕ | enc (f^[n + 1] a) = []} (r a)) (hρ : ∀ (a : α), r a ≤ ρ (enc a).length) (hl : ∀ (a : α), ∀ n ≤ r a, (enc (f^[n] a)).length ≤ l (enc a).length) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpaceOfLength (fun (a : α) => f^[r a] a) enc enc (fun (n : ℕ) => (ρ n + 1) * (t (l n) + c * (l n + 1))) fun (n : ℕ) => c * (s (l n) + l n + 1)

If f is tidily computable in time t and space s of the length of its input, for monotone t and s, so is a ↦ f^[r a] a, where r a is the least n such that f^[n + 1] a has the empty encoding, provided that for inputs of length n, r a ≤ ρ n and the encodings of all f^[i] a for i ≤ r a have length at most l n.