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.

instance Cslib.Circuits.Line.instFinite {σ : Signature} [Finite σ.Op] (n g : ℕ) : Finite (Line σ n g)

instance Cslib.Circuits.Program.instFinite {σ : Signature} [Finite σ.Op] (n g : ℕ) : Finite (Program σ n g)

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.

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.

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

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.

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.

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.

instance Cslib.Circuits.FullOp.instFinite {U : Type u_1} [Finite U] {k : ℕ} : Finite (FullOp k U)

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

instance Cslib.Circuits.instFiniteOpFullSignature {U : Type u_1} [Finite U] {k : ℕ} : Finite (fullSignature k U).Op

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.