Deterministic replay of Boolean oracle replies

One transcript bit is assigned to every native instruction. A query installs that bit as its one-symbol reply; a local instruction ignores it. Thus replay requires no external oracle and is polynomial-time in the input and transcript lengths, including the construction of adaptive requests. The canonical transcript records the actual oracle reply at query instructions and false elsewhere. Replaying it recovers the complete coin-fixed configuration and output.

The replay* declarations here replay supplied oracle replies with the coin fixed to false. The saved-coin controller Turing.MultiTapePTM.replay in Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay.lean instead replays supplied random coins for a closed machine using an additional work tape.

Main definitions

• Turing.MultiTapePTM.replyStep: one native instruction with a supplied Boolean reply.
• Turing.MultiTapePTM.replayConfig: replay a transcript from the initial configuration.
• Turing.MultiTapePTM.replayPrefix: replay only the given prefix of a transcript.
• Turing.MultiTapePTM.oracleReplies: the canonical instruction-indexed oracle transcript.

Main results

• Turing.MultiTapePTM.replayConfig_pt: replay is polynomial-time.
• Turing.MultiTapePTM.computableInPolyTime_replayPrefix, Turing.MultiTapePTM.computableInPolyTime_replayOutput: prefix configurations and the replayed output are polynomial-time.
• Turing.MultiTapePTM.length_pendingRequest_replayPrefix_le: request size is bounded by the number of elapsed instructions.
• Turing.MultiTapePTM.replayOutput_oracleReplies: canonical replay is the certified oracle run.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 3.4.

def Turing.MultiTapePTM.replyStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (bit : Bool) : MultiTapeMachine.FiniteConfig k Bool Control Operation

Execute one native instruction, using bit only if that instruction makes a query.

def Turing.MultiTapePTM.replayFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (answers : List Bool) : MultiTapeMachine.FiniteConfig k Bool Control Operation

Replay assigns one bit to every native instruction, including local and halted ones.

def Turing.MultiTapePTM.replayConfig {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) : MultiTapeMachine.FiniteConfig k Bool Control Operation

Replay the given instruction-indexed replies from the initial configuration.

def Turing.MultiTapePTM.replayPrefix {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) (index : ℕ) : MultiTapeMachine.FiniteConfig k Bool Control Operation

The configuration immediately before instruction index, or after the whole transcript if index exceeds its length.

def Turing.MultiTapePTM.replayOutput {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) : List Bool

The output tape after replaying the entire transcript.

theorem Turing.MultiTapePTM.replyStep_eq_answerStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (bit : Bool) : machine.replyStep cfg bit = machine.answerStep (fun (x : Operation × List Bool) => [bit]) cfg

A supplied bit is equivalent to a constant one-bit oracle for this instruction.

theorem Turing.MultiTapePTM.replyStep_pendingRequest {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) : machine.replyStep cfg (g (machine.pendingRequest cfg)) = machine.answerStep (fun (q : Operation × List Bool) => [g q.2]) cfg

Supplying the answer to the pending request recovers an instruction against that oracle.

theorem Turing.MultiTapePTM.replyStep_of_pendingQuery_eq_none {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) {cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation} (h : machine.pendingQuery cfg = none) (bit : Bool) : machine.replyStep cfg bit = machine.localStep cfg

A local instruction ignores its transcript bit.

theorem Turing.MultiTapePTM.replayFrom_append {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (first second : List Bool) : machine.replayFrom cfg (first ++ second) = machine.replayFrom (machine.replayFrom cfg first) second

Replaying concatenated transcripts is sequential replay.

theorem Turing.MultiTapePTM.replayConfig_append_singleton {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) (bit : Bool) : machine.replayConfig input (answers ++ [bit]) = machine.replyStep (machine.replayConfig input answers) bit

Appending a bit executes exactly one further instruction.

theorem Turing.MultiTapePTM.replayPrefix_succ {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) (index : ℕ) (hindex : index < answers.length) : machine.replayPrefix input answers (index + 1) = machine.replyStep (machine.replayPrefix input answers index) answers[index]

Advancing a transcript prefix executes its next bit, whenever that bit is present.

theorem Turing.MultiTapePTM.spaceBound_replyStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) {inputSize steps : ℕ} {cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation} (h : MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps 1 cfg) (bit : Bool) : MultiTapeMachine.FiniteConfig.SpaceBound inputSize (steps + 1) 1 (machine.replyStep cfg bit)

Every replayed instruction preserves the native one-bit-reply storage bound.

theorem Turing.MultiTapePTM.spaceBound_replayFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) {inputSize steps : ℕ} {cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation} (h : MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps 1 cfg) (answers : List Bool) : MultiTapeMachine.FiniteConfig.SpaceBound inputSize (steps + answers.length) 1 (machine.replayFrom cfg answers)

A transcript of length r executes r instructions with replies of length one.

theorem Turing.MultiTapePTM.spaceBound_replayConfig {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) : MultiTapeMachine.FiniteConfig.SpaceBound input.length answers.length 1 (machine.replayConfig input answers)

Replay from the initial configuration has linear storage in the input and transcript.

theorem Turing.MultiTapePTM.length_pendingRequest_replayConfig_le {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) : (machine.pendingRequest (machine.replayConfig input answers)).length ≤ answers.length

A pending request contains at most one symbol per elapsed native instruction.

theorem Turing.MultiTapePTM.length_pendingRequest_replayPrefix_le {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (input answers : List Bool) (index : ℕ) : (machine.pendingRequest (machine.replayPrefix input answers index)).length ≤ min index answers.length

A prefix query has at most min index answers.length symbols.

theorem Turing.MultiTapePTM.replyStep_pt {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime (fun (p : MultiTapeMachine.FiniteConfig k Bool Control Operation × Bool) => machine.replyStep p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encFiniteConfig MultiTapeTM.encBool) MultiTapeTM.encFiniteConfig

The next replay instruction is polynomial-time, uniformly in its reply bit.

theorem Turing.MultiTapePTM.replayConfig_pt {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => machine.replayConfig p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encFiniteConfig

Deterministic oracle replay is polynomial-time in the encoded input and transcript.

theorem Turing.MultiTapePTM.computableInPolyTime_replayPrefix {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : MultiTapeTM.ComputableInPolyTime (fun (p : (List Bool × List Bool) × ℕ) => machine.replayPrefix p.1.1 p.1.2 p.2) (MultiTapeTM.encPair (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encUnary) MultiTapeTM.encFiniteConfig

Prefix replay is jointly polynomial-time in input, transcript and unary instruction index.

theorem Turing.MultiTapePTM.computableInPolyTime_replayOutput {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Finite Operation] : MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => machine.replayOutput p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encBits

The replayed output is polynomial-time.

theorem Turing.MultiTapePTM.replayPrefix_pendingRequest_pt {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Finite Operation] : MultiTapeTM.ComputableInPolyTime (fun (p : (List Bool × List Bool) × ℕ) => machine.pendingRequest (machine.replayPrefix p.1.1 p.1.2 p.2)) (MultiTapeTM.encPair (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encUnary) MultiTapeTM.encBits

The next query in a guessed-reply execution is uniformly polynomial-time.

theorem Turing.MultiTapePTM.replayPrefix_isQuery_pt {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) [Finite Control] [Finite Operation] : MultiTapeTM.ComputableInPolyTime (fun (p : (List Bool × List Bool) × ℕ) => (machine.pendingQuery (machine.replayPrefix p.1.1 p.1.2 p.2)).isSome) (MultiTapeTM.encPair (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encUnary) MultiTapeTM.encBool

Whether the next guessed-reply instruction is a query is uniformly polynomial-time.

def Turing.MultiTapePTM.oracleRepliesFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) : MultiTapeMachine.FiniteConfig k Bool Control Operation → ℕ → List Bool

The instruction-indexed transcript of an oracle execution. Local and halted instructions receive the canonical padding bit false.

def Turing.MultiTapePTM.oracleReplies {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : List Bool

The canonical transcript of a clocked execution from the initial configuration.

theorem Turing.MultiTapePTM.length_oracleRepliesFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (fuel : ℕ) : (machine.oracleRepliesFrom g cfg fuel).length = fuel

A canonical transcript has exactly one bit per clocked instruction.

theorem Turing.MultiTapePTM.length_oracleReplies {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : (machine.oracleReplies g fuel input).length = fuel

The initial canonical transcript has exactly the clock length.

theorem Turing.MultiTapePTM.take_oracleRepliesFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (fuel index : ℕ) : List.take index (machine.oracleRepliesFrom g cfg fuel) = machine.oracleRepliesFrom g cfg (min index fuel)

Canonical transcripts are consistent under truncation of their clock.

theorem Turing.MultiTapePTM.replayFrom_oracleRepliesFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (fuel : ℕ) : machine.replayFrom cfg (machine.oracleRepliesFrom g cfg fuel) = (machine.answerStep fun (q : Operation × List Bool) => [g q.2])^[fuel] cfg

Canonical replay recovers the entire finite configuration, not only its output.

theorem Turing.MultiTapePTM.replayConfig_oracleReplies {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : machine.replayConfig input (machine.oracleReplies g fuel input) = (machine.answerStep fun (q : Operation × List Bool) => [g q.2])^[fuel] (MultiTapeMachine.FiniteConfig.init machine.initial input)

The canonical transcript replays the coin-fixed oracle run from its initial configuration.

theorem Turing.MultiTapePTM.replayPrefix_oracleReplies {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) (index : ℕ) : machine.replayPrefix input (machine.oracleReplies g fuel input) index = (machine.answerStep fun (q : Operation × List Bool) => [g q.2])^[min index fuel] (MultiTapeMachine.FiniteConfig.init machine.initial input)

A canonical prefix recovers the configuration after the corresponding elapsed instructions.

theorem Turing.MultiTapePTM.getD_oracleRepliesFrom {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (cfg : MultiTapeMachine.FiniteConfig k Bool Control Operation) (fuel index : ℕ) (hindex : index < fuel) : (machine.oracleRepliesFrom g cfg fuel).getD index false = have current := (machine.answerStep fun (q : Operation × List Bool) => [g q.2])^[index] cfg; if (machine.pendingQuery current).isSome = true then g (machine.pendingRequest current) else false

The bit of a canonical transcript at a live clock index is the pending oracle answer, with false at local or halted instructions.

theorem Turing.MultiTapePTM.getD_oracleReplies {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) (index : ℕ) (hindex : index < fuel) : (machine.oracleReplies g fuel input).getD index false = have current := machine.replayPrefix input (machine.oracleReplies g fuel input) index; if (machine.pendingQuery current).isSome = true then g (machine.pendingRequest current) else false

Canonical transcript bits agree with the queries seen by replay of their own prefix.

theorem Turing.MultiTapePTM.replayOutput_oracleReplies {k : ℕ} {Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool Control Operation) (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : machine.replayOutput input (machine.oracleReplies g fuel input) = 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)) fuel input)

Replayed canonical outputs agree exactly with interpretation of the clocked oracle program.