Enriched categorical semantics for distributed calculi (Q1208210): Difference between revisions

The authors propose a general categorical framework in which many of the existing proposals for the mathematical semantics of the interaction between concurrent or parallel computations can be expressed and, therefore, compared. They propose a two-tier formalization of synchronization between (concurrent) computing agents. At the first level we find computations, described as labelled trees. Formally, they introduce the topos of labelled budding trees (constructed out of the topos of labelled \(A\)-trees, \({\mathbf T}/F(A)\), which is a monoidal category with respect to a notion of concatenation between trees. Since this topos, however, if not monoidal closed, its reflective subcategory \({\mathbf N}{\mathbf T}\) of nice trees is introduced, which turns out to be monoidal closed (but not biclosed, a fact which accounts for nondeterminism). Finally, an operation of synchronization is introduced on \({\mathbf N}{\mathbf T}\) and shown to be a monoidal functor. The second level of the proposed semantics aims to model processes and computations among them, described as enriched categories over \({\mathbf N}{\mathbf T}\). Synchronization among processes is obtained by lifting to the enriched structure the corresponding operation of the base monoidal category. Particular relevance assumes a notion of hereditary fullness, characterizing the ``good semantics''. With this set up, the concepts of relabelling, restrictions, insertion and deletion of idle moves are then described, with particular emphasis of the comparison with similar operations of other formal descriptions (e.g., CCS and ACP). The paper tries to motivate the formal notions through intuitive operations on computations and the analogy with regular languages and automata.