Internal: Nondeterministic Quantification Circuit Constructions #
This internal module provides the circuit constructions needed for the
nondeterministic quantification complexity bounds in Circ.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 restrictGateP, 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 #
The OR of two Boolean functions has circuit complexity bounded by the sum
of their complexities plus one, using ShannonUpper.binopCircuit.
Gate evaluation helpers #
Restriction gate construction #
Restricted circuit #
def
CircuitComplexity.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 restrictGateP to account for the hardwired first input.
Equations
- One or more equations did not get rendered due to their size.