Closure properties of the oracle classes

Polynomial time relative to an oracle composes with polynomial-time pre- and postprocessing (Cslib.Complexity.ComputableInPolyTimeWithOracle.preprocess, Cslib.Complexity.ComputableInPolyTimeWithOracle.map), through the compositional rules of strict oracle PPT. One request decides the oracle language itself (Cslib.Complexity.computableInPolyTimeWithOracle_mem): the request is copied onto the query buffer, and only the first bit of the reply is read (Cslib.Complexity.queryBit).

Hence P relative to A contains A and lies inside NP relative to A, and both classes are closed under polynomial-time many-one reductions of the problem (Cslib.Complexity.PolyTimeReducible.mem_PWithOracle, Cslib.Complexity.PolyTimeReducible.mem_NPWithOracle). For NP the certificates are padded to a polynomial of the instance length, and the verifier reads only the prefix of the length the reduced instance requires.

Main results

• Cslib.Complexity.ComputableInPolyTimeWithOracle.preprocess, Cslib.Complexity.ComputableInPolyTimeWithOracle.map, Cslib.Complexity.ComputableInPolyTimeWithOracle.map_with: pre- and postprocessing.
• Cslib.Complexity.ComputableInPolyTimeWithOracle.prod: retain two oracle results.
• Cslib.Complexity.PolyTimeOracleProgram.of_query: one polynomial-time request decides membership in every admissible oracle language.
• Cslib.Complexity.computableInPolyTimeWithOracle_mem, Cslib.Complexity.mem_PWithOracle_self: one request decides the oracle language.
• Cslib.Complexity.PWithOracle_subset_NPWithOracle.
• Cslib.Complexity.PolyTimeReducible.mem_PWithOracle, Cslib.Complexity.PolyTimeReducible.mem_NPWithOracle: closure under polynomial-time many-one reductions.

References

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

theorem Cslib.Complexity.ComputableInPolyTimeWithOracle.preprocess {α β γ : Type} {A : Set (List Bool)} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableInPolyTimeWithOracle A f middle output) (hg : Turing.MultiTapeTM.ComputableInPolyTime g input middle) : ComputableInPolyTimeWithOracle A (fun (a : α) => f (g a)) input output

Polynomial-time preprocessing of the argument.

theorem Cslib.Complexity.ComputableInPolyTimeWithOracle.map_with {α β γ : Type} {A : Set (List Bool)} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {f : α → β} {g : α → β → γ} (hf : ComputableInPolyTimeWithOracle A f input middle) (hg : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : α × β) => g pair.1 pair.2) (Turing.MultiTapeTM.encPair input middle) output) : ComputableInPolyTimeWithOracle A (fun (a : α) => g a (f a)) input output

Polynomial-time postprocessing of the result, which may also use the argument.

theorem Cslib.Complexity.ComputableInPolyTimeWithOracle.map {α β γ : Type} {A : Set (List Bool)} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {f : α → β} {g : β → γ} (hf : ComputableInPolyTimeWithOracle A f input middle) (hg : Turing.MultiTapeTM.ComputableInPolyTime g middle output) : ComputableInPolyTimeWithOracle A (fun (a : α) => g (f a)) input output

Polynomial-time postprocessing of the result.

theorem Cslib.Complexity.ComputableInPolyTimeWithOracle.prod {α β γ : Type} {A : Set (List Bool)} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {f : α → β} {g : α → γ} (hf : ComputableInPolyTimeWithOracle A f input middle) (hg : ComputableInPolyTimeWithOracle A g input output) : ComputableInPolyTimeWithOracle A (fun (a : α) => (f a, g a)) input (Turing.MultiTapeTM.encPair middle output)

Compute two results sequentially against the same oracle, retaining both outputs.

theorem Cslib.Complexity.PolyTimeOracleProgram.of_query {α : Type} {req : α → List Bool} {input : α ↪ List Bool} {Admissible : Set (List Bool) → Prop} {Spec : (α → Bool) → Prop} (hreq : Turing.MultiTapeTM.ComputableInPolyTime req input Turing.MultiTapeTM.encBits) (hSpec : ∀ (A : Set (List Bool)), Admissible A → Spec fun (a : α) => decide (req a ∈ A)) : PolyTimeOracleProgram input Turing.MultiTapeTM.encBool Admissible Spec

One polynomial-time request req a to the oracle language decides whether req a ∈ A against every admissible oracle language A.

theorem Cslib.Complexity.computableInPolyTimeWithOracle_mem (A : Set (List Bool)) : ComputableInPolyTimeWithOracle A (fun (w : List Bool) => decide (w ∈ A)) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool

One request decides the oracle language. The word is copied onto the query buffer and the first bit of the reply is read.

theorem Cslib.Complexity.mem_PWithOracle_self (A : Set (List Bool)) : A ∈ PWithOracle A Turing.MultiTapeTM.encBits

P relative to A contains A.

theorem Cslib.Complexity.PWithOracle_subset_NPWithOracle {α : Type} (A : Set (List Bool)) (enc : α ↪ List Bool) : PWithOracle A enc ⊆ NPWithOracle A enc

P relative to A lies inside NP relative to A: a decider ignores the empty certificate.

theorem Cslib.Complexity.PolyTimeReducible.mem_PWithOracle {α β : Type} {A : Set (List Bool)} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {L : Set α} {L' : Set β} (h : PolyTimeReducible encA encB L L') (hL' : L' ∈ PWithOracle A encB) : L ∈ PWithOracle A encA

P relative to an oracle is closed under polynomial-time many-one reductions.

theorem Cslib.Complexity.PolyTimeReducible.mem_NPWithOracle {α β : Type} {A : Set (List Bool)} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {L : Set α} {L' : Set β} (h : PolyTimeReducible encA encB L L') (hL' : L' ∈ NPWithOracle A encB) : L ∈ NPWithOracle A encA

NP relative to an oracle is closed under polynomial-time many-one reductions. The certificates are padded to a polynomial of the instance length; the verifier reads the prefix of the length required by the reduced instance.