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. The universality predicates require the compiler to be computable, so a compiled program cannot carry undecidable information such as whether the source halts.

Main definitions

• TM.IsComputable -- a string function computed by some deterministic machine
• 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 → ℕ → ℕ)

def Complexity.TM.IsComputable (function : List Bool → List Bool) : Prop

A string function is computable when some deterministic machine, with any number of work tapes, halts on every input with exactly the function's value on its output tape.

Equations

• Complexity.TM.IsComputable function = ∃ (tapes : ℕ) (machine : Complexity.TM tapes), machine.Computes function

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 computable program compiler.

Computability of the compiler is essential. Without it the predicate is trivial: a machine that prints the rest of its input after a leading 0 and diverges after a leading 1 would qualify, with a compiler that consults the source machine's halting behavior and output.

Equations

• simulator.IsUniversal = ∀ (sourceTapes : ℕ) (source : Complexity.TM sourceTapes), ∃ (compile : List Bool → List Bool), Complexity.TM.IsComputable compile ∧ 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 computable 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