Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.TMConfig.Sparse.Containment.Internal

TM-to-RAM time-class containment -- proof internals #

This module lifts the checked public-ABI sparse simulation from one halting run to deciders and then discharges the polynomial-bound arithmetic needed for the forward machine-model robustness theorem.

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

Polynomial bounds on the sparse simulation's resource functions #

Extensions of the generic PolyBound API of Complexitylib.Asymptotics.PolyBound to the register, word, marshalling, and running-time bounds of this simulation. They live in the root PolyBound namespace so that dot notation reaches them.

source
theorem Complexity.PolyBound.width {f : ℕ → ℕ} (hf : PolyBound f) :
PolyBound fun (inputLength : ℕ) => RAM.bitlen (f inputLength) + 1
source
theorem Complexity.PolyBound.registerBound (workTapes : ℕ) {f : ℕ → ℕ} (hf : PolyBound f) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.registerBound workTapes (f inputLength)
source
theorem Complexity.PolyBound.wordBound {n : ℕ} (tm : TM n) {f : ℕ → ℕ} (hf : PolyBound f) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.wordBound tm (f inputLength)
source
theorem Complexity.PolyBound.wordWidth {n : ℕ} (tm : TM n) {f : ℕ → ℕ} (hf : PolyBound f) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.wordWidth tm (f inputLength)
source
theorem Complexity.PolyBound.marshalBaseBound (workTapes : ℕ) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalBaseBound workTapes inputLength
source
theorem Complexity.PolyBound.marshalBound (workTapes : ℕ) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalBound workTapes inputLength
source
theorem Complexity.PolyBound.marshalBaseWidth (workTapes : ℕ) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalBaseWidth workTapes inputLength
source
theorem Complexity.PolyBound.marshalWidth (workTapes : ℕ) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalWidth workTapes inputLength
source
theorem Complexity.PolyBound.marshalLoopTimeBound (workTapes : ℕ) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalLoopTimeBound workTapes inputLength
source
theorem Complexity.PolyBound.marshalLeafTimeBound {n : ℕ} (tm : TM n) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalLeafTimeBound tm inputLength
source
theorem Complexity.PolyBound.marshalTimeBound {n : ℕ} (tm : TM n) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.marshalTimeBound tm inputLength
source
theorem Complexity.PolyBound.decisionTimeBound {n : ℕ} (tm : TM n) {T : ℕ → ℕ} (hT : PolyBound T) :
PolyBound fun (inputLength : ℕ) => RAM.TMConfig.Sparse.decisionTimeBound tm inputLength (T inputLength)
source
theorem Complexity.RAM.TMConfig.Sparse.P_subset_internal :
Complexity.P ⊆ P