Exact circuit syntax counts

This file equips lines, programs, and circuits over a finite signature with finite enumerations and proves exact formulas for their cardinalities.

def Algebraic.lineEquiv (σ : Signature) (n g : ℕ) : Line σ n g ≃ (op : σ.Op) × (Fin (σ.Arity op) → Wire n g)

A line is an operation symbol together with one wire for each argument.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Algebraic.instFintypeLine {σ : Signature} {n g : ℕ} [Fintype σ.Op] : Fintype (Line σ n g)

Equations

• Algebraic.instFintypeLine = Fintype.ofEquiv ((op : σ.Op) × (Fin (σ.Arity op) → Cslib.Circuits.Wire n g)) (Algebraic.lineEquiv σ n g).symm

theorem Algebraic.card_line {σ : Signature} {n g : ℕ} [Fintype σ.Op] : Fintype.card (Line σ n g) = ∑ op : σ.Op, (n + g) ^ σ.Arity op

Exact number of possible lines with n inputs and g available gates.

def Algebraic.programZeroEquiv (σ : Signature) (n : ℕ) : Program σ n 0 ≃ Unit

A zero-gate program carries no data.

Equations

• Algebraic.programZeroEquiv σ n = { toFun := fun (x : Cslib.Circuits.Program σ n 0) => (), invFun := fun (x : Unit) => Cslib.Circuits.Program.empty, left_inv := ⋯, right_inv := ⋯ }

def Algebraic.programSuccEquiv (σ : Signature) (n g : ℕ) : Program σ n (g + 1) ≃ Program σ n g × Line σ n g

A program with one additional gate is its prefix paired with its last line.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def Cslib.Circuits.Program.fintype {σ : Signature} [Fintype σ.Op] (n g : ℕ) : Fintype (Program σ n g)

Recursive finite enumeration of straight-line programs.

Equations

• Cslib.Circuits.Program.fintype n 0 = Fintype.ofEquiv Unit (Algebraic.programZeroEquiv σ n).symm
• Cslib.Circuits.Program.fintype n g.succ = Fintype.ofEquiv (Cslib.Circuits.Program σ n g × Cslib.Circuits.Line σ n g) (Algebraic.programSuccEquiv σ n g).symm

@[instance_reducible]

noncomputable instance Algebraic.instFintypeProgram {σ : Signature} {n g : ℕ} [Fintype σ.Op] : Fintype (Program σ n g)

Equations

• Algebraic.instFintypeProgram = Cslib.Circuits.Program.fintype n g

theorem Algebraic.card_program {σ : Signature} {n g : ℕ} [Fintype σ.Op] : Fintype.card (Program σ n g) = ∏ j ∈ Finset.range g, ∑ op : σ.Op, (n + j) ^ σ.Arity op

Exact number of topologically ordered programs.

def Algebraic.circuitEquiv (σ : Signature) (n g m : ℕ) : { circuit : Circuit σ n m // circuit.size = g } ≃ Program σ n g × (Fin m → Wire n g)

A circuit with exactly g gates is its program paired with its designated output wires.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Algebraic.instFintypeCircuit {σ : Signature} {n m g : ℕ} [Fintype σ.Op] : Fintype { circuit : Circuit σ n m // circuit.size = g }

Equations

• Algebraic.instFintypeCircuit = Fintype.ofEquiv (Cslib.Circuits.Program σ n g × (Fin m → Cslib.Circuits.Wire n g)) (Algebraic.circuitEquiv σ n g m).symm

theorem Algebraic.card_circuit {σ : Signature} {n m g : ℕ} [Fintype σ.Op] : Fintype.card { circuit : Circuit σ n m // circuit.size = g } = (∏ j ∈ Finset.range g, ∑ op : σ.Op, (n + j) ^ σ.Arity op) * (n + g) ^ m

Exact number of circuits with g gates and m designated outputs.

noncomputable def Algebraic.Target.count (U : Type u_1) (n m : ℕ) : ℕ

Number of functions from U^n to U^m.

Equations

• Algebraic.Target.count U n m = Nat.card (Algebraic.Target U n m)

theorem Algebraic.Target.count_eq {U : Type u_1} {n m : ℕ} [Finite U] : count U n m = Nat.card U ^ (m * Nat.card U ^ n)

theorem Algebraic.card_target {U : Type u_1} {n m : ℕ} [Finite U] : Nat.card (Target U n m) = Nat.card U ^ (m * Nat.card U ^ n)

Exact number of functions from U^n to U^m.

def Cslib.Circuits.Signature.lineCount (σ : Signature) [Fintype σ.Op] (w : ℕ) : ℕ

Number of possible lines when w wires are available.

Equations

• σ.lineCount w = ∑ op : σ.Op, w ^ σ.Arity op

theorem Algebraic.card_line_eq_lineCount {σ : Signature} {n g : ℕ} [Fintype σ.Op] : Fintype.card (Line σ n g) = σ.lineCount (n + g)