Concrete OpenTheory model backed by OpenProcess

This file provides the first concrete realization of UC.OpenTheory using actual open processes (OpenProcess Party Δ).

Implemented operations

• map adapts boundary actions along a PortBoundary.Hom, with a proven IsLawfulMap instance (functoriality).

• par places two open processes side by side using binary-choice interleaving: a scheduling node chooses left or right, then runs the selected subprocess's step protocol. Emitted packets are injected into the appropriate summand of the tensor output interface.

• wire connects a shared internal boundary between two processes. Packets on the shared boundary are filtered out (deferred to runtime routing), while packets on the remaining external boundaries are preserved.

• plug closes an open system against a matching context by internalizing all boundary traffic.

def Interaction.UC.openTheory (Party : Type u) : OpenTheory

The concrete open-composition theory backed by OpenProcess.

• Obj Δ is OpenProcess Party Δ, the boundary-indexed family of open concurrent processes.
• map adapts boundary actions along a PortBoundary.Hom.
• par, wire, and plug all use ProcessOver.interleave with the appropriate context morphisms.

instance Interaction.UC.instIsLawfulMapOpenTheory (Party : Type u) : (openTheory Party).IsLawfulMap

instance Interaction.UC.instIsLawfulParOpenTheory (Party : Type u) : (openTheory Party).IsLawfulPar

instance Interaction.UC.instIsLawfulWireOpenTheory (Party : Type u) : (openTheory Party).IsLawfulWire

instance Interaction.UC.instIsLawfulPlugOpenTheory (Party : Type u) : (openTheory Party).IsLawfulPlug

instance Interaction.UC.instIsLawfulOpenTheory (Party : Type u) : (openTheory Party).IsLawful

theorem Interaction.UC.openTheory_par_assoc_iso (Party : Type u) {Δ₁ Δ₂ Δ₃ : PortBoundary} (W₁ : OpenProcess Party Δ₁) (W₂ : OpenProcess Party Δ₂) (W₃ : OpenProcess Party Δ₃) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom ((openTheory Party).par ((openTheory Party).par W₁ W₂) W₃)) ((openTheory Party).par W₁ ((openTheory Party).par W₂ W₃))

Parallel composition of open processes is associative up to bisimilarity: reassociating the internal scheduler nesting does not change the observable boundary behavior.

theorem Interaction.UC.openTheory_par_comm_iso (Party : Type u) {Δ₁ Δ₂ : PortBoundary} (W₁ : OpenProcess Party Δ₁) (W₂ : OpenProcess Party Δ₂) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom ((openTheory Party).par W₁ W₂)) ((openTheory Party).par W₂ W₁)

Parallel composition of open processes is commutative up to bisimilarity.

def Interaction.UC.openTheory_unit (Party : Type u) : OpenProcess Party PortBoundary.empty

The unit for parallel composition is the trivial process with no boundary and PUnit state.

theorem Interaction.UC.openTheory_par_leftUnit_iso (Party : Type u) {Δ : PortBoundary} (W : OpenProcess Party Δ) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft Δ).toHom ((openTheory Party).par (openTheory_unit Party) W)) W

The monoidal unit is a left identity for parallel composition up to bisimilarity.

theorem Interaction.UC.openTheory_par_rightUnit_iso (Party : Type u) {Δ : PortBoundary} (W : OpenProcess Party Δ) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyRight Δ).toHom ((openTheory Party).par W (openTheory_unit Party))) W

The monoidal unit is a right identity for parallel composition up to bisimilarity.

def Interaction.UC.openTheory_idWire (Party : Type u) (Γ : PortBoundary) : OpenProcess Party (Γ.swap.tensor Γ)

The identity wire (coevaluation) on boundary Γ: relays messages bidirectionally between swap Γ and Γ.

theorem Interaction.UC.openTheory_wire_idWire_iso (Party : Type u) (Γ : PortBoundary) {Δ₂ : PortBoundary} (W₂ : OpenProcess Party (Γ.swap.tensor Δ₂)) : OpenProcessIso ((openTheory Party).wire (openTheory_idWire Party Γ) W₂) W₂

Left zig-zag: wiring the identity wire on the left is a no-op up to bisimilarity.

theorem Interaction.UC.openTheory_wire_idWire_right_iso (Party : Type u) (Γ : PortBoundary) {Δ₁ : PortBoundary} (W₁ : OpenProcess Party (Δ₁.tensor Γ)) : OpenProcessIso ((openTheory Party).wire W₁ (openTheory_idWire Party Γ)) W₁

Right zig-zag: wiring the identity wire on the right is a no-op up to bisimilarity.

theorem Interaction.UC.openTheory_plug_eq_wire_iso (Party : Type u) {Δ : PortBoundary} (W : OpenProcess Party Δ) (K : OpenProcess Party Δ.swap) : OpenProcessIso ((openTheory Party).plug W K) (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom ((openTheory Party).wire (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft Δ).symm.toHom W) (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyRight Δ.swap).symm.toHom K)))

plug is derivable from wire plus boundary reshaping, up to bisimilarity.

theorem Interaction.UC.openTheory_unit_eq_iso (Party : Type u) : OpenProcessIso (openTheory_unit Party) (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (openTheory_idWire Party PortBoundary.empty))

The monoidal unit equals the coevaluation at the trivial boundary, up to bisimilarity.