The Boolean basis with unbounded fan-in

The basis of AC⁰: negation, and conjunctions and disjunctions of any number of arguments. Circuits and formulas over this basis of constant depth are the setting of Håstad's lower bound for parity. The conjunction and the disjunction of no arguments are the constants true and false.

Adding one gate of every arity, computing a given family of Boolean functions g, gives the bases of TC⁰ (majority gates) and AC⁰[q] (MOD_q gates): extSignature and extInterpretation g, into which the unbounded fan-in basis maps by toExt.

Main definitions

• Cslib.Circuits.Boolean.Unbounded.signature: negation, and conjunction and disjunction of every arity.
• Cslib.Circuits.Boolean.Unbounded.interpretation: their Boolean meaning.
• Cslib.Circuits.Boolean.Unbounded.andOrCost: the costs of the AND/OR depth, in which negations are free.
• Cslib.Circuits.Boolean.Unbounded.deMorganToUnbounded: the De Morgan basis inside it.
• Cslib.Circuits.Boolean.Unbounded.extSignature, Cslib.Circuits.Boolean.Unbounded.extInterpretation: the basis with one extra gate of every arity.

Main results

• Cslib.Circuits.Boolean.Unbounded.interpretation_of_op_eq_not, Cslib.Circuits.Boolean.Unbounded.interpretation_of_op_eq_and, Cslib.Circuits.Boolean.Unbounded.interpretation_of_op_eq_or: the values of the gates of a program.
• Cslib.Circuits.Boolean.Unbounded.cost_andOrCost_eq_card: the AND/OR cost of a program is its number of conjunctions and disjunctions.
• Cslib.Circuits.Boolean.Unbounded.preserves_deMorganToUnbounded: the De Morgan basis embeds with its meaning.

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

Negation, and conjunction and disjunction of m arguments for every m.

• not : Op

  Negation.

• and (m : ℕ) : Op

  Conjunction of m arguments.

• or (m : ℕ) : Op

  Disjunction of m arguments.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Unbounded.instDecidableEqOp : DecidableEq Op

def Cslib.Circuits.Boolean.Unbounded.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

@[reducible, inline]

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

The arity of an operation.

@[reducible, inline]

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

The signature of negation and of conjunction and disjunction of unbounded fan-in. It is reducible, so that case analysis on its operations sees their arities.

def Cslib.Circuits.Boolean.Unbounded.interpretation : Interpretation signature Bool

The Boolean meaning of the operations.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.interpretation_not (x : Fin 1 → Bool) : interpretation Op.not x = !x 0

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.interpretation_and (m : ℕ) (x : Fin m → Bool) : interpretation (Op.and m) x = decide (∀ (j : Fin m), x j = true)

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.interpretation_or (m : ℕ) (x : Fin m → Bool) : interpretation (Op.or m) x = decide (∃ (j : Fin m), x j = true)

theorem Cslib.Circuits.Boolean.Unbounded.interpretation_of_op_eq_not {n g : ℕ} {l : Line signature n g} (h : l.op = Op.not) (v : Wire n g → Bool) : (interpretation l.op fun (a : Fin (signature.Arity l.op)) => v (l.wires a)) = !v (l.wires ⟨0, ⋯⟩)

A negation gate negates its argument.

theorem Cslib.Circuits.Boolean.Unbounded.interpretation_of_op_eq_and {n g : ℕ} {l : Line signature n g} {m : ℕ} (h : l.op = Op.and m) (v : Wire n g → Bool) : (interpretation l.op fun (a : Fin (signature.Arity l.op)) => v (l.wires a)) = true ↔ ∀ (a : Fin (signature.Arity l.op)), v (l.wires a) = true

A conjunction gate is true when all its arguments are.

theorem Cslib.Circuits.Boolean.Unbounded.interpretation_of_op_eq_or {n g : ℕ} {l : Line signature n g} {m : ℕ} (h : l.op = Op.or m) (v : Wire n g → Bool) : (interpretation l.op fun (a : Fin (signature.Arity l.op)) => v (l.wires a)) = true ↔ ∃ (a : Fin (signature.Arity l.op)), v (l.wires a) = true

A disjunction gate is true when one of its arguments is.

def Cslib.Circuits.Boolean.Unbounded.andOrCost : Op → ℕ

The cost of an operation in the AND/OR depth: negations are free. With these costs, Circuit.depthWith is the largest number of conjunctions and disjunctions on a path, the usual depth of AC⁰ circuits, in which negations sit at the inputs.

This is the counterpart of Boolean.binaryCost and Monotone.binaryCost for the bases of fan-in two, which charge one for AND and OR and nothing for negations and constants. It is not their transport along deMorganToUnbounded: this basis has no constants, and the De Morgan constants become the conjunction and the disjunction of no arguments, which cost one here.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.andOrCost_not : andOrCost Op.not = 0

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.andOrCost_and (m : ℕ) : andOrCost (Op.and m) = 1

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.andOrCost_or (m : ℕ) : andOrCost (Op.or m) = 1

theorem Cslib.Circuits.Boolean.Unbounded.andOrCost_le_one (op : Op) : andOrCost op ≤ 1

theorem Cslib.Circuits.Boolean.Unbounded.andOrCost_eq_one_of_ne_not {op : Op} (hop : op ≠ Op.not) : andOrCost op = 1

Conjunctions and disjunctions cost one in the AND/OR depth.

theorem Cslib.Circuits.Boolean.Unbounded.cost_andOrCost_eq_card {n g : ℕ} (p : Program signature n g) : p.cost andOrCost = {k : Fin g | (p.lines k).op ≠ Op.not}.card

The AND/OR cost of a program is its number of conjunctions and disjunctions.

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

The operations of the unbounded fan-in basis, and one extra gate of every arity.

• ac (op : Op) : ExtOp

  An operation of the unbounded fan-in basis.

• gate (m : ℕ) : ExtOp

  The extra gate of m arguments.

def Cslib.Circuits.Boolean.Unbounded.instDecidableEqExtOp.decEq (x✝ x✝¹ : ExtOp) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Unbounded.instDecidableEqExtOp : DecidableEq ExtOp

@[reducible, inline]

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

The arity of an operation of the extended basis.

@[reducible, inline]

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

The signature of the unbounded fan-in basis with one extra gate of every arity. It is reducible, so that case analysis on its operations sees their arities.

def Cslib.Circuits.Boolean.Unbounded.extInterpretation (g : (m : ℕ) → BooleanFunction m) : Interpretation extSignature Bool

The Boolean meaning of the extended basis, with the extra gate of m arguments computing g m.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.extInterpretation_ac (g : (m : ℕ) → BooleanFunction m) (op : Op) (x : Fin op.arity → Bool) : extInterpretation g (ExtOp.ac op) x = interpretation op x

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.extInterpretation_gate (g : (m : ℕ) → BooleanFunction m) (m : ℕ) (x : Fin m → Bool) : extInterpretation g (ExtOp.gate m) x = g m x

def Cslib.Circuits.Boolean.Unbounded.toExt : signature.Hom extSignature

The unbounded fan-in basis inside its extension.

instance Cslib.Circuits.Boolean.Unbounded.preserves_toExt (g : (m : ℕ) → BooleanFunction m) : toExt.Preserves interpretation (extInterpretation g)

def Cslib.Circuits.Boolean.Unbounded.deMorganOp : Boolean.Op → Op

The operations of the De Morgan basis as operations of the unbounded fan-in basis: the constants as the conjunction and disjunction of nothing.

def Cslib.Circuits.Boolean.Unbounded.deMorganToUnbounded : Boolean.signature.Hom signature

The De Morgan basis inside the unbounded fan-in basis.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.deMorganToUnbounded_apply (op : Boolean.Op) : deMorganToUnbounded op = deMorganOp op

instance Cslib.Circuits.Boolean.Unbounded.preserves_deMorganToUnbounded : deMorganToUnbounded.Preserves Boolean.interpretation interpretation