A categorical reduction system for linear logic

TL;DR

This paper introduces a rewriting calculus for the categorical semantics of linear logic, enabling mechanical diagram chasing and verification of morphism equality, thus advancing the mechanization of categorical reasoning.

Contribution

It develops a new calculus on the free category of linear logic semantics, facilitating diagram chasing through rewriting rules and proving its weak termination.

Findings

The calculus enables one-way diagram chasing computations.

Weak termination of the calculus is verified.

First step towards mechanized diagram chasing in linear logic.

Abstract

Diagram chasing is not an easy task. The coherence holds in a generalized sense if we have a mechanical method to judge whether given two morphisms are equal to each other. A simple way to this end is to reform a concerned category into a calculus, where the instructions for the diagram chasing are given in the form of rewriting rules. We apply this idea to the categorical semantics of the linear logic. We build a calculus directly on the free category of the semantics. It enables us to perform diagram chasing as essentially one-way computations led by the rewriting rules. We verify the weak termination property of this calculus. This gives the first step towards the mechanization of diagram chasing.