Dynamics and Coherence for the Free Cornering with Protocol Choice

TL;DR

This paper introduces a term rewriting system for modeling process interactions in monoidal categories, proving confluence, termination, and coherence in the context of free cornering with protocol choice.

Contribution

It presents a novel term rewriting framework that ensures confluence and termination, leading to a coherence theorem for free cornering with protocol choice.

Findings

Rewrites are confluent and terminating.

Established a coherence theorem for the categorical model.

Provides a formal tool for process interaction analysis.

Abstract

We present a term rewriting system that models the dynamic aspects of the free cornering with protocol choice of a monoidal category, which has been proposed as a categorical model of process interaction. This term rewriting system is confluent and terminating in an appropriate sense. We use this machinery to prove a coherence theorem for the free cornering with protocol choice.