Oracle circuits and inlining

An oracle circuit for a language A over Bool is a De Morgan circuit with, in addition, an oracle gate of every arity q, which answers whether the word formed by its q arguments is in A (oracleSignature, oracleInterpretation A). The arguments of an oracle gate may be computed from the answers of other oracle gates, so the queries are adaptive. Such circuits are the relativized circuits of Wilson.

Inlining replaces every oracle gate of arity q by a De Morgan circuit D q computing the slice of A at q (inlineOracle), which is the simulation of the oracle basis by the De Morgan basis (Circuit.simulate): the result computes what the oracle circuit computes (eval_inlineOracle), each oracle gate costing the size and the depth of its replacement (size_inlineOracle, depth_inlineOracle_le).

PPolyOracle A is P/poly relative to A: the languages with oracle circuits of polynomial size whose gates have polynomially many arguments. Every language in P/poly is in it (PPoly.subset_PPolyOracle), and when A is in P/poly, inlining its circuits, of polynomial size at the polynomially bounded arities of the queries, shows the converse (PPolyOracle_subset_PPoly): P/poly with oracle gates for a language in P/poly is P/poly (PPolyOracle_eq_PPoly).

Main definitions

• Cslib.Circuits.Boolean.OracleOp, Cslib.Circuits.Boolean.oracleSignature, Cslib.Circuits.Boolean.oracleInterpretation: the De Morgan basis with oracle gates.
• Cslib.Circuits.Boolean.toOracle: the De Morgan basis inside it.
• Cslib.Circuits.Boolean.inlineOracle: the circuit with its oracle gates replaced.
• Cslib.Circuits.Boolean.PPolyOracle: P/poly relative to an oracle.

Main results

• Cslib.Circuits.Boolean.eval_inlineOracle, size_inlineOracle, size_inlineOracle_le, depth_inlineOracle_le: the inlined circuit computes what the oracle circuit computes, with bounds on its size and depth.
• Cslib.Circuits.Boolean.PPolyOracle_subset_PPoly, Cslib.Circuits.Boolean.PPolyOracle_eq_PPoly: P/poly relative to a language in P/poly is P/poly.

References

• C. B. Wilson, Relativized circuit complexity

inductive Cslib.Circuits.Boolean.OracleOp : Type

The operations of the De Morgan basis, and an oracle gate of every arity.

• base (op : Op) : OracleOp

  An operation of the De Morgan basis.

• query (q : ℕ) : OracleOp

  The oracle gate of q arguments.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.OracleOp.arity : OracleOp → ℕ

The arity of an operation of the oracle basis.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.oracleSignature : Signature

The De Morgan basis with an oracle gate of every arity. It is reducible, so that case analysis on its operations sees their arities.

noncomputable def Cslib.Circuits.Boolean.oracleInterpretation (A : Language Bool) : Interpretation oracleSignature Bool

The meaning of the oracle basis for the oracle A: the oracle gate of q arguments answers whether the word they form is in A.

@[simp]

theorem Cslib.Circuits.Boolean.oracleInterpretation_base (A : Language Bool) (op : Op) (x : Fin (signature.Arity op) → Bool) : oracleInterpretation A (OracleOp.base op) x = interpretation op x

@[simp]

theorem Cslib.Circuits.Boolean.oracleInterpretation_query (A : Language Bool) (q : ℕ) (x : Fin q → Bool) : oracleInterpretation A (OracleOp.query q) x = A.slice q x

def Cslib.Circuits.Boolean.toOracle : signature.Hom oracleSignature

The De Morgan basis inside the oracle basis.

instance Cslib.Circuits.Boolean.preserves_toOracle (A : Language Bool) : toOracle.Preserves interpretation (oracleInterpretation A)

Inlining

def Cslib.Circuits.Boolean.oracleImpl (D : (q : ℕ) → Circuit signature q 1) (op : oracleSignature.Op) : Circuit signature (oracleSignature.Arity op) 1

The De Morgan circuit replacing each operation of the oracle basis: a gate for an operation of the De Morgan basis, and D q for the oracle gate of q arguments.

def Cslib.Circuits.Boolean.oracleSize (D : (q : ℕ) → Circuit signature q 1) : OracleOp → ℕ

The cost of an operation of the oracle basis in the size of the inlined circuit: one gate for an operation of the De Morgan basis, and the size of D q for the oracle gate of q arguments.

def Cslib.Circuits.Boolean.oracleDepth (D : (q : ℕ) → Circuit signature q 1) : OracleOp → ℕ

The cost of an operation of the oracle basis in the depth of the inlined circuit: one level for an operation of the De Morgan basis, and the depth of D q for the oracle gate of q arguments.

def Cslib.Circuits.Boolean.inlineOracle {n m : ℕ} (C : Circuit oracleSignature n m) (D : (q : ℕ) → Circuit signature q 1) : Circuit signature n m

The oracle circuit C with every oracle gate of q arguments replaced by the De Morgan circuit D q.

theorem Cslib.Circuits.Boolean.eval_inlineOracle {n m : ℕ} {A : Language Bool} (C : Circuit oracleSignature n m) {D : (q : ℕ) → Circuit signature q 1} (hD : ∀ (q : ℕ), (D q).Computes interpretation (single (A.slice q))) : (inlineOracle C D).eval interpretation = C.eval (oracleInterpretation A)

Inlining an oracle. If every D q computes the slice of A at q, the inlined circuit computes what the oracle circuit computes with the oracle A.

theorem Cslib.Circuits.Boolean.size_inlineOracle {n m : ℕ} (C : Circuit oracleSignature n m) (D : (q : ℕ) → Circuit signature q 1) : (inlineOracle C D).size = C.program.cost (oracleSize D)

The inlined circuit has one gate for each gate of the De Morgan basis and the gates of D q for each oracle gate of q arguments.

theorem Cslib.Circuits.Boolean.depth_inlineOracle_le {n m : ℕ} (C : Circuit oracleSignature n m) (D : (q : ℕ) → Circuit signature q 1) : (inlineOracle C D).depth ≤ Circuit.depthWith (oracleDepth D) C

The inlined circuit is at most as deep as the oracle circuit when an oracle gate of q arguments costs the depth of D q.

theorem Cslib.Circuits.Boolean.size_inlineOracle_le {n m : ℕ} (C : Circuit oracleSignature n m) (D : (q : ℕ) → Circuit signature q 1) {r s : ℕ} (hC : C.FanInAtMost r) (hD : ∀ q ≤ r, (D q).size ≤ s) : (inlineOracle C D).size ≤ C.size * max 1 s

If every gate of an oracle circuit has at most r arguments, and every D q with q ≤ r has at most s gates, the inlined circuit has at most size C * max 1 s gates.

P/poly relative to an oracle

def Cslib.Circuits.Boolean.PPolyOracle (A : Language Bool) : Set (Language Bool)

P/poly relative to the oracle A: the languages with oracle circuits, one for each input length n, with at most s n gates, each of at most s n arguments, for a polynomially bounded s. The size counts gates; bounding arity too bounds incoming wire occurrences by s n ^ 2.

theorem Cslib.Circuits.Boolean.fanInAtMost_mapOp_toOracle {n g : ℕ} (p : Program signature n g) {r : ℕ} (hr : 2 ≤ r) : (Program.mapOp toOracle p).FanInAtMost r

A De Morgan program in the oracle basis has fan-in at most two.

theorem Cslib.Circuits.Boolean.PPoly.subset_PPolyOracle (A : Language Bool) : PPoly ⊆ PPolyOracle A

A language in P/poly is in P/poly relative to any oracle.

theorem Cslib.Circuits.Boolean.PPolyOracle_subset_PPoly {A : Language Bool} (hA : A ∈ PPoly) : PPolyOracle A ⊆ PPoly

Inlining an oracle in P/poly. If A is in P/poly, so is every language in P/poly relative to A: its oracle gates have polynomially many arguments, at which A has circuits of polynomial size.

theorem Cslib.Circuits.Boolean.PPolyOracle_eq_PPoly {A : Language Bool} (hA : A ∈ PPoly) : PPolyOracle A = PPoly

P/poly relative to a language in P/poly is P/poly.