Simulating a clocked oracle machine with a computed oracle

The run of a fair-coin oracle machine with every coin fixed to false, against a deterministic answer function, is the iteration of one instruction on finite storage (Turing.MultiTapePTM.answerStep, Turing.MultiTapePTM.interpret_run_pure_false): a local instruction updates the tapes, and a query installs the answer to the pending request.

Against an oracle that answers a request w with the bit g w, an instruction costs polynomial time in the encoded configuration plus one evaluation of g on the pending request (Turing.MultiTapePTM.answerStep_inO). Along a clocked run the configuration grows by a bounded amount per instruction and every request is no longer than the clock (Turing.MultiTapePTM.spaceBound_answerStep, Turing.MultiTapePTM.length_pendingRequest_le). Iterating the instruction with a binary counter (Turing.MultiTapeTM.ComputableInO.iterate) therefore simulates a run of polynomial clock within polynomial space whenever g is computable within polynomial space (Turing.MultiTapePTM.exists_computableInO_run). The time is not bounded by a polynomial: it charges, for every instruction, the largest time of g on a word no longer than the clock (Turing.MultiTapeTM.wordMax). When g is polynomial-time, both the instruction and the clocked run are polynomial-time (Turing.MultiTapePTM.computableInPolyTime_answerStep, Turing.MultiTapePTM.computableInPolyTime_run).

Main definitions

• Turing.MultiTapePTM.answerStep: one instruction against an answer function.
• Turing.MultiTapePTM.pendingQuery, Turing.MultiTapePTM.pendingRequest: the query about to be submitted and its request word.
• Turing.MultiTapeTM.wordMax: the largest value of a function on the words up to a length.

Main results

• Turing.MultiTapePTM.interpret_run_pure_false: a coin-fixed run is an iteration of answerStep.
• Turing.MultiTapePTM.answerStep_inO: the bounds of an instruction.
• Turing.MultiTapePTM.exists_computableInO_run: a clocked run against an oracle computed within polynomial space is computable within polynomial space.
• Turing.MultiTapePTM.computableInPolyTime_answerStep: an instruction against a polynomial-time oracle is polynomial-time.
• Turing.MultiTapePTM.computableInPolyTime_run: a clocked run against a polynomial-time oracle is polynomial-time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 3.4 (oracle Turing machines) and Theorem 3.7.

noncomputable def Turing.MultiTapeTM.wordMax (f : List Bool → ℕ) (N : ℕ) : ℕ

The largest value of f on the words of length at most N.

theorem Turing.MultiTapeTM.le_wordMax (f : List Bool → ℕ) {N : ℕ} {w : List Bool} (hw : w.length ≤ N) : f w ≤ wordMax f N

One instruction against an answer function

def Turing.MultiTapePTM.answerStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (answer : Operation × List Bool → List Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) : MultiTapeMachine.FiniteConfig k Bool Control Operation

One instruction of the run with every coin false, the reply to a query given by answer. A halted configuration is unchanged.

theorem Cslib.OracleComp.interpret_id_iterate {State Query : Type} {spec : OracleSpec Query} (answer : (q : Query) → spec q) (n : ℕ) (step : State → OracleComp spec State) (s : State) : interpret answer (iterate n step s) = (fun (s : Id State) => interpret answer (step s))^[n] s

Interpreting a bounded loop against an answer function iterates the interpreted body.

theorem Turing.MultiTapePTM.interpret_run_pure_false {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (answer : Operation × List Bool → List Bool) (fuel : ℕ) (input : List Bool) : Cslib.OracleComp.interpret answer (machine.run (pure false) (fun (op : Operation) (word : List Bool) => Cslib.OracleComp.query (op, word)) fuel input) = ((machine.answerStep answer)^[fuel] (MultiTapeMachine.FiniteConfig.init machine.initial input)).tapes.output

A coin-fixed run is an iteration of answerStep on finite storage, against every answer function.

The parts of an instruction

def Turing.MultiTapePTM.pendingQuery {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) : Option (Operation × Control)

The query about to be submitted: its channel and the next control state, if the machine has not halted and its next instruction, with coin false, is a query.

def Turing.MultiTapePTM.pendingRequest {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) : List Bool

The request word of the pending query, or the empty word.

def Turing.MultiTapePTM.localStep {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) : MultiTapeMachine.FiniteConfig k Bool Control Operation

The next instruction if it is local; otherwise the configuration is unchanged.

def Turing.MultiTapePTM.receiveBit {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (p : MultiTapeMachine.FiniteConfig k Bool Control Operation × Bool) : MultiTapeMachine.FiniteConfig k Bool Control Operation

Install a one-bit reply to the pending query.

theorem Turing.MultiTapePTM.answerStep_bit {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) : machine.answerStep (fun (q : Operation × List Bool) => [g q.2]) cfg = if (machine.pendingQuery cfg).isSome = true then machine.receiveBit (cfg, g (machine.pendingRequest cfg)) else machine.localStep cfg

Against an oracle answering one bit, an instruction either installs the bit for the pending request or is local.

theorem Turing.MultiTapePTM.pendingQuery_pt {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime machine.pendingQuery MultiTapeTM.encFiniteConfig (MultiTapeTM.encFinite (Option (Operation × Control)))

theorem Turing.MultiTapePTM.localStep_pt {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime machine.localStep MultiTapeTM.encFiniteConfig MultiTapeTM.encFiniteConfig

theorem Turing.MultiTapePTM.pendingRequest_pt {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime machine.pendingRequest MultiTapeTM.encFiniteConfig MultiTapeTM.encBits

theorem Turing.MultiTapePTM.receiveBit_pt {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime machine.receiveBit (MultiTapeTM.encPair MultiTapeTM.encFiniteConfig MultiTapeTM.encBool) MultiTapeTM.encFiniteConfig

Bounds

theorem Turing.MultiTapePTM.answerStep_inO {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] {g : List Bool → Bool} {Tg Sg : List Bool → ℕ} (hg : MultiTapeTM.ComputableInO g MultiTapeTM.encBits MultiTapeTM.encBool Tg Sg) : ∃ (e : ℕ), MultiTapeTM.ComputableInO (machine.answerStep fun (q : Operation × List Bool) => [g q.2]) MultiTapeTM.encFiniteConfig MultiTapeTM.encFiniteConfig (fun (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) => ((MultiTapeTM.encFiniteConfig cfg).length + 1) ^ e + Tg (machine.pendingRequest cfg)) fun (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) => ((MultiTapeTM.encFiniteConfig cfg).length + 1) ^ e + Sg (machine.pendingRequest cfg)

The bounds of an instruction. Against an oracle answering [g w] to a request w, an instruction takes polynomial time and space in the encoded configuration, plus the time and space of g on the pending request.

theorem Turing.MultiTapePTM.spaceBound_answerStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) {inputSize steps : ℕ} {cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation} (h : MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps 1 cfg) : MultiTapeMachine.FiniteConfig.SpaceBound inputSize (steps + 1) 1 (machine.answerStep (fun (q : Operation × List Bool) => [g q.2]) cfg)

An instruction against a one-bit oracle grows the storage by a bounded amount.

theorem Turing.MultiTapePTM.length_pendingRequest_le {k : ℕ} {Control Operation : Type} (machine : MultiTapePTM k Bool Control Operation) {inputSize steps answerSize : ℕ} {cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation} (h : MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps answerSize cfg) : (machine.pendingRequest cfg).length ≤ steps

A pending request after steps instructions has at most steps symbols.

theorem Turing.MultiTapePTM.exists_computableInO_run {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Finite Operation] {α : Type} {input : α ↪ List Bool} {g : List Bool → Bool} {Tg Sg : List Bool → ℕ} (hg : MultiTapeTM.ComputableInO g MultiTapeTM.encBits MultiTapeTM.encBool Tg Sg) (hSg : MultiTapeTM.PolyBounded List.length Sg) (c d : ℕ) : ∃ (T : α → ℕ) (S : α → ℕ), MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) S ∧ MultiTapeTM.ComputableInO (fun (a : α) => Cslib.OracleComp.interpret (fun (q : Operation × List Bool) => [g q.2]) (machine.run (pure false) (fun (op : Operation) (word : List Bool) => Cslib.OracleComp.query (op, word)) (c * ((input a).length + 1) ^ d) (input a))) input MultiTapeTM.encBits T S

A clocked coin-false run against a plain oracle decider is computable within polynomial space. Both oracle and run certificates charge encoded output in workspace. The independent time and workspace bounds are exactly those of the tidy simulation; only the realizing-machine presentation changes. No polynomial time bound on the oracle is assumed.

theorem Turing.MultiTapePTM.computableInPolyTime_answerStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] {g : List Bool → Bool} (hg : MultiTapeTM.ComputableInPolyTime g MultiTapeTM.encBits MultiTapeTM.encBool) : MultiTapeTM.ComputableInPolyTime (machine.answerStep fun (q : Operation × List Bool) => [g q.2]) MultiTapeTM.encFiniteConfig MultiTapeTM.encFiniteConfig

An instruction against a polynomial-time oracle is polynomial-time. Against an oracle answering [g w] to a request w, with g polynomial-time, an instruction is polynomial-time in the encoded configuration: it either installs g of the pending request or is local.

theorem Turing.MultiTapePTM.computableInPolyTime_run {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Finite Operation] {α : Type} {input : α ↪ List Bool} {g : List Bool → Bool} (hg : MultiTapeTM.ComputableInPolyTime g MultiTapeTM.encBits MultiTapeTM.encBool) (c d : ℕ) : MultiTapeTM.ComputableInPolyTime (fun (a : α) => Cslib.OracleComp.interpret (fun (q : Operation × List Bool) => [g q.2]) (machine.run (pure false) (fun (op : Operation) (word : List Bool) => Cslib.OracleComp.query (op, word)) (c * ((input a).length + 1) ^ d) (input a))) input MultiTapeTM.encBits

A clocked run against a polynomial-time oracle is polynomial-time. Against the oracle answering [g w] to a request w, where g is polynomial-time, the run with every coin fixed to false under the clock c * (n + 1) ^ d is polynomial-time in the encoded input.