Minimum-cost circuit realizations

A realization chooses one implementation circuit for each source operation. This module minimizes those choices independently, turning pulled-back cost into the intrinsic implementation cost of each operation rather than the cost of an arbitrary selected gadget.

def Cslib.Circuits.Interpretation.operationTarget {σ : Signature} {U : Type u_2} (interpretation : Interpretation σ U) (op : σ.Op) : Algebraic.Target U (σ.Arity op) 1

The scalar target associated with one interpreted operation.

Equations

• interpretation.operationTarget op input x✝ = interpretation op input

theorem Algebraic.Realization.operation_computes {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (op : σ.Op) : (realization.operation op).ComputesWith target (source.operationTarget op)

Every operation circuit in a realization computes its source operation.

noncomputable def Algebraic.Realization.ofFunctionalCompleteness {σ : Signature} {U : Type u_2} {τ : Signature} (source : Interpretation σ U) (target : Interpretation τ U) (complete : target.FunctionallyComplete) : Realization σ τ source target

Functional completeness supplies a realization of every interpreted signature on the same carrier. The choice is classical, not executable.

Equations

• Algebraic.Realization.ofFunctionalCompleteness source target complete = { operation := fun (op : σ.Op) => Classical.choose ⋯, realizes := ⋯ }

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

A realization whose selected implementation of every source operation is minimum for the target cost model.

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

  Each selected operation circuit has minimum target cost.

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

Replace every selected operation gadget by a minimum-cost implementation. Ties are broken by internal gate count through Circuit.minimum.

Equations

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

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

The intrinsic implementation cost obtained by minimizing the realization's gadgets. Its value is independent of the initial realization.

Equations

• realization.minimumCost operationCost = (realization.minimize operationCost).pullCost operationCost

theorem Algebraic.OptimalRealization.pullCost_le {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} {operationCost : OperationCost τ} (optimal : OptimalRealization σ τ source target operationCost) (competitor : Realization σ τ source target) (op : σ.Op) : optimal.pullCost operationCost op ≤ competitor.pullCost operationCost op

An optimal realization charges no more for an operation than any other realization of the same interpreted signatures.

theorem Algebraic.OptimalRealization.pullCost_eq {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} {operationCost : OperationCost τ} (left right : OptimalRealization σ τ source target operationCost) : left.pullCost operationCost = right.pullCost operationCost

Any two optimal realizations induce exactly the same source cost model.

theorem Algebraic.Realization.minimumCost_le {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} (realization competitor : Realization σ τ source target) (operationCost : OperationCost τ) (op : σ.Op) : realization.minimumCost operationCost op ≤ competitor.pullCost operationCost op

Intrinsic operation cost is bounded by the cost pulled back through any chosen realization.

theorem Algebraic.Realization.minimumCost_congr {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} (left right : Realization σ τ source target) (operationCost : OperationCost τ) : left.minimumCost operationCost = right.minimumCost operationCost

Intrinsic minimum cost does not depend on the initial realization used to establish implementability.

theorem Algebraic.Realization.minimumCost_eq {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} {operationCost : OperationCost τ} (optimal : OptimalRealization σ τ source target operationCost) : optimal.minimumCost operationCost = optimal.pullCost operationCost

Minimizing an already optimal realization recovers the same intrinsic cost model.