Iterating a polynomial-time step until it stops

A loop whose number of rounds is not known in advance: apply a polynomial-time step to a polynomial-time start value until the result has the empty encoding, then apply a polynomial-time fin to the last value before the empty one. Neither the number of rounds r a nor a bound on the intermediate values needs to be computable. They only need to hold along the trajectory from the start value of each instance. The loop then runs within time c (r a + 1) N ^ d and space c N ^ d, where N is one more than a bound on the encoded intermediate values and the encoded instance.

This is the loop of algorithms that iterate until a fixed point, such as breadth-first search until no new element is found, where the number of rounds is bounded only through the analysis. It is built from the machine-level loop Turing.MultiTapeTM.iterateWhile, which needs the round count only along the trajectory.

Main results

• Turing.MultiTapeTM.exists_computableInTimeAndSpace_iterateWhile: iterating a polynomial-time step until the empty encoding is computable within the number of rounds times a polynomial in the size of the intermediate values.

theorem Turing.MultiTapeTM.exists_computableInTimeAndSpace_iterateWhile {α β γ : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {encOut : γ ↪ List Bool} {init : α → β} {step : β → β} {fin : β → γ} (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime step encState encState) (hfin : ComputableInPolyTime fin encState encOut) {r l : α → ℕ} (hl : ∀ (a : α), ∀ n ≤ r a, (encState (step^[n] (init a))).length ≤ l a) (hne : ∀ (a : α), ∀ n < r a, encState (step^[n + 1] (init a)) ≠ []) (hnil : ∀ (a : α), encState (step^[r a + 1] (init a)) = []) : ∃ (c : ℕ) (d : ℕ), ComputableInTimeAndSpace (fun (a : α) => fin (step^[r a] (init a))) encIn encOut (fun (a : α) => c * (r a + 1) * (l a + (encIn a).length + 1) ^ d) fun (a : α) => c * (l a + (encIn a).length + 1) ^ d

Iterating a polynomial-time step until it stops. Let init, step and fin be polynomial-time, and along the trajectory from init a let step produce a value with the empty encoding first after r a + 1 rounds, with the values up to round r a encoded within l a bits. Then fin of the value after r a rounds is computable within time c (r a + 1) N ^ d and space c N ^ d, for N = l a + |encIn a| + 1. Neither r nor l needs to be computable.