Tagless-final free model of open composition

This module defines Interp, the final (tagless-final / Church-encoded) free model of OpenTheory.

An Interp Atom Δ stores no syntax tree. Instead it is determined entirely by its universal interpretation function: for every lawful target OpenTheory and every atom interpretation, it produces an object of boundary Δ in the target.

This representation is convenient for proving universal properties because its lawfulness reduces immediately to the target theory's laws.

See OpenSyntax.Expr for the quotiented initial model that supports pattern matching and inspection.

structure Interaction.UC.OpenSyntax.Interp (Atom : PortBoundary → Type u) (Δ : PortBoundary) : Type (max 4 (u + 2))

Interp Atom Δ is the tagless-final free open-system expression of boundary Δ generated by primitive atoms Atom.

An element stores its universal elimination principle: for every lawful target open theory T and every atom interpretation, it produces an object of boundary Δ in T.

• run (T : OpenTheory) : T.CompactClosed → ({Δ : PortBoundary} → Atom Δ → T.Obj Δ) → T.Obj Δ

  Interpret the free expression in an arbitrary compact closed target theory.

@[reducible, inline]

abbrev Interaction.UC.OpenSyntax.Interp.interpret {Atom : PortBoundary → Type u} {Δ : PortBoundary} (W : Interp Atom Δ) (T : OpenTheory) (hT : T.CompactClosed) (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : T.Obj Δ

Interpret a tagless-final expression in a compact closed target theory.

This is just the run field restated as a named eliminator.

theorem Interaction.UC.OpenSyntax.Interp.ext {Atom : PortBoundary → Type u} {Δ : PortBoundary} {W₁ W₂ : Interp Atom Δ} (h : ∀ (T : OpenTheory) (hT : T.CompactClosed) (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ), (W₁.run T hT fun {Δ : PortBoundary} => interp) = W₂.run T hT fun {Δ : PortBoundary} => interp) : W₁ = W₂

Two tagless-final expressions are equal when they have the same interpretation in every lawful target theory.

theorem Interaction.UC.OpenSyntax.Interp.ext_iff {Atom : PortBoundary → Type u} {Δ : PortBoundary} {W₁ W₂ : Interp Atom Δ} : W₁ = W₂ ↔ ∀ (T : OpenTheory) (hT : T.CompactClosed) (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ), (W₁.run T hT fun {Δ : PortBoundary} => interp) = W₂.run T hT fun {Δ : PortBoundary} => interp

def Interaction.UC.OpenSyntax.Interp.atom {Atom : PortBoundary → Type u} {Δ : PortBoundary} : Atom Δ → Interp Atom Δ

Inject a primitive open component into the tagless-final syntax.

@[simp]

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

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

Adapt the exposed boundary of a tagless-final expression.

@[simp]

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

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

Place two tagless-final expressions side by side.

@[simp]

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

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

Connect one shared boundary between two tagless-final expressions.

@[simp]

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

def Interaction.UC.OpenSyntax.Interp.plug {Atom : PortBoundary → Type u} {Δ : PortBoundary} : Interp Atom Δ → Interp Atom Δ.swap → Interp Atom PortBoundary.empty

Close a tagless-final expression against a matching context.

@[simp]

theorem Interaction.UC.OpenSyntax.Interp.interpret_plug {Atom : PortBoundary → Type u} {Δ : PortBoundary} (W : Interp Atom Δ) (K : Interp Atom Δ.swap) (T : OpenTheory) (hT : T.CompactClosed) (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : ((W.plug K).interpret T hT fun {Δ : PortBoundary} => interp) = T.plug (W.interpret T hT fun {Δ : PortBoundary} => interp) (K.interpret T hT fun {Δ : PortBoundary} => interp)

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

The monoidal unit (closed system with no boundary).

@[simp]

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

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

The identity wire (coevaluation) on boundary Γ.

@[simp]

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

@[reducible, inline]

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

The free lawful OpenTheory generated by tagless-final expressions over Atom.

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

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

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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