Inlining polynomial circuit oracles -- definitions

For each round of an adaptive oracle program, a polynomial circuit oracle selects the family member at that round's query width. The generic adaptive compiler then replaces all oracle calls by those selected circuits.

def Complexity.PolynomialCircuitOracle.implementation {language : Language} (circuitOracle : PolynomialCircuitOracle language) {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) : program.OracleCircuitImplementation

Select the circuit-family member matching each query width of an adaptive oracle program.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.AdaptiveOracleProgram.inlineCircuitOracle {language : Language} {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (circuitOracle : PolynomialCircuitOracle language) : (internalGates : ℕ) × Circuit Basis.andOr2 inputWidth outputWidth internalGates

Replace every oracle call in program by the matching member of a polynomial-size circuit oracle.

Equations

• program.inlineCircuitOracle circuitOracle = program.inline (circuitOracle.implementation program)