Document Open Access Logo

Coherence by Normalization for Linear Multicategorical Structures

Author Federico Olimpieri

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.43.pdf
  • Filesize: 0.8 MB
  • 17 pages

Document Identifiers

Author Details

Federico Olimpieri
  • School of Mathematics, University of Leeds, UK

Funding

  • Olimpieri, Federico: This work was supported by the US Air Force Office for Scientific Research under award number FA9550-21-1-0007.

Cite AsGet BibTex

Federico Olimpieri. Coherence by Normalization for Linear Multicategorical Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 43:1-43:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.43

Abstract

We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane’s coherence theorems for (symmetric) monoidal categories.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • Coherence
  • Linear Multicategories
  • Resource Calculi
  • Normalization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Beniamino Accattoli. Exponentials as substitutions and the cost of cut elimination in linear logic. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2-5, 2022, pages 49:1-49:15. ACM, 2022. URL: https://doi.org/10.1145/3531130.3532445.
  2. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  3. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes scott, berry, kahn and plotkin. Proc. ACM Program. Lang., 4(POPL):1:1-1:23, 2020. URL: https://doi.org/10.1145/3371069.
  4. Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. In Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA). Springer, January 1993. Google Scholar
  5. R.F. Blute, J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble. Natural deduction and coherence for weakly distributive categories. Journal of Pure and Applied Algebra, 113(3):229-296, 1996. URL: https://doi.org/10.1016/0022-4049(95)00159-X.
  6. Gérard Boudol. The lambda-calculus with multiplicities. In Eike Best, editor, CONCUR'93, pages 1-6, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  7. Pierre-Louis Curien, Richard Garner, and Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. Theoretical Computer Science, 546:99-119, 2014. Models of Interaction: Essays in Honour of Glynn Winskel. URL: https://doi.org/10.1016/j.tcs.2014.03.003.
  8. Roberto Di Cosmo and Delia Kesner. Combining algebraic rewriting, extensional lambda calculi, and fixpoints. Theoretical Computer Science, 169(2):201-220, 1996. URL: https://doi.org/10.1016/S0304-3975(96)00121-1.
  9. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary λ-terms. Theoretical Computer Science, 403(2-3), 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  10. Marcelo Fiore and Philip Saville. Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 425-439. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394769.
  11. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  12. Claudio Hermida. Representable multicategories. Advances in Mathematics, 151(2):164-225, 2000. URL: https://doi.org/10.1006/aima.1999.1877.
  13. Dominic J.D. Hughes. Simple free star-autonomous categories and full coherence. Journal of Pure and Applied Algebra, 216(11):2386-2410, 2012. URL: https://doi.org/10.1016/j.jpaa.2012.03.020.
  14. J. M. E. Hyland. Classical lambda calculus in modern dress. Mathematical Structures in Computer Science, 27(5):762-781, 2017. URL: https://doi.org/10.1017/S0960129515000377.
  15. J.M.E. Hyland. Elements of a theory of algebraic theories. Theoretical Computer Science, 546:132-144, 2014. Models of Interaction: Essays in Honour of Glynn Winskel. URL: https://doi.org/10.1016/j.tcs.2014.03.005.
  16. C. Barry Jay and Neil Ghani. The virtues of eta-expansion. Journal of Functional Programming, 5(2):135-154, 1995. URL: https://doi.org/10.1017/S0956796800001301.
  17. G.M. Kelly and S. Maclane. Coherence in closed categories. Journal of Pure and Applied Algebra, 1(1):97-140, 1971. URL: https://doi.org/10.1016/0022-4049(71)90013-2.
  18. Delia Kesner. The theory of calculi with explicit substitutions revisited. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 238-252, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  19. AJ Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411-436, 2000. URL: https://doi.org/10.1093/logcom/10.3.411.
  20. Yves Lafont. Logiques, Categories & Machines: Implantation de Langages de Programmation guidée par la Logique Catégorique. Phd thesis, Université Paris VII, 1988. Google Scholar
  21. Joachim Lambek. Deductive systems and categories ii. standard constructions and closed categories. In Peter J. Hilton, editor, Category Theory, Homology Theory and their Applications I, pages 76-122, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. Google Scholar
  22. Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, USA, 1986. Google Scholar
  23. Tom Leinster. Higher operads, higher categories, 2003. URL: https://arxiv.org/abs/math/0305049.
  24. Saunders Maclane. Natural associativity and commutativity. Rice Institute Pamphlet - Rice University Studies, 49:28-46, 1963. Google Scholar
  25. Damiano Mazza. Polyadic Approximations in Logic and Computation. Habilitation thesis, Université Paris 13, 2017. Google Scholar
  26. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. PACMPL, 2018. URL: https://doi.org/10.1145/3158094.
  27. Paul-André Melliès, Federico Olimpieri, and Lionel Vaux Auclair. An explicit construction of the homotopy span model of differential linear logic. Google Scholar
  28. G. E. Mints. Closed categories and the theory of proofs. Journal of Soviet Mathematics, 1981. URL: https://doi.org/10.1007/BF01404107.
  29. Yo Ohta and Masahito Hasegawa. A terminating and confluent linear lambda calculus. In Frank Pfenning, editor, Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, volume 4098 of Lecture Notes in Computer Science, pages 166-180. Springer, 2006. URL: https://doi.org/10.1007/11805618_13.
  30. Federico Olimpieri. Intersection Types and Resource Calculi in the Denotational Semantics of Lambda-Calculus. PhD thesis, Aix-Marseille Université, 2020. Google Scholar
  31. P. Selinger. A Survey of Graphical Languages for Monoidal Categories, pages 289-355. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  32. Michael Shulman. Categorical logic from a categorical point of view. Draft for AARMS Summer School 2016, 2016. URL: https://mikeshulman.github.io/catlog/catlog.pdf.
  33. Michael Shulman. A practical type theory for symmetric monoidal categories. Theory and Applications of Categories, 37(25):863-907, 2021. Google Scholar
  34. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In Proceedings of the 32rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, 2017. URL: https://doi.org/10.1109/LICS.2017.8005093.
  35. Lionel Vaux. Taylor expansion, β-reduction and normalization. In Ccomputer Science Logic 2017, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.39.
  36. Niccolò Veltri. Coherence via focusing for symmetric skew monoidal categories. In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, pages 184-200. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_12.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact