Concrete OpenTheory model backed by OpenProcess m

This file provides the first concrete realization of UC.OpenTheory using actual open processes (OpenProcess m Party Δ), i.e., processes that carry a per-step nodewise-monadic sampler in the intermediate monad m.

Implemented operations

• map adapts boundary actions along a PortBoundary.Hom, with a proven IsLawfulMap instance (functoriality). The per-step sampler is left unchanged; only the boundary-action decoration is pushed forward.

• 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. The scheduler move is resolved by the theory's shared schedulerSampler : m (ULift Bool); per-branch samplers are assembled via Spec.Sampler.interleave.

• 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. Samplers are threaded the same way as for par.

• plug closes an open system against a matching context by internalizing all boundary traffic. Samplers are again threaded via the scheduler-interleaving pattern.

def Interaction.UC.openTheory (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) : OpenTheory

The concrete open-composition theory backed by OpenProcess m.

• Obj Δ is OpenProcess m Party Δ, the boundary-indexed family of open concurrent processes carrying per-step m-samplers.
• map adapts boundary actions along a PortBoundary.Hom, preserving samplers verbatim.
• par, wire, and plug all use OpenProcess.interleave with the appropriate context morphisms and thread the shared schedulerSampler through Spec.Sampler.interleave.

instance Interaction.UC.lawfulMap_openTheory (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) : (openTheory Party m schedulerSampler).IsLawfulMap

instance Interaction.UC.lawfulPar_openTheory (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) : (openTheory Party m schedulerSampler).IsLawfulPar

instance Interaction.UC.lawfulWire_openTheory (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) : (openTheory Party m schedulerSampler).IsLawfulWire

instance Interaction.UC.lawfulPlug_openTheory (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) : (openTheory Party m schedulerSampler).IsLawfulPlug

instance Interaction.UC.instIsLawfulOpenTheory (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) : (openTheory Party m schedulerSampler).IsLawful

Monoidal and compact closed laws up to bisimilarity

theorem Interaction.UC.openTheory_par_assoc_iso (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) {Δ₁ Δ₂ Δ₃ : PortBoundary} (W₁ : OpenProcess m Party Δ₁) (W₂ : OpenProcess m Party Δ₂) (W₃ : OpenProcess m Party Δ₃) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom ((openTheory Party m schedulerSampler).par ((openTheory Party m schedulerSampler).par W₁ W₂) W₃)) ((openTheory Party m schedulerSampler).par W₁ ((openTheory Party m schedulerSampler).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) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) {Δ₁ Δ₂ : PortBoundary} (W₁ : OpenProcess m Party Δ₁) (W₂ : OpenProcess m Party Δ₂) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom ((openTheory Party m schedulerSampler).par W₁ W₂)) ((openTheory Party m schedulerSampler).par W₂ W₁)

Parallel composition of open processes is commutative up to bisimilarity.

def Interaction.UC.openTheory_unit (Party : Type u) (m : Type w → Type w') : OpenProcess m Party PortBoundary.empty

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

theorem Interaction.UC.openTheory_par_leftUnit_iso (Party : Type u) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) {Δ : PortBoundary} (W : OpenProcess m Party Δ) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft Δ).toHom ((openTheory Party m schedulerSampler).par (openTheory_unit Party m) 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) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) {Δ : PortBoundary} (W : OpenProcess m Party Δ) : OpenProcessIso (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyRight Δ).toHom ((openTheory Party m schedulerSampler).par W (openTheory_unit Party m))) W

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

def Interaction.UC.openTheory_idWire (Party : Type u) (m : Type w → Type w') (Γ : PortBoundary) : OpenProcess m 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) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) (Γ : PortBoundary) {Δ₂ : PortBoundary} (W₂ : OpenProcess m Party (Γ.swap.tensor Δ₂)) : OpenProcessIso ((openTheory Party m schedulerSampler).wire (openTheory_idWire Party m Γ) 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) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) (Γ : PortBoundary) {Δ₁ : PortBoundary} (W₁ : OpenProcess m Party (Δ₁.tensor Γ)) : OpenProcessIso ((openTheory Party m schedulerSampler).wire W₁ (openTheory_idWire Party m Γ)) 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) (m : Type w → Type w') (schedulerSampler : m (ULift.{w, 0} Bool)) {Δ : PortBoundary} (W : OpenProcess m Party Δ) (K : OpenProcess m Party Δ.swap) : OpenProcessIso ((openTheory Party m schedulerSampler).plug W K) (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom ((openTheory Party m schedulerSampler).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) (m : Type w → Type w') : OpenProcessIso (openTheory_unit Party m) (OpenProcess.mapBoundary (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (openTheory_idWire Party m PortBoundary.empty))

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