Polynomial time relative to an oracle language

An oracle language A : Set (List Bool) answers a word request w with the one-bit word [decide (w ∈ A)] (Cslib.Complexity.languageOracle). A deterministic oracle algorithm is a program WordQueryComp Unit β: a PFunctor.FreeM program whose calls are word requests and whose later requests may depend on earlier replies. Run against A, it returns OracleComp.interpret (m := Id) (languageOracle A) program.

f is computable in polynomial time relative to A (Cslib.Complexity.ComputableInPolyTimeWithOracle) when one deterministic program computes f against A and the program is strict oracle PPT (Cslib.Probability.IsOraclePPTOn) with one channel: one finite-control machine, under one polynomial clock in the encoded input length, reproduces the program's complete interaction with every stateful oracle. This is the oracle Turing machine of Arora and Barak, Section 3.4 on the common machine (Turing.MultiTapeMachine with oracle channels): each request symbol is written onto the query buffer at the cost of one instruction, submitting a request costs one instruction, and the reply bit is the first cell of the answer tape, read by the answer head with no further instruction. The oracle's own computation is not charged. The certificate quantifies over every handler, not only language oracles, so the program, not the oracle, determines which requests are made; the machine's clock also bounds their number and length (Cslib.Probability.IsOraclePPTOn.query_bounds).

The classes relativize P and NP by this one substitution: PWithOracle A enc and NPWithOracle A enc are Cslib.Complexity.P and Cslib.Complexity.NP with ComputableInPolyTime replaced by ComputableInPolyTimeWithOracle A. Hence NPWithOracle uses verifiers with an oracle and certificates of exactly polynomial length. When the oracle is a promise problem or an encoded class of oracles (PWithSharpPOracle, PWithPPOracle, RPWithPromiseOracle), Cslib.Complexity.PolyTimeOracleProgram asks for one deterministic polynomial-time oracle program whose function against every admissible oracle language satisfies a given specification.

For a deterministic program and an answer function, OracleComp.queriesWith (CslibFrontier/Languages/Probabilistic/QueriesWith.lean) lists the requests made. Only their answers matter (OracleComp.interpret_id_congr), which is the locality on which oracle constructions rest.

Main definitions

• Cslib.Complexity.WordQueryComp: deterministic programs making word requests.
• Cslib.Complexity.languageOracle: the replies of an oracle language.
• Cslib.Complexity.ComputableInPolyTimeWithOracle: polynomial time relative to an oracle.
• Cslib.Complexity.PolyTimeOracleProgram: one polynomial-time oracle program satisfying a specification across every admissible oracle language.
• Cslib.Complexity.PWithOracle, Cslib.Complexity.NPWithOracle: P and NP relative to an oracle language.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithOracle: polynomial time is polynomial time relative to every oracle.
• Cslib.Complexity.PolyTimeOracleProgram.of_polyTime, Cslib.Complexity.PolyTimeOracleProgram.exists_computableInPolyTimeWithOracle, Cslib.Complexity.PolyTimeOracleProgram.of_computableInPolyTimeWithOracle.
• Cslib.Complexity.P_subset_PWithOracle, Cslib.Complexity.NP_subset_NPWithOracle.

References

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

@[reducible, inline]

abbrev Cslib.Complexity.WordQueryComp (Operation β : Type) : Type

Deterministic programs whose calls are word requests on the channels Operation, answered by words.

noncomputable def Cslib.Complexity.languageOracle {Operation : Type} (A : Set (List Bool)) (q : Operation × List Bool) : List Bool

The oracle language A answers a request (op, w) with the one-bit word [decide (w ∈ A)], on every channel op.

theorem Cslib.Complexity.languageOracle_apply {Operation : Type} (A : Set (List Bool)) (q : Operation × List Bool) : languageOracle A q = [decide (q.2 ∈ A)]

theorem Cslib.Complexity.interpret_languageOracle_congr {Operation α : Type} {A B : Set (List Bool)} (program : WordQueryComp Operation α) (h : ∀ q ∈ OracleComp.queriesWith (languageOracle A) program, q.2 ∈ B ↔ q.2 ∈ A) : OracleComp.interpret (languageOracle B) program = OracleComp.interpret (languageOracle A) program ∧ OracleComp.queriesWith (languageOracle B) program = OracleComp.queriesWith (languageOracle A) program

Language oracles that agree on every word requested by program under one of them give the same run.

def Cslib.Complexity.ComputableInPolyTimeWithOracle {α β : Type} (A : Set (List Bool)) (f : α → β) (input : α ↪ List Bool) (output : β ↪ List Bool) : Prop

f is computable in polynomial time relative to the oracle language A: a deterministic word-query program computes f against A, and one finite machine under one polynomial clock realizes the program against every stateful oracle, charging request construction and reply access. This is the oracle Turing machine of Arora and Barak, Section 3.4.

theorem Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithOracle {α β : Type} {f : α → β} {input : α ↪ List Bool} {output : β ↪ List Bool} (h : ComputableInPolyTime f input output) (A : Set (List Bool)) : Cslib.Complexity.ComputableInPolyTimeWithOracle A f input output

A polynomial-time computation makes no request, so it is polynomial time relative to every oracle.

def Cslib.Complexity.PolyTimeOracleProgram {α β : Type} (input : α ↪ List Bool) (output : β ↪ List Bool) (Admissible : Set (List Bool) → Prop) (Spec : (α → β) → Prop) : Prop

One deterministic polynomial-time oracle program whose function against every oracle language satisfying Admissible satisfies Spec. The program is fixed before the oracle language, so answers on words unconstrained by Admissible may be arbitrary.

theorem Cslib.Complexity.computableInPolyTimeWithOracle_iff_polyTimeOracleProgram {α β : Type} {A : Set (List Bool)} {f : α → β} {input : α ↪ List Bool} {output : β ↪ List Bool} : ComputableInPolyTimeWithOracle A f input output ↔ PolyTimeOracleProgram input output (fun (x : Set (List Bool)) => x = A) fun (x : α → β) => x = f

ComputableInPolyTimeWithOracle is PolyTimeOracleProgram for a single oracle language and a single target function.

theorem Cslib.Complexity.PolyTimeOracleProgram.of_polyTime {α β : Type} {g : α → β} {input : α ↪ List Bool} {output : β ↪ List Bool} {Admissible : Set (List Bool) → Prop} {Spec : (α → β) → Prop} (hg : Turing.MultiTapeTM.ComputableInPolyTime g input output) (hSpec : ∀ (A : Set (List Bool)), Admissible A → Spec g) : PolyTimeOracleProgram input output Admissible Spec

A polynomial-time function makes no oracle request, so it satisfies Spec against every admissible oracle language whenever g does.

theorem Cslib.Complexity.PolyTimeOracleProgram.exists_computableInPolyTimeWithOracle {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {Admissible : Set (List Bool) → Prop} {Spec : (α → β) → Prop} (h : PolyTimeOracleProgram input output Admissible Spec) {A : Set (List Bool)} (hA : Admissible A) : ∃ (g : α → β), ComputableInPolyTimeWithOracle A g input output ∧ Spec g

Evaluating a PolyTimeOracleProgram against any admissible oracle language A yields a function computable in polynomial time relative to A satisfying Spec.

theorem Cslib.Complexity.PolyTimeOracleProgram.of_computableInPolyTimeWithOracle {α β : Type} {A : Set (List Bool)} {g : α → β} {input : α ↪ List Bool} {output : β ↪ List Bool} {Admissible : Set (List Bool) → Prop} {Spec : (α → β) → Prop} (hg : ComputableInPolyTimeWithOracle A g input output) (hSpec : ∀ (A' : Set (List Bool)), Admissible A' → A' = A ∧ Spec g) : PolyTimeOracleProgram input output Admissible Spec

A function computable in polynomial time relative to a single oracle language A witnesses PolyTimeOracleProgram whenever A is the unique admissible oracle language.

def Cslib.Complexity.PWithOracle {α : Type} (A : Set (List Bool)) (enc : α ↪ List Bool) : Set (Set α)

The problems decidable in polynomial time relative to the oracle language A, with respect to the encoding enc of instances: Cslib.Complexity.P with an oracle Arora and Barak, Section 3.4.

theorem Cslib.Complexity.mem_PWithOracle {α : Type} {A : Set (List Bool)} {enc : α ↪ List Bool} {L : Set α} : L ∈ PWithOracle A enc ↔ ∃ (f : α → Bool), ComputableInPolyTimeWithOracle A f enc Turing.MultiTapeTM.encBool ∧ ∀ (a : α), a ∈ L ↔ f a = true

def Cslib.Complexity.NPWithOracle {α : Type} (A : Set (List Bool)) (enc : α ↪ List Bool) : Set (Set α)

The problems with verifiers computable in polynomial time relative to the oracle language A and polynomially long certificates: Cslib.Complexity.NP with an oracle Arora and Barak, Section 3.4.

theorem Cslib.Complexity.mem_NPWithOracle {α : Type} {A : Set (List Bool)} {enc : α ↪ List Bool} {L : Set α} : L ∈ NPWithOracle A enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), ComputableInPolyTimeWithOracle A V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ IsVerifier enc p V L

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

Every problem in P is in P relative to every oracle.

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

Every problem in NP is in NP relative to every oracle.