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.Realizable — whether a function is computed by some circuit over a basis
• Circuit.sizeComplexityWithTop — generic minimum size, with ⊤ for unrealizable functions
• Circuit.sizeComplexity — natural-valued minimum size over a complete basis

Main results

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

@[reducible, inline]

abbrev Complexity.BitString (n : ℕ) : Type

A BitString of length n.

Equations

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

@[reducible, inline]

abbrev Complexity.BoolFunFamily : Type

A family of Boolean functions indexed by input length N.

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

Equations

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

inductive Complexity.Arity : Type

Arity constraint for operations in a basis.

• unbounded : Arity

  Any number of inputs is allowed.

• exactly (k : ℕ) : Arity

  Exactly k inputs are required.

• upto (k : ℕ) : Arity

  At most k inputs are allowed.

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

Equations

• One or more equations did not get rendered due to their size.
• Complexity.instReprArity.repr Complexity.Arity.unbounded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Arity.unbounded")).group prec✝

@[implicit_reducible]

instance Complexity.instReprArity : Repr Arity

Equations

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

@[implicit_reducible]

instance Complexity.instDecidableEqArity : DecidableEq Arity

Equations

• Complexity.instDecidableEqArity = Complexity.instDecidableEqArity.decEq

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

Equations

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

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

Whether n satisfies an arity constraint.

Equations

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

@[implicit_reducible]

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

Equations

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

structure Complexity.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 Complexity.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 basis operation this gate computes.

• fanIn : ℕ

  The number of inputs this gate reads.

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

  Proof that fanIn satisfies the arity constraint of op.

• inputs : Fin self.fanIn → Fin W

  The wire each of the gate's fanIn inputs is connected to.

• negated : Fin self.fanIn → Bool

  Per-input negation flag. Negations are free under this library's size convention.

def Complexity.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 Complexity.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 internal gates; gate i drives wire N + i.

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

  The output gates; output bit j is the value of gate outputs j.

• 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 Complexity.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 Complexity.Circuit.wireValue_of_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⟩

On primary input wires (index < N), wireValue is the corresponding input bit.

theorem Complexity.Circuit.wireValue_of_not_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 = (c.gates ⟨↑w - N, ⋯⟩).eval (c.wireValue input)

On internal gate wires (index ≥ N), wireValue is the evaluation of gate w − N on the values of its input wires.

@[irreducible]

def Complexity.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 Complexity.Circuit.wireDepth_of_lt {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 Complexity.Circuit.wireDepth_of_not_lt {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 Complexity.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 Complexity.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 Complexity.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 Complexity.Circuit.size {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] : Circuit B N M G → ℕ

The library's circuit size: internal gates plus output gates.

Primary input vertices are not counted, and the negation flags on gate inputs have zero cost. Some texts instead count input vertices and explicit NOT gates; those conventions agree only up to additive/linear overhead, not on exact size bounds.

Equations

• x✝.size = G + M

class Complexity.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

  Every function BitString N → BitString M is the evaluation of some circuit over B.

theorem Complexity.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.

def Complexity.Circuit.Realizable {N : ℕ} [NeZero N] (B : Basis) (f : BitString N → Bool) : Prop

A Boolean function is realizable over B when some single-output circuit over B computes it.

Equations

• Complexity.Circuit.Realizable B f = ∃ (G : ℕ) (c : Complexity.Circuit B N 1 G), (fun (x : Complexity.BitString N) => c.eval x 0) = f

def Complexity.Circuit.realizationSizes {N : ℕ} [NeZero N] (B : Basis) (f : BitString N → Bool) : Set ℕ

Sizes of all single-output circuits over B that realize f.

Equations

• Complexity.Circuit.realizationSizes B f = {s : ℕ | ∃ (G : ℕ) (c : Complexity.Circuit B N 1 G), c.size = s ∧ (fun (x : Complexity.BitString N) => c.eval x 0) = f}

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

The minimum circuit size over an arbitrary basis, as an extended natural.

A single-output circuit Circuit B N 1 G has size G + 1. The value is ⊤ exactly when no circuit over B computes f; thus an unrealizable function cannot be confused with a zero-size function.

Equations

• Complexity.Circuit.sizeComplexityWithTop B f = sInf ((fun (s : ℕ) => ↑s) '' Complexity.Circuit.realizationSizes B f)

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

The minimum circuit size over a complete basis B computing f.

This natural-valued interface requires completeness so that the set of realizing circuits is nonempty. Use sizeComplexityWithTop when the basis may be incomplete.

Equations

• Complexity.Circuit.sizeComplexity B f = sInf (Complexity.Circuit.realizationSizes B f)

theorem Complexity.Circuit.sizeComplexityWithTop_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) : sizeComplexityWithTop B f ≤ ↑c.size

Any circuit computing f gives an upper bound on the generic extended size complexity.

theorem Complexity.Circuit.sizeComplexityWithTop_eq_top_iff {B : Basis} {N : ℕ} [NeZero N] (f : BitString N → Bool) : sizeComplexityWithTop B f = ⊤ ↔ ¬Realizable B f

Generic size complexity is infinite exactly for functions that cannot be realized over the chosen basis.

theorem Complexity.Circuit.sizeComplexityWithTop_ne_top_iff {B : Basis} {N : ℕ} [NeZero N] (f : BitString N → Bool) : sizeComplexityWithTop B f ≠ ⊤ ↔ Realizable B f

Generic size complexity is finite exactly for realizable functions.

theorem Complexity.Circuit.sizeComplexityWithTop_witness {B : Basis} {N : ℕ} [NeZero N] (f : BitString N → Bool) (hfinite : sizeComplexityWithTop B f ≠ ⊤) : ∃ (G : ℕ) (c : Circuit B N 1 G), ↑c.size = sizeComplexityWithTop B f ∧ (fun (x : BitString N) => c.eval x 0) = f

Whenever the generic size complexity is finite, a circuit realizes its minimum value.

theorem Complexity.Circuit.sizeComplexityWithTop_eq_coe {B : Basis} {N : ℕ} [NeZero N] [CompleteBasis B] (f : BitString N → Bool) : sizeComplexityWithTop B f = ↑(sizeComplexity B f)

Over a complete basis, the generic extended measure agrees with the natural-valued minimum.

theorem Complexity.Circuit.sizeComplexity_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 Complexity.Circuit.sizeComplexity_le {B : Basis} {N : ℕ} [NeZero N] [CompleteBasis B] {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 Complexity.Circuit.sizeComplexity_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.