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.

Iterating a computable function

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterateWhile {α : Type u_1} {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_1} {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.