Fixed-round adaptive oracle circuit programs -- definitions

A program makes a fixed number of adaptive Boolean-oracle calls. Before round i, its history consists of the original input followed by the i previous answer bits. A query circuit maps that history to a positive-width query, and a final circuit maps the complete history to the program output.

Query widths may vary by round. A variable-call computation can use dummy queries after it has logically terminated, while retaining a fixed circuit shape at each outer input length.

structure Complexity.AdaptiveOracleProgram (inputWidth outputWidth rounds : ℕ) [NeZero inputWidth] [NeZero outputWidth] : Type

A fixed-round adaptive oracle computation whose query generators and final output map are fan-in-two AND/OR circuits.

• queryWidth : Fin rounds → ℕ

  Width of the query issued in each round.

• queryWidth_neZero (round : Fin rounds) : NeZero (self.queryWidth round)

  Every query has positive width, as required by the circuit model.

• queryGates : Fin rounds → ℕ

  Internal-gate count of each query circuit.

• query (round : Fin rounds) : Circuit Basis.andOr2 (inputWidth + ↑round) (self.queryWidth round) (self.queryGates round)

  Query circuit for each round, reading the input and previous answers.

• finalGates : ℕ

  Internal-gate count of the final output circuit.

• final : Circuit Basis.andOr2 (inputWidth + rounds) outputWidth self.finalGates

  Final output circuit, reading the input and every oracle answer.

def Complexity.AdaptiveOracleProgram.history {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (oracle : BooleanOracle) (input : BitString inputWidth) (completed : ℕ) : completed ≤ rounds → BitString (inputWidth + completed)

Semantic history after completed oracle calls. It consists of the original input followed in order by the answers to the first completed queries.

Equations

• One or more equations did not get rendered due to their size.
• program.history oracle input 0 x_2 = input

def Complexity.AdaptiveOracleProgram.eval {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (oracle : BooleanOracle) (input : BitString inputWidth) : BitString outputWidth

Output of the adaptive program relative to a Boolean oracle.

Equations

• program.eval oracle input = program.final.eval (program.history oracle input rounds ⋯)

structure Complexity.AdaptiveOracleProgram.OracleCircuitImplementation {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) : Type

One single-output oracle circuit for each query round of program. The query width fixes which circuit may be used at that round.

• internalGates : Fin rounds → ℕ

  Internal-gate count of the oracle circuit used in each round.

• circuit (round : Fin rounds) : Circuit Basis.andOr2 (program.queryWidth round) 1 (self.internalGates round)

  Oracle circuit at the query width of each round.

def Complexity.AdaptiveOracleProgram.OracleCircuitImplementation.Implements {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] {program : AdaptiveOracleProgram inputWidth outputWidth rounds} (implementation : program.OracleCircuitImplementation) (oracle : BooleanOracle) : Prop

The selected oracle circuits implement oracle when every round circuit returns the oracle's answer on every fixed-width query.

Equations

• implementation.Implements oracle = ∀ (round : Fin rounds) (query : Complexity.BitString (program.queryWidth round)), (implementation.circuit round).eval query 0 = oracle query.toList

def Complexity.AdaptiveOracleProgram.inlineHistorySize {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) (completed : ℕ) : completed ≤ rounds → ℕ

Exact size of the circuit producing a prefix of the inlined adaptive history. This recurrence mirrors inlineHistory: the base identity costs one output gate per original input, and each round pays to retain the old history and to evaluate its query and oracle circuits.

Equations

• One or more equations did not get rendered due to their size.
• program.inlineHistorySize implementation 0 x_2 = inputWidth

def Complexity.AdaptiveOracleProgram.inlineHistory {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) (completed : ℕ) : completed ≤ rounds → (internalGates : ℕ) × Circuit Basis.andOr2 inputWidth (inputWidth + completed) internalGates

Compile the first completed adaptive calls into one circuit producing the original input followed by their answer bits.

Equations

• One or more equations did not get rendered due to their size.
• program.inlineHistory implementation 0 x_2 = ⟨0, Complexity.Circuit.projectInputs fun (input : Fin inputWidth) => input⟩

def Complexity.AdaptiveOracleProgram.inline {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) : (internalGates : ℕ) × Circuit Basis.andOr2 inputWidth outputWidth internalGates

Compile every adaptive call and then the final output circuit into one ordinary oracle-free circuit.

Equations

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