Oracle programs for relative approximate counting #
Inlining exact oracle circuits preserves the hashing estimator semantics.
Consequently, a program using any language in P/poly yields an ordinary
circuit that becomes accurate on all inputs after one random seed is fixed.
theorem
Complexity.ApproximateCounting.Relative.inlineCircuitImplements
{inputWidth outputWidth domainWidth rounds precision failureBits : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{program : AdaptiveOracleProgram (seedWidth domainWidth precision failureBits + inputWidth) outputWidth rounds}
{oracle : BooleanOracle}
(implementation : program.OracleCircuitImplementation)
(himplementation : implementation.Implements oracle)
(hprogram : OracleProgramImplements precision failureBits setOfInput program oracle)
:
CircuitImplements precision failureBits setOfInput (program.inline implementation).snd
Inlining an exact implementation of the Boolean oracle preserves the program's relative-estimator semantics.
theorem
Complexity.ApproximateCounting.Relative.exists_hardwired_accurate_of_mem_PPoly
{language : Language}
{inputWidth outputWidth domainWidth rounds precision : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
(program : AdaptiveOracleProgram (seedWidth domainWidth precision (inputWidth + 1) + inputWidth) outputWidth rounds)
(hprecision : 0 < precision)
(hlanguage : language ∈ PPoly)
(hprogram :
∀ (oracle : BooleanOracle),
oracle.Decides language → OracleProgramImplements precision (inputWidth + 1) setOfInput program oracle)
:
∃ (circuitOracle : PolynomialCircuitOracle language) (fixed :
Circuit Basis.andOr2 inputWidth outputWidth (program.inlineCircuitOracle circuitOracle).fst),
(∀ (input : BitString inputWidth), OutputIsAccurate precision setOfInput input (fixed.eval input)) ∧ fixed.size = (program.inlineCircuitOracle circuitOracle).snd.size
If the program's oracle language is in P/poly, oracle inlining followed
by seed fixing produces one ordinary circuit accurate on every input.