Documentation

Complexity.Computability.Circuit.Pi

Circuits side by side #

Circuit.pi cs runs the single-output circuits cs j on the same inputs and lists their outputs (Circuit.eval_pi); its size is the sum of their sizes (Circuit.size_pi) and its depth the largest of their depths (Circuit.depth_pi_le), also with costs (Circuit.depthWith_pi_le).

Main definitions #

Main results #

source
def Cslib.Circuits.Circuit.pi {σ : Signature} {n m : ℕ} :
(Fin m → Circuit σ n 1) → Circuit σ n m

The single-output circuits cs j on shared inputs, with output j the output of cs j.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Circuit.eval_pi {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} {m : ℕ} (cs : Fin m → Circuit σ n 1) (x : Fin n → U) :
    (pi cs).eval I x = fun (j : Fin m) => (cs j).eval I x 0

    Output j of pi cs is the output of cs j.

    source
    @[simp]
    theorem Cslib.Circuits.Circuit.size_pi {σ : Signature} {n m : ℕ} (cs : Fin m → Circuit σ n 1) :
    (pi cs).size = ∑ j : Fin m, (cs j).size

    The size of pi cs is the sum of the sizes.

    source
    theorem Cslib.Circuits.Circuit.depthWith_pi_le {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) {m : ℕ} (cs : Fin m → Circuit σ n 1) {D : ℕ} (h : ∀ (j : Fin m), depthWith cost (cs j) ≤ D) :
    depthWith cost (pi cs) ≤ D

    With costs, the depth of pi cs is at most the largest depth.

    source
    def Cslib.Circuits.Circuit.oneGate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Fin n) :
    Circuit σ n 1

    The circuit of one gate: the operation op applied to the inputs args.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Circuit.eval_oneGate {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} (op : σ.Op) (args : Fin (σ.Arity op) → Fin n) (x : Fin n → U) (j : Fin 1) :
      (oneGate op args).eval I x j = I op fun (a : Fin (σ.Arity op)) => x (args a)
      source
      @[simp]
      theorem Cslib.Circuits.Circuit.size_oneGate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Fin n) :
      (oneGate op args).size = 1
      source
      @[simp]
      theorem Cslib.Circuits.Circuit.depthWith_oneGate {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) (op : σ.Op) (args : Fin (σ.Arity op) → Fin n) :
      depthWith cost (oneGate op args) = cost op

      With costs, one gate has the depth of its cost.

      source
      theorem Cslib.Circuits.Circuit.depth_pi_le {σ : Signature} {n m : ℕ} (cs : Fin m → Circuit σ n 1) {D : ℕ} (h : ∀ (j : Fin m), (cs j).depth ≤ D) :
      (pi cs).depth ≤ D

      The depth of pi cs is at most the largest depth.

      source
      @[simp]
      theorem Cslib.Circuits.Circuit.depth_oneGate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Fin n) :
      (oneGate op args).depth = 1

      One gate has depth one.