Boolean Circuit Complexity

This file defines Boolean circuits parameterized by a basis of operations and establishes the circuit size complexity measure for Boolean functions.

Main definitions

• BitString — a string of bits of a specific length
• BoolFunFamily — a family of Boolean functions indexed by input length
• Basis — a basis of Boolean operations with arity constraints
• Circuit — an acyclic Boolean circuit (well-formedness by construction)
• CompleteBasis — typeclass for functionally complete bases
• Circuit.wireDepth — depth of a wire in the circuit DAG
• Circuit.outputDepth — depth of a single output gate
• Circuit.depth — depth of a (possibly multi-output) circuit
• Circuit.sizeComplexity — minimum circuit size computing a given function

Main results

• Circuit.size_complexity_pos — for complete bases, size complexity is positive

@[reducible, inline]

abbrev CircuitComplexity.BitString (n : ℕ) : Type

A BitString of length n.

Equations

• CircuitComplexity.BitString n = (Fin n → Bool)

@[reducible, inline]

abbrev CircuitComplexity.BoolFunFamily : Type

A family of Boolean functions indexed by input length N.

Each member maps N-bit strings to a single output bit.

Equations

• CircuitComplexity.BoolFunFamily = ((N : ℕ) → CircuitComplexity.BitString N → Bool)

inductive CircuitComplexity.Arity : Type

Arity constraint for operations in a basis.

• unbounded : Arity
• exactly (k : ℕ) : Arity
• upto (k : ℕ) : Arity

@[implicit_reducible]

instance CircuitComplexity.instReprArity : Repr Arity

Equations

• CircuitComplexity.instReprArity = { reprPrec := CircuitComplexity.instReprArity.repr }

def CircuitComplexity.instReprArity.repr : Arity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def CircuitComplexity.instDecidableEqArity.decEq (x✝ x✝¹ : Arity) : Decidable (x✝ = x✝¹)

Equations

• CircuitComplexity.instDecidableEqArity.decEq CircuitComplexity.Arity.unbounded CircuitComplexity.Arity.unbounded = isTrue ⋯
• CircuitComplexity.instDecidableEqArity.decEq CircuitComplexity.Arity.unbounded (CircuitComplexity.Arity.exactly k) = isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq CircuitComplexity.Arity.unbounded (CircuitComplexity.Arity.upto k) = isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq (CircuitComplexity.Arity.exactly k) CircuitComplexity.Arity.unbounded = isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq (CircuitComplexity.Arity.exactly a) (CircuitComplexity.Arity.exactly b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq (CircuitComplexity.Arity.exactly k) (CircuitComplexity.Arity.upto k_1) = isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq (CircuitComplexity.Arity.upto k) CircuitComplexity.Arity.unbounded = isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq (CircuitComplexity.Arity.upto k) (CircuitComplexity.Arity.exactly k_1) = isFalse ⋯
• CircuitComplexity.instDecidableEqArity.decEq (CircuitComplexity.Arity.upto a) (CircuitComplexity.Arity.upto b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CircuitComplexity.instDecidableEqArity : DecidableEq Arity

Equations

• CircuitComplexity.instDecidableEqArity = CircuitComplexity.instDecidableEqArity.decEq

def CircuitComplexity.Arity.satisfiedBy : Arity → ℕ → Prop

Whether n satisfies an arity constraint.

Equations

• CircuitComplexity.Arity.unbounded.satisfiedBy x✝ = True
• (CircuitComplexity.Arity.exactly k).satisfiedBy x✝ = (x✝ = k)
• (CircuitComplexity.Arity.upto k).satisfiedBy x✝ = (x✝ ≤ k)

@[implicit_reducible]

instance CircuitComplexity.instDecidableSatisfiedBy (a : Arity) (n : ℕ) : Decidable (a.satisfiedBy n)

Equations

• One or more equations did not get rendered due to their size.

structure CircuitComplexity.Basis : Type 1

A basis of Boolean operations.

Each operation has an arity constraint and an evaluation function that computes the output bit from any valid number of input bits.

• Op : Type

  The type of operations (e.g., AND, OR, NOT).

• arity : self.Op → Arity

  The arity constraint for each operation.

• eval (op : self.Op) (n : ℕ) : (self.arity op).satisfiedBy n → BitString n → Bool

  Evaluate an operation on n input bits, given that n satisfies the arity.

structure CircuitComplexity.Gate (B : Basis) (W : ℕ) : Type

A gate in a circuit over basis B with W wires available as inputs. The gate's fan-in must satisfy the arity constraint of its operation, and each input is wired to one of the W available wires.

• op : B.Op

  The operation computed by this gate.

• fanIn : ℕ

  The number of inputs (fan-in) of this gate.

• arityOk : (B.arity self.op).satisfiedBy self.fanIn

  Proof that the fan-in satisfies the operation's arity constraint.

• inputs : Fin self.fanIn → Fin W

  Wiring: each gate input is connected to one of the W available wires.

• negated : Fin self.fanIn → Bool

  Per-input negation flag. Negations are free in circuit complexity.

def CircuitComplexity.Gate.eval {B : Basis} {W : ℕ} (g : Gate B W) (wireVal : BitString W) : Bool

Evaluate a gate given a wire-value assignment.

Equations

• g.eval wireVal = B.eval g.op g.fanIn ⋯ fun (i : Fin g.fanIn) => g.negated i ^^ wireVal (g.inputs i)

structure CircuitComplexity.Circuit (B : Basis) (N M G : ℕ) [NeZero N] [NeZero M] : Type

A Boolean circuit over basis B with N inputs, M outputs, and G internal gates.

All gates reference wires from Fin (N + G). The acyclic field ensures that internal gate i only reads wires 0, …, N + i − 1, preventing cycles.

• gates : Fin G → Gate B (N + G)

  The G internal gates of the circuit.

• outputs : Fin M → Gate B (N + G)

  The M output gates of the circuit.

• acyclic (i : Fin G) (k : Fin (self.gates i).fanIn) : ↑((self.gates i).inputs k) < N + ↑i

  Acyclicity: internal gate i only reads wires 0, …, N + i − 1.

@[irreducible]

def CircuitComplexity.Circuit.wireValue {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) (w : Fin (N + G)) : Bool

Value of wire w when the circuit is fed input.

The first N wires carry the primary inputs. Wire N + i carries the output of internal gate i.

Equations

• One or more equations did not get rendered due to their size.

theorem CircuitComplexity.Circuit.wireValue_lt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) (w : Fin (N + G)) (h : ↑w < N) : c.wireValue input w = input ⟨↑w, h⟩

theorem CircuitComplexity.Circuit.wireValue_ge {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) (w : Fin (N + G)) (h : ¬↑w < N) : c.wireValue input w = (c.gates ⟨↑w - N, ⋯⟩).eval (c.wireValue input)

@[irreducible]

def CircuitComplexity.Circuit.wireDepth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (w : Fin (N + G)) : ℕ

Depth of wire w in the circuit DAG.

Primary inputs have depth 0. Wire N + i (internal gate i) has depth 1 + max over input wires.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CircuitComplexity.Circuit.inputWireDepth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (w : Fin (N + G)) (h : ↑w < N) : c.wireDepth w = 0

Primary input wires (index < N) have depth 0.

theorem CircuitComplexity.Circuit.gateWireDepth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (w : Fin (N + G)) (h : ¬↑w < N) : c.wireDepth w = 1 + Fin.foldl (c.gates ⟨↑w - N, ⋯⟩).fanIn (fun (acc : ℕ) (k : Fin (c.gates ⟨↑w - N, ⋯⟩).fanIn) => max acc (c.wireDepth ((c.gates ⟨↑w - N, ⋯⟩).inputs k))) 0

Internal gate wires (index ≥ N) have depth 1 + max over their input wires. Unfolds one step of wireDepth for the gate case.

def CircuitComplexity.Circuit.outputDepth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (j : Fin M) : ℕ

Depth contributed by a single output gate: one layer for the gate itself plus the maximum wireDepth of its inputs. Always ≥ 1.

Equations

• c.outputDepth j = 1 + Fin.foldl (c.outputs j).fanIn (fun (acc : ℕ) (k : Fin (c.outputs j).fanIn) => max acc (c.wireDepth ((c.outputs j).inputs k))) 0

def CircuitComplexity.Circuit.depth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : ℕ

Depth of a circuit: the maximum outputDepth over all output gates.

Equations

• c.depth = Fin.foldl M (fun (acc : ℕ) (j : Fin M) => max acc (c.outputDepth j)) 0

def CircuitComplexity.Circuit.eval {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) : BitString M

Evaluate a circuit: map an N-bit input to an M-bit output.

Equations

• c.eval input j = (c.outputs j).eval (c.wireValue input)

def CircuitComplexity.Circuit.size {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : ℕ

The size of a circuit is its total number of gates (internal + output).

Equations

• c.size = G + M + (c.outputs 0).fanIn * 0

class CircuitComplexity.CompleteBasis (B : Basis) : Prop

A basis is complete if every Boolean function can be computed by some circuit over it.

• complete {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) : ∃ (G : ℕ) (c : Circuit B N M G), c.eval = f

theorem CircuitComplexity.CompleteBasis.of_simulation (B₁ B₂ : Basis) [CompleteBasis B₁] (sim : ∀ {N M G : ℕ} [inst : NeZero N] [inst_1 : NeZero M] (c : Circuit B₁ N M G), ∃ (G' : ℕ) (c' : Circuit B₂ N M G'), c'.eval = c.eval) : CompleteBasis B₂

If every circuit over B₁ can be simulated by a circuit over B₂ (possibly with a different number of internal gates), then completeness of B₁ implies completeness of B₂.

This is the generic tool for proving new bases complete: show you can compile each gate of a known-complete basis into a subcircuit of the new basis.

noncomputable def CircuitComplexity.Circuit.sizeComplexity {N : ℕ} [NeZero N] (B : Basis) (f : BitString N → Bool) : ℕ

The minimum circuit size over basis B computing a Boolean function f.

A single-output circuit Circuit B N 1 G computes f when (fun x => (c.eval x) 0) = f. The size is G + 1 (internal gates + output gate). Returns 0 if no circuit over B computes f.

Equations

• One or more equations did not get rendered due to their size.

theorem CircuitComplexity.Circuit.size_complexity_pos {B : Basis} {N : ℕ} [NeZero N] [CompleteBasis B] (f : BitString N → Bool) : 0 < sizeComplexity B f

For a complete basis, circuit size complexity is always positive.

theorem CircuitComplexity.Circuit.size_complexity_le {B : Basis} {N : ℕ} [NeZero N] {G : ℕ} (c : Circuit B N 1 G) (f : BitString N → Bool) (hf : (fun (x : BitString N) => c.eval x 0) = f) : sizeComplexity B f ≤ c.size

Any circuit computing f has size at least sizeComplexity B f.

theorem CircuitComplexity.Circuit.size_complexity_witness {B : Basis} {N : ℕ} [NeZero N] [CompleteBasis B] (f : BitString N → Bool) : ∃ (G : ℕ) (c : Circuit B N 1 G), c.size = sizeComplexity B f ∧ (fun (x : BitString N) => c.eval x 0) = f

For a complete basis, sizeComplexity is realized by some circuit.