Semantic circuit normalization

Programs are hash-consed by the scalar functions computed at their gates. The result computes the same values, has no duplicate gate functions, and never has more gates. This is the semantic bridge needed for the factorial Shannon count.

Program normalization

structure Cslib.Circuits.Program.Normalization {σ : Signature} {n g : ℕ} {U : Type u_2} (program : Program σ n g) (interpretation : Interpretation σ U) : Type u_1

The result and semantic invariant produced by hash-consing a program's gate functions.

• gateCount : ℕ

  Number of gates after semantic hash-consing.

• result : Program σ n self.gateCount

  Program with pairwise distinct gate functions.

• wireMap : Wire.Renaming n g self.gateCount

  Input-fixing translation of old wires to their representatives.

• trace_eq (input : Fin n → U) (wire : Wire n g) : self.result.trace interpretation input (self.wireMap.apply wire) = program.trace interpretation input wire

  Every translated wire computes its original value.

• injective_gateFunction : Function.Injective (self.result.gateFunction interpretation)

  No two retained gates compute the same scalar function.

• gateCount_le : self.gateCount ≤ g

  Normalization never adds gates.

• cost_le (operationCost : Algebraic.OperationCost σ) : cost operationCost self.result ≤ cost operationCost program

  Normalization does not increase any nonnegative operation cost.

noncomputable def Cslib.Circuits.Program.normalize {U : Type u_1} {σ : Signature} {n g : ℕ} [Fintype U] (interpretation : Interpretation σ U) (program : Program σ n g) : program.Normalization interpretation

Hash-cons a program by semantic gate function, preserving every wire value.

Equations

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

Circuit normalization

structure Cslib.Circuits.Circuit.Normalization {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) : Type u_1

A semantics-preserving circuit normalization with pairwise distinct internal gate functions.

• result : Circuit σ n m

  The normalized circuit.

• eval_eq : self.result.eval interpretation = circuit.eval interpretation
• injective_gateFunction : Function.Injective (self.result.program.gateFunction interpretation)
• gateCount_le : self.result.size ≤ circuit.size
• cost_le (operationCost : Algebraic.OperationCost σ) : self.result.cost operationCost ≤ circuit.cost operationCost

  Normalization does not increase any nonnegative operation cost.

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.Normalization.gateCount {σ : Signature} {n m : ℕ} {U : Type u_2} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} (normalization : circuit.Normalization interpretation) : ℕ

Number of internal gates after normalization.

Equations

• normalization.gateCount = normalization.result.size

noncomputable def Cslib.Circuits.Circuit.normalize {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype U] (circuit : Circuit σ n m) (interpretation : Interpretation σ U) : circuit.Normalization interpretation

Normalize the program and rename the designated output wires.

Equations

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

Irredundant function families

noncomputable def Cslib.Circuits.Circuit.irredundantFunctions {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n g m : ℕ) : Finset (Algebraic.Target U n m)

Functions computed by irredundant circuits with exactly g internal gates.

Equations

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

theorem Cslib.Circuits.Circuit.mem_irredundantFunctions_iff {U : Type u_1} {σ : Signature} {n m g : ℕ} [Fintype σ.Op] [Fintype U] {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} : target ∈ irredundantFunctions interpretation n g m ↔ ∃ (circuit : Circuit σ n m), circuit.size = g ∧ circuit.Irredundant interpretation ∧ circuit.eval interpretation = target

noncomputable def Cslib.Circuits.Circuit.irredundantFunctionsAtMost {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m G : ℕ) : Finset (Algebraic.Target U n m)

Functions computed by irredundant circuits with at most G internal gates.

Equations

• Cslib.Circuits.Circuit.irredundantFunctionsAtMost interpretation n m G = (Finset.range (G + 1)).biUnion fun (g : ℕ) => Cslib.Circuits.Circuit.irredundantFunctions interpretation n g m

theorem Cslib.Circuits.Circuit.functionsAtMost_subset_irredundantFunctionsAtMost {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m G : ℕ) : functionsAtMost interpretation n m G ⊆ irredundantFunctionsAtMost interpretation n m G

theorem Cslib.Circuits.Circuit.card_functionsAtMost_le_sum_irredundant {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m G : ℕ) : (functionsAtMost interpretation n m G).card ≤ ∑ g ∈ Finset.range (G + 1), (irredundantFunctions interpretation n g m).card