A Simple Categorical Calculus of Interacting Processes

TL;DR

This paper introduces a simple process calculus modeled by a rewrite system, which is shown to be confluent and terminating, and relates it to a double categorical model of process interaction.

Contribution

It presents a new process calculus with a categorical semantics, establishing confluence, termination, and a functorial relation to a double categorical model.

Findings

Calculus is confluent and terminating.

Terms modulo convertibility form a virtual double category.

Provides a sound denotational semantics via a functor.

Abstract

We present a calculus that models a simple sort of process interaction. Our calculus consists of a collection of terms together with a rewrite relation, parameterised by an arbitrary multicategory whose morphisms we understand as non-interactive processes. We show that our calculus is confluent and terminating, and that terms modulo the induced convertibility relation form a virtual double category. We relate our calculus to the free cornering of a monoidal category, which is a double-categorical model of process interaction that is similar in spirit to the calculus presented herein. Precisely, we construct a functor from the virtual double category given by our calculus into the underlying virtual double category of the free cornering of the free monoidal category on the multicategory of non-interacting processes. If we think of the terms of our calculus as programs and the rewriting system as an operational semantics for these programs, this functor gives a sound denotational semantics for our calculus in terms of the free cornering.