The universal machine: headline theorems

Arora–Barak Theorem 1.9 (efficient universal simulation), in two forms:

• utmTM_simulates_decider — for any description α (with the standing region side condition, satisfied by every canonical encoding), if the interpreted machine decides L in time T, then the fixed machine utmTM decides membership of x from the input pair α x within utmTime α (T |x|) |x| steps — linear in T with per-description constants.
• utmTM_universal — one fixed six-work-tape machine universally simulates every multi-tape decider: for each TM k deciding L in time T there is a description α such that utmTM decides L's membership from paired inputs within utmTime α (singleTapeSimTime k T ·) · — the quadratic factor coming solely from the single-tape reduction.

def Complexity.TM.UTMBody.utmTime (α : List Bool) (T n : ℕ) : ℕ

Total running time of the universal machine on pair α x when the simulated machine halts within T steps (n = |x|). Linear in T; all other dependence is on the description alone.

Equations

• Complexity.TM.UTMBody.utmTime α T n = 4 * (2 * α.length + 2 + n) + 4 * (Complexity.groupPairs α).length + 25 + ((T + 1) * Complexity.TM.UTMBody.utmStepTime α + 1 + (2 * T + 9))

theorem Complexity.TM.UTMBody.utmTM_simulates_decider {α : List Bool} (hterm : TerminatedRegion α) {L : Language} {T : ℕ → ℕ} (hdec : (decodeDesc α).toTM.DecidesInTime L T) (x : List Bool) : ∃ (c' : Cfg 6 utmTM.Q), ∃ t ≤ utmTime α (T x.length) x.length, utmTM.reachesIn t (utmTM.initCfg (pair α x)) c' ∧ utmTM.halted c' ∧ (x ∈ L → c'.output.cells 1 = Γ.one) ∧ (x ∉ L → c'.output.cells 1 = Γ.zero)

Universal simulation of deciders (AB Theorem 1.9). If the machine described by α decides L within T, the universal machine reads pair α x and reports x ∈ L within utmTime α (T |x|) |x| steps.

theorem Complexity.TM.UTMBody.utmTM_universal {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) : ∃ (α : List Bool), ∀ (x : List Bool), ∃ (c' : Cfg 6 utmTM.Q), ∃ t ≤ utmTime α (NTM.singleTapeSimTime k T x.length) x.length, utmTM.reachesIn t (utmTM.initCfg (pair α x)) c' ∧ utmTM.halted c' ∧ (x ∈ L → c'.output.cells 1 = Γ.one) ∧ (x ∉ L → c'.output.cells 1 = Γ.zero)

One machine simulates them all: for every multi-tape decider there is a description under which the fixed universal machine decides the same language from paired inputs, at single-tape-reduction (quadratic) cost.

theorem Complexity.TM.UTMBody.utmTM_universal_padded {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) : ∃ (α₀ : List Bool), ∀ (junk x : List Bool), ∃ (c' : Cfg 6 utmTM.Q), ∃ t ≤ utmTime (α₀ ++ junk) (NTM.singleTapeSimTime k T x.length) x.length, utmTM.reachesIn t (utmTM.initCfg (pair (α₀ ++ junk) x)) c' ∧ utmTM.halted c' ∧ (x ∈ L → c'.output.cells 1 = Γ.one) ∧ (x ∉ L → c'.output.cells 1 = Γ.zero)

Padded universality: the description of a decider works under arbitrary padding — every machine has descriptions of every sufficiently large length, all correctly simulated. This is the form the hierarchy-theorem diagonalization consumes.