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.computableInO_universal: a plain native machine certificate for the strengthened time and space bounds, including a zero clock.

• 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) ^ 4 * J ^ 2 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) ^ 4 * J ^ 2 ∧ 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 + 1) ^ 4 * J ^ 2) and its space O((B + 1) ^ 2 * J). Here B includes the encoded input length, so this is not a fixed-machine quadratic-time simulation bound when the input length varies. The buffered logarithmic-overhead simulation requires a different tape representation.

theorem Turing.MultiTapeTM.Universal.computableInO_universal : ComputableInO universal eIn eOut (fun (i : Desc × List ℕ × ℕ) => ((eIn i).length + 1) ^ 4 * (i.2.2 + 1) ^ 2) fun (i : Desc × List ℕ × ℕ) => ((eIn i).length + 1) ^ 2 * (i.2.2 + 1)

A plain native machine computes the clocked universal function within a quartic factor in the complete encoded input length and a quadratic factor in the number of simulated steps. The statement includes a zero clock. Its size factor includes the simulated input and binary clock, so it does not assert fixed-machine quadratic simulation as those inputs vary.