Polynomial resource bounds for the universal simulator

The resource functions of Christian Reitwiessner's universal simulator admit explicit polynomial bounds in the encoded description length, encoded input length, clock length, and number of simulated steps. These estimates are shared by unary-clock polynomial-time simulation and the time-hierarchy construction.

Main results

• Turing.MultiTapeTM.Universal.runBound_mono: the space bound grows with the number of steps.
• Turing.MultiTapeTM.Universal.universal_bounds_le: for D, N, L ≤ B and 1 ≤ J, the time expression is at most 100000 * (B + 1) ^ 5 * J ^ 3 and the space bound is at most 200 * (B + 1) ^ 2 * J.

theorem Turing.MultiTapeTM.Universal.runBound_mono {D N t t' : ℕ} (h : t ≤ t') : runBound D N t ≤ runBound D N t'

The universal simulator's space bound grows with the number of simulated steps.

theorem Turing.MultiTapeTM.Universal.universal_bounds_le {D N J B L : ℕ} (hD : D ≤ B) (hN : N ≤ B) (hL : L ≤ B) (hJ : 1 ≤ J) : (J + 1) * (stepBound D N J + runBound D N J + (L + 1) ^ 2) ≤ 100000 * (B + 1) ^ 5 * J ^ 3 ∧ runBound D N J ≤ 200 * (B + 1) ^ 2 * J

The resources of the universal run. If the encoded description, the encoded input and the number of digits L of the clock have length at most B, the time of the universal function on J ≥ 1 steps is O(B ^ 5 * J ^ 3) and its space O(B ^ 2 * J).