TM-to-RAM time-class containment

The fixed sparse simulator transfers deterministic Turing deciders to logarithmic-cost RAM deciders through the public input/output ABI. Polynomial Turing time is therefore contained in polynomial RAM time.

theorem Complexity.RAM.TMConfig.Sparse.compiledDecision_decidesInTime {n : ℕ} {tm : TM n} {L : Language} {T : ℕ → ℕ} (hdecides : tm.DecidesInTime L T) : (compiledDecision tm).DecidesInTime L fun (inputLength : ℕ) => decisionTimeBound tm inputLength (T inputLength)

A deterministic TM time bound transfers to the fixed compiled sparse RAM simulator through the complete public input/output ABI.

theorem Complexity.RAM.TMConfig.Sparse.mem_DTIME_of_decidesInTime {n : ℕ} {tm : TM n} {L : Language} {T : ℕ → ℕ} (hdecides : tm.DecidesInTime L T) : L ∈ DTIME fun (inputLength : ℕ) => decisionTimeBound tm inputLength (T inputLength)

The explicit transferred bound packages the fixed simulator as a member of the corresponding RAM time class.

theorem Complexity.RAM.TMConfig.Sparse.P_subset_RAM_P : Complexity.P ⊆ P

Every polynomial-time Turing language is decidable in polynomial logarithmic-cost RAM time.

theorem Complexity.RAM.TMConfig.Sparse.DTIME_pow_subset_RAM_P (degree : ℕ) : (Complexity.DTIME fun (x : ℕ) => x ^ degree) ⊆ P

Every fixed polynomial Turing-time class embeds into polynomial RAM time.