Documentation

Cslib.Computability.Circuit.Finite

Finite circuit syntax #

A finite signature gives finitely many lines and programs of each fixed size. Their cardinalities count syntax and are independent of any interpretation or carrier. Line.card_le bounds the number of lines when all operation arities are bounded. For the full basis on a carrier of size q, there are q ^ (q ^ k) operation tables and q constants. Line.card_full counts their possible arguments separately.

source
instance Cslib.Circuits.Line.instFinite {σ : Signature} [Finite σ.Op] (n g : ℕ) :
Finite (Line σ n g)
source
instance Cslib.Circuits.Program.instFinite {σ : Signature} [Finite σ.Op] (n g : ℕ) :
Finite (Program σ n g)
source
theorem Cslib.Circuits.Line.card {σ : Signature} [Finite σ.Op] (n g : ℕ) :
Nat.card (Line σ n g) = ∑ᶠ (op : σ.Op), (n + g) ^ σ.Arity op

For each operation, choose one wire for each of its arguments.

source
theorem Cslib.Circuits.Line.card_le {σ : Signature} [Finite σ.Op] (n g r : ℕ) (arity_le : ∀ (op : σ.Op), σ.Arity op ≤ r) :
Nat.card (Line σ n g) ≤ Nat.card σ.Op * (n + g + 1) ^ r

A uniform arity bound gives a uniform bound on the number of lines, including when there are no available wires.

source
@[simp]
theorem Cslib.Circuits.Program.card_zero {σ : Signature} (n : ℕ) :
Nat.card (Program σ n 0) = 1

There is one empty program, regardless of the signature or number of inputs.

source
theorem Cslib.Circuits.Program.card_succ {σ : Signature} (n g : ℕ) :
Nat.card (Program σ n (g + 1)) = Nat.card (Program σ n g) * Nat.card (Line σ n g)

Choose a prefix program and then its last line.

source
theorem Cslib.Circuits.Program.card {σ : Signature} [Finite σ.Op] (n g : ℕ) :
Nat.card (Program σ n g) = ∏ j ∈ Finset.range g, ∑ᶠ (op : σ.Op), (n + j) ^ σ.Arity op

The line at each position may refer to the inputs and all preceding gates.

source
def Cslib.Circuits.FullOp.equiv (k : ℕ) (U : Type u_1) :
FullOp k U ≃ ((Fin k → U) → U) ⊕ U

A full-basis operation is either a k-ary function or a constant.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance Cslib.Circuits.FullOp.instFinite {U : Type u_1} [Finite U] {k : ℕ} :
    Finite (FullOp k U)
    source
    @[simp]
    theorem Cslib.Circuits.FullOp.card (k : ℕ) (U : Type u_1) [Finite U] :
    Nat.card (FullOp k U) = Nat.card U ^ Nat.card U ^ k + Nat.card U

    Full-basis operations consist of all function tables and all constants.

    source
    instance Cslib.Circuits.instFiniteOpFullSignature {U : Type u_1} [Finite U] {k : ℕ} :
    Finite (fullSignature k U).Op
    source
    theorem Cslib.Circuits.Line.card_full (k n g : ℕ) (U : Type u_1) [Finite U] :
    Nat.card (Line (fullSignature k U) n g) = Nat.card U ^ Nat.card U ^ k * (n + g) ^ k + Nat.card U

    A function table takes k wire arguments; a constant takes none.