Finite circuit syntax

A finite signature gives computable enumerations of 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.

@[instance_reducible]

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

Equations

• Cslib.Circuits.Line.instFintype n g = Fintype.ofEquiv ((op : σ.Op) × (Fin (σ.Arity op) → Cslib.Circuits.Wire n g)) (Cslib.Circuits.Line.equiv σ n g).symm

@[instance_reducible]

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

Equations

• Cslib.Circuits.Program.instFintype n 0 = Fintype.ofEquiv PUnit.{1} (Cslib.Circuits.Program.emptyEquiv σ n).symm
• Cslib.Circuits.Program.instFintype n g.succ = Fintype.ofEquiv (Cslib.Circuits.Program σ n g × Cslib.Circuits.Line σ n g) (Cslib.Circuits.Program.gateEquiv σ n g).symm

theorem Cslib.Circuits.Line.card {σ : Signature} [Fintype σ.Op] (n g : ℕ) : Fintype.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} [Fintype σ.Op] (n g r : ℕ) (arity_le : ∀ (op : σ.Op), σ.Arity op ≤ r) : Fintype.card (Line σ n g) ≤ Fintype.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} [Fintype σ.Op] (n : ℕ) : Fintype.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} [Fintype σ.Op] (n g : ℕ) : Fintype.card (Program σ n (g + 1)) = Fintype.card (Program σ n g) * Fintype.card (Line σ n g)

Choose a prefix program and then its last line.

theorem Cslib.Circuits.Program.card {σ : Signature} [Fintype σ.Op] (n g : ℕ) : Fintype.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.