Pointwise output semantics for deterministic oracle TMs -- definitions

Programs are ordinary finite binary inputs; the Boolean oracle is a separate semantic parameter. Production records the complete binary output and an explicit bound on local steps plus one-step oracle lookups.

def Complexity.OracleTM.HaltsInTime {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (program : List Bool) (time : ℕ) : Prop

An oracle machine halts on a program within an explicit step budget.

Equations

• machine.HaltsInTime oracle program time = ∃ (cfg : Complexity.OracleCfg n machine.Q), ∃ steps ≤ time, machine.reachesIn oracle steps (machine.initCfg program) cfg ∧ machine.halted cfg

def Complexity.OracleTM.Halts {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (program : List Bool) : Prop

Eventual oracle-machine halting, expressed through some finite clock.

Equations

• machine.Halts oracle program = ∃ (time : ℕ), machine.HaltsInTime oracle program time

def Complexity.OracleTM.ProducesInTime {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (program output : List Bool) (time : ℕ) : Prop

An oracle machine produces an exact output within an explicit step budget.

Equations

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

def Complexity.OracleTM.Produces {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (program output : List Bool) : Prop

Eventual oracle-machine production, expressed through some finite clock.

Equations

• machine.Produces oracle program output = ∃ (time : ℕ), machine.ProducesInTime oracle program output time