Geodesic
A Categorical Reduction System for Linear Logic
Theory and applications of categories, Tome 35 (2020), pp. 1833-1870

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.

Publié le :
Classification : 03B40, 68N18
Keywords: type theory, linear logic, rewriting system 
@article{TAC_2020_35_a49,
     author = {Ryu Hasegawa},
     title = {A {Categorical} {Reduction} {System} for {Linear} {Logic}},
     journal = {Theory and applications of categories},
     pages = {1833--1870},
     publisher = {mathdoc},
     volume = {35},
     year = {2020},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2020_35_a49/}
}
TY  - JOUR
AU  - Ryu Hasegawa
TI  - A Categorical Reduction System for Linear Logic
JO  - Theory and applications of categories
PY  - 2020
SP  - 1833
EP  - 1870
VL  - 35
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2020_35_a49/
LA  - en
ID  - TAC_2020_35_a49
ER  - 
%0 Journal Article
%A Ryu Hasegawa
%T A Categorical Reduction System for Linear Logic
%J Theory and applications of categories
%D 2020
%P 1833-1870
%V 35
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2020_35_a49/
%G en
%F TAC_2020_35_a49
Ryu Hasegawa. A Categorical Reduction System for Linear Logic. Theory and applications of categories, Tome 35 (2020), pp. 1833-1870. http://geodesic.mathdoc.fr/item/TAC_2020_35_a49/