Semantic Proof of Confluence of the Categorical Reduction System for Linear Logic
Category Theory
2021-05-04 v1 Programming Languages
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.
Keywords
Cite
@article{arxiv.2105.00399,
title = {Semantic Proof of Confluence of the Categorical Reduction System for Linear Logic},
author = {Ryu Hasegawa},
journal= {arXiv preprint arXiv:2105.00399},
year = {2021}
}