Weighted circuit cost

Gate-elimination arguments often count only selected operations. An operation cost assigns a natural-number weight to every symbol; program and circuit cost are the corresponding sums over gates. Designating output wires is free.

@[reducible, inline]

abbrev Algebraic.OperationCost (σ : Signature) : Type u_1

A natural-number cost assigned to every operation in a signature.

Equations

• Algebraic.OperationCost σ = (σ.Op → ℕ)

def Algebraic.OperationCost.unit {σ : Signature} : OperationCost σ

Unit cost charges one for every gate.

Equations

• Algebraic.OperationCost.unit x✝ = 1

def Cslib.Circuits.Program.cost {σ : Signature} {n g : ℕ} (operationCost : Algebraic.OperationCost σ) : Program σ n g → ℕ

The cost of all gates in a straight-line program.

Equations

• Cslib.Circuits.Program.cost operationCost Cslib.Circuits.Program.empty = 0
• Cslib.Circuits.Program.cost operationCost (program.gate line) = Cslib.Circuits.Program.cost operationCost program + operationCost line.op

@[simp]

theorem Cslib.Circuits.Program.cost_empty {σ : Signature} {n : ℕ} (operationCost : Algebraic.OperationCost σ) : cost operationCost empty = 0

@[simp]

theorem Cslib.Circuits.Program.cost_gate {σ : Signature} {n g : ℕ} (operationCost : Algebraic.OperationCost σ) (program : Program σ n g) (line : Line σ n g) : cost operationCost (program.gate line) = cost operationCost program + operationCost line.op

theorem Cslib.Circuits.Program.cost_eq_sum_lines {σ : Signature} {n g : ℕ} (program : Program σ n g) (operationCost : Algebraic.OperationCost σ) : cost operationCost program = ∑ gate : Fin g, operationCost (program.lines gate).op

Program cost is the sum of the costs of its gates viewed in the final wire namespace.

theorem Cslib.Circuits.Program.cost_le_mul_gateCount {σ : Signature} {n g K : ℕ} (program : Program σ n g) (operationCost : Algebraic.OperationCost σ) (bounded : ∀ (op : σ.Op), operationCost op ≤ K) : cost operationCost program ≤ K * g

If every operation costs at most K, a program of g gates costs at most K * g.

@[simp]

theorem Cslib.Circuits.Program.cost_unit {σ : Signature} {n g : ℕ} (program : Program σ n g) : cost Algebraic.OperationCost.unit program = g

Unit cost is exactly the number of program gates.

def Cslib.Circuits.Circuit.cost {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (operationCost : Algebraic.OperationCost σ) : ℕ

The cost of all gates in a circuit.

Equations

• circuit.cost operationCost = Cslib.Circuits.Program.cost operationCost circuit.program

@[simp]

theorem Cslib.Circuits.Circuit.cost_id {σ : Signature} {n : ℕ} (operationCost : Algebraic.OperationCost σ) : (id σ n).cost operationCost = 0

theorem Cslib.Circuits.Circuit.cost_le_mul_size {σ : Signature} {n m K : ℕ} (circuit : Circuit σ n m) (operationCost : Algebraic.OperationCost σ) (bounded : ∀ (op : σ.Op), operationCost op ≤ K) : circuit.cost operationCost ≤ K * circuit.size

If every operation costs at most K, circuit cost is at most K times its gate count.

@[simp]

theorem Cslib.Circuits.Circuit.cost_unit {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) : circuit.cost Algebraic.OperationCost.unit = circuit.size

Unit cost is exactly circuit size.