A sequent calculus for compact closed categories
作者： Masaru Shirahata
DOI:
关键词:
摘要: In this paper, we introduce the system CMLL of sequent calculus and establish its correspondence with compact closed categories. is equivalent in provability to MLL classical linear logic tensor par connectives identified. We show that allows a fairly simple cut-elimination, proofs have natural interpretation However, soundness cut-elimination procedure terms categorical by no means evident. answer question affirmatively using coherence result on categories Kelly Laplaza.
参考文章(7)
G. M. Kelly, Many-variable functorial calculus. I. Coherence in Categories. pp. 66- 105 ,(1972) , 10.1007/BFB0059556
G. M. Kelly, An abstract approach to coherence Coherence in Categories. pp. 106- 147 ,(1972) , 10.1007/BFB0059557
G.M. Kelly, M.L. Laplaza, Coherence for compact closed categories Journal of Pure and Applied Algebra. ,vol. 19, pp. 193- 213 ,(1980) , 10.1016/0022-4049(80)90101-2
S.V. Soloviev, On natural transformations of distinguished functors and their superpositions in certain closed categories Journal of Pure and Applied Algebra. ,vol. 47, pp. 181- 204 ,(1987) , 10.1016/0022-4049(87)90061-2
Richard Blute, Linear logic, coherence and dinaturality Theoretical Computer Science. ,vol. 115, pp. 3- 41 ,(1993) , 10.1016/0304-3975(93)90053-V
Robin Milner, Calculi for interaction Acta Informatica. ,vol. 33, pp. 707- 737 ,(1996) , 10.1007/BF03036472
Samson Abramsky, SJ Gay, R Nagarajan, Interaction Categories formal methods. pp. 57- 69 ,(1993)