Circuit complexity

The complexity of a function f on a support S, written C^S(f), is the least number of gates in a circuit whose outputs agree with f on every input in S. The function may have several values, one for each output of the circuit, and nothing is asked of the circuit outside S, so C^S(f) depends only on the restriction of f to S. The complexity C(f) of f is its complexity on all inputs, and the complexity of f relative to a function g, in Cslib.Computability.Circuit.RelativeComplexity, is a complexity on the graph of g.

Over an arbitrary signature and interpretation some functions have no circuit at all, so ecomplexityOn I S f takes values in ℕ∞, with ⊤ when no circuit computes f on S. Over a complete basis, one over which every function has a circuit, the complexity is a natural number, complexityOn I S f, and this is the notion of interest in the Boolean case.

Support complexity obeys a small calculus from which the rules for complexity and relative complexity follow. It grows with the support and ignores the function outside the support. Wiring, which only selects, permutes, or duplicates inputs, costs nothing. The composite g ∘ f costs at most the complexity of f on S plus that of g on the image of S, and computing two functions side by side costs at most the sum of their complexities.

See [Jukna, Chapter 1][Jukna2012] for the Boolean case.

References

• [Stasys Jukna, Boolean Function Complexity: Advances and Frontiers][Jukna2012]

class Cslib.Circuits.Interpretation.IsComplete {σ : Signature} {U : Type u} (I : Interpretation σ U) : Prop

Following [Jukna, Section 1.1][Jukna2012], a basis is complete when every single-valued function, on every number of inputs, is computed by some circuit over it. Circuits here have no constant inputs, so this includes the constants, which is why NAND alone is not complete in this sense. Functions with several values then have circuits too, built by running circuits for their values side by side.

• exists_computes_single {n : ℕ} (f : (Fin n → U) → U) : ∃ (c : Circuit σ n 1), c.Computes I fun (x : Fin n → U) (x_1 : Fin 1) => f x

  Every single-valued function has a circuit.

theorem Cslib.Circuits.Interpretation.IsComplete.exists_computes {σ : Signature} {U : Type u} {I : Interpretation σ U} [I.IsComplete] {n m : ℕ} (f : (Fin n → U) → Fin m → U) : ∃ (c : Circuit σ n m), c.Computes I f

Over a complete basis every function, with any number of values, has a circuit.

noncomputable def Cslib.Circuits.ecomplexityOn {σ : Signature} {U : Type u} {n m : ℕ} (I : Interpretation σ U) (S : Set (Fin n → U)) (f : (Fin n → U) → Fin m → U) : ℕ∞

The complexity C^S(f) of f on the support S: the least size of a circuit computing f on S under I, or ⊤ if there is none.

Equations

• Cslib.Circuits.ecomplexityOn I S f = ⨅ (c : { c : Cslib.Circuits.Circuit σ n m // c.ComputesOn I S f }), ↑(↑c).size

noncomputable def Cslib.Circuits.ecomplexity {σ : Signature} {U : Type u} {n m : ℕ} (I : Interpretation σ U) (f : (Fin n → U) → Fin m → U) : ℕ∞

The complexity C(f) of f: its complexity on all inputs.

Equations

• Cslib.Circuits.ecomplexity I f = Cslib.Circuits.ecomplexityOn I Set.univ f

Complexity on a support

theorem Cslib.Circuits.ecomplexityOn_le_of_computesOn {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} (c : Circuit σ n m) (hc : c.ComputesOn I S f) : ecomplexityOn I S f ≤ ↑c.size

theorem Cslib.Circuits.ecomplexityOn_ne_top_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} : ecomplexityOn I S f ≠ ⊤ ↔ ∃ (c : Circuit σ n m), c.ComputesOn I S f

theorem Cslib.Circuits.exists_computesOn_size_eq_ecomplexityOn {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} (h : ∃ (c : Circuit σ n m), c.ComputesOn I S f) : ∃ (c : Circuit σ n m), c.ComputesOn I S f ∧ ↑c.size = ecomplexityOn I S f

When some circuit computes f on S, the least size is attained.

theorem Cslib.Circuits.ecomplexityOn_le_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} {k : ℕ} : ecomplexityOn I S f ≤ ↑k ↔ ∃ (c : Circuit σ n m), c.ComputesOn I S f ∧ c.size ≤ k

theorem Cslib.Circuits.ecomplexityOn_mono {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S T : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} (h : S ⊆ T) : ecomplexityOn I S f ≤ ecomplexityOn I T f

A larger support is harder to compute on.

theorem Cslib.Circuits.ecomplexityOn_congr {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f f' : (Fin n → U) → Fin m → U} (h : Set.EqOn f f' S) : ecomplexityOn I S f = ecomplexityOn I S f'

Complexity on a support depends only on the values of the function on the support.

theorem Cslib.Circuits.ecomplexityOn_le_ecomplexity {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} : ecomplexityOn I S f ≤ ecomplexity I f

@[simp]

theorem Cslib.Circuits.ecomplexityOn_wiring {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} (select : Fin m → Fin n) : (ecomplexityOn I S fun (x : Fin n → U) => x ∘ select) = 0

Selecting, permuting, or duplicating inputs costs nothing.

theorem Cslib.Circuits.ecomplexityOn_comp_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} (f : (Fin n → U) → Fin m → U) (g : (Fin m → U) → Fin p → U) : ecomplexityOn I S (g ∘ f) ≤ ecomplexityOn I S f + ecomplexityOn I (f '' S) g

The composition rule: computing g ∘ f on S costs at most computing f on S and then g on the values f takes there.

theorem Cslib.Circuits.ecomplexityOn_append_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin p → U) : (ecomplexityOn I S fun (x : Fin n → U) => Fin.append (f x) (g x)) ≤ ecomplexityOn I S f + ecomplexityOn I S g

The pairing rule: computing f and g side by side on S costs at most the sum of their complexities on S.

theorem Cslib.Circuits.ecomplexityOn_comp_wiring_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {S : Set (Fin p → U)} (select : Fin n → Fin p) (f : (Fin n → U) → Fin m → U) : (ecomplexityOn I S fun (x : Fin p → U) => f (x ∘ select)) ≤ ecomplexityOn I ((fun (x : Fin p → U) => x ∘ select) '' S) f

Reading the inputs through a wiring costs nothing beyond computing f on the rewired support.

theorem Cslib.Circuits.ecomplexityOn_wiring_comp_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} (select : Fin p → Fin m) (f : (Fin n → U) → Fin m → U) : (ecomplexityOn I S fun (x : Fin n → U) => f x ∘ select) ≤ ecomplexityOn I S f

Selecting, permuting, or duplicating the values of f costs nothing.

Complexity on all inputs

theorem Cslib.Circuits.ecomplexity_le_of_computes {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} (c : Circuit σ n m) (hc : c.Computes I f) : ecomplexity I f ≤ ↑c.size

theorem Cslib.Circuits.ecomplexity_ne_top_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} : ecomplexity I f ≠ ⊤ ↔ ∃ (c : Circuit σ n m), c.Computes I f

theorem Cslib.Circuits.exists_computes_size_eq_ecomplexity {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} (h : ∃ (c : Circuit σ n m), c.Computes I f) : ∃ (c : Circuit σ n m), c.Computes I f ∧ ↑c.size = ecomplexity I f

When some circuit computes f, the least size is attained.

theorem Cslib.Circuits.ecomplexity_le_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} {k : ℕ} : ecomplexity I f ≤ ↑k ↔ ∃ (c : Circuit σ n m), c.Computes I f ∧ c.size ≤ k

theorem Cslib.Circuits.ecomplexity_comp_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin m → U) → Fin p → U) : ecomplexity I (g ∘ f) ≤ ecomplexity I f + ecomplexity I g

theorem Cslib.Circuits.ecomplexity_append_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin p → U) : (ecomplexity I fun (x : Fin n → U) => Fin.append (f x) (g x)) ≤ ecomplexity I f + ecomplexity I g

theorem Cslib.Circuits.ecomplexity_le_ecomplexity_append_left {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin p → U) : ecomplexity I f ≤ ecomplexity I fun (x : Fin n → U) => Fin.append (f x) (g x)

Computing f alongside g is at least as hard as computing f.

theorem Cslib.Circuits.ecomplexity_le_ecomplexity_append_right {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin p → U) : ecomplexity I g ≤ ecomplexity I fun (x : Fin n → U) => Fin.append (f x) (g x)

Computing g alongside f is at least as hard as computing g.

theorem Cslib.Circuits.Synthesis.ecomplexity_le {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → U} {cost : ℕ} (h : Synthesis I (inputs n) {f} cost) : (ecomplexity I fun (x : Fin n → U) (x_1 : Fin 1) => f x) ≤ ↑cost

A synthesis bound on the input projections bounds the extended complexity.

Over a complete basis

theorem Cslib.Circuits.ecomplexityOn_ne_top {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} [I.IsComplete] : ecomplexityOn I S f ≠ ⊤

theorem Cslib.Circuits.ecomplexity_ne_top {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} [I.IsComplete] : ecomplexity I f ≠ ⊤

noncomputable def Cslib.Circuits.complexityOn {σ : Signature} {U : Type u} {n m : ℕ} (I : Interpretation σ U) [I.IsComplete] (S : Set (Fin n → U)) (f : (Fin n → U) → Fin m → U) : ℕ

The complexity C^S(f) of f on the support S over a complete basis, as a natural number.

Equations

• Cslib.Circuits.complexityOn I S f = WithTop.untop (Cslib.Circuits.ecomplexityOn I S f) ⋯

noncomputable def Cslib.Circuits.complexity {σ : Signature} {U : Type u} {n m : ℕ} (I : Interpretation σ U) [I.IsComplete] (f : (Fin n → U) → Fin m → U) : ℕ

The complexity C(f) of f over a complete basis, as a natural number.

Equations

• Cslib.Circuits.complexity I f = Cslib.Circuits.complexityOn I Set.univ f

@[simp]

theorem Cslib.Circuits.natCast_complexityOn {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} [I.IsComplete] : ↑(complexityOn I S f) = ecomplexityOn I S f

@[simp]

theorem Cslib.Circuits.natCast_complexity {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} [I.IsComplete] : ↑(complexity I f) = ecomplexity I f

theorem Cslib.Circuits.complexity_le_of_computes {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} [I.IsComplete] (c : Circuit σ n m) (hc : c.Computes I f) : complexity I f ≤ c.size

theorem Cslib.Circuits.le_size_of_le_complexity {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} {k : ℕ} [I.IsComplete] (h : k ≤ complexity I f) {c : Circuit σ n m} (hc : c.Computes I f) : k ≤ c.size

A lower bound on the complexity is a lower bound on the size of every circuit.

theorem Cslib.Circuits.exists_computes_size_eq_complexity {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} [I.IsComplete] : ∃ (c : Circuit σ n m), c.Computes I f ∧ c.size = complexity I f

Over a complete basis the least size is attained.

theorem Cslib.Circuits.complexity_le_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} {k : ℕ} [I.IsComplete] : complexity I f ≤ k ↔ ∃ (c : Circuit σ n m), c.Computes I f ∧ c.size ≤ k

theorem Cslib.Circuits.le_complexity_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} {k : ℕ} [I.IsComplete] : k ≤ complexity I f ↔ ∀ (c : Circuit σ n m), c.Computes I f → k ≤ c.size

Over a complete basis, lower bounds on complexity are exactly lower bounds on the size of every circuit.

theorem Cslib.Circuits.complexityOn_mono {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {S T : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} [I.IsComplete] (h : S ⊆ T) : complexityOn I S f ≤ complexityOn I T f

theorem Cslib.Circuits.complexityOn_comp_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin m → U) → Fin p → U) : complexityOn I S (g ∘ f) ≤ complexityOn I S f + complexityOn I (f '' S) g

theorem Cslib.Circuits.complexityOn_append_le {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {S : Set (Fin n → U)} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin p → U) : (complexityOn I S fun (x : Fin n → U) => Fin.append (f x) (g x)) ≤ complexityOn I S f + complexityOn I S g

theorem Cslib.Circuits.Synthesis.complexity_le {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} [I.IsComplete] {f : (Fin n → U) → U} {cost : ℕ} (h : Synthesis I (inputs n) {f} cost) : (complexity I fun (x : Fin n → U) (x_1 : Fin 1) => f x) ≤ cost

A synthesis bound on the input projections bounds the complexity.