Semántica categórica para subexponenciales en SELL

• Ramírez, Carlos Ernesto ^[1]
  1. [1] Universidad del Valle
• Localización: Integración: Temas de matemáticas, ISSN 0120-419X, Vol. 32, Nº. 1, 2014 (Ejemplar dedicado a: Revista Integración), págs. 39-54
• Idioma: español
• Títulos paralelos:
  • Categorical semantics for subexponentials in SELL
• Enlaces
  • Texto completo (pdf)
• Resumen
  • español

    La semántica categórica ha permitido establecer de forma precisa y formal el significado de los términos y conectivos de distintas lógicas. En particular, los trabajos de distintos autores empezando por de Paiva y Hyland [3] han permitido abordar desde el enfoque categórico la semántica de la lógica lineal, tanto clásica como intuicionista. Uno de los aspectos más relevantes consiste en intentar dar una interpretación categórica al operador exponencial !. Mellies [11] y Bierman [4] finalmente han mostrado que esta interpretación corresponde a un composición entre adjuntos monoidales. Con la aparición de SELL, ahora se cuenta con una familia de subexponenciales ajustados dentro de una estructura de preorden. Lo que se pretende en este trabajo es obtener una interpretación categórica para esta familia de subexponenciales, inspirados en la misma noción de adjuntos monoidales, pero que respete la estructura de preorden asignada para la familia de exponenciales.

  • English

    Categorical semantics have established formal and accurately the meaning of the terms and connectives of different logics. In particular, the work of various authors, starting with de Paiva and Hyland [3], have allowed to look at the semantics of linear logic, both classical and intuitionists, from a categorical point of view. One of the most important task is to try to give a categorical interpretation to the exponential operator !. Mellies [11] and Bierman [4] have finally shown that this interpretation corresponds to a composition between monoidal adjoints. With the emergence of SELL, now we have a family of subexponential, adjusted within a preorder structure. The intention in this work is to obtain a categorical interpretation for this family of subexponentials, inspired by the very notion of monoidal adjoints, but preserving the preorder structure assigned to the exponential family. 

• Referencias bibliográficas
  • Citas [1] Andreoli J.-M., “Logic Programming with Focusing Proofs in Linear Logic”, J. of Logic and Computation 2 (1992), no. 3, 297–347.
  • [2] Benton P.N., A mixed linear and non-linear logic: proofs, terms and models, Proceedings of Computer Scienca Logic 94, Springer Verlag,...
  • [3] Benton P.N., Bierman G.M., de Paiva V.C.V., Hyland J.M.E., Term assignment for intuitionist linear logic, Technical Report 262, Computer...
  • [4] Bierman G., On intuitionist linear logic, Thesis (Ph.D.), University of Cambridge, 1994.
  • [5] Danos V., Joinet J.-B. and Schellinx H., The Structure of Exponentials: Uncovering the Dynamics of Linear Logic Proofs, In Georg Gottlob,...
  • editeurs, Kurt Gödel Colloquium, 713 of LNCS, p. 159-171. Springer, 1993.
  • [6] Girard J.-Y., “Linear logic”, Theoretical Computer Science 50 (1987), 1–102.
  • [7] Kelly M., Basic concepts of enriched category theory, volume 64 of LMS, Lecture Notes. Cambridge University Press, 1982.
  • [8] Kelly M., “Doctrinal adjuntion”, Lecture Notes in Math. 420 (1974), 257–280.
  • [9] Lafont Y., Logiques, catégories et machines, Ph.D. Thesis, Université Paris 7, 1988.
  • [10] Mac Lane S., Categories for the Working Mathematician, Springer Verlag, 1971.
  • [11] Melliès P.-A., Categorical Semantics of Linear Logic, Panoramas et Synthèses 27, Société Mathématique de France, 2009.
  • [12] Melliès P.-A., Categorical semantics of linear logic, Interactive models of computation and program behaviour, Société Mathématique de...
  • [13] Nigam V., Exploiting non-canonicity in the sequent calculus, Thesis (Ph.D.), Ecole Polytechnique, 2009.
  • [14] Nigam V. and Miller D., Algorithmic specifications in linear logic with subexponentials, In ACM SIG1015 PLAN Conference on Principles...
  • [15] Pimentel E., Nigam V. and Reis G., An Extended Framework for Specifying and Reasoning about Proof Systems, submitted to Logical Journal...
  • [16] Seely R., Linear logic, *-autonomous categories and cofree coalgebras, Applications of categories in logic and computer science, Contemporary...