Generic universal-machine interfaces

This module gives machine-independent definitions of semantic and efficient universality. A simulation compiler acts on arbitrary binary programs; its correctness does not mention a concrete description codec. Additive description overhead and an explicit program-sensitive clock are separate reusable hypotheses.

The default IsEfficientlyUniversal policy asks for a polynomial in source running time and source-program length. IsEfficientlyUniversalFor remains available for sharper policies.

Main results

• TM.Simulates.refl, TM.Simulates.comp -- semantic simulation is compositional
• TM.HasAdditiveProgramOverhead.comp -- additive compiler costs compose
• TM.SimulatesInTime.comp -- exact simulation clocks compose
• TM.PolynomialTimeOverhead.comp -- polynomial clocks survive compilation
• TM.IsEfficientlyUniversalFor.isUniversal -- efficient implies semantic
• TM.Simulates.isUniversal -- universality transfers through a simulator

theorem Complexity.TM.Simulates.refl {firstTapes : ℕ} (machine : TM firstTapes) : machine.Simulates machine id

Every machine simulates itself under the identity compiler.

theorem Complexity.TM.Simulates.comp {firstTapes secondTapes thirdTapes : ℕ} {first : TM firstTapes} {second : TM secondTapes} {third : TM thirdTapes} {compileFirst compileSecond : List Bool → List Bool} (hFirst : first.Simulates second compileFirst) (hSecond : second.Simulates third compileSecond) : first.Simulates third (compileFirst ∘ compileSecond)

Semantic simulations compose, with the inner compiler applied first.

theorem Complexity.TM.HasAdditiveProgramOverhead.id : HasAdditiveProgramOverhead _root_.id 0

The identity compiler has zero additive program overhead.

theorem Complexity.TM.HasAdditiveProgramOverhead.mono {compile : List Bool → List Bool} {first second : ℕ} (hbound : first ≤ second) (hoverhead : HasAdditiveProgramOverhead compile first) : HasAdditiveProgramOverhead compile second

A larger additive constant preserves a compiler-length bound.

theorem Complexity.TM.HasAdditiveProgramOverhead.comp {compileFirst compileSecond : List Bool → List Bool} {first second : ℕ} (hFirst : HasAdditiveProgramOverhead compileFirst first) (hSecond : HasAdditiveProgramOverhead compileSecond second) : HasAdditiveProgramOverhead (compileFirst ∘ compileSecond) (second + first)

Additive compiler-length bounds compose by addition.

theorem Complexity.TM.SimulatesInTime.refl {firstTapes : ℕ} (machine : TM firstTapes) : machine.SimulatesInTime machine id fun (x : List Bool) (sourceTime : ℕ) => sourceTime

Identity execution has the identity time overhead.

theorem Complexity.TM.SimulatesInTime.mono {firstTapes secondTapes : ℕ} {simulator : TM firstTapes} {source : TM secondTapes} {compile : List Bool → List Bool} {firstClock secondClock : TimeOverhead} (hclock : ∀ (program : List Bool) (sourceTime : ℕ), firstClock program sourceTime ≤ secondClock program sourceTime) (hsim : simulator.SimulatesInTime source compile firstClock) : simulator.SimulatesInTime source compile secondClock

Enlarging a simulation clock preserves a timed simulation.

theorem Complexity.TM.SimulatesInTime.comp {firstTapes secondTapes thirdTapes : ℕ} {first : TM firstTapes} {second : TM secondTapes} {third : TM thirdTapes} {compileFirst compileSecond : List Bool → List Bool} {clockFirst clockSecond : TimeOverhead} (hFirst : first.SimulatesInTime second compileFirst clockFirst) (hSecond : second.SimulatesInTime third compileSecond clockSecond) : first.SimulatesInTime third (compileFirst ∘ compileSecond) fun (program : List Bool) (sourceTime : ℕ) => clockFirst (compileSecond program) (clockSecond program sourceTime)

Timed simulations compose by feeding the inner compiled program and clock to the outer clock.

theorem Complexity.TM.PolynomialTimeOverhead.identity : PolynomialTimeOverhead fun (_program : List Bool) (sourceTime : ℕ) => sourceTime

The identity clock is polynomial.

theorem Complexity.TM.PolynomialTimeOverhead.comp {compileInner : List Bool → List Bool} {additive : ℕ} {clockOuter clockInner : TimeOverhead} (hlength : HasAdditiveProgramOverhead compileInner additive) (hOuter : PolynomialTimeOverhead clockOuter) (hInner : PolynomialTimeOverhead clockInner) : PolynomialTimeOverhead fun (program : List Bool) (sourceTime : ℕ) => clockOuter (compileInner program) (clockInner program sourceTime)

Polynomial clocks compose through a compiler with additive length overhead.

theorem Complexity.TM.IsEfficientlyUniversalFor.isUniversal {firstTapes : ℕ} {simulator : TM firstTapes} {admissible : TimeOverhead → Prop} (h : simulator.IsEfficientlyUniversalFor admissible) : simulator.IsUniversal

Universality for any admissible time policy implies semantic universality.

theorem Complexity.TM.IsEfficientlyUniversal.isUniversal {firstTapes : ℕ} {simulator : TM firstTapes} (h : simulator.IsEfficientlyUniversal) : simulator.IsUniversal

Polynomially efficient universality implies semantic universality.

theorem Complexity.TM.IsEfficientlyUniversalFor.mono {firstTapes : ℕ} {simulator : TM firstTapes} {firstPolicy secondPolicy : TimeOverhead → Prop} (hpolicy : ∀ (clock : TimeOverhead), firstPolicy clock → secondPolicy clock) (h : simulator.IsEfficientlyUniversalFor firstPolicy) : simulator.IsEfficientlyUniversalFor secondPolicy

Weakening the admissibility policy preserves efficient universality.

theorem Complexity.TM.Simulates.isUniversal {firstTapes secondTapes : ℕ} {first : TM firstTapes} {second : TM secondTapes} {compile : List Bool → List Bool} (hsim : first.Simulates second compile) (huniversal : second.IsUniversal) : first.IsUniversal

A simulator of a universal machine is itself universal.