From De Morgan circuits to programs with shared gates

The fan-out of a gate of a circuit is the number of argument slots of gates that read it plus the number of designated outputs equal to it (gateFanOut), and sharedGateCount counts the gates of fan-out at least two. Every single-output circuit over the De Morgan basis computing f yields a SharedProgram computing f with at most sharedGateCount c shared gates and at most as many AND and OR gates as the circuit (exists_sharedProgram_of_circuit); NOT, identity, and constant gates are free, as in DeMorgan.binaryCost.

The program is built from the last gate down. Its variables are all wires of the circuit, so the initial program outputs the literal of the output wire. A gate of fan-out at least two becomes a shared gate computing its formula, and its wire is then exactly the new shared variable (SharedProgram.share). Any other gate is substituted into the program (SharedProgram.substVar); since its variable occurs at most once, this adds the gate's own cost and keeps every earlier gate occurring at most as often as its fan-out.

Consequently Khrapchenko's bound with shared gates holds for the library's De Morgan circuits: a circuit computing the parity of n ≥ 1 bits in which at most k gates have fan-out at least two has n² ≤ (k + 1) · (cost + k + 1), where cost counts the AND and OR gates (parity_sq_le_cost). It has at least C · n AND and OR gates when (k + 1) · (C + 1) ≤ n (mul_le_cost_of_parity), and a family of such circuits with k(n) = o(n) gates of fan-out at least two has superlinear cost (isLittleO_cost_of_parity). Analogous quadratic and superlinear bounds hold for threshold and majority circuits (threshold_mul_le_cost, majority_mul_le_cost, majority_sq_le_cost_of_odd, mul_le_cost_of_majority, isLittleO_cost_of_majority).

Fan-out of circuit gates

def Algebraic.KW.argUses {σ : Signature} {n t : ℕ} (line : Line σ n t) (g : Fin t) : ℕ

The number of arguments of a gate that are equal to gate g.

Equations

• Algebraic.KW.argUses line g = {a : Fin (σ.Arity line.op) | line.wires a = Cslib.Circuits.Wire.gate g}.card

def Algebraic.KW.slotUses {σ : Signature} {n t : ℕ} : Program σ n t → Fin t → ℕ

The number of argument slots of the program's gates that read gate g. The last gate is read by no gate of the program; an earlier gate is read by the gates before the last one and by the arguments of the last gate that are equal to it.

Equations

• Algebraic.KW.slotUses Cslib.Circuits.Program.empty = Fin.elim0
• Algebraic.KW.slotUses (p.gate line) = fun (i : Fin (gateCount + 1)) => Fin.lastCases 0 (fun (g : Fin gateCount) => Algebraic.KW.slotUses p g + Algebraic.KW.argUses line g) i

def Algebraic.KW.gateFanOut {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (g : Fin c.size) : ℕ

The fan-out of gate g of a circuit: the number of argument slots of gates that read g plus the number of designated outputs equal to g.

Equations

• Algebraic.KW.gateFanOut c g = Algebraic.KW.slotUses c.program g + {o : Fin m | c.outputs o = Cslib.Circuits.Wire.gate g}.card

def Algebraic.KW.sharedGateCount {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ℕ

The number of gates of a circuit whose fan-out is at least two.

Equations

• Algebraic.KW.sharedGateCount c = {g : Fin c.size | 2 ≤ Algebraic.KW.gateFanOut c g}.card

@[simp]

theorem Algebraic.KW.slotUses_gate_last {σ : Signature} {n t : ℕ} (p : Program σ n t) (line : Line σ n t) : slotUses (p.gate line) (Fin.last t) = 0

@[simp]

theorem Algebraic.KW.slotUses_gate_castSucc {σ : Signature} {n t : ℕ} (p : Program σ n t) (line : Line σ n t) (g : Fin t) : slotUses (p.gate line) g.castSucc = slotUses p g + argUses line g

def Algebraic.KW.sharedCount {σ : Signature} {n t : ℕ} (p : Program σ n t) (u : Fin t → ℕ) : ℕ

The number of gates of p whose fan-out is at least two when, besides the gates of p, gate g is read u g more times.

Equations

• Algebraic.KW.sharedCount p u = {g : Fin t | 2 ≤ Algebraic.KW.slotUses p g + u g}.card

theorem Algebraic.KW.sharedGateCount_eq {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : sharedGateCount c = sharedCount c.program fun (g : Fin c.size) => {o : Fin m | c.outputs o = Wire.gate g}.card

Occurrences and substitution of a variable

def Algebraic.KW.insertVal {N d : ℕ} (y : Fin (N + d) → Bool) (b : Bool) : Fin (N + 1 + d) → Bool

Insert the value b at position N of y, moving the later entries up by one.

Equations

• Algebraic.KW.insertVal y b i = if h : ↑i < N then y ⟨↑i, ⋯⟩ else if h' : ↑i = N then b else y ⟨↑i - 1, ⋯⟩

theorem Algebraic.KW.insertVal_zero {N : ℕ} (y : Fin N → Bool) (b : Bool) : insertVal y b = Fin.snoc y b

theorem Algebraic.KW.insertVal_snoc {N d : ℕ} (y : Fin (N + d) → Bool) (g b : Bool) : insertVal (Fin.snoc y g) b = Fin.snoc (insertVal y b) g

def Algebraic.KW.Formula.occ {N : ℕ} (v : ℕ) : Formula N → ℕ

The number of literal leaves on the variable with index v.

Equations

• Algebraic.KW.Formula.occ v (Algebraic.KW.Formula.lit i positive) = if ↑i = v then 1 else 0
• Algebraic.KW.Formula.occ v (Algebraic.KW.Formula.const value) = 0
• Algebraic.KW.Formula.occ v (l.and r) = Algebraic.KW.Formula.occ v l + Algebraic.KW.Formula.occ v r
• Algebraic.KW.Formula.occ v (l.or r) = Algebraic.KW.Formula.occ v l + Algebraic.KW.Formula.occ v r

@[simp]

theorem Algebraic.KW.Formula.occ_neg {N : ℕ} (v : ℕ) (F : Formula N) : occ v F.neg = occ v F

@[simp]

theorem Algebraic.KW.Formula.occ_mapIndex_castLE {N M : ℕ} (v : ℕ) (h : N ≤ M) (F : Formula N) : occ v (mapIndex (Fin.castLE h) F) = occ v F

def Algebraic.KW.Formula.substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (i : Fin (N + 1 + d)) : Formula (N + d)

The substitution behind SharedProgram.substVar: the variable N becomes φ, the variables below N are kept, and those above N move down by one.

Equations

• φ.substVarMap d i = if h : ↑i < N then Algebraic.KW.Formula.lit ⟨↑i, ⋯⟩ true else if h' : ↑i = N then Algebraic.KW.Formula.mapIndex (Fin.castLE ⋯) φ else Algebraic.KW.Formula.lit ⟨↑i - 1, ⋯⟩ true

theorem Algebraic.KW.Formula.gates_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (F : Formula (N + 1 + d)) : (subst (φ.substVarMap d) F).gates = F.gates + occ N F * φ.gates

theorem Algebraic.KW.Formula.occ_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) {w : ℕ} (hw : w < N) (F : Formula (N + 1 + d)) : occ w (subst (φ.substVarMap d) F) = occ w F + occ N F * occ w φ

theorem Algebraic.KW.Formula.eval_subst_substVarMap {N : ℕ} (φ : Formula N) (d : ℕ) (F : Formula (N + 1 + d)) (y : Fin (N + d) → Bool) : (subst (φ.substVarMap d) F).eval y = F.eval (insertVal y (φ.eval fun (j : Fin N) => y (Fin.castLE ⋯ j)))

def Algebraic.KW.SharedProgram.occ (v : ℕ) {N k : ℕ} : SharedProgram N k → ℕ

The number of literal leaves on the variable with index v, summed over the formulas.

Equations

• Algebraic.KW.SharedProgram.occ v (Algebraic.KW.SharedProgram.output F) = Algebraic.KW.Formula.occ v F
• Algebraic.KW.SharedProgram.occ v (Algebraic.KW.SharedProgram.share G P) = Algebraic.KW.Formula.occ v G + Algebraic.KW.SharedProgram.occ v P

@[simp]

theorem Algebraic.KW.SharedProgram.occ_output {N : ℕ} (v : ℕ) (F : Formula N) : occ v (output F) = Formula.occ v F

@[simp]

theorem Algebraic.KW.SharedProgram.occ_share {N k : ℕ} (v : ℕ) (G : Formula N) (P : SharedProgram (N + 1) k) : occ v (share G P) = Formula.occ v G + occ v P

@[simp]

theorem Algebraic.KW.SharedProgram.gates_output {N : ℕ} (F : Formula N) : (output F).gates = F.gates

@[simp]

theorem Algebraic.KW.SharedProgram.gates_share {N k : ℕ} (G : Formula N) (P : SharedProgram (N + 1) k) : (share G P).gates = G.gates + P.gates

def Algebraic.KW.SharedProgram.substVar {N : ℕ} (φ : Formula N) {d k : ℕ} : SharedProgram (N + 1 + d) k → SharedProgram (N + d) k

Substitute the formula φ for the variable N of a program reading N + 1 + d variables, the last d of them shared values: the variables above N move down by one, and the program then reads φ wherever it read variable N.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.KW.SharedProgram.substVar φ (Algebraic.KW.SharedProgram.output F) = Algebraic.KW.SharedProgram.output (Algebraic.KW.Formula.subst (φ.substVarMap x✝) F)

theorem Algebraic.KW.SharedProgram.eval_substVar {N : ℕ} (φ : Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) (y : Fin (N + d) → Bool) : (substVar φ P).eval y = P.eval (insertVal y (φ.eval fun (j : Fin N) => y (Fin.castLE ⋯ j)))

theorem Algebraic.KW.SharedProgram.gates_substVar {N : ℕ} (φ : Formula N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : (substVar φ P).gates = P.gates + occ N P * φ.gates

theorem Algebraic.KW.SharedProgram.occ_substVar {N : ℕ} (φ : Formula N) {w : ℕ} (hw : w < N) {d k : ℕ} (P : SharedProgram (N + 1 + d) k) : occ w (substVar φ P) = occ w P + occ N P * Formula.occ w φ

De Morgan gates as formulas

def Algebraic.KW.lineFormula {n t : ℕ} : Line DeMorgan.signature n t → Formula (n + t)

The formula of one De Morgan gate over the earlier wires, numbered by Wire.index.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.KW.lineFormula { op := Algebraic.DeMorgan.Op.false, wires := wires } = Algebraic.KW.Formula.const false
• Algebraic.KW.lineFormula { op := Algebraic.DeMorgan.Op.true, wires := wires } = Algebraic.KW.Formula.const true
• Algebraic.KW.lineFormula { op := Algebraic.DeMorgan.Op.id, wires := w } = Algebraic.KW.Formula.lit (w ⟨0, Algebraic.KW.lineFormula._proof_3⟩).index true
• Algebraic.KW.lineFormula { op := Algebraic.DeMorgan.Op.not, wires := w } = Algebraic.KW.Formula.lit (w ⟨0, Algebraic.KW.lineFormula._proof_4⟩).index false

def Algebraic.KW.wireValues {n t : ℕ} (p : Program DeMorgan.signature n t) (x : Fin n → Bool) : Fin (n + t) → Bool

The values of the inputs and gates of a De Morgan program, numbered by Wire.index.

Equations

• Algebraic.KW.wireValues p x = Fin.append x (p.eval Algebraic.DeMorgan.interpretation x)

theorem Algebraic.KW.append_index {n t : ℕ} (x : Fin n → Bool) (vals : Fin t → Bool) (w : Wire n t) : Fin.append x vals w.index = Wire.elim x vals w

theorem Algebraic.KW.eval_lineFormula {n t : ℕ} (line : Line DeMorgan.signature n t) (x : Fin n → Bool) (vals : Fin t → Bool) : (lineFormula line).eval (Fin.append x vals) = line.eval DeMorgan.interpretation x vals

theorem Algebraic.KW.gates_lineFormula {n t : ℕ} (line : Line DeMorgan.signature n t) : (lineFormula line).gates = DeMorgan.binaryCost line.op

theorem Algebraic.KW.index_val_eq_iff {n t : ℕ} (w : Wire n t) (g : Fin t) : ↑w.index = n + ↑g ↔ w = Wire.gate g

theorem Algebraic.KW.occ_lineFormula_le {n t : ℕ} (line : Line DeMorgan.signature n t) (g : Fin t) : Formula.occ (n + ↑g) (lineFormula line) ≤ argUses line g

theorem Algebraic.KW.eval_gate {n t : ℕ} (p : Program DeMorgan.signature n t) (line : Line DeMorgan.signature n t) (x : Fin n → Bool) : (p.gate line).eval DeMorgan.interpretation x = Fin.snoc (p.eval DeMorgan.interpretation x) (line.eval DeMorgan.interpretation x (p.eval DeMorgan.interpretation x))

theorem Algebraic.KW.wireValues_gate {n t : ℕ} (p : Program DeMorgan.signature n t) (line : Line DeMorgan.signature n t) (x : Fin n → Bool) : wireValues (p.gate line) x = Fin.snoc (wireValues p x) ((lineFormula line).eval (wireValues p x))

theorem Algebraic.KW.wireValues_empty {n : ℕ} (x : Fin n → Bool) : wireValues Program.empty x = x

From circuits to programs

theorem Algebraic.KW.sharedCount_gate {σ : Signature} {n t : ℕ} (p : Program σ n t) (line : Line σ n t) (u : Fin (t + 1) → ℕ) : sharedCount (p.gate line) u = (if 2 ≤ u (Fin.last t) then 1 else 0) + sharedCount p fun (g : Fin t) => u g.castSucc + argUses line g

theorem Algebraic.KW.exists_sharedProgram_of_program {n : ℕ} (f : Cslib.BooleanFunction n) {t : ℕ} (p : Program DeMorgan.signature n t) (u : Fin t → ℕ) {j : ℕ} (Q : SharedProgram (n + t) j) : (∀ (x : Fin n → Bool), Q.eval (wireValues p x) = f x) → (∀ (g : Fin t), SharedProgram.occ (n + ↑g) Q ≤ u g) → ∃ (k : ℕ) (P : SharedProgram n k), k ≤ j + sharedCount p u ∧ P.Computes f ∧ P.gates ≤ Q.gates + Program.cost DeMorgan.binaryCost p

Build a program from the last gate of a De Morgan program down. Q reads all wires of p, gate g occurring at most u g times; a gate of total fan-out slotUses p g + u g at least two becomes a shared gate and any other gate is substituted.

theorem Algebraic.KW.exists_sharedProgram_of_circuit {n : ℕ} (c : Circuit DeMorgan.signature n 1) {f : Cslib.BooleanFunction n} (hc : c.ComputesWith DeMorgan.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : ∃ (k : ℕ) (P : SharedProgram n k), k ≤ sharedGateCount c ∧ P.Computes f ∧ P.gates ≤ c.cost DeMorgan.binaryCost

De Morgan circuits as programs with shared gates. A single-output circuit over the De Morgan basis computing f yields a program computing f with at most as many shared gates as the circuit has gates of fan-out at least two, and at most as many AND and OR gates as the circuit.

Parity

theorem Algebraic.KW.parity_sq_le_cost {n : ℕ} [NeZero n] {k : ℕ} (c : Circuit DeMorgan.signature n 1) (computes : c.ComputesWith DeMorgan.interpretation (GateElimination.Xor.parityTarget n)) (hk : sharedGateCount c ≤ k) : n ^ 2 ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1)

Parity in De Morgan circuits with few shared gates. If a De Morgan circuit computes the parity of n ≥ 1 bits and at most k of its gates have fan-out at least two, then n² ≤ (k + 1) · (cost + k + 1), where cost counts its AND and OR gates; so it has at least n² / (k + 1) - (k + 1) AND and OR gates.

theorem Algebraic.KW.mul_le_cost_of_parity {n k C : ℕ} (hkn : (k + 1) * (C + 1) ≤ n) (c : Circuit DeMorgan.signature n 1) (computes : c.ComputesWith DeMorgan.interpretation (GateElimination.Xor.parityTarget n)) (hk : sharedGateCount c ≤ k) : C * n ≤ c.cost DeMorgan.binaryCost

Superlinear cost for parity with few shared gates. If (k + 1) · (C + 1) ≤ n, every De Morgan circuit computing the parity of n bits in which at most k gates have fan-out at least two has at least C · n AND and OR gates.

theorem Algebraic.KW.isLittleO_cost_of_parity {k : ℕ → ℕ} (hk : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (c : (n : ℕ) → Circuit DeMorgan.signature n 1) (computes : ∀ (n : ℕ), (c n).ComputesWith DeMorgan.interpretation (GateElimination.Xor.parityTarget n)) (hshared : ∀ (n : ℕ), sharedGateCount (c n) ≤ k n) : (fun (n : ℕ) => ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑((c n).cost DeMorgan.binaryCost)

Parity needs superlinear De Morgan circuits when o(n) gates have fan-out at least two. If k n = o(n) and, for every n, c n is a De Morgan circuit computing the parity of n bits in which at most k n gates have fan-out at least two, then the number of AND and OR gates of c n grows faster than n.

Threshold and majority

@[reducible, inline]

abbrev Algebraic.KW.thresholdTarget (n t : ℕ) : Target Bool n 1

Single-output circuit target for the t-threshold function on n bits.

Equations

• Algebraic.KW.thresholdTarget n t x x✝ = Algebraic.KW.threshold t x

@[reducible, inline]

abbrev Algebraic.KW.majorityTarget (n : ℕ) : Target Bool n 1

Single-output circuit target for the strict majority function on n bits.

Equations

• Algebraic.KW.majorityTarget n x x✝ = Algebraic.KW.majority x

theorem Algebraic.KW.threshold_mul_le_cost {n t k : ℕ} (ht : 1 ≤ t) (htn : t ≤ n) (c : Circuit DeMorgan.signature n 1) (computes : c.ComputesWith DeMorgan.interpretation (thresholdTarget n t)) (hk : sharedGateCount c ≤ k) : (n + 1 - t) * t ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1)

Threshold functions in De Morgan circuits with few shared gates. For 1 ≤ t ≤ n, every De Morgan circuit computing threshold t in which at most k gates have fan-out at least two satisfies (n + 1 - t) · t ≤ (k + 1) · (cost + k + 1), where cost counts its AND and OR gates.

theorem Algebraic.KW.majority_mul_le_cost {n k : ℕ} (hn : 1 ≤ n) (c : Circuit DeMorgan.signature n 1) (computes : c.ComputesWith DeMorgan.interpretation (majorityTarget n)) (hk : sharedGateCount c ≤ k) : (n - n / 2) * (n / 2 + 1) ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1)

Majority in De Morgan circuits with few shared gates. Every De Morgan circuit computing strict majority of n ≥ 1 bits in which at most k gates have fan-out at least two satisfies (n - ⌊n/2⌋) · (⌊n/2⌋ + 1) ≤ (k + 1) · (cost + k + 1), where cost counts its AND and OR gates.

theorem Algebraic.KW.majority_sq_le_cost_of_odd {n k : ℕ} (hodd : Odd n) (c : Circuit DeMorgan.signature n 1) (computes : c.ComputesWith DeMorgan.interpretation (majorityTarget n)) (hk : sharedGateCount c ≤ k) : (n / 2 + 1) ^ 2 ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1)

Odd-input majority in De Morgan circuits with few shared gates. For odd n, every De Morgan circuit computing strict majority of n bits in which at most k gates have fan-out at least two satisfies (⌊n/2⌋ + 1)² ≤ (k + 1) · (cost + k + 1).

theorem Algebraic.KW.mul_le_cost_of_majority {m k C : ℕ} (hkm : (k + 1) * (C + 1) ≤ m) (c : Circuit DeMorgan.signature (2 * m + 1) 1) (computes : c.ComputesWith DeMorgan.interpretation (majorityTarget (2 * m + 1))) (hk : sharedGateCount c ≤ k) : C * m ≤ c.cost DeMorgan.binaryCost

Superlinear cost for majority with few shared gates. If (k + 1) · (C + 1) ≤ m, every De Morgan circuit computing the majority of 2 * m + 1 bits in which at most k gates have fan-out at least two has at least C · m AND and OR gates.

theorem Algebraic.KW.isLittleO_cost_of_majority {k : ℕ → ℕ} (hk : (fun (m : ℕ) => ↑(k m)) =o[Filter.atTop] fun (m : ℕ) => ↑m) (c : (m : ℕ) → Circuit DeMorgan.signature (2 * m + 1) 1) (computes : ∀ (m : ℕ), (c m).ComputesWith DeMorgan.interpretation (majorityTarget (2 * m + 1))) (hshared : ∀ (m : ℕ), sharedGateCount (c m) ≤ k m) : (fun (m : ℕ) => ↑m) =o[Filter.atTop] fun (m : ℕ) => ↑((c m).cost DeMorgan.binaryCost)

Majority needs superlinear De Morgan circuits when o(m) gates have fan-out at least two. If k m = o(m) and, for every m, c m is a De Morgan circuit computing the majority of 2 * m + 1 bits in which at most k m gates have fan-out at least two, then the number of AND and OR gates of c m grows faster than m.