#
A Categorical Reduction System for Linear Logic

##
Ryu Hasegawa

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.

Keywords:
type theory, linear logic, rewriting system

2020 MSC:
03B40, 68N18

*Theory and Applications of Categories,*
Vol. 35, 2020,
No. 50, pp 1833-1870.

Published 2020-11-16.

http://www.tac.mta.ca/tac/volumes/35/50/35-50.pdf

TAC Home