×

Proof nets, coends and the Yoneda isomorphism. (English) Zbl 1486.03111

Ehrhard, Thomas (ed.) et al., Proceedings of the joint international workshop on linearity & trends in linear logic and applications, Linearity-TLLA 2018, Oxford, UK, July 7–8, 2018. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 292, 148-167 (2019).
Summary: Proof nets provide permutation-independent representations of proofs and are used to investigate coherence problems for monoidal categories. We investigate a coherence problem concerning Second Order Multiplicative Linear Logic (MLL2), that is, the one of characterizing the equivalence over proofs generated by the interpretation of quantifiers by means of ends and coends.
We provide a compact representation of proof nets for a fragment of MLL2 related to the Yoneda isomorphism. By adapting the “rewiring approach” used in coherence results for star-autonomous categories, we define an equivalence relation over proof nets called “re-witnessing”. We prove that this relation characterizes, in this fragment, the equivalence generated by coends.
For the entire collection see [Zbl 1436.68024].

MSC:

03F52 Proof-theoretic aspects of linear logic and other substructural logics
03F05 Cut-elimination and normal-form theorems
03G30 Categorical logic, topoi
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] E.S. Bainbridge, Peter J. Freyd, Andre Scedrov & Philip J. Scott (1990): Functorial polymorphism. Theoret-ical Computer Science 70, pp. 35-64, doi:10.1016/0304-3975(90)90151-7. · Zbl 0717.18005 · doi:10.1016/0304-3975(90)90151-7
[2] Michael Barr (1979): * -Autonomous Categories. Lecture Notes in Mathematics 752, Springer-Verlag, Berlin, Heidelberg, doi:10.1007/BFb0064582. · Zbl 0415.18008 · doi:10.1007/BFb0064582
[3] R. F. Blute & P. J. Scott (1996): Linear Läuchli semantics. Ann. Pure Appl. Logic 77(2), pp. 101-142, doi:10.1016/0168-0072(95)00017-8. · Zbl 0856.03006 · doi:10.1016/0168-0072(95)00017-8
[4] Richard Blute (1991): Proof nets and coherence theorems. In P.L. Curien, S. Abramsky, A.M. Pitts, A. Poigné & D.E. Rydeheard, editors: Category Theory and Computer Science. CTCS 1991, Lecture Notes in Computer Science 530, Springer, Berlin, Heidelberg, pp. 121-137, doi:10.1007/BFb0013461. · Zbl 0795.18008 · doi:10.1007/BFb0013461
[5] Richard Blute (1993): Linear Logic, coherence and dinaturality. Theoretical Computer Science 115(1), pp. 3-41, doi:10.1016/0304-3975(93)90053-V. · Zbl 0782.18001 · doi:10.1016/0304-3975(93)90053-V
[6] Richard Blute, Robin Cockett, R.A.G. Seely & T.H. Trimble (1996): Natural deduction and coherence for weakly distributive categories. Journal of Pure and Applied Algebra 113(229), p. 296, doi:10.1016/ 0022-4049(95)00159-X. · Zbl 0858.03064 · doi:10.1016/0022-4049(95)00159-X
[7] Daniel de Carvalho & Lorenzo Tortora de Falco (2012): The relational model is injective for multiplicative exponential linear logic (without weakenings). Annals of Pure and Applied Logic 163(9), pp. 1210-1236, doi:10.1016/j.apal.2012.01.004. · Zbl 1251.03080 · doi:10.1016/j.apal.2012.01.004
[8] Lorenzo Tortora de Falco (2000): Réseaux, cohérence et expériences obsessionnelles. Ph.D. thesis, Université Paris 7.
[9] Fernando Ferreira & Gilda Ferreira (2009): Commuting conversions vs. the standard conversions of the “good” connectives. Studia Logica 92(1), pp. 63-84, doi:10.1007/s11225-009-9186-1. · Zbl 1185.03081 · doi:10.1007/s11225-009-9186-1
[10] Fernando Ferreira & Gilda Ferreira (2013): Atomic polymorphism. Journal of Symbolic Logic 78(1), pp. 260-274, doi:10.1007/s10992-005-9001-z. · Zbl 1101.03014 · doi:10.1007/s10992-005-9001-z
[11] M.P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini & I. Stark (1996): Domains and denota-tional semantics: history, accomplishments and open problems. Bulletin EATCS 59, pp. 227-256.
[12] Jürgen Fuchs, Christoph Schweigert & Carl Stigner (2012): Modular invariant Frobenius algebras from ribbon Hopf algebra automorphisms. Journal of Algebra 363, pp. 29-72, doi:10.1016/j.jalgebra.2012. 04.008. · Zbl 1296.16029 · doi:10.1016/j.jalgebra.2012.04.008
[13] Jean-Yves Girard (1987): Linear logic. Theoretical Computer Science 50(1), pp. 1-102, doi:10.1016/ 0304-3975(87)90045-4. · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[14] Jean-Yves Girard (1988): Quantifiers in Linear Logic. In: Atti del congresso “Temi e Prospettive della Logica e della Filosofia della Scienza”, Cesena, 7-10 Gennaio 1987, CLUEB, Bologna.
[15] Jean-Yves Girard (1991): Quantifiers in Linear Logic II. In: Atti del congresso “Nuovi Problemi della Logica e della Filosofia della Scienza”, Viareggio, 8-13 Gennatio 1990, CLUEB, Bologna.
[16] Jean-Yves Girard, Andre Scedrov & Philip J. Scott (1992): Normal forms and cut-free proofs as natural transformations. In Y. Moschovakis, editor: Logic from Computer Science, 21, Springer-Verlag, pp. 217-241, doi:10.1007/978-1-4612-2822-6_8. · Zbl 0753.03024 · doi:10.1007/978-1-4612-2822-6_8
[17] Rye Hasegawa (2009): Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science 4(1), pp. 71-109, doi:10.1016/S0049-237X(08)70843-7. · Zbl 0802.68083 · doi:10.1016/S0049-237X(08)70843-7
[18] Willem Heijltjes & Robin Houston (2014): No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete. In: CSL-LICS 2014, doi:10.1145/2603088.2603126. · Zbl 1395.03036 · doi:10.1145/2603088.2603126
[19] Willem Heijltjes & Luz Straßburger (2016): Proof nets and semi-star-autonomous categories. Mathematical Structures in Computer Science 26(5), pp. 789-828, doi:10.1016/0001-8708(91)90003-P. · Zbl 0738.18005 · doi:10.1016/0001-8708(91)90003-P
[20] Robin Houston, Dominic Hughes & Andrea Schalk (2017): Modeling Linear Logic without Units (Prelimi-nary Results). https://arxiv.org/pdf/math/0504037.pdf.
[21] Dominic J.D. Hughes: Unification nets: canonical proof net quantifiers. https://arxiv.org/abs/1802. 03224. · Zbl 1452.03134
[22] Dominic J.D. Hughes (2012): Simple free star-autonomous categories and full coherence. Journal of Pure and Applied Algebra 216(11), pp. 2386-2410, doi:10.1016/j.jpaa.2012.03.020. · Zbl 1264.18009 · doi:10.1016/j.jpaa.2012.03.020
[23] Thomas Kerler & Volodymyr V. Lyubashenko (2001): Coends and construction of Hopf algebras. In: Non-Semisimple Topological Quantum Field Theoreis for 3-Manifols with Corners, chapter 5, Lecture Notes in Mathematics 1765, Springer, Berlin, Heidelberg, doi:10.1007/3-540-44625-7_6. · Zbl 0982.57013 · doi:10.1007/3-540-44625-7_6
[24] François Lamarche & Luz Straßburger (2004): On proof nets for multiplicative linear logic with units. In: CSL 2004, Lecture Notes in Computer Science 3210, pp. 145-159, doi:10.1007/978-3-540-30124-0_14. · Zbl 1095.03072 · doi:10.1007/978-3-540-30124-0_14
[25] François Lamarche & Luz Straßburger (2006): From Proof Nets to the Free * -Autonomous Category. Logical Methods in Computer Science 2(4), doi:10.2168/LMCS-2(4:3)2006. · Zbl 1127.03044 · doi:10.2168/LMCS-2(4:3)2006
[26] Joachim de Lataillade (2009): Dinatural terms in System F. In: Proceedings of the Twenty-Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 2009), IEEE Computer Society Press, Los Angeles, California, USA, pp. 267-276, doi:10.1109/LICS.2009.30. · doi:10.1109/LICS.2009.30
[27] Fosco Loregian (2015): This is the (co)end, my only (co)friend. https://arxiv.org/abs/1501.02503. · Zbl 07344233
[28] Saunders MacLane (1978): Categories for the working mathematicians. Graduate Texts in Mathematics 5, Springer-Verlag, New York, doi:10.1007/978-1-4757-4721-8. · Zbl 0705.18001 · doi:10.1007/978-1-4757-4721-8
[29] Richard McKinley (2013): Proof nets for Herbrand’s theorem. ACM Transactions on Computational Logic 14(1), doi:10.1145/2422085.2422090. · Zbl 1354.03085 · doi:10.1145/2422085.2422090
[30] Paul-André Melliès (2012): Game semantics in string diagrams. In: LICS ’12, New Orleans, Louisiana, pp. 481-490, doi:10.1109/LICS.2012.58. · Zbl 1364.03083 · doi:10.1109/LICS.2012.58
[31] Paul-André Melliès & Noam Zeilberger (2016): A bifibrational reconstruction of Lawvere’s presheaf hyper-doctrine. In: LICS ’16, New York, pp. 555-564, doi:10.1145/2933575.2934525. · Zbl 1395.03040 · doi:10.1145/2933575.2934525
[32] Paolo Pistone (2018): Proof nets and the instantiation overflow property. https://arxiv.org/abs/1803. 09297. · Zbl 1496.03023
[33] Gordon Plotkin & Martin Abadi (1993): A logic for parametric polymorphism. In: TLCA ’93, International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 664, Springer Berlin Heidelberg, pp. 361-375, doi:10.1007/BFb0037118. · Zbl 0788.68091 · doi:10.1007/BFb0037118
[34] R.A.G. Seely (1990): Polymorphic linear logic and topos models. Comptes Rendus Mathématiques de l’Académie des Sciences Canada 12(1). · Zbl 0701.03012
[35] Luz Straßburger (2009): Some Observations on the Proof Theory of Second Order Propositional Multiplica-tive Linear Logic. In P.L. Curien, editor: TLCA 2009, Lecture Notes in Computer Science 5608, pp. 309-324, doi:10.1007/BF01622878. · Zbl 0689.03013 · doi:10.1007/BF01622878
[36] Luca Tranchini, Paolo Pistone & Mattia Petrolo (2017): The naturality of natural deduction. Studia Logica, doi:10.1007/s11225-017-9772-6. · Zbl 07055417 · doi:10.1007/s11225-017-9772-6
[37] Todd Trimble (1994): Linear logic, bimodules, and full coherence for autonomous categories. Ph.D. thesis, Rutgers University.
[38] Tarmo Uustalu & Varmo Vene (2011): The Recursion Scheme from the Cofree Recursive Comonad. Elec-tronic Notes in Theoretical Computer Science 229(5), pp. 135-157, doi:10.1016/j.entcs.2011.02.020. · Zbl 1291.68149 · doi:10.1016/j.entcs.2011.02.020
[39] A * -autonomous categories and coends We recall that a * -autonomous category is a category C endowed with functors_⊗_: C 2 → C and_⊥ : C op → C, an object 1 C , the following natural isomorphisms:
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.