Deterministic Boolean-oracle Turing machines -- definitions

This module adds a dedicated query tape and a one-step Boolean-oracle query mechanism to the library's deterministic Turing-machine model. Local steps retain the named read-only input, read-write work, and output tapes. A query state instead reads the binary prefix currently delimited by the query-tape head, leaves every tape unchanged, and branches to one of two states according to the oracle answer.

The query cost convention is explicit: one oracle lookup is one machine step, while writing and positioning the query takes ordinary local steps. Query strings use cells 1, ..., head - 1; 1 is true and every other tape symbol is false. Constructions that need a canonical binary query should establish that those cells contain only 0 or 1.

@[reducible, inline]

abbrev Complexity.BooleanOracle : Type

A Boolean oracle answers one bit for every finite binary query string.

Equations

• Complexity.BooleanOracle = (List Bool → Bool)

def Complexity.BooleanOracle.Decides (oracle : BooleanOracle) (language : Language) : Prop

An oracle decides a language when its answer bit is its exact characteristic function on every finite query string.

Equations

• oracle.Decides language = ∀ (query : List Bool), oracle query = true ↔ query ∈ language

def Complexity.Tape.oracleQuery (tape : Tape) : List Bool

Query string delimited by the query-tape head. Cells strictly between the left marker and the head are read in increasing order. The convention is total: only 1 maps to true; 0, blank, and the left marker map to false.

Equations

• tape.oracleQuery = List.ofFn fun (index : Fin (tape.head - 1)) => match tape.cells (↑index + 1) with | Complexity.Γ.one => true | x => false

structure Complexity.OracleCfg (n : ℕ) (Q : Type) : Type

Configuration of an oracle TM with n ordinary work tapes and one dedicated read-write query tape.

• state : Q

  Current finite-control state.

• input : Tape

  Read-only input tape.

• query : Tape

  Dedicated query tape.

• work : Fin n → Tape

  Ordinary read-write work tapes.

• output : Tape

  Read-write output tape.

@[reducible, inline]

abbrev Complexity.OracleCfg.init {Q : Type} {n : ℕ} (qstart : Q) (input : List Bool) : OracleCfg n Q

Initial oracle-machine configuration.

Equations

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

def Complexity.OracleCfg.erase {n : ℕ} {Q : Type} (cfg : OracleCfg n Q) : Cfg n Q

Forget the dedicated query tape.

Equations

• cfg.erase = { state := cfg.state, input := cfg.input, work := cfg.work, output := cfg.output }

structure Complexity.OracleLocalTransition (n : ℕ) (Q : Type) : Type

One ordinary, non-query transition of an oracle TM.

• nextState : Q

  Next finite-control state.

• queryWrite : Γw

  Symbol written on the query tape.

• workWrites : Fin n → Γw

  Symbols written on the ordinary work tapes.

• outputWrite : Γw

  Symbol written on the output tape.

• inputDir : Dir3

  Input-head movement.

• queryDir : Dir3

  Query-head movement.

• workDirs : Fin n → Dir3

  Ordinary work-head movements.

• outputDir : Dir3

  Output-head movement.

structure Complexity.OracleTM (n : ℕ) : Type 1

A deterministic oracle TM with one dedicated query tape.

If queryTransition q = some (yesState, noState), state q performs an oracle lookup rather than applying localTransition; a true answer enters yesState and a false answer enters noState.

• Q : Type

  Finite type of machine states.

• decEq : DecidableEq self.Q
• finQ : Fintype self.Q
• qstart : self.Q

  Designated start state.

• qhalt : self.Q

  Designated halt state.

• queryTransition : self.Q → Option (self.Q × self.Q)

  States that perform an oracle query and their true/false successors.

• localTransition : self.Q → Γ → Γ → (Fin n → Γ) → Γ → OracleLocalTransition n self.Q

  Transition used at every non-query, non-halted state.

• localTransition_right_of_start (q : self.Q) (inputHead queryHead : Γ) (workHeads : Fin n → Γ) (outputHead : Γ) : let transition := self.localTransition q inputHead queryHead workHeads outputHead; (inputHead = Γ.start → transition.inputDir = Dir3.right) ∧ (queryHead = Γ.start → transition.queryDir = Dir3.right) ∧ (∀ (index : Fin n), workHeads index = Γ.start → transition.workDirs index = Dir3.right) ∧ (outputHead = Γ.start → transition.outputDir = Dir3.right)

  A local transition reading a left marker moves that head right.

def Complexity.OracleTM.step {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (cfg : OracleCfg n machine.Q) : Option (OracleCfg n machine.Q)

Execute one oracle-machine step. A query lookup costs exactly one step and changes only the finite-control state.

Equations

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

@[reducible, inline]

abbrev Complexity.OracleTM.initCfg {n : ℕ} (machine : OracleTM n) (input : List Bool) : OracleCfg n machine.Q

Initial configuration for an oracle TM.

Equations

• machine.initCfg input = Complexity.OracleCfg.init machine.qstart input

@[reducible, inline]

abbrev Complexity.OracleTM.halted {n : ℕ} (machine : OracleTM n) (cfg : OracleCfg n machine.Q) : Prop

An oracle configuration is halted in the designated halt state.

Equations

• machine.halted cfg = (cfg.state = machine.qhalt)

def Complexity.OracleTM.stepRel {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (cfg next : OracleCfg n machine.Q) : Prop

One-step oracle execution relation.

Equations

• machine.stepRel oracle cfg next = (machine.step oracle cfg = some next)

inductive Complexity.OracleTM.reachesIn {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) : ℕ → OracleCfg n machine.Q → OracleCfg n machine.Q → Prop

Exact-time deterministic oracle execution.

• zero {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg : OracleCfg n machine.Q} : machine.reachesIn oracle 0 cfg cfg
• step {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {cfg middle : OracleCfg n machine.Q} {time : ℕ} {result : OracleCfg n machine.Q} : machine.step oracle cfg = some middle → machine.reachesIn oracle time middle result → machine.reachesIn oracle (time + 1) cfg result

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

Oracle-machine acceptance.

Equations

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

def Complexity.OracleTM.AcceptsInTime {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (input : List Bool) (timeBound : ℕ) : Prop

Oracle-machine acceptance within a time budget.

Equations

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

def Complexity.OracleTM.DecidesInTime {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (language : Language) (timeBound : ℕ → ℕ) : Prop

An oracle TM decides a language within a length-dependent time bound.

Equations

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

def Complexity.TM.toOracleTM {n : ℕ} (machine : TM n) : OracleTM n

Regard an ordinary TM as an oracle TM whose query-state map is everywhere none. The extra query tape is operationally inert and never affects the ordinary tapes.

Equations

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