Counting functions computed by finite circuits

For a finite signature, only finitely many functions can be computed with a fixed gate budget, even when the carrier is infinite. We enumerate the programs of each size together with an output wire and collect the scalar functions they compute, so that computableFunctions I n s is the finite set of functions whose ecomplexity is at most s. Semantic equality and normalization use classical reasoning; the syntax enumeration is computable.

After merging gates that compute the same function, a circuit with g gates has g! distinct labeled presentations. This factorial correction sharpens the count used in Shannon's lower bound. The main bound accepts any uniform bound on the number of lines; card_computableFunctions_mul_factorial_le_of_arity_le specializes it to operation arities.

noncomputable def Cslib.Circuits.computableFunctions {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n s : ℕ) : Finset ((Fin n → U) → U)

Scalar functions computable with at most s gates. Enumerating the programs of each size with an output wire makes this set finite without requiring a finite carrier.

Equations

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

@[simp]

theorem Cslib.Circuits.mem_computableFunctions {σ : Signature} [Fintype σ.Op] {U : Type u} {I : Interpretation σ U} {n s : ℕ} {f : (Fin n → U) → U} : f ∈ computableFunctions I n s ↔ ∃ (c : Circuit σ n 1), (c.Computes I fun (x : Fin n → U) (x_1 : Fin 1) => f x) ∧ c.size ≤ s

theorem Cslib.Circuits.mem_computableFunctions_iff_ecomplexity_le {σ : Signature} [Fintype σ.Op] {U : Type u} {I : Interpretation σ U} {n s : ℕ} {f : (Fin n → U) → U} : f ∈ computableFunctions I n s ↔ (ecomplexity I fun (x : Fin n → U) (x_1 : Fin 1) => f x) ≤ ↑s

The functions computable with at most s gates are those of complexity at most s.

noncomputable def Cslib.Circuits.irredundantFunctions {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n g : ℕ) : Finset ((Fin n → U) → U)

Functions computed at an output wire of a program whose g gates compute pairwise distinct functions. Permuting the gates of such a program, ignoring their order, gives g! distinct gate lists; this is the factorial saving in the counting bound.

Equations

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

@[simp]

theorem Cslib.Circuits.mem_irredundantFunctions {σ : Signature} [Fintype σ.Op] {U : Type u} {I : Interpretation σ U} {n g : ℕ} {f : (Fin n → U) → U} : f ∈ irredundantFunctions I n g ↔ ∃ (c : Circuit σ n 1), (c.Computes I fun (x : Fin n → U) (x_1 : Fin 1) => f x) ∧ c.Irredundant I ∧ c.size = g

theorem Cslib.Circuits.card_irredundantFunctions_mul_factorial_le {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n g : ℕ) : (irredundantFunctions I n g).card * g.factorial ≤ Fintype.card (Line σ n g) ^ g * (n + g)

Distinct functions and permutations of their irredundant gates give distinct presentations.

theorem Cslib.Circuits.card_computableFunctions_le_sum {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n s : ℕ) : (computableFunctions I n s).card ≤ ∑ g ∈ Finset.range (s + 1), (irredundantFunctions I n g).card

Normalizing a circuit with at most s gates leaves an irredundant program with at most s gates computing the same function.

theorem Cslib.Circuits.card_computableFunctions_mul_factorial_le {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n s B : ℕ) (hB : s ≤ B) (hlines : ∀ g ≤ s, Fintype.card (Line σ n g) ≤ B) : (computableFunctions I n s).card * s.factorial ≤ (s + 1) * B ^ s * (n + s)

Bound the number of computable functions using a uniform line count B. The condition s ≤ B absorbs the extra factorial factors from circuits with fewer than s gates.

theorem Cslib.Circuits.card_computableFunctions_mul_factorial_le_of_arity_le {σ : Signature} [Fintype σ.Op] {U : Type u} (I : Interpretation σ U) (n s r : ℕ) (arity_le : ∀ (op : σ.Op), σ.Arity op ≤ r) : (computableFunctions I n s).card * s.factorial ≤ (s + 1) * max s (Fintype.card σ.Op * (n + s + 1) ^ r) ^ s * (n + s)

A cardinality bound for any finite signature with bounded arities. The maximum also covers empty signatures and signatures containing only nullary operations.