Routing a single oracle channel

Embed a single-channel fair-coin oracle machine into a named channel of a multi-channel machine. The embedding preserves every machine step and the complete stateful interaction.

Main definitions

• Turing.MultiTapePTM.singleOracle: route the machine's sole channel to a selected channel.
• Turing.MultiTapePTM.embedSingleConfig: place a single-channel configuration on that channel.

Main results

• Turing.MultiTapePTM.runOracle_singleOracle: the embedded run interprets each query on the selected channel.

def Turing.MultiTapePTM.singleOracle {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] (i₀ : ι) (machine : MultiTapePTM k Symbol State Unit) : MultiTapePTM k Symbol State ι

Embed a single-channel fair-coin machine on channel i₀ : ι, leaving all other channels unused.

def Turing.MultiTapePTM.embedSingleConfig {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] {input : List Symbol} (i₀ : ι) (cfg : MultiTapeMachine.Config k Symbol State Unit input) : MultiTapeMachine.Config k Symbol State ι input

Configuration embedding placing the single channel on i₀ and empty channels elsewhere.

@[simp]

theorem Turing.MultiTapePTM.embedSingleConfig_tapes {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] {input : List Symbol} (i₀ : ι) (cfg : MultiTapeMachine.Config k Symbol State Unit input) : (embedSingleConfig i₀ cfg).tapes = cfg.tapes

@[simp]

theorem Turing.MultiTapePTM.embedSingleConfig_initial {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] (i₀ : ι) (machine : MultiTapePTM k Symbol State Unit) (input : List Symbol) : embedSingleConfig i₀ (MultiTapeMachine.initialConfig machine input) = MultiTapeMachine.initialConfig (singleOracle i₀ machine) input

@[simp]

theorem Turing.MultiTapePTM.embedSingleConfig_answerSymbols {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] {input : List Symbol} (i₀ : ι) (cfg : MultiTapeMachine.Config k Symbol State Unit input) : (embedSingleConfig i₀ cfg).answerSymbols i₀ = cfg.answerSymbols ()

theorem Turing.MultiTapePTM.embedSingleConfig_step {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] {input : List Symbol} (i₀ : ι) (cfg : MultiTapeMachine.Config k Symbol State Unit input) (action : Action k Symbol State) (qSym : Unit → Option Symbol) (aMove : Unit → SignType) : ((embedSingleConfig i₀ cfg).step action (fun (j : ι) => if j = i₀ then qSym () else none) fun (j : ι) => if j = i₀ then aMove () else 0) = embedSingleConfig i₀ (cfg.step action qSym aMove)

theorem Turing.MultiTapePTM.embedSingleConfig_receive {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] {input : List Symbol} (i₀ : ι) (cfg : MultiTapeMachine.Config k Symbol State Unit input) (next : State) (answer : List Symbol) : (embedSingleConfig i₀ cfg).receive i₀ next answer = embedSingleConfig i₀ (cfg.receive () next answer)

theorem Turing.MultiTapePTM.runOracle_singleOracle {k : ℕ} {Symbol State ι : Type} [DecidableEq ι] (i₀ : ι) (machine : MultiTapePTM k Symbol State Unit) (fuel : ℕ) (input : List Symbol) : (singleOracle i₀ machine).runOracle fuel input = Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => Cslib.OracleComp.query (Sum.inl n)) fun (q : Unit × List Symbol) => Cslib.ProbOracleComp.query (i₀, q.2)) (machine.runOracle fuel input)

Running singleOracle i₀ machine forwards every query ((), word) to (i₀, word).