Hostname: page-component-78c5997874-s2hrs Total loading time: 0 Render date: 2024-11-13T09:23:44.924Z 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: [email protected], [email protected]
NICOLAS TABAREAU
Affiliation:
Univ Paris Diderot, Sorbonne Paris Cité, IRIF, UMR 8243, CNRS, F-75205 Paris, France Email: [email protected], [email protected]
CHRISTINE TASSON
Affiliation:
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes - Bretagne Atlantiquezd Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 28 , Special Issue 7: Differential Linear Logic, Nets and Other Quantitative and Parallel Approaches to Proof-Theory , August 2018 , pp. 1253 - 1286
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

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