Oracle-uniform universal-machine interfaces

The same finite compiler and simulation clock must work for every Boolean oracle. Semantic and timed simulations compose, and efficient oracle universality implies semantic oracle universality.

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

Every oracle machine simulates itself under the identity compiler.

theorem Complexity.OracleTM.Simulates.comp {firstTapes secondTapes thirdTapes : ℕ} {first : OracleTM firstTapes} {second : OracleTM secondTapes} {third : OracleTM thirdTapes} {compileFirst compileSecond : List Bool → List Bool} (hfirst : first.Simulates second compileFirst) (hsecond : second.Simulates third compileSecond) : first.Simulates third (compileFirst ∘ compileSecond)

Oracle-uniform semantic simulations compose.

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

Identity execution has identity oracle-simulation overhead.

theorem Complexity.OracleTM.SimulatesInTime.comp {firstTapes secondTapes thirdTapes : ℕ} {first : OracleTM firstTapes} {second : OracleTM secondTapes} {third : OracleTM thirdTapes} {compileFirst compileSecond : List Bool → List Bool} {clockFirst clockSecond : TM.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 oracle-uniform simulations compose by nesting their clocks.

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

Efficient oracle universality for any clock policy implies semantic oracle universality.

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

Polynomially efficient oracle universality implies semantic oracle universality.

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

Weakening the admissible clock policy preserves oracle universality.