Oracle-uniform universal-machine interfaces -- definitions

An oracle simulation uses one compiler and one clock for every Boolean oracle. This quantifier order is essential: allowing the compiler to depend on the oracle could hide an entire test truth table in a nominal constant.

The admissibility policies for program length and time reuse the ordinary machine interfaces because they concern only finite program strings and numeric clocks. Oracle lookup cost is already charged by OracleTM.reachesIn.

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

Uniform semantic simulation of one oracle machine by another. The compiler is independent of the Boolean oracle.

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

  Compilation preserves and reflects halting for every oracle.

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

  Compilation preserves and reflects eventual exact output for every oracle.

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

Forward oracle-uniform simulation under an explicit clock transform.

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

  Bounded production transfers for every oracle under the same clock.

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

Oracle universality uses one compiler per source machine, uniformly over all Boolean oracles.

Equations

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

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

Oracle universality relative to an admissible clock policy. The compiler, additive length constant, and clock are all selected before the oracle.

Equations

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

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

Polynomially efficient oracle universality with additive description overhead, uniformly across every Boolean oracle.

Equations

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