Documentation

Complexity.Computability.Circuit.InnerSize

Inner gates #

A gate of arity zero is a constant: like an input, it is a leaf of the circuit. The inner gates of a program are its gates of positive arity, and the inner size of a circuit counts them. A lower bound that holds over every basis can only count inner gates, since every value of the alphabet may be a constant gate of the basis.

Main definitions #

Main results #

source
def Cslib.Circuits.Program.innerGates {σ : Signature} {n g : ℕ} (p : Program σ n g) :
Finset (Fin g)

The inner gates of a program: those of positive arity. A gate of arity zero is a constant, a leaf of the circuit like an input.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Program.mem_innerGates {σ : Signature} {n g : ℕ} {p : Program σ n g} {k : Fin g} :
    k ∈ p.innerGates ↔ σ.Arity (p.lines k).op ≠ 0

    A gate k belongs to p.innerGates if and only if its operation has nonzero arity.

    source
    def Cslib.Circuits.Circuit.innerSize {σ : Signature} {n m : ℕ} (c : Circuit σ n m) :
    ℕ

    The inner size of a circuit: the number of its gates of positive arity. Constant gates are free. For arithmetic circuits this counts the additions and multiplications.

    Instances For
      source
      theorem Cslib.Circuits.Circuit.innerSize_le_size {σ : Signature} {n m : ℕ} (c : Circuit σ n m) :
      c.innerSize ≤ c.size

      Constant gates are free: the inner size is at most the size.

      source
      theorem Cslib.Circuits.Circuit.innerSize_eq_zero_of_fanInAtMost_zero {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (h : c.FanInAtMost 0) :
      c.innerSize = 0

      Without arguments every gate is a constant, so a circuit of fan-in zero has inner size zero.

      source
      @[simp]
      theorem Cslib.Circuits.Circuit.innerSize_wiring {σ : Signature} {n m : ℕ} (select : Fin m → Fin n) :
      (wiring σ select).innerSize = 0

      A pure input-wiring circuit has 0 inner gates.

      source
      theorem Cslib.Circuits.Circuit.innerSize_eq_size_of_forall_arity_ne_zero {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (h : ∀ (op : σ.Op), σ.Arity op ≠ 0) :
      c.innerSize = c.size

      In a signature without nullary operations, every gate has positive arity, so the inner size is the full gate count.

      source
      theorem Cslib.Circuits.Program.fanInAtMost_of_forall_arity_le {σ : Signature} {n g : ℕ} (p : Program σ n g) {r : ℕ} (h : ∀ (op : σ.Op), σ.Arity op ≤ r) :
      p.FanInAtMost r

      If every operation symbol has arity at most r, every program over the signature has fan-in at most r.

      source
      theorem Cslib.Circuits.Circuit.fanInAtMost_of_forall_arity_le {σ : Signature} {n m : ℕ} (c : Circuit σ n m) {r : ℕ} (h : ∀ (op : σ.Op), σ.Arity op ≤ r) :
      c.FanInAtMost r

      If every operation symbol has arity at most r, every circuit over the signature has fan-in at most r.

      source
      theorem Cslib.Circuits.Circuit.fanInAtMost_fullSignature {n m : ℕ} {U : Type u_1} {r : ℕ} (c : Circuit (fullSignature r U) n m) :
      c.FanInAtMost r

      Every circuit over the full basis of arity r has fan-in at most r.