Relativization and oracle separations
TheoremBaker-Gill-Solovay: oracles separate and collapse P vs NP#●ready to prove
For an oracle \(O\), a function from bitstrings to booleans, write \(\mathsf{P}^O\) and \(\mathsf{NP}^O\) for the classes of decision problems decidable in polynomial time, respectively in nondeterministic polynomial time, by machines that may query \(O\). There is an oracle \(O\) such that \(\mathsf{P}^O \ne \mathsf{NP}^O\), and there is an oracle \(O\) such that \(\mathsf{P}^O = \mathsf{NP}^O\).
public theorem_wanted baker_gill_solovay :
(∃ O : List Bool → Bool, PWithOracle O ≠ NPWithOracle O) ∧
(∃ O : List Bool → Bool, PWithOracle O = NPWithOracle O)def PWithOracle (O : List Bool → Bool) : DecisionComplexityClass :=
{L | ∃ p q : Polynomial ℕ,
∃ nextQ : List Bool × List (List Bool × Bool) → List Bool,
∃ final : List Bool × List (List Bool × Bool) → Bool,
IsPolyTime nextQ ∧ IsPolyTime final ∧
∀ x, L x ↔
evalOracle (q.eval x.length) nextQ final O x (p.eval x.length) [] = true}CSLibExt/Computability/Complexity/Classes.lean:259
def NPWithOracle (O : List Bool → Bool) : DecisionComplexityClass :=
{L | ∃ p q : Polynomial ℕ,
∃ nextQ : List Bool × List (List Bool × Bool) → List Bool,
∃ final : List Bool × List (List Bool × Bool) → Bool,
IsPolyTime nextQ ∧ IsPolyTime final ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧
evalOracle (q.eval x.length) nextQ final O (MetaMathlibExt.BitstringEncoding.bitEncode (x, w))
(p.eval x.length) [] = true}CSLibExt/Computability/Complexity/Classes.lean:269
Sources
- T. Baker, J. Gill, and R. Solovay, "Relativizations of the P =? NP question", SIAM Journal on Computing 4 (1975), 431-442.
Uses 3
TheoremAn oracle separates NP from coNP#●ready to prove
There is an oracle \(O\), a function from bitstrings to booleans, such that \(\mathrm{NP}^O\) differs from the class \(\mathrm{coNP}^O\) of decision problems \(L\) whose complement, the decision problem that accepts exactly the bitstrings that \(L\) rejects, belongs to \(\mathrm{NP}^O\).
public theorem_wanted oracle_np_co_np_separation :
∃ O : List Bool → Bool, NPWithOracle O ≠ {L | Lᶜ ∈ NPWithOracle O}def NPWithOracle (O : List Bool → Bool) : DecisionComplexityClass :=
{L | ∃ p q : Polynomial ℕ,
∃ nextQ : List Bool × List (List Bool × Bool) → List Bool,
∃ final : List Bool × List (List Bool × Bool) → Bool,
IsPolyTime nextQ ∧ IsPolyTime final ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧
evalOracle (q.eval x.length) nextQ final O (MetaMathlibExt.BitstringEncoding.bitEncode (x, w))
(p.eval x.length) [] = true}CSLibExt/Computability/Complexity/Classes.lean:269
Sources
- T. Baker, J. Gill, and R. Solovay, "Relativizations of the P =? NP question", SIAM Journal on Computing 4 (1975), 431-442 (oracles separating NP from coNP); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 3 (relativization).
Uses 3
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.