Deterministic Boolean-oracle Turing machines

The oracle model has a dedicated query tape and charges one step per lookup. Writing the query remains part of ordinary machine execution. Exact-time runs are deterministic, and the ordinary-TM embedding has no query states, is independent of the supplied oracle, and erases step-for-step to the source TM.

This first layer is deterministic. Nondeterministic oracle execution and relativized complexity classes are deliberately left to subsequent modules.

@[simp]

theorem Complexity.Tape.length_oracleQuery (tape : Tape) : tape.oracleQuery.length = tape.head - 1

A query contains exactly the cells strictly between the left marker and the query-tape head.

@[simp]

theorem Complexity.OracleCfg.erase_init {Q : Type} {n : ℕ} (qstart : Q) (input : List Bool) : (init qstart input).erase = Cfg.init qstart input

Erasing the query tape from an initial oracle configuration gives the ordinary initial configuration.

theorem Complexity.OracleTM.step_eq_none_iff_halted {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} : machine.step oracle cfg = none ↔ machine.halted cfg

An oracle step is absent exactly at the halt state.

theorem Complexity.OracleTM.stepRel_functional {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg first second : OracleCfg n machine.Q} (hfirst : machine.stepRel oracle cfg first) (hsecond : machine.stepRel oracle cfg second) : first = second

Deterministic one-step oracle execution has at most one successor.

theorem Complexity.OracleTM.reachesIn_functional {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {time : ℕ} {start first second : OracleCfg n machine.Q} (hfirst : machine.reachesIn oracle time start first) (hsecond : machine.reachesIn oracle time start second) : first = second

An exact-time deterministic oracle run has a unique final configuration.

theorem Complexity.OracleTM.reachesIn_map {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {workTapes : ℕ} {target : TM workTapes} (mapCfg : OracleCfg n machine.Q → Cfg workTapes target.Q) (hstep : ∀ {cfg next : OracleCfg n machine.Q}, machine.step oracle cfg = some next → target.step (mapCfg cfg) = some (mapCfg next)) {time : ℕ} {start result : OracleCfg n machine.Q} (hreach : machine.reachesIn oracle time start result) : target.reachesIn time (mapCfg start) (mapCfg result)

A step-preserving configuration map sends an exact-time oracle run to an exact-time run of an ordinary target machine.

theorem Complexity.OracleTM.step_query_true {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = true) : machine.step oracle cfg = some { state := yesState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

A true oracle answer enters the declared true-successor state and leaves all tapes unchanged.

theorem Complexity.OracleTM.step_query_false {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = false) : machine.step oracle cfg = some { state := noState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

A false oracle answer enters the declared false-successor state and leaves all tapes unchanged.

theorem Complexity.OracleTM.reachesIn_one_query_true {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = true) : machine.reachesIn oracle 1 cfg { state := yesState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

A true oracle lookup is one exact execution step.

theorem Complexity.OracleTM.reachesIn_one_query_false {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} {yesState noState : machine.Q} (hhalt : cfg.state ≠ machine.qhalt) (hquery : machine.queryTransition cfg.state = some (yesState, noState)) (hanswer : oracle cfg.query.oracleQuery = false) : machine.reachesIn oracle 1 cfg { state := noState, input := cfg.input, query := cfg.query, work := cfg.work, output := cfg.output }

A false oracle lookup is one exact execution step.

@[simp]

theorem Complexity.TM.toOracleTM_queryTransition {n : ℕ} (machine : TM n) (state : machine.Q) : machine.toOracleTM.queryTransition state = none

The ordinary-machine embedding has no query states.

theorem Complexity.TM.toOracleTM_step_oracle_independent {n : ℕ} (machine : TM n) (first second : BooleanOracle) (cfg : OracleCfg n machine.Q) : machine.toOracleTM.step first cfg = machine.toOracleTM.step second cfg

Every step of an embedded ordinary machine is independent of the oracle.

theorem Complexity.TM.erase_toOracleTM_step {n : ℕ} (machine : TM n) (oracle : BooleanOracle) (cfg : OracleCfg n machine.Q) : Option.map OracleCfg.erase (machine.toOracleTM.step oracle cfg) = machine.step cfg.erase

Erasing the query tape after one embedded-machine step agrees exactly with one step of the source ordinary TM.

theorem Complexity.TM.erase_toOracleTM_reachesIn {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {time : ℕ} {start result : OracleCfg n machine.Q} (hreach : machine.toOracleTM.reachesIn oracle time start result) : machine.reachesIn time start.erase result.erase

Erasing the query tape sends every exact-time embedded-machine run to the source ordinary-machine run with the same number of steps.

theorem Complexity.TM.exists_toOracleTM_step_of_step_erase {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {cfg : OracleCfg n machine.Q} {next : Cfg n machine.Q} (hstep : machine.step cfg.erase = some next) : ∃ (oracleNext : OracleCfg n machine.toOracleTM.Q), machine.toOracleTM.step oracle cfg = some oracleNext ∧ oracleNext.erase = next

Every source-machine step lifts to an embedded oracle-machine step from any configuration with the required erased ordinary state.

theorem Complexity.TM.exists_toOracleTM_reachesIn_of_reachesIn_erase {n : ℕ} (machine : TM n) (oracle : BooleanOracle) {time : ℕ} (start : OracleCfg n machine.Q) {result : Cfg n machine.Q} (hreach : machine.reachesIn time start.erase result) : ∃ (oracleResult : OracleCfg n machine.toOracleTM.Q), machine.toOracleTM.reachesIn oracle time start oracleResult ∧ oracleResult.erase = result

Every exact-time source run lifts to an exact-time embedded oracle run; the final configuration erases to the source result.

theorem Complexity.TM.toOracleTM_decidesInTime_iff {n : ℕ} (machine : TM n) (oracle : BooleanOracle) (language : Language) (timeBound : ℕ → ℕ) : machine.toOracleTM.DecidesInTime oracle language timeBound ↔ machine.DecidesInTime language timeBound

The ordinary-machine embedding decides exactly the same timed languages, for every supplied oracle.