The Process Corner

Process calculi model concurrent interaction — agents communicating, synchronizing, competing for resources. Category theory models composition — arrows combining, diagrams commuting, structures transforming. The connection between them is old but usually informal: processes are “like” arrows, interaction is “like” composition.

This paper makes it formal by parameterizing a term calculus over an arbitrary multicategory, proving the system confluent and terminating, and showing that terms modulo convertibility form a virtual double category. The result connects directly to the free cornering of a monoidal category, providing a sound denotational semantics.

The virtual double category is the right structure because processes have two kinds of composition: sequential (one process follows another) and parallel (processes run side by side). Ordinary categories handle one kind of composition. Double categories handle two — horizontal and vertical arrows that interact through cells. The “virtual” qualifier means certain composites exist only up to equivalence, reflecting the fact that parallel composition of processes is associative only up to behavioral equivalence, not strict equality.

The cornering construction is what makes the semantics work. It takes a monoidal category (modeling sequential and parallel composition abstractly) and produces the double category of “corners” — the places where horizontal and vertical composition meet. The functor from the process calculus into the free cornering is the semantic bridge: operational behavior (rewriting) maps faithfully to denotational structure (double-categorical composition).

Confluence and termination guarantee that the operational semantics is well-defined. The categorical semantics guarantees it means something.