Symmetric gates reading their wires with multiplicities

The extra gates of the bases of TC (majority) and of ACⁱ[q] (MOD_q) are symmetric: their value depends only on the number of their true arguments. Unlike a conjunction or a disjunction, such a gate depends on how often it reads a wire, so its fan-in is not bounded by the size of the circuit (Unbounded.dedup does not apply). It is determined, however, by the distinct wires it reads and their multiplicities.

Unbounded.multSignature is the unbounded fan-in basis together with a gate .gate N mult for every N and every mult : Fin N → ℕ, reading N wires, the ith of them mult i times; under Unbounded.multInterpretation G it computes G (∑ i, mult i) of the number of true arguments counted with multiplicity (Unbounded.multWeight). Replacing every gate of a circuit over Unbounded.extSignature by the gate reading its distinct wires with their multiplicities, and every conjunction and disjunction by Unbounded.dedupLine, gives a circuit over multSignature (Unbounded.multCircuit) computing the same function, when the extra gates of m arguments compute G m of the number of their true arguments (Unbounded.eval_multCircuit), with the same size, no larger depth, and every gate reading at most n + s wires (Unbounded.arity_lines_multCircuit_le).

Main definitions

• Cslib.Circuits.Boolean.Unbounded.multSignature, Cslib.Circuits.Boolean.Unbounded.multInterpretation: symmetric gates with multiplicities.
• Cslib.Circuits.Boolean.Unbounded.multCircuit: the circuit whose symmetric gates read their distinct wires with multiplicities.

Main results

• Cslib.Circuits.Boolean.Unbounded.eval_multCircuit, Cslib.Circuits.Boolean.Unbounded.depth_multCircuit_le, Cslib.Circuits.Boolean.Unbounded.arity_lines_multCircuit_le: aggregating multiplicities keeps the function and the size, makes no gate deeper, and bounds the fan-in by the number of inputs and gates.

References

• H. Vollmer, Introduction to Circuit Complexity

inductive Cslib.Circuits.Boolean.Unbounded.MultOp : Type

The operations of the unbounded fan-in basis, and a symmetric gate reading N wires, the ith of them mult i times.

• ac (op : Op) : MultOp

  An operation of the unbounded fan-in basis.

• gate (N : ℕ) (mult : Fin N → ℕ) : MultOp

  A symmetric gate reading N wires with multiplicities mult.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Unbounded.MultOp.arity : MultOp → ℕ

The arity of an operation: the number of distinct wires a symmetric gate reads.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Unbounded.multSignature : Signature

The signature of the unbounded fan-in basis with symmetric gates reading their wires with multiplicities. It is reducible, so that case analysis on its operations sees their arities.

def Cslib.Circuits.Boolean.Unbounded.multWeight {N : ℕ} (mult : Fin N → ℕ) (x : Fin N → Bool) : ℕ

The number of true arguments, the ith counted mult i times.

def Cslib.Circuits.Boolean.Unbounded.multInterpretation (G : ℕ → ℕ → Bool) : Interpretation multSignature Bool

The meaning of the basis with symmetric gates: the gate of multiplicities mult computes G (∑ i, mult i) of the number of true arguments counted with multiplicity.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.multInterpretation_ac (G : ℕ → ℕ → Bool) (op : Op) (x : Fin op.arity → Bool) : multInterpretation G (MultOp.ac op) x = interpretation op x

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.multInterpretation_gate (G : ℕ → ℕ → Bool) (N : ℕ) (mult : Fin N → ℕ) (x : Fin N → Bool) : multInterpretation G (MultOp.gate N mult) x = G (∑ i : Fin N, mult i) (multWeight mult x)

Aggregating multiplicities

def Cslib.Circuits.Boolean.Unbounded.multLine {n g : ℕ} : Line extSignature n g → Line multSignature n g

The line reading the distinct wires of line: a conjunction or disjunction reads each once, and a symmetric gate reads each with its multiplicity in line.

theorem Cslib.Circuits.Boolean.Unbounded.multWeight_count_dedup {n g k : ℕ} (w : Fin k → Wire n g) (v : Wire n g → Bool) : (multWeight (fun (j : Fin (List.ofFn w).dedup.length) => List.count (List.ofFn w).dedup[↑j] (List.ofFn w)) fun (j : Fin (List.ofFn w).dedup.length) => v (List.ofFn w).dedup[↑j]) = BitString.weight (v ∘ w)

Reading the distinct wires with their multiplicities counts the true arguments.

theorem Cslib.Circuits.Boolean.Unbounded.sum_count_dedup {n g k : ℕ} (w : Fin k → Wire n g) : ∑ j : Fin (List.ofFn w).dedup.length, List.count (List.ofFn w).dedup[↑j] (List.ofFn w) = k

Reading the distinct wires with their multiplicities keeps the number of arguments.

theorem Cslib.Circuits.Boolean.Unbounded.eval_multLine {n g : ℕ} {G : ℕ → ℕ → Bool} {f : (m : ℕ) → BooleanFunction m} (hf : ∀ (m : ℕ) (x : BitString m), f m x = G m (BitString.weight x)) (line : Line extSignature n g) (x : Fin n → Bool) (gates : Fin g → Bool) : (multLine line).eval (multInterpretation G) x gates = line.eval (extInterpretation f) x gates

Aggregating multiplicities keeps the value of a line, when the extra gate of m arguments computes G m of the number of its true arguments.

theorem Cslib.Circuits.Boolean.Unbounded.depth_multLine_le {n g : ℕ} (line : Line extSignature n g) (depths : Wire n g → ℕ) : (multLine line).depth depths ≤ line.depth depths

Aggregating multiplicities makes no line deeper.

theorem Cslib.Circuits.Boolean.Unbounded.arity_multLine_le {n g : ℕ} (line : Line extSignature n g) : multSignature.Arity (multLine line).op ≤ n + g

A line reading its distinct wires reads at most all n + g wires.

def Cslib.Circuits.Boolean.Unbounded.multCircuit {n m : ℕ} (C : Circuit extSignature n m) : Circuit multSignature n m

The circuit whose symmetric gates read their distinct wires with multiplicities, and whose conjunctions and disjunctions read their distinct wires once.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.size_multCircuit {n m : ℕ} (C : Circuit extSignature n m) : (multCircuit C).size = C.size

Aggregating multiplicities keeps the size.

theorem Cslib.Circuits.Boolean.Unbounded.eval_multCircuit {n m : ℕ} {G : ℕ → ℕ → Bool} {f : (m : ℕ) → BooleanFunction m} (hf : ∀ (m : ℕ) (x : BitString m), f m x = G m (BitString.weight x)) (C : Circuit extSignature n m) : (multCircuit C).eval (multInterpretation G) = C.eval (extInterpretation f)

Aggregating multiplicities keeps the function computed, when the extra gate of m arguments computes G m of the number of its true arguments.

theorem Cslib.Circuits.Boolean.Unbounded.depth_multCircuit_le {n m : ℕ} (C : Circuit extSignature n m) : (multCircuit C).depth ≤ C.depth

Aggregating multiplicities makes no gate deeper.

theorem Cslib.Circuits.Boolean.Unbounded.arity_lines_multCircuit_le {n m : ℕ} (C : Circuit extSignature n m) (k : Fin C.size) : multSignature.Arity ((multCircuit C).program.lines k).op ≤ n + C.size

Every gate of multCircuit C reads at most all n + C.size wires.

theorem Cslib.Circuits.Boolean.Unbounded.fanInAtMost_multCircuit {n m : ℕ} (C : Circuit extSignature n m) : (multCircuit C).FanInAtMost (n + C.size)

Fan-in reduction: the gates of multCircuit C have fan-in at most the number of inputs and gates of C.