Monotonicity of the oracle classes under reductions

If the oracle language A reduces to B by a polynomial-time map g, a computation relative to A becomes one relative to B: every request w is replaced by the request g w, of which one reply bit is kept (Cslib.Complexity.ComputableInPolyTimeWithOracle.of_polyTimeReducible). The certificate is open oracle substitution (Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess_open): the handler answering requests to A is itself an oracle program querying B, charged for computing g w and for reading one bit of the reply. Hence P^A ⊆ P^B and NP^A ⊆ NP^B (Cslib.Complexity.PolyTimeReducible.PWithOracle_subset, Cslib.Complexity.PolyTimeReducible.NPWithOracle_subset), and polynomial-time equivalent oracles give the same classes.

Main results

• Cslib.Complexity.ComputableInPolyTimeWithOracle.of_polyTimeReducible: oracle monotonicity.
• Cslib.Complexity.PolyTimeReducible.PWithOracle_subset, Cslib.Complexity.PolyTimeReducible.NPWithOracle_subset: P^A ⊆ P^B and NP^A ⊆ NP^B.

References

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

theorem Cslib.Complexity.ComputableInPolyTimeWithOracle.of_polyTimeReducible {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {A B : Set (List Bool)} {f : α → β} (hAB : PolyTimeReducible Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits A B) (hf : ComputableInPolyTimeWithOracle A f input output) : ComputableInPolyTimeWithOracle B f input output

Oracle monotonicity. If A reduces to B in polynomial time, then polynomial time relative to A is polynomial time relative to B: every request w is replaced by the request g w, keeping one bit of the reply.

theorem Cslib.Complexity.PolyTimeReducible.PWithOracle_subset {α : Type} {A B : Set (List Bool)} (hAB : PolyTimeReducible Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits A B) (enc : α ↪ List Bool) : PWithOracle A enc ⊆ PWithOracle B enc

P relative to an oracle is monotone under polynomial-time reductions of the oracle.

theorem Cslib.Complexity.PolyTimeReducible.NPWithOracle_subset {α : Type} {A B : Set (List Bool)} (hAB : PolyTimeReducible Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits A B) (enc : α ↪ List Bool) : NPWithOracle A enc ⊆ NPWithOracle B enc

NP relative to an oracle is monotone under polynomial-time reductions of the oracle.