Counting the binary gates of De Morgan circuits

The size of a De Morgan circuit counts every gate. The usual measure for lower bounds charges only the AND and OR gates and lets negations and constants be free Jukna, Section 1.2. It is the cost of a program for binaryCost, and it is at most the size (Program.cost_binaryCost_le).

Because only binary AND and OR gates have arity two while constants have arity zero and negations have arity one (Boolean.arity_le_one_add_binaryCost), only binary gates increase the number of supporting inputs in the backward cone of a frontier (Program.card_biUnion_wireSupport_le_cost_binaryCost). Every De Morgan circuit with m outputs therefore depends on at most m + c.program.cost binaryCost inputs (Circuit.card_inputSupport_le_cost_binaryCost).

Main definitions

• Cslib.Circuits.Boolean.Op.IsBinary: AND and OR, the operations of arity two.
• Cslib.Circuits.Boolean.binaryCost: the cost function charging one for each AND and OR gate.

Main results

• Cslib.Circuits.Boolean.arity_le_one_add_binaryCost: every De Morgan operation has arity at most 1 + binaryCost op.
• Cslib.Circuits.Program.cost_binaryCost_le: the number of binary gates is at most the size.
• Cslib.Circuits.Program.cost_binaryCost_eq_iff_forall_isBinary: p.cost binaryCost = g iff every line of p is a binary AND or OR gate.
• Cslib.Circuits.Program.card_biUnion_wireSupport_le_cost_binaryCost: the number of inputs supporting a frontier of wires is at most frontier.card + p.cost binaryCost.
• Cslib.Circuits.Circuit.card_inputSupport_le_cost_binaryCost, Cslib.Circuits.Circuit.essential_le_cost_binaryCost: a De Morgan circuit with m outputs has at most m + c.program.cost binaryCost supporting (or essential) inputs.
• Cslib.Circuits.Circuit.cost_binaryCost_eq_size_of_size_le: a one-output De Morgan circuit with all n inputs in its support and c.size + 1 ≤ n has c.program.cost binaryCost = c.size = n - 1 and consists solely of binary AND/OR gates.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Circuits.Boolean.Op.IsBinary (op : Op) : Prop

The binary operations of the De Morgan basis, AND and OR.

@[instance_reducible]

instance Cslib.Circuits.Boolean.instDecidablePredOpIsBinary : DecidablePred Op.IsBinary

Decidability of whether a De Morgan operation is binary.

theorem Cslib.Circuits.Boolean.Op.isBinary_iff {op : Op} : op.IsBinary ↔ op = and ∨ op = or

A De Morgan operation is binary if and only if it is .and or .or.

theorem Cslib.Circuits.Boolean.Op.isBinary_and : and.IsBinary

The conjunction operation .and is binary.

theorem Cslib.Circuits.Boolean.Op.isBinary_or : or.IsBinary

The disjunction operation .or is binary.

theorem Cslib.Circuits.Boolean.Op.IsBinary.val_lt_two {op : Op} (h : op.IsBinary) (s : Fin (signature.Arity op)) : ↑s < 2

The arguments of a binary operation are numbered 0 and 1.

theorem Cslib.Circuits.Boolean.Op.IsBinary.eq_or_eq {op : Op} (h : op.IsBinary) {s t : Fin (signature.Arity op)} (hst : s ≠ t) (u : Fin (signature.Arity op)) : u = s ∨ u = t

Two different arguments of a binary operation are all of its arguments.

def Cslib.Circuits.Boolean.binaryCost : Op → ℕ

The cost function charging one for each AND and OR gate and nothing for negations and constants. Its counterparts for the other bases are Monotone.binaryCost, its restriction to the monotone basis (Monotone.binaryCost_toDeMorgan), and Unbounded.andOrCost, which also charges the constants of the unbounded fan-in basis, its AND and OR gates of no arguments.

@[simp]

theorem Cslib.Circuits.Boolean.binaryCost_and : binaryCost Op.and = 1

A conjunction gate has binary cost 1.

@[simp]

theorem Cslib.Circuits.Boolean.binaryCost_or : binaryCost Op.or = 1

A disjunction gate has binary cost 1.

@[simp]

theorem Cslib.Circuits.Boolean.binaryCost_not : binaryCost Op.not = 0

A negation gate has binary cost 0.

@[simp]

theorem Cslib.Circuits.Boolean.binaryCost_const (b : Bool) : binaryCost (Op.const b) = 0

A constant gate has binary cost 0.

theorem Cslib.Circuits.Boolean.binaryCost_le_one (op : Op) : binaryCost op ≤ 1

Every De Morgan operation has binary cost at most 1.

theorem Cslib.Circuits.Boolean.binaryCost_eq_ite (op : Op) : binaryCost op = if op.IsBinary then 1 else 0

The binary cost of an operation is 1 if it is binary and 0 otherwise.

theorem Cslib.Circuits.Boolean.arity_le_one_add_binaryCost (op : Op) : signature.Arity op ≤ 1 + binaryCost op

Every operation in the De Morgan basis has arity at most 1 + binaryCost op: constants have arity 0, negations have arity 1, and binary AND/OR gates have arity 2 = 1 + 1.

theorem Cslib.Circuits.Program.cost_binaryCost_le {n g : ℕ} (p : Program Boolean.signature n g) : p.cost Boolean.binaryCost ≤ g

The number of binary gates of a program is at most its number of gates.

theorem Cslib.Circuits.Program.card_biUnion_wireSupport_le_cost_binaryCost {n g : ℕ} (p : Program Boolean.signature n g) (frontier : Finset (Wire n g)) : (frontier.biUnion p.wireSupport).card ≤ frontier.card + p.cost Boolean.binaryCost

In a De Morgan program, the number of inputs supporting a frontier of wires is at most the size of the frontier plus the number of binary (AND/OR) gates in the program.

theorem Cslib.Circuits.Circuit.card_inputSupport_le_cost_binaryCost {n m : ℕ} (c : Circuit Boolean.signature n m) : c.inputSupport.card ≤ m + c.program.cost Boolean.binaryCost

A De Morgan circuit with m outputs has at most m + c.program.cost binaryCost supporting inputs, since only binary AND and OR gates increase the number of reachable inputs.

theorem Cslib.Circuits.Circuit.essential_le_cost_binaryCost {n m : ℕ} (c : Circuit Boolean.signature n m) {target : (Fin n → Bool) → Fin m → Bool} {selected : Finset (Fin n)} (hc : c.Computes Boolean.interpretation target) (h : ∀ k ∈ selected, EssentialAt target k) : selected.card ≤ m + c.program.cost Boolean.binaryCost

If a De Morgan circuit computes target and every coordinate in selected is essential to target, then selected.card ≤ m + c.program.cost binaryCost.

theorem Cslib.Circuits.Program.cost_binaryCost_eq_iff_forall_isBinary {n g : ℕ} {p : Program Boolean.signature n g} : p.cost Boolean.binaryCost = g ↔ ∀ (k : Fin g), Boolean.Op.IsBinary (p.lines k).op

A De Morgan program has binaryCost equal to its gate count g if and only if every gate in the program is a binary AND or OR gate.

theorem Cslib.Circuits.Circuit.cost_binaryCost_eq_size_of_size_le {n : ℕ} {c : Circuit Boolean.signature n 1} (hsupp : n ≤ c.inputSupport.card) (hsize : c.size + 1 ≤ n) : c.program.cost Boolean.binaryCost = c.size ∧ c.size = n - 1 ∧ ∀ (k : Fin c.size), Boolean.Op.IsBinary (c.program.lines k).op

In a one-output De Morgan circuit whose input support has size at least n, if c.size + 1 ≤ n then c has size n - 1, binary cost n - 1, and every gate of c is a binary AND or OR gate.