The observational category of circuit translations

Dependent gate indices make raw compiler output too intensional for useful categorical equality. We quotient translations by the behavior they induce on all interpretations over a fixed carrier and on all weighted cost models. Compilation respects this relation, and the quotient forms an ordinary Mathlib category.

structure Algebraic.Translation.EquivalentOn {σ : Signature} {τ : Signature} (U : Type u) (left right : Translation σ τ) : Prop

Two translations are observationally equivalent over U when they induce the same interpretation pullback on U and the same pullback of every cost model.

• pull_eq (interpretation : Interpretation τ U) : left.pull interpretation = right.pull interpretation
• pullCost_eq (operationCost : OperationCost τ) : left.pullCost operationCost = right.pullCost operationCost

theorem Algebraic.Translation.EquivalentOn.refl {σ : Signature} {τ : Signature} {U : Type u_3} (translation : Translation σ τ) : EquivalentOn U translation translation

theorem Algebraic.Translation.EquivalentOn.symm {σ : Signature} {τ : Signature} {U : Type u_3} {left right : Translation σ τ} (equivalent : EquivalentOn U left right) : EquivalentOn U right left

theorem Algebraic.Translation.EquivalentOn.trans {σ : Signature} {τ : Signature} {U : Type u_3} {first second third : Translation σ τ} (left : EquivalentOn U first second) (right : EquivalentOn U second third) : EquivalentOn U first third

theorem Algebraic.Translation.EquivalentOn.compile_eval_eq {σ : Signature} {τ : Signature} {U : Type u_3} {n m : ℕ} {left right : Translation σ τ} (equivalent : EquivalentOn U left right) (circuit : Circuit σ n m) (interpretation : Interpretation τ U) (input : Fin n → U) : (left.compile circuit).eval interpretation input = (right.compile circuit).eval interpretation input

Equivalent translations compile every circuit to the same semantics over the observed carrier.

theorem Algebraic.Translation.EquivalentOn.compile_cost_eq {σ : Signature} {τ : Signature} {U : Type u_3} {n m : ℕ} {left right : Translation σ τ} (equivalent : EquivalentOn U left right) (circuit : Circuit σ n m) (operationCost : OperationCost τ) : (left.compile circuit).cost operationCost = (right.compile circuit).cost operationCost

Equivalent translations compile every circuit to the same weighted cost.

theorem Algebraic.Translation.comp_equivalentOn {τ : Signature} {υ : Signature} {σ : Signature} {U : Type u_4} {outerLeft outerRight : Translation τ υ} {innerLeft innerRight : Translation σ τ} (outer : EquivalentOn U outerLeft outerRight) (inner : EquivalentOn U innerLeft innerRight) : EquivalentOn U (outerLeft.comp innerLeft) (outerRight.comp innerRight)

Observational equivalence is a congruence for translation composition.

theorem Algebraic.Translation.id_comp_equivalentOn {σ : Signature} {τ : Signature} {U : Type u_3} (translation : Translation σ τ) : EquivalentOn U ((id τ).comp translation) translation

Left identity law, up to observational equivalence.

theorem Algebraic.Translation.comp_id_equivalentOn {σ : Signature} {τ : Signature} {U : Type u_3} (translation : Translation σ τ) : EquivalentOn U (translation.comp (id σ)) translation

Right identity law, up to observational equivalence.

theorem Algebraic.Translation.comp_assoc_equivalentOn {υ : Signature} {φ : Signature} {τ : Signature} {σ : Signature} {U : Type u_5} (outer : Translation υ φ) (middle : Translation τ υ) (inner : Translation σ τ) : EquivalentOn U ((outer.comp middle).comp inner) (outer.comp (middle.comp inner))

Associativity law, up to observational equivalence.

def Algebraic.Translation.equivalentOnSetoid (U : Type u) (σ : Signature) (τ : Signature) : Setoid (Translation σ τ)

Setoid used to form the observational quotient of translations.

Equations

• Algebraic.Translation.equivalentOnSetoid U σ τ = { r := Algebraic.Translation.EquivalentOn U, iseqv := ⋯ }

structure Algebraic.ObservedSignature (U : Type u) : Type 1

A signature regarded as an object whose translations are observed over the carrier U.

• signature : Signature

  The underlying signature.

def Algebraic.ObservedTranslation (U : Type u) (source target : ObservedSignature U) : Type

A morphism of observed signatures is an observational equivalence class of circuit translations.

Equations

• Algebraic.ObservedTranslation U source target = Quotient (Algebraic.Translation.equivalentOnSetoid U source.signature target.signature)

def Algebraic.ObservedTranslation.mk {U : Type u_1} {source target : ObservedSignature U} (translation : Translation source.signature target.signature) : ObservedTranslation U source target

Include a raw translation in the observational quotient.

Equations

• Algebraic.ObservedTranslation.mk translation = ⟦translation⟧

def Algebraic.ObservedTranslation.id {U : Type u_1} (signature : ObservedSignature U) : ObservedTranslation U signature signature

Identity morphism in the observational quotient.

Equations

• Algebraic.ObservedTranslation.id signature = Algebraic.ObservedTranslation.mk (Algebraic.Translation.id signature.signature)

def Algebraic.ObservedTranslation.comp {U : Type u_1} {source middle target : ObservedSignature U} (inner : ObservedTranslation U source middle) (outer : ObservedTranslation U middle target) : ObservedTranslation U source target

Composition in the observational quotient.

Equations

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

@[instance_reducible]

instance Algebraic.instCategoryObservedSignature (U : Type u) : CategoryTheory.Category.{0, 1} (ObservedSignature U)

Circuit signatures and translations modulo semantic-and-cost observation form a category.

Equations

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