Boolean Circuit Complexity

This file establishes the circuit size complexity measure for Boolean functions over a basis. It re-exports the bases of Complexitylib.Circuits.Basis.Defs and the typed circuits of Complexitylib.Circuits.Typed.Defs, so importing it provides the whole circuit model.

Main definitions

• Circuit.Realizable — whether a function is computed by some circuit over a basis
• Circuit.realizationSizes — the sizes of the circuits over a basis that compute a function
• 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

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.