Semantic Proof of Confluence of the Categorical Reduction System for Linear Logic

TL;DR

This paper proves confluence and coherence for a rewriting calculus in linear categories, providing a method to determine morphism equivalence, which advances the understanding of categorical structures in linear logic.

Contribution

It introduces a confluence proof for the categorical reduction system in linear logic, complementing previous termination results to establish a generalized coherence theorem.

Findings

Proves confluence of the rewriting calculus in linear categories

Establishes a generalized coherence theorem for linear categories

Provides a method to determine morphism equality up to a certain equivalence

Abstract

We verify a confluence result for the rewriting calculus of the linear category introduced in our previous paper. Together with the termination result proved therein, the generalized coherence theorem for linear category is established. Namely, we obtain a method to determine if two morphisms are equal up to a certain equivalence.