Circuit translations between signatures

A translation implements every source operation by a target circuit of the same arity. Compiling a source circuit substitutes these implementation circuits gate by gate. Evaluation and arbitrary weighted gate costs are preserved exactly.

structure Algebraic.Translation (σ : Signature) (τ : Signature) : Type (max u_1 u_2)

An implementation of every operation of σ by a scalar τ-circuit with the same inputs.

• operation (op : σ.Op) : Circuit τ (σ.Arity op) 1

  Target circuit implementing a source operation.

@[reducible, inline]

abbrev Algebraic.Translation.gateCount {σ : Signature} {τ : Signature} (translation : Translation σ τ) (op : σ.Op) : ℕ

Number of target gates used to implement a source operation.

Equations

• translation.gateCount op = (translation.operation op).size

def Algebraic.Translation.pull {σ : Signature} {τ : Signature} {U : Type u_3} (translation : Translation σ τ) (interpretation : Interpretation τ U) : Interpretation σ U

Pull a target interpretation back through a circuit translation.

Equations

• translation.pull interpretation op input = (translation.operation op).eval interpretation input 0

def Algebraic.Translation.pullCost {σ : Signature} {τ : Signature} (translation : Translation σ τ) (operationCost : OperationCost τ) : OperationCost σ

Charge a source operation exactly the target cost of its implementation.

Equations

• translation.pullCost operationCost op = (translation.operation op).cost operationCost

def Algebraic.Translation.pullHomomorphism {σ : Signature} {τ : Signature} {U : Type u_3} {V : Type u_4} (translation : Translation σ τ) {source : Interpretation τ U} {target : Interpretation τ V} (homomorphism : Homomorphism source target) : Homomorphism (translation.pull source) (translation.pull target)

Pulling interpretations through a translation also pulls ordinary homomorphisms between them.

Equations

• translation.pullHomomorphism homomorphism = { map := homomorphism.map, homomorphic := ⋯ }

structure Algebraic.Translation.ProgramCompilation {σ : Signature} {τ : Signature} {n g : ℕ} (translation : Translation σ τ) (source : Program σ n g) : Type u_2

The compiled target program and the image of every source wire.

• gateCount : ℕ

  Number of target gates in the compiled program.

• program : Program τ n self.gateCount

  Compiled target program.

• wires : Wire.Renaming n g self.gateCount

  Image of every source gate wire in the compiled program.

def Algebraic.Translation.compileProgram {σ : Signature} {τ : Signature} {n g : ℕ} (translation : Translation σ τ) (source : Program σ n g) : translation.ProgramCompilation source

Compile a program by replacing each source gate by its implementation circuit.

Equations

• One or more equations did not get rendered due to their size.
• translation.compileProgram Cslib.Circuits.Program.empty = { gateCount := 0, program := Cslib.Circuits.Program.empty, wires := Cslib.Circuits.Wire.Renaming.id }

def Algebraic.Translation.compiledGateCount {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) : ℕ

Number of target gates produced when compiling a source circuit.

Equations

• translation.compiledGateCount circuit = (translation.compileProgram circuit.program).gateCount

def Algebraic.Translation.compile {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) : Circuit τ n m

Compile a circuit through a signature translation.

Equations

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

@[simp]

theorem Algebraic.Translation.size_compile {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) : (translation.compile circuit).size = translation.compiledGateCount circuit

A compiled circuit has the compiled gate count.

theorem Algebraic.Translation.compileProgram_trace {σ : Signature} {τ : Signature} {n g : ℕ} {U : Type u_3} (translation : Translation σ τ) (source : Program σ n g) (interpretation : Interpretation τ U) (input : Fin n → U) (wire : Wire n g) : (translation.compileProgram source).program.trace interpretation input ((translation.compileProgram source).wires.apply wire) = source.trace (translation.pull interpretation) input wire

Program compilation preserves the value of every source wire.

theorem Algebraic.Translation.compile_eval {σ : Signature} {τ : Signature} {n m : ℕ} {U : Type u_3} (translation : Translation σ τ) (circuit : Circuit σ n m) (interpretation : Interpretation τ U) (input : Fin n → U) : (translation.compile circuit).eval interpretation input = circuit.eval (translation.pull interpretation) input

Compiling a circuit preserves evaluation exactly.

theorem Algebraic.Translation.compileProgram_cost {σ : Signature} {τ : Signature} {n g : ℕ} (translation : Translation σ τ) (source : Program σ n g) (operationCost : OperationCost τ) : Program.cost operationCost (translation.compileProgram source).program = Program.cost (translation.pullCost operationCost) source

Program compilation preserves pulled-back weighted cost exactly.

theorem Algebraic.Translation.compile_cost {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) (operationCost : OperationCost τ) : (translation.compile circuit).cost operationCost = circuit.cost (translation.pullCost operationCost)

Circuit compilation preserves pulled-back weighted cost exactly.

theorem Algebraic.Translation.compile_cost_le_mul_size {σ : Signature} {τ : Signature} {n m K : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) (operationCost : OperationCost τ) (bounded : ∀ (op : σ.Op), translation.pullCost operationCost op ≤ K) : (translation.compile circuit).cost operationCost ≤ K * circuit.size

If every source operation implementation costs at most K, compilation costs at most K times the source gate count.

theorem Algebraic.Translation.compile_size {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) : (translation.compile circuit).size = circuit.cost (translation.pullCost OperationCost.unit)

The compiled gate count is exactly source cost when each source operation is charged by the size of its implementation.

theorem Algebraic.Translation.compile_size_le_mul {σ : Signature} {τ : Signature} {n m K : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) (bounded : ∀ (op : σ.Op), (translation.operation op).size ≤ K) : (translation.compile circuit).size ≤ K * circuit.size

If every implementation uses at most K gates, compilation increases size by at most a factor of K.

def Algebraic.Translation.id (σ : Signature) : Translation σ σ

The identity translation implements each operation with one gate.

Equations

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

@[simp]

theorem Algebraic.Translation.pull_id {σ : Signature} {U : Type u_2} (interpretation : Interpretation σ U) : (id σ).pull interpretation = interpretation

@[simp]

theorem Algebraic.Translation.pullCost_id {σ : Signature} (operationCost : OperationCost σ) : (id σ).pullCost operationCost = operationCost

theorem Algebraic.Translation.compile_id_eval {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) : ((id σ).compile circuit).eval interpretation input = circuit.eval interpretation input

Compilation through the identity translation preserves semantics.

theorem Algebraic.Translation.compile_id_cost {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (operationCost : OperationCost σ) : ((id σ).compile circuit).cost operationCost = circuit.cost operationCost

Compilation through the identity translation preserves weighted cost.

def Algebraic.Translation.comp {τ : Signature} {υ : Signature} {σ : Signature} (outer : Translation τ υ) (inner : Translation σ τ) : Translation σ υ

Compose translations by compiling every operation implementation of the first translation through the second.

Equations

• outer.comp inner = { operation := fun (op : σ.Op) => outer.compile (inner.operation op) }

theorem Algebraic.Translation.pull_comp {τ : Signature} {υ : Signature} {σ : Signature} {U : Type u_4} (outer : Translation τ υ) (inner : Translation σ τ) (interpretation : Interpretation υ U) : (outer.comp inner).pull interpretation = inner.pull (outer.pull interpretation)

Interpretations pull back contravariantly through composition.

theorem Algebraic.Translation.pullCost_comp {τ : Signature} {υ : Signature} {σ : Signature} (outer : Translation τ υ) (inner : Translation σ τ) (operationCost : OperationCost υ) : (outer.comp inner).pullCost operationCost = inner.pullCost (outer.pullCost operationCost)

Weighted costs pull back contravariantly through composition.

theorem Algebraic.Translation.compile_comp_eval {τ : Signature} {υ : Signature} {σ : Signature} {n m : ℕ} {U : Type u_4} (outer : Translation τ υ) (inner : Translation σ τ) (circuit : Circuit σ n m) (interpretation : Interpretation υ U) (input : Fin n → U) : ((outer.comp inner).compile circuit).eval interpretation input = (outer.compile (inner.compile circuit)).eval interpretation input

Compiling through a composite or in two stages has the same semantics.

theorem Algebraic.Translation.compile_comp_cost {τ : Signature} {υ : Signature} {σ : Signature} {n m : ℕ} (outer : Translation τ υ) (inner : Translation σ τ) (circuit : Circuit σ n m) (operationCost : OperationCost υ) : ((outer.comp inner).compile circuit).cost operationCost = (outer.compile (inner.compile circuit)).cost operationCost

Compiling through a composite or in two stages has the same weighted cost.

structure Algebraic.Realization {U : Type u_1} (σ : Signature) (τ : Signature) (source : Interpretation σ U) (target : Interpretation τ U) extends Algebraic.Translation σ τ : Type (max u_2 u_3)

A translation whose operation circuits realize a specified source interpretation in a specified target interpretation.

• operation (op : σ.Op) : Circuit τ (σ.Arity op) 1
• realizes : self.pull target = source

  Pulling back the target interpretation gives the source interpretation.

def Algebraic.Realization.id {σ : Signature} {U : Type u_2} (interpretation : Interpretation σ U) : Realization σ σ interpretation interpretation

The identity translation realizes every interpretation in itself.

Equations

• Algebraic.Realization.id interpretation = { toTranslation := Algebraic.Translation.id σ, realizes := ⋯ }

def Algebraic.Realization.comp {σ : Signature} {U : Type u_2} {τ : Signature} {υ : Signature} {source : Interpretation σ U} {middle : Interpretation τ U} {target : Interpretation υ U} (outer : Realization τ υ middle target) (inner : Realization σ τ source middle) : Realization σ υ source target

Compose realizations over a common carrier.

Equations

• outer.comp inner = { toTranslation := outer.comp inner.toTranslation, realizes := ⋯ }

@[simp]

theorem Algebraic.Realization.operation_eval {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (op : σ.Op) (input : Fin (σ.Arity op) → U) : (realization.operation op).eval target input 0 = source op input

Every selected operation circuit has the promised source semantics.

def Algebraic.Realization.compile {σ : Signature} {U : Type u_2} {τ : Signature} {n m : ℕ} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (circuit : Circuit σ n m) : Circuit τ n m

Compile a circuit through a realization.

Equations

• realization.compile circuit = realization.compile circuit

def Algebraic.Realization.pullCost {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (operationCost : OperationCost τ) : OperationCost σ

Pull a weighted target cost back through a realization.

Equations

• realization.pullCost operationCost = realization.pullCost operationCost

theorem Algebraic.Realization.compile_eval {σ : Signature} {U : Type u_2} {τ : Signature} {n m : ℕ} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (circuit : Circuit σ n m) (input : Fin n → U) : (realization.compile circuit).eval target input = circuit.eval source input

Compilation through a realization preserves the specified semantics.

theorem Algebraic.Realization.compile_cost {σ : Signature} {U : Type u_2} {τ : Signature} {n m : ℕ} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (circuit : Circuit σ n m) (operationCost : OperationCost τ) : (realization.compile circuit).cost operationCost = circuit.cost (realization.pullCost operationCost)

Compilation through a realization preserves pulled-back cost exactly.

theorem Algebraic.Realization.transport_lowerBound {σ : Signature} {U : Type u_2} {τ : Signature} {n m L : ℕ} {source : Interpretation σ U} {targetInterpretation : Interpretation τ U} (realization : Realization σ τ source targetInterpretation) (operationCost : OperationCost τ) (target : Target U n m) (lowerBound : ∀ (targetCircuit : Circuit τ n m), targetCircuit.ComputesWith targetInterpretation target → L ≤ targetCircuit.cost operationCost) (circuit : Circuit σ n m) (computes : circuit.ComputesWith source target) : L ≤ circuit.cost (realization.pullCost operationCost)

Transport an arbitrary target-basis cost lower bound back through a realization.