Hostname: page-component-6898cfcb55-zsp5v Total loading time: 0 Render date: 2026-11-11T12:14:35.608Z Has data issue: false hasContentIssue false
  • English
  • Français

An explicit formula for the free exponential modality of linear logic

Published online by Cambridge University Press:  21 April 2017

PAUL-ANDRÉ MELLIÈS,
NICOLAS TABAREAU and
CHRISTINE TASSON
PAUL-ANDRÉ MELLIÈS
Affiliation:
Univ Paris Diderot, Sorbonne Paris Cité, IRIF, UMR 8243, CNRS, F-75205 Paris, France Email: mellies@irif.fr, nicolas.tabareau@inria.fr
NICOLAS TABAREAU
Affiliation:
Univ Paris Diderot, Sorbonne Paris Cité, IRIF, UMR 8243, CNRS, F-75205 Paris, France Email: mellies@irif.fr, nicolas.tabareau@inria.fr
CHRISTINE TASSON
Affiliation:
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes - Bretagne Atlantiquezd Email: christine.tasson@irif.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

The exponential modality of linear logic associates to every formula A a commutative comonoid !A which can be duplicated in the course of reasoning. Here, we explain how to compute the free commutative comonoid !A as a sequential limit of equalizers in any symmetric monoidal category where this sequential limit exists and commutes with the tensor product. We apply this general recipe to a series of models of linear logic, typically based on coherence spaces, Conway games and finiteness spaces. This algebraic description unifies for the first time a number of apparently different constructions of the exponential modality in spaces and games. It also sheds light on the duplication policy of linear logic, and its interaction with classical duality and double negation completion.

References

Ehrhard, T. (2002). On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 (05) 579–623.Google Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 (4) 615–646.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–102.CrossRefGoogle Scholar
Girard, J.-Y. (2006). Le point aveugle: Cours de logique: Tome 1, vers la perfection. Vision des Sciences, Hermann.Google Scholar
Hyland, M. and Schalk, A. (2002). Games on graphs and sequentially realizable functionals. In: Logic in Computer Science 02, IEEE Computer Society Press, Kopenhavn, 257–264.Google Scholar
Joyal, A. (1977). Remarques sur la théorie des jeux à deux personnes. Gazette des Sciences Mathématiques du Québec 1 (4) 46–52.Google Scholar
Kelly, M. (1982). Basic Concepts of Enriched Category Theory, Lecture Notes in Mathematics, vol. 64, Cambridge University Press.Google Scholar
Kelly, M. and Laplaza, M. (1980). Coherence for compact closed categories. Journal of Pure and Applied Algebra 19 193–213.Google Scholar
Lafont, Y. (1988). Logique, catégories et machines, Thèse de doctorat, Université de Paris 7, Denis Diderot.Google Scholar
Lawvere, W. (1963). Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories. PhD thesis, Columbia University.Google Scholar
Melliès, P. and Tabareau, N. (2008). Free models of T-algebraic theories computed as Kan extensions. Available at: http://hal.archives-ouvertes.fr/hal-00339331/fr/.Google Scholar
Melliès, P.-A. (2005). Asynchronous games 3: An innocent model of linear logic. Electronic Notes in Theoretical Computer Science 122 171–192.Google Scholar
Melliès, P.-A. (2009). Categorical Semantics of Linear Logic, Panoramas et Synthèses vol. 27, Société Mathématique de France.Google Scholar
Melliès, P.-A., Tabareau, N. and Tasson, C. (2009). An explicit formula for the free exponential modality of linear logic. In: ICALP '09: Proceedings of the 36th Internatilonal Collogquium on Automata, Languages and Programming, Lecture Notes in Computer Science, Part II. vol. 5556, Springer-Verlag, 247–260.Google Scholar
Seely, R. (1989). Linear logic,*-autonomous categories and cofree coalgebras. In: Gray, J. and Scedrov, A. (eds.) Applications of Categories in Logic and Computer Science, Contemporary Mathematics, vol. 92. Americab Mathematis Society.Google Scholar
Tasson, C. (2009). Sémantiques et syntaxes vectorielles de la logique linéaire. PhD thesis, Université Paris Diderot.Google Scholar