Internal: Nondeterministic Quantification Circuit Constructions #

This internal module provides the circuit constructions needed for the nondeterministic quantification complexity bounds in Complexitylib.Circuits.Nondeterminism.

Circuit restriction #

Given a circuit computing f : BitString ((k+1)+m) → Bool, we construct a circuit of the same size computing restrictFirst f b : BitString (k+m) → Bool (the function with its first input hardwired to b).

The key construction is restrictGateBounded, which transforms each gate in-place:

If both inputs reference wire 0 (the hardwired input), the gate becomes a constant gate producing the correct value.
If one input references wire 0, the gate simplifies to either a constant or an identity on the other input, depending on the operation and the hardwired value.
If neither input references wire 0, both wire indices are shifted down by 1 (since the hardwired input is removed).

In all cases, the gate count is preserved.

OR combination #

This module also imports Complexitylib.Circuits.Internal.ShannonUpper so that the surface module can use ShannonUpper.binopCircuit to bound the circuit complexity of the OR of two Boolean functions by the sum of their complexities plus one; no OR-specific construction is defined here.

Gate evaluation helpers #

Restriction gate construction #

Restricted circuit #

source

def Complexity.restrictCircuit {k m G : ℕ} [NeZero m] (b : Bool) (c : Circuit Basis.andOr2 (k + 1 + m) 1 G) :

Circuit Basis.andOr2 (k + m) 1 G

The restricted circuit: same gate count, with each gate transformed by restrictGateBounded to account for the hardwired first input.

Equations

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

Instances For

Correctness of restriction #

source

theorem Complexity.restrictCircuit_eval {k m G : ℕ} [NeZero m] (b : Bool) (c : Circuit Basis.andOr2 (k + 1 + m) 1 G) (f : BitString (k + 1 + m) → Bool) (heval : (fun (x : BitString (k + 1 + m)) => c.eval x 0) = f) :

(fun (x : BitString (k + m)) => (restrictCircuit b c).eval x 0) = restrictFirst f b

The restricted circuit computes restrictFirst f b.

Documentation