Quotiented free model of open composition

This module defines Expr, the initial (quotiented) free model of OpenTheory.

Expr Atom Δ is the quotient of the raw syntax tree Raw Atom Δ by the equivalence relation Raw.Equiv, which identifies raw expressions that should be equal according to the OpenTheory equations (functoriality of map, naturality of par, wire, and plug).

The quotient construction yields a lawful OpenTheory instance by construction: each law holds because it is a constructor of Raw.Equiv.

Main definitions

• Expr: quotient of Raw by Raw.Equiv.
• Expr.mk: canonical projection from Raw to Expr.
• Expr.map, Expr.par, Expr.wire, Expr.plug: lifted operations.
• Expr.interpret: interpretation into any lawful OpenTheory, lifted from Raw.interpret.
• Expr.theory: the free lawful OpenTheory over Atom.
• Expr.toInterp: embedding into the tagless-final Interp model.

def Interaction.UC.OpenSyntax.Expr (Atom : PortBoundary → Type u) (Δ : PortBoundary) : Type (u + 1)

Expr Atom Δ is the free open-system expression of boundary Δ, generated by primitive atoms Atom.

This is the quotient of Raw Atom Δ by the OpenTheory equations. Unlike the raw syntax tree, Expr satisfies map_id, map_comp, and the naturality laws, so it forms a lawful OpenTheory.

For pattern matching on the underlying syntax, project to Raw via Expr.liftOn or work with Raw directly.

def Interaction.UC.OpenSyntax.Expr.mk {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Raw Atom Δ) : Expr Atom Δ

Project a raw expression into the quotiented Expr.

def Interaction.UC.OpenSyntax.Expr.atom {Atom : PortBoundary → Type u} {Δ : PortBoundary} (a : Atom Δ) : Expr Atom Δ

Inject a primitive open component.

def Interaction.UC.OpenSyntax.Expr.map {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (e : Expr Atom Δ₁) : Expr Atom Δ₂

Adapt the exposed boundary along a structural morphism.

def Interaction.UC.OpenSyntax.Expr.par {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} (e₁ : Expr Atom Δ₁) (e₂ : Expr Atom Δ₂) : Expr Atom (Δ₁.tensor Δ₂)

Place two open systems side by side.

def Interaction.UC.OpenSyntax.Expr.wire {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} (e₁ : Expr Atom (Δ₁.tensor Γ)) (e₂ : Expr Atom (Γ.swap.tensor Δ₂)) : Expr Atom (Δ₁.tensor Δ₂)

Connect one shared boundary between two open systems.

def Interaction.UC.OpenSyntax.Expr.idWire {Atom : PortBoundary → Type u} (Γ : PortBoundary) : Expr Atom (Γ.swap.tensor Γ)

The identity wire (coevaluation) on boundary Γ.

def Interaction.UC.OpenSyntax.Expr.plug {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Expr Atom Δ) (k : Expr Atom Δ.swap) : Expr Atom PortBoundary.empty

Close an open system against a matching context. Derived from wire and map, mirroring Raw.plug.

def Interaction.UC.OpenSyntax.Expr.unit {Atom : PortBoundary → Type u} : Expr Atom PortBoundary.empty

The monoidal unit (closed system with no boundary). Derived from idWire and map, mirroring Raw.unit.

def Interaction.UC.OpenSyntax.Expr.interpret {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Expr Atom Δ) (T : OpenTheory) [hT : T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : T.Obj Δ

Interpret a quotiented expression in a compact closed target theory.

Well-defined on the quotient because Raw.Equiv.interpret_eq shows that equivalent raw expressions interpret the same way in any compact closed theory.

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_mk {Atom : PortBoundary → Type u} {Δ : PortBoundary} (r : Raw Atom Δ) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((mk r).interpret T fun {Δ : PortBoundary} => interp) = r.interpret T (fun {Δ : PortBoundary} => interp) OpenTheory.CompactClosed.idWire

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_atom {Atom : PortBoundary → Type u} {Δ : PortBoundary} (a : Atom Δ) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((atom a).interpret T fun {Δ : PortBoundary} => interp) = interp a

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_map {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (e : Expr Atom Δ₁) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((map f e).interpret T fun {Δ : PortBoundary} => interp) = T.map f (e.interpret T fun {Δ : PortBoundary} => interp)

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_par {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} (e₁ : Expr Atom Δ₁) (e₂ : Expr Atom Δ₂) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((e₁.par e₂).interpret T fun {Δ : PortBoundary} => interp) = T.par (e₁.interpret T fun {Δ : PortBoundary} => interp) (e₂.interpret T fun {Δ : PortBoundary} => interp)

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_wire {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} (e₁ : Expr Atom (Δ₁.tensor Γ)) (e₂ : Expr Atom (Γ.swap.tensor Δ₂)) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((e₁.wire e₂).interpret T fun {Δ : PortBoundary} => interp) = T.wire (e₁.interpret T fun {Δ : PortBoundary} => interp) (e₂.interpret T fun {Δ : PortBoundary} => interp)

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_idWire {Atom : PortBoundary → Type u} (Γ : PortBoundary) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((idWire Γ).interpret T fun {Δ : PortBoundary} => interp) = OpenTheory.CompactClosed.idWire Γ

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_plug {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Expr Atom Δ) (k : Expr Atom Δ.swap) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((e.plug k).interpret T fun {Δ : PortBoundary} => interp) = T.plug (e.interpret T fun {Δ : PortBoundary} => interp) (k.interpret T fun {Δ : PortBoundary} => interp)

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.interpret_unit {Atom : PortBoundary → Type u} (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : (unit.interpret T fun {Δ : PortBoundary} => interp) = OpenTheory.Monoidal.unit

@[reducible, inline]

abbrev Interaction.UC.OpenSyntax.Expr.theory (Atom : PortBoundary → Type u) : OpenTheory

The free lawful OpenTheory whose objects are quotiented expressions over Atom.

instance Interaction.UC.OpenSyntax.Expr.lawfulMap (Atom : PortBoundary → Type u) : (theory Atom).IsLawfulMap

instance Interaction.UC.OpenSyntax.Expr.lawfulPar (Atom : PortBoundary → Type u) : (theory Atom).IsLawfulPar

instance Interaction.UC.OpenSyntax.Expr.lawfulWire (Atom : PortBoundary → Type u) : (theory Atom).IsLawfulWire

instance Interaction.UC.OpenSyntax.Expr.lawfulPlug (Atom : PortBoundary → Type u) : (theory Atom).IsLawfulPlug

instance Interaction.UC.OpenSyntax.Expr.lawful (Atom : PortBoundary → Type u) : (theory Atom).IsLawful

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Expr.monoidal (Atom : PortBoundary → Type u) : (theory Atom).Monoidal

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Expr.compactClosed (Atom : PortBoundary → Type u) : (theory Atom).CompactClosed

def Interaction.UC.OpenSyntax.Expr.toInterp {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Expr Atom Δ) : Interp Atom Δ

Embed a quotiented expression into the tagless-final representation.

Well-defined on the quotient because equivalent raw expressions interpret the same way in every compact closed theory (which is exactly what Interp.ext requires).

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_mk {Atom : PortBoundary → Type u} {Δ : PortBoundary} (r : Raw Atom Δ) : (mk r).toInterp = { run := fun (T : OpenTheory) (hCC : T.CompactClosed) (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) => r.interpret T (fun {Δ : PortBoundary} => interp) OpenTheory.CompactClosed.idWire }

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_atom {Atom : PortBoundary → Type u} {Δ : PortBoundary} (a : Atom Δ) : (atom a).toInterp = Interp.atom a

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_map {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (e : Expr Atom Δ₁) : (map f e).toInterp = Interp.map f e.toInterp

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_par {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} (e₁ : Expr Atom Δ₁) (e₂ : Expr Atom Δ₂) : (e₁.par e₂).toInterp = e₁.toInterp.par e₂.toInterp

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_wire {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} (e₁ : Expr Atom (Δ₁.tensor Γ)) (e₂ : Expr Atom (Γ.swap.tensor Δ₂)) : (e₁.wire e₂).toInterp = e₁.toInterp.wire e₂.toInterp

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_idWire {Atom : PortBoundary → Type u} (Γ : PortBoundary) : (idWire Γ).toInterp = Interp.idWire Γ

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_plug {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Expr Atom Δ) (k : Expr Atom Δ.swap) : (e.plug k).toInterp = e.toInterp.plug k.toInterp

@[simp]

theorem Interaction.UC.OpenSyntax.Expr.toInterp_unit {Atom : PortBoundary → Type u} : unit.toInterp = Interp.unit