Uniform circuit compilation for polynomial-time function families

The Boolean tableau compiler is applied to a fixed output-bit selector. Hardwiring its instance and selector inputs, and combining its outputs, gives circuit codes for fixed-length function families. Construction time is certified separately from circuit semantics.

The selector has a fixed length equal to the output width. All output-bit circuits therefore have equal gate counts and can be bundled by fixed offsets. The construction repeats the computation for each output; it establishes polynomial construction time without an optimized gate count. Arbitrary instance encodings need no decoder, and correctness concerns their image.

Main results

• Cslib.Complexity.CircuitValue.exists_uniformCircuitFamily: one polynomial-time circuit-code constructor for an entire polynomial-time family, with separately prescribed unary widths.

References

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

theorem Cslib.Complexity.CircuitValue.exists_uniformCircuitFamily {α : Type} {enc : α ↪ List Bool} {n m : α → ℕ} {F : α × List Bool → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n enc Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m enc Turing.MultiTapeTM.encUnary) (hF : Turing.MultiTapeTM.ComputableTidilyInPolyTime F (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : ∃ (circuits : (a : α) → Circuits.Circuit Circuits.Boolean.signature (n a) (m a)), Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (circuits a).code) enc Circuits.Boolean.encCode ∧ ∀ (a : α) (x : Fin (n a) → Bool) (j : Fin (m a)), (circuits a).eval Circuits.Boolean.interpretation x j = (F (a, List.ofFn x)).getD (↑j) false

Compile a polynomial-time function family into circuits with prescribed input and output widths. One polynomial-time constructor outputs the code for every instance. Output j is the jth bit of the function value, defaulting to false when that value is shorter than m a.