More bounds on circuit complexity

Bounds on the complexity of single functions and of several functions computed side by side.

The coordinate projections cost nothing, and they are the only functions computed without gates, since a circuit without gates outputs one of its inputs. Applying a unary or binary operation to functions costs at most their complexities plus the complexity of the operation on fresh inputs: compute the arguments, then feed them to a circuit for the operation. Computing m functions of the same inputs at once costs at most the sum of their complexities: the circuits are placed next to each other.

Main results

• Cslib.Circuits.complexity_single_proj, Cslib.Circuits.one_le_complexity_single: exactly the projections are computed without gates.
• Cslib.Circuits.complexity_single_unary_le, Cslib.Circuits.complexity_single_binary_le: applying an operation to functions costs at most their complexities plus its complexity on fresh inputs.
• Cslib.Circuits.ecomplexity_pi_le, Cslib.Circuits.complexity_pi_le: computing functions side by side costs at most the sum of their complexities.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

Single functions

@[simp]

theorem Cslib.Circuits.complexity_single_proj {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} [I.IsComplete] (i : Fin n) : complexity I (single fun (x : Fin n → U) => x i) = 0

The coordinate projections cost no gates.

theorem Cslib.Circuits.one_le_complexity_single {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} [I.IsComplete] {f : (Fin n → U) → U} (hf : ∀ (i : Fin n), f ≠ fun (x : Fin n → U) => x i) : 1 ≤ complexity I (single f)

A function that is not a coordinate projection needs a gate: circuits without gates compute projections.

theorem Cslib.Circuits.complexity_single_unary_le {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} [I.IsComplete] (op : U → U) (f : (Fin n → U) → U) : complexity I (single fun (x : Fin n → U) => op (f x)) ≤ complexity I (single f) + complexity I (single fun (y : Fin 1 → U) => op (y 0))

Applying a unary operation to an output costs at most the complexity of the operation on one input.

theorem Cslib.Circuits.complexity_single_binary_le {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} [I.IsComplete] (op : U → U → U) (f g : (Fin n → U) → U) : complexity I (single fun (x : Fin n → U) => op (f x) (g x)) ≤ complexity I (single f) + complexity I (single g) + complexity I (single fun (y : Fin 2 → U) => op (y 0) (y 1))

Combining two outputs by a binary operation costs at most the complexity of the operation on two inputs.

Several functions side by side

theorem Cslib.Circuits.ecomplexity_pi_le {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n m : ℕ} (f : Fin m → (Fin n → U) → U) : (ecomplexity I fun (x : Fin n → U) (i : Fin m) => f i x) ≤ ∑ i : Fin m, ecomplexity I (single (f i))

Computing m functions side by side costs at most the sum of their complexities.

theorem Cslib.Circuits.complexity_pi_le {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} [I.IsComplete] {m : ℕ} (f : Fin m → (Fin n → U) → U) : (complexity I fun (x : Fin n → U) (i : Fin m) => f i x) ≤ ∑ i : Fin m, complexity I (single (f i))

Computing m functions side by side costs at most the sum of their complexities.