Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Simple Categorical Calculus of Interacting Processes

Chad Nester, Niels Voorneveld

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.

A Simple Categorical Calculus of Interacting Processes

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.
Paper Structure (31 sections, 17 theorems, 47 equations, 3 figures)

This paper contains 31 sections, 17 theorems, 47 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Organisation
  3. Prerequisites
  4. Related Work
  5. The Free Cornering of A Monoidal Category
  6. The Term Calculus
  7. Sequent Calculus for Multicategories
  8. Terms
  9. Rewrite Rules
  10. Termination and Confluence
  11. A Virtual Double Category of Terms
  12. Concluding Remarks
  13. Proofs
  14. Lemma \ref{['lem:substitution-coherent']}
  15. Lemma \ref{['lem:interpretation-coherent']}
  16. ...and 16 more sections

Key Result

Lemma 3.7

$\llbracket \textsf{let } x_1 ,\!\ldots\!, x_n \downarrow ([v_1] \mid \cdots \mid [v_n]) \textsf{ in } t \rrbracket = \llbracket t[v_1 ,\!\ldots\!, v_n / x_1 ,\!\ldots\!, x_n]\rrbracket$ whenever this makes sense.

Figures (3)

  • Figure 1: Term formation rules for $T(\mathcal{M})$.
  • Figure 2: Interpretation of terms in $T(\mathcal{M})$ as cells of ${^\ulcorner_\llcorner\!{F(\mathcal{M})}\!_\lrcorner^\urcorner}$.
  • Figure 3: Generating rewrites for $\to$.

Theorems & Definitions (30)

  • Definition 2.1
  • Definition 2.2
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Example 3.5
  • Example 3.6
  • Lemma 3.7
  • Lemma 3.8
  • ...and 20 more