Raw syntax trees for open composition

This module defines the raw (un-quotiented) syntax trees for open-system expressions, together with a structural interpretation function into any target OpenTheory.

The inductive Raw Atom Δ has five native constructors (atom, map, par, wire, idWire) forming the minimal generating set for a compact closed open-system algebra. The derived operations plug and unit are defined as abbreviations. The raw tree is not quotiented, so syntactically distinct trees are distinct values even when they would evaluate the same way in any lawful OpenTheory; Raw.map (Hom.id Δ) e is a fresh .map node, not definitionally equal to e.

The quotient of Raw by the OpenTheory equations is defined in OpenSyntax.Expr. The tagless-final (Church-encoded) companion is defined in OpenSyntax.Interp.

Main definitions

• Raw: inductive syntax tree for open-system expressions.
• Raw.interpret: structural recursion into any target OpenTheory.
• Raw.Equiv: the smallest equivalence relation containing the OpenTheory equations and closed under all constructors.
• Raw.setoid: packages Raw.Equiv as a Setoid.

inductive Interaction.UC.OpenSyntax.Raw (Atom : PortBoundary → Type u) : PortBoundary → Type (u + 1)

Raw Atom Δ is the raw syntax tree for open-system expressions of boundary Δ generated by primitive atoms Atom.

The five native constructors form the minimal generating set for a compact closed open-system algebra. The derived operations plug and unit are abbreviations defined below.

See Expr for the quotiented version.

• atom {Atom : PortBoundary → Type u} {Δ : PortBoundary} : Atom Δ → Raw Atom Δ

  Inject a primitive open component.

• map {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} : Δ₁.Hom Δ₂ → Raw Atom Δ₁ → Raw Atom Δ₂

  Adapt the exposed boundary along a structural morphism.

• par {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} : Raw Atom Δ₁ → Raw Atom Δ₂ → Raw Atom (Δ₁.tensor Δ₂)

  Place two open systems side by side.

• wire {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} : Raw Atom (Δ₁.tensor Γ) → Raw Atom (Γ.swap.tensor Δ₂) → Raw Atom (Δ₁.tensor Δ₂)

  Connect one shared boundary between two open systems.

• idWire {Atom : PortBoundary → Type u} (Γ : PortBoundary) : Raw Atom (Γ.swap.tensor Γ)

  The identity wire (coevaluation) on boundary Γ.

@[reducible, inline]

abbrev Interaction.UC.OpenSyntax.Raw.unit {Atom : PortBoundary → Type u} : Raw Atom PortBoundary.empty

The monoidal unit: idWire on the trivial boundary, mapped through a unitor. Derived from the two primitives map and idWire.

@[reducible, inline]

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

Close an open system against a matching context. Derived from wire by embedding both operands into a tensored boundary and collapsing via a unitor.

def Interaction.UC.OpenSyntax.Raw.interpret {Atom : PortBoundary → Type u} {Δ : PortBoundary} (e : Raw Atom Δ) (T : OpenTheory) (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) (idWireVal : (Γ : PortBoundary) → T.Obj (Γ.swap.tensor Γ)) : T.Obj Δ

Interpret a raw expression in an arbitrary target open theory.

This is structural recursion: each constructor maps to the corresponding OpenTheory operation. The target theory need not be lawful; lawfulness is only required when reasoning about equivalence of interpretations.

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.interpret_atom {Atom : PortBoundary → Type u} {T : OpenTheory} {interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ} {idWireVal : (Γ : PortBoundary) → T.Obj (Γ.swap.tensor Γ)} {Δ : PortBoundary} (a : Atom Δ) : (atom a).interpret T (fun {Δ : PortBoundary} => interp) idWireVal = interp a

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.interpret_map {Atom : PortBoundary → Type u} {T : OpenTheory} {interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ} {idWireVal : (Γ : PortBoundary) → T.Obj (Γ.swap.tensor Γ)} {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (e : Raw Atom Δ₁) : (map f e).interpret T (fun {Δ : PortBoundary} => interp) idWireVal = T.map f (e.interpret T (fun {Δ : PortBoundary} => interp) idWireVal)

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.interpret_par {Atom : PortBoundary → Type u} {T : OpenTheory} {interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ} {idWireVal : (Γ : PortBoundary) → T.Obj (Γ.swap.tensor Γ)} {Δ₁ Δ₂ : PortBoundary} (e₁ : Raw Atom Δ₁) (e₂ : Raw Atom Δ₂) : (e₁.par e₂).interpret T (fun {Δ : PortBoundary} => interp) idWireVal = T.par (e₁.interpret T (fun {Δ : PortBoundary} => interp) idWireVal) (e₂.interpret T (fun {Δ : PortBoundary} => interp) idWireVal)

@[simp]

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

@[simp]

theorem Interaction.UC.OpenSyntax.Raw.interpret_idWire {Atom : PortBoundary → Type u} {T : OpenTheory} {interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ} {idWireVal : (Γ : PortBoundary) → T.Obj (Γ.swap.tensor Γ)} (Γ : PortBoundary) : (idWire Γ).interpret T (fun {Δ : PortBoundary} => interp) idWireVal = idWireVal Γ

inductive Interaction.UC.OpenSyntax.Raw.Equiv {Atom : PortBoundary → Type u} {Δ : PortBoundary} : Raw Atom Δ → Raw Atom Δ → Prop

Raw.Equiv e₁ e₂ is the smallest equivalence relation on raw expressions at the same boundary that contains the OpenTheory equations and is closed under all constructors.

The equation constructors capture functoriality of map, naturality of par and wire, monoidal coherence (par_assoc, par_comm, unit laws), and the zig-zag identity (wire_idWire). The congruence constructors ensure that equivalent sub-expressions can be substituted anywhere in a larger tree.

Since plug and unit are abbreviations, laws like plug_eq_wire and congr_plug are now definitional and do not need dedicated constructors.

• refl {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e : Raw Atom Δ} : e.Equiv e
• symm {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e₁ e₂ : Raw Atom Δ} : e₁.Equiv e₂ → e₂.Equiv e₁
• trans {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e₁ e₂ e₃ : Raw Atom Δ} : e₁.Equiv e₂ → e₂.Equiv e₃ → e₁.Equiv e₃
• map_id {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e : Raw Atom Δ} : (map (PortBoundary.Hom.id Δ) e).Equiv e
• map_comp {Atom : PortBoundary → Type u} {Δ₁ Δ₂ Δ₃ : PortBoundary} {g : Δ₂.Hom Δ₃} {f : Δ₁.Hom Δ₂} {e : Raw Atom Δ₁} : (map (g.comp f) e).Equiv (map g (map f e))
• map_par {Atom : PortBoundary → Type u} {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} {f₁ : Δ₁.Hom Δ₁'} {f₂ : Δ₂.Hom Δ₂'} {e₁ : Raw Atom Δ₁} {e₂ : Raw Atom Δ₂} : (map (f₁.tensor f₂) (e₁.par e₂)).Equiv ((map f₁ e₁).par (map f₂ e₂))
• map_wire {Atom : PortBoundary → Type u} {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} {f₁ : Δ₁.Hom Δ₁'} {f₂ : Δ₂.Hom Δ₂'} {e₁ : Raw Atom (Δ₁.tensor Γ)} {e₂ : Raw Atom (Γ.swap.tensor Δ₂)} : (map (f₁.tensor f₂) (e₁.wire e₂)).Equiv ((map (f₁.tensor (PortBoundary.Hom.id Γ)) e₁).wire (map ((PortBoundary.Hom.id Γ.swap).tensor f₂) e₂))
• map_plug {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} {f : Δ₁.Hom Δ₂} {e : Raw Atom Δ₁} {k : Raw Atom Δ₂.swap} : ((map f e).plug k).Equiv (e.plug (map f.swap k))
• par_assoc {Atom : PortBoundary → Type u} {Δ₁ Δ₂ Δ₃ : PortBoundary} {e₁ : Raw Atom Δ₁} {e₂ : Raw Atom Δ₂} {e₃ : Raw Atom Δ₃} : (map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom ((e₁.par e₂).par e₃)).Equiv (e₁.par (e₂.par e₃))
• par_comm {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} {e₁ : Raw Atom Δ₁} {e₂ : Raw Atom Δ₂} : (map (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom (e₁.par e₂)).Equiv (e₂.par e₁)
• par_leftUnit {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e : Raw Atom Δ} : (map (PortBoundary.Equiv.tensorEmptyLeft Δ).toHom (unit.par e)).Equiv e
• par_rightUnit {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e : Raw Atom Δ} : (map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (e.par unit)).Equiv e
• wire_idWire {Atom : PortBoundary → Type u} {Γ Δ₂ : PortBoundary} {e₂ : Raw Atom (Γ.swap.tensor Δ₂)} : ((idWire Γ).wire e₂).Equiv e₂
• wire_idWire_right {Atom : PortBoundary → Type u} {Γ Δ₁ : PortBoundary} {e₁ : Raw Atom (Δ₁.tensor Γ)} : (e₁.wire (idWire Γ)).Equiv e₁
• wire_assoc {Atom : PortBoundary → Type u} {Δ₁ Γ₁ Γ₂ Δ₃ : PortBoundary} {e₁ : Raw Atom (Δ₁.tensor Γ₁)} {e₂ : Raw Atom (Γ₁.swap.tensor Γ₂)} {e₃ : Raw Atom (Γ₂.swap.tensor Δ₃)} : ((e₁.wire e₂).wire e₃).Equiv (e₁.wire (e₂.wire e₃))
• wire_par_superpose {Atom : PortBoundary → Type u} {Δ₁ Δ₂ Γ Δ₃ : PortBoundary} {e₁ : Raw Atom Δ₁} {e₂ : Raw Atom (Δ₂.tensor Γ)} {e₃ : Raw Atom (Γ.swap.tensor Δ₃)} : ((map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Γ).symm.toHom (e₁.par e₂)).wire e₃).Equiv (map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).symm.toHom (e₁.par (e₂.wire e₃)))
• wire_comm {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} {e₁ : Raw Atom (Δ₁.tensor Γ)} {e₂ : Raw Atom (Γ.swap.tensor Δ₂)} : (e₁.wire e₂).Equiv (map (PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom ((map (PortBoundary.Equiv.tensorComm Γ.swap Δ₂).toHom e₂).wire (map (PortBoundary.Equiv.tensorComm Δ₁ Γ).toHom e₁)))
• plug_par_left {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} {e₁ : Raw Atom Δ₁} {e₂ : Raw Atom Δ₂} {K : Raw Atom (Δ₁.tensor Δ₂).swap} : ((e₁.par e₂).plug K).Equiv (e₁.plug (map (PortBoundary.Equiv.tensorEmptyRight Δ₁.swap).toHom (K.wire (map (PortBoundary.Equiv.tensorEmptyRight Δ₂).symm.toHom e₂))))
• plug_wire_left {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} {e₁ : Raw Atom (Δ₁.tensor Γ)} {e₂ : Raw Atom (Γ.swap.tensor Δ₂)} {K : Raw Atom (Δ₁.tensor Δ₂).swap} : ((e₁.wire e₂).plug K).Equiv (e₁.plug (K.wire (map (PortBoundary.Equiv.tensorComm Γ.swap Δ₂).toHom e₂)))
• congr_map {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} {f : Δ₁.Hom Δ₂} {e₁ e₂ : Raw Atom Δ₁} : e₁.Equiv e₂ → (map f e₁).Equiv (map f e₂)
• congr_par {Atom : PortBoundary → Type u} {Δ₁ Δ₂ : PortBoundary} {e₁ e₁' : Raw Atom Δ₁} {e₂ e₂' : Raw Atom Δ₂} : e₁.Equiv e₁' → e₂.Equiv e₂' → (e₁.par e₂).Equiv (e₁'.par e₂')
• congr_wire {Atom : PortBoundary → Type u} {Δ₁ Γ Δ₂ : PortBoundary} {e₁ e₁' : Raw Atom (Δ₁.tensor Γ)} {e₂ e₂' : Raw Atom (Γ.swap.tensor Δ₂)} : e₁.Equiv e₁' → e₂.Equiv e₂' → (e₁.wire e₂).Equiv (e₁'.wire e₂')

theorem Interaction.UC.OpenSyntax.Raw.Equiv.interpret_eq {Atom : PortBoundary → Type u} {Δ : PortBoundary} {e₁ e₂ : Raw Atom Δ} (h : e₁.Equiv e₂) (T : OpenTheory) [T.CompactClosed] (interp : {Δ : PortBoundary} → Atom Δ → T.Obj Δ) : e₁.interpret T (fun {Δ : PortBoundary} => interp) OpenTheory.CompactClosed.idWire = e₂.interpret T (fun {Δ : PortBoundary} => interp) OpenTheory.CompactClosed.idWire

Equivalent raw expressions interpret the same way in any lawful OpenTheory.

@[implicit_reducible]

instance Interaction.UC.OpenSyntax.Raw.setoid (Atom : PortBoundary → Type u) (Δ : PortBoundary) : Setoid (Raw Atom Δ)

The Setoid on Raw Atom Δ induced by Raw.Equiv.