Generic universal-machine interfaces

These definitions describe universal simulation independently of any concrete machine encoding, pairing function, work-tape count, or overhead formula. Semantic simulation, compiler length, and simulation time are separate predicates so later invariance theorems can request exactly the hypotheses they need.

Main definitions

• TM.Simulates -- preservation of halting and exact string output
• TM.HasAdditiveProgramOverhead -- an additive compiler-length bound
• TM.SimulatesInTime -- forward simulation under an explicit clock transform
• TM.PolynomialTimeOverhead -- a polynomial policy for clock transforms
• TM.IsUniversal -- semantic universality over every work-tape count
• TM.IsEfficientlyUniversalFor -- universality relative to an overhead policy
• TM.IsEfficientlyUniversal -- the polynomial-overhead specialization

@[reducible, inline]

abbrev Complexity.TM.TimeOverhead : Type

A simulation clock may depend on the source program and its source-machine time budget. Keeping the complete program available makes clock composition exact; asymptotic policies below constrain this dependence through its length.

Equations

• Complexity.TM.TimeOverhead = (List Bool → ℕ → ℕ)

structure Complexity.TM.Simulates {simulatorTapes sourceTapes : ℕ} (simulator : TM simulatorTapes) (source : TM sourceTapes) (compile : List Bool → List Bool) : Prop

simulator semantically simulates source under compile when compilation preserves both raw halting and every exact binary-string output. This is a partial-function semantics: no concrete description syntax is built in.

• halts_iff (program : List Bool) : simulator.Halts (compile program) ↔ source.Halts program

  Compilation preserves and reflects halting.

• produces_iff (program output : List Bool) : simulator.Produces (compile program) output ↔ source.Produces program output

  Compilation preserves and reflects exact string outputs.

def Complexity.TM.HasAdditiveProgramOverhead (compile : List Bool → List Bool) (constant : ℕ) : Prop

Compiler compile adds at most constant bits to every program.

Equations

• Complexity.TM.HasAdditiveProgramOverhead compile constant = ∀ (program : List Bool), (compile program).length ≤ program.length + constant

structure Complexity.TM.SimulatesInTime {simulatorTapes sourceTapes : ℕ} (simulator : TM simulatorTapes) (source : TM sourceTapes) (compile : List Bool → List Bool) (clock : TimeOverhead) : Prop

A forward, resource-aware simulation statement. Source halting and exact output production under budget sourceTime are reproduced under clock clock program sourceTime. Untimed reflection belongs to Simulates and is intentionally separate.

• halts (program : List Bool) (sourceTime : ℕ) : source.HaltsInTime program sourceTime → simulator.HaltsInTime (compile program) (clock program sourceTime)

  Bounded source halting transfers through the compiler and clock.

• produces (program output : List Bool) (sourceTime : ℕ) : source.ProducesInTime program output sourceTime → simulator.ProducesInTime (compile program) output (clock program sourceTime)

  Bounded exact-output production transfers through the compiler and clock.

def Complexity.TM.PolynomialTimeOverhead (clock : TimeOverhead) : Prop

A clock transform is polynomial when one bivariate polynomial in source time and source-program length bounds it everywhere. Constants may depend on the simulated machine, as they do for ordinary universal simulation.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.IsUniversal {simulatorTapes : ℕ} (simulator : TM simulatorTapes) : Prop

A machine is semantically universal when it simulates every deterministic machine, with any finite number of work tapes, under some program compiler.

Equations

• simulator.IsUniversal = ∀ (sourceTapes : ℕ) (source : Complexity.TM sourceTapes), ∃ (compile : List Bool → List Bool), simulator.Simulates source compile

def Complexity.TM.IsEfficientlyUniversalFor {simulatorTapes : ℕ} (simulator : TM simulatorTapes) (admissible : TimeOverhead → Prop) : Prop

Universality relative to a chosen admissibility policy for time overhead. Every source machine receives a semantic compiler, an additive program-length constant, and an explicit clock satisfying admissible.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.IsEfficientlyUniversal {simulatorTapes : ℕ} (simulator : TM simulatorTapes) : Prop

Polynomially efficient universality with additive description overhead.

Equations

• simulator.IsEfficientlyUniversal = simulator.IsEfficientlyUniversalFor Complexity.TM.PolynomialTimeOverhead