Documentation

Complexity.Computability.Circuit.Complexity

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 #

References #

Single functions #

source
theorem Cslib.Circuits.Circuit.computesOn_single_iff {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} {c : Circuit σ n 1} {S : Set (Fin n → U)} {f : (Fin n → U) → U} :
c.ComputesOn I S (single f) ↔ ∀ x ∈ S, c.eval I x 0 = f x

A one-output circuit computes single f on S exactly when its output 0 agrees with f on S.

source
theorem Cslib.Circuits.Circuit.computes_single_iff {σ : Signature} {U : Type u_1} {I : Interpretation σ U} {n : ℕ} {c : Circuit σ n 1} {f : (Fin n → U) → U} :
c.Computes I (single f) ↔ ∀ (x : Fin n → U), c.eval I x 0 = f x

A one-output circuit computes single f exactly when its output 0 agrees with f on every input.

source
@[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.

source
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.

source
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.

source
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 #

source
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.

source
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.