Gate elimination: parity needs 3 (n - 1) binary gates

A De Morgan circuit computing the parity of n bits has at least 3 (n - 1) AND and OR gates, however many negations and constants it uses (three_mul_le_cost_of_computes_parity). This is Schnorr's bound [Sch74], Jukna, Section 1.6. It is attained by chaining x ⊕ y = (x ∨ y) ∧ ¬(x ∧ y), which spends three binary gates on each bit after the first (exists_computes_parity), so 3 (n - 1) is the exact count (isLeast_cost_parity). It is the prototypical gate-elimination argument: fixing one bit suitably makes three binary gates superfluous and leaves the parity of the other bits, possibly negated.

The proof does not rewrite circuits. For a restriction (partial assignment) ρ it counts the nonredundant gates: AND and OR gates whose function, once the bits fixed by ρ are hardwired, is neither constant, nor a literal, nor one of its arguments up to negation (GateElimination.NonRedundant). Fixing more bits never makes a redundant gate nonredundant (GateElimination.nonRedundant_update_subset). Every nonredundant gate survives the simplifications of the textbook proof, so their number is a lower bound on the number of binary gates, and it is what each step of the proof decreases.

The step follows Schnorr. Consider the nonredundant gates from which a chain of nonredundant gates, negations and gates that compute one of their arguments up to negation leads to the output. The first of them reads two different bits xᵢ and xⱼ, each of which, suitably fixed, makes it constant. Another of them reads xᵢ: otherwise fixing xⱼ would make the output ignore xᵢ. Fixing xᵢ then makes three of them redundant: the first gate, the other reader of xᵢ, and a gate reading the first one, or reading the other reader of xᵢ if that is the same gate.

Main definitions

• Cslib.Circuits.Boolean.GateElimination.restricted: the function of a wire under a restriction.
• Cslib.Circuits.Boolean.GateElimination.NonRedundant: nonredundant gates under a restriction.

Main results

• Cslib.Circuits.Boolean.three_mul_le_cost_of_computes_parity: a circuit computing the parity of n bits has at least 3 (n - 1) AND and OR gates.
• Cslib.Circuits.Boolean.isLeast_cost_parity: and some circuit has exactly that many.
• Cslib.Circuits.Boolean.three_mul_le_complexity_parity: the circuit complexity of parity is at least 3 (n - 1).

References

• C.-P. Schnorr, Zwei lineare untere Schranken für die Komplexität Boolescher Funktionen
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

Constants, literals and negations

def Cslib.Circuits.Boolean.GateElimination.EqUpToNeg {n : ℕ} (φ ψ : BooleanFunction n) : Prop

φ is ψ or its negation.

def Cslib.Circuits.Boolean.GateElimination.IsConstOrLiteral {n : ℕ} (φ : BooleanFunction n) : Prop

φ is constant or a literal.

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.refl {n : ℕ} (φ : BooleanFunction n) : EqUpToNeg φ φ

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.symm {n : ℕ} {φ ψ : BooleanFunction n} (h : EqUpToNeg φ ψ) : EqUpToNeg ψ φ

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.trans {n : ℕ} {φ ψ χ : BooleanFunction n} (h₁ : EqUpToNeg φ ψ) (h₂ : EqUpToNeg ψ χ) : EqUpToNeg φ χ

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.isConst {n : ℕ} {φ ψ : BooleanFunction n} (h : EqUpToNeg φ ψ) (hψ : Function.IsConst ψ) : Function.IsConst φ

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.isConstOrLiteral {n : ℕ} {φ ψ : BooleanFunction n} (h : EqUpToNeg φ ψ) (hψ : IsConstOrLiteral ψ) : IsConstOrLiteral φ

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.dependsOn {n : ℕ} {φ ψ : BooleanFunction n} {s : Set (Fin n)} (h : EqUpToNeg φ ψ) (hψ : DependsOn ψ s) : DependsOn φ s

theorem Cslib.Circuits.Boolean.GateElimination.EqUpToNeg.comp_right {n : ℕ} {φ ψ : BooleanFunction n} (h : EqUpToNeg φ ψ) (f : BitString n → BitString n) : EqUpToNeg (φ ∘ f) (ψ ∘ f)

theorem Cslib.Circuits.Boolean.GateElimination.isConstOrLiteral_literal {n : ℕ} (i : Fin n) : IsConstOrLiteral fun (x : BitString n) => x i

theorem Cslib.Circuits.Boolean.GateElimination.isConstOrLiteral_of_eq_comp {n : ℕ} {φ : BooleanFunction n} {i : Fin n} (f : Bool → Bool) (h : ∀ (x : BitString n), φ x = f (x i)) : IsConstOrLiteral φ

A function of bit i alone is constant or a literal.

theorem Cslib.Circuits.Boolean.GateElimination.IsConstOrLiteral.comp_fill {n : ℕ} {φ : BooleanFunction n} (h : IsConstOrLiteral φ) (ρ : BitString.PartialAssignment (Fin n)) : IsConstOrLiteral (φ ∘ ρ.fill)

Hardwiring bits keeps constants and literals.

theorem Cslib.Circuits.Boolean.GateElimination.IsConstOrLiteral.eqUpToNeg_or_dependsOn {n : ℕ} {φ : BooleanFunction n} (h : IsConstOrLiteral φ) (i : Fin n) : (EqUpToNeg φ fun (x : BitString n) => x i) ∨ DependsOn φ {i}ᶜ

A constant or a literal is bit i up to negation or ignores it.

Gates

Restricted programs

def Cslib.Circuits.Boolean.GateElimination.restricted {n g : ℕ} (p : Program signature n g) (ρ : BitString.PartialAssignment (Fin n)) (w : Wire n g) : BooleanFunction n

The function computed at wire w once the bits fixed by ρ are hardwired.

theorem Cslib.Circuits.Boolean.GateElimination.restricted_gate_apply {n g : ℕ} (p : Program signature n g) (ρ : BitString.PartialAssignment (Fin n)) (k : Fin g) (x : BitString n) : restricted p ρ (Wire.gate k) x = interpretation (p.lines k).op fun (s : Fin (signature.Arity (p.lines k).op)) => restricted p ρ ((p.lines k).wires s) x

theorem Cslib.Circuits.Boolean.GateElimination.isConstOrLiteral_restricted_input {n g : ℕ} (p : Program signature n g) (ρ : BitString.PartialAssignment (Fin n)) (i : Fin n) : IsConstOrLiteral (restricted p ρ (Wire.input i))

theorem Cslib.Circuits.Boolean.GateElimination.restricted_update {n g : ℕ} {p : Program signature n g} {ρ : BitString.PartialAssignment (Fin n)} {i : Fin n} (hi : ρ i = none) (b : Bool) (w : Wire n g) : restricted p (Function.update ρ i (some b)) w = restricted p ρ w ∘ BitString.PartialAssignment.fill (Function.update ρ i (some b))

Fixing one more free bit is restricting the restricted function.

theorem Cslib.Circuits.Boolean.GateElimination.restricted_update_of_ne_none {n g : ℕ} {p : Program signature n g} {ρ : BitString.PartialAssignment (Fin n)} {i : Fin n} (hi : ρ i ≠ none) (w : Wire n g) (x : BitString n) (c : Bool) : restricted p ρ w (Function.update x i c) = restricted p ρ w x

theorem Cslib.Circuits.Boolean.GateElimination.isConst_update_of_eqUpToNeg {n g : ℕ} {p : Program signature n g} {ρ : BitString.PartialAssignment (Fin n)} {i : Fin n} (hi : ρ i = none) (a : Bool) {w w' : Wire n g} (h : EqUpToNeg (restricted p ρ w) (restricted p ρ w')) (hc : Function.IsConst (restricted p (Function.update ρ i (some a)) w')) : Function.IsConst (restricted p (Function.update ρ i (some a)) w)

A wire that is another up to negation is constant when the other is, after fixing a bit.

theorem Cslib.Circuits.Boolean.GateElimination.restricted_update_of_parity {n g : ℕ} {p : Program signature n g} {ρ : BitString.PartialAssignment (Fin n)} {i : Fin n} {o : Wire n g} (hi : ρ i = none) (b : Bool) {c : Bool} (ho : ∀ (x : BitString n), restricted p ρ o x = (c ^^ parityOn ρ.free x)) (x : BitString n) : restricted p (Function.update ρ i (some b)) o x = (c ^^ b ^^ parityOn (BitString.PartialAssignment.free (Function.update ρ i (some b))) x)

Fixing a free bit of the parity of all free bits leaves the parity of the others, possibly negated.

Nonredundant gates

def Cslib.Circuits.Boolean.GateElimination.NonRedundant {n g : ℕ} (p : Program signature n g) (ρ : BitString.PartialAssignment (Fin n)) (k : Fin g) : Prop

Gate k is a nonredundant binary gate once the bits fixed by ρ are hardwired: an AND or OR gate whose function is neither constant, nor a literal, nor one of its arguments up to negation.

noncomputable def Cslib.Circuits.Boolean.GateElimination.nonRedundant {n g : ℕ} (p : Program signature n g) (ρ : BitString.PartialAssignment (Fin n)) : Finset (Fin g)

The nonredundant binary gates under ρ.

@[simp]

theorem Cslib.Circuits.Boolean.GateElimination.mem_nonRedundant {n g : ℕ} {p : Program signature n g} {ρ : BitString.PartialAssignment (Fin n)} {k : Fin g} : k ∈ nonRedundant p ρ ↔ NonRedundant p ρ k

theorem Cslib.Circuits.Boolean.GateElimination.card_nonRedundant_le {n g : ℕ} (p : Program signature n g) (ρ : BitString.PartialAssignment (Fin n)) : (nonRedundant p ρ).card ≤ p.cost binaryCost

There are at most as many nonredundant gates as binary gates.

theorem Cslib.Circuits.Boolean.GateElimination.nonRedundant_update_subset {n g : ℕ} {p : Program signature n g} {ρ : BitString.PartialAssignment (Fin n)} {i : Fin n} (hi : ρ i = none) (b : Bool) : nonRedundant p (Function.update ρ i (some b)) ⊆ nonRedundant p ρ

Fixing one more bit only makes gates redundant.

Wires that may matter

Eliminating three gates

theorem Cslib.Circuits.Boolean.GateElimination.not_isConstOrLiteral_parityOn {n : ℕ} {s : Finset (Fin n)} (hs : 2 ≤ s.card) (c : Bool) : ¬IsConstOrLiteral fun (x : BitString n) => c ^^ parityOn s x

theorem Cslib.Circuits.Boolean.GateElimination.exists_card_add_three_le {n g : ℕ} (p : Program signature n g) {ρ : BitString.PartialAssignment (Fin n)} (o : Wire n g) {c : Bool} (ho : ∀ (x : BitString n), restricted p ρ o x = (c ^^ parityOn ρ.free x)) (hV : 2 ≤ ρ.free.card) : ∃ (i : Fin n) (b : Bool), ρ i = none ∧ (nonRedundant p (Function.update ρ i (some b))).card + 3 ≤ (nonRedundant p ρ).card

Schnorr's elimination step. If, under ρ, the wire o computes the parity of all free bits, possibly negated, and at least two bits are free, then fixing one free bit suitably makes at least three nonredundant gates redundant.

theorem Cslib.Circuits.Boolean.GateElimination.three_mul_le_card_nonRedundant {n g : ℕ} (p : Program signature n g) (o : Wire n g) (m : ℕ) (ρ : BitString.PartialAssignment (Fin n)) (c : Bool) (hρ : ρ.free.card = m + 1) (ho : ∀ (x : BitString n), restricted p ρ o x = (c ^^ parityOn ρ.free x)) : 3 * m ≤ (nonRedundant p ρ).card

Under a restriction leaving m + 1 bits free for which the wire o computes their parity, possibly negated, at least 3 m gates are nonredundant.

theorem Cslib.Circuits.Boolean.three_mul_le_cost_of_computes_parity {n : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) : 3 * (n - 1) ≤ C.program.cost binaryCost

Schnorr's bound. A De Morgan circuit computing the parity of n bits has at least 3 (n - 1) AND and OR gates, however many negations and constants it uses.

theorem Cslib.Circuits.Boolean.isLeast_cost_parity (n : ℕ) : IsLeast {k : ℕ | ∃ (C : Circuit signature n 1), C.Computes interpretation (single (parity n)) ∧ C.program.cost binaryCost = k} (3 * (n - 1))

The least number of AND and OR gates in a De Morgan circuit computing the parity of n bits is 3 (n - 1).

theorem Cslib.Circuits.Boolean.three_mul_le_size_of_computes_parity {n : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) : 3 * (n - 1) ≤ C.size

A De Morgan circuit computing the parity of n bits has at least 3 (n - 1) gates.

theorem Cslib.Circuits.Boolean.three_mul_le_complexity_parity (n : ℕ) : 3 * (n - 1) ≤ complexity interpretation (single (parity n))

The De Morgan circuit complexity of the parity of n bits is at least 3 (n - 1).