Abstract
The exponential modality of linear logic associates a commutative comonoid !A to every formula A in order to duplicate it. 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 then apply this general recipe to two familiar models of linear logic, based on coherence spaces and on Conway games. This algebraic approach enables to unify for the first time apparently different constructions of the exponential modality in spaces and games. It also sheds light on the subtle duplication policy of linear logic. On the other hand, we explain at the end of the article why the formula does not work in the case of the finiteness space model.
This work has been supported by the ANR Curry-Howard Correspondence and Concurrency Theory (CHOCO).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ehrhard, T.: On finiteness spaces and extensional presheaves over the lawvere theory of polynomials. Journal of Pure and Applied Algebra (to appear)
Ehrhard, T.: Finiteness spaces. Mathematical. Structures in Comp. Sci. 15(4) (2005)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Joyal, A.: Remarques sur la théorie des jeux à deux personnes. Gazette des Sciences Mathématiques du Québec 1(4), 46–52 (1977); English version by Robin Houston
Kelly, M., Laplaza, M.: Coherence for compact closed categories. Journal of Pure and Applied Algebra 19, 193–213 (1980)
Lafont, Y.: Logique, catégories et machines. Thèse de doctorat, Université de Paris 7, Denis Diderot (1988)
Lefschetz, S., et al.: Algebraic topology. American Mathematical Society (1942)
Melliès, P.A., Tabareau, N.: Free models of T-algebraic theories computed as Kan extensions. Submitted to Journal of Pure and Applied Algebra
Melliès, P.A.: Asynchronous Games 3: An Innocent Model of Linear Logic. Electronic Notes in Theoretical Computer Science 122, 171–192 (2005)
Seely, R.: Linear logic, *-autonomous categories and cofree coalgebras. In: Applications of categories in logic and computer science, vol. (92), Contemporary Mathematics (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melliès, PA., Tabareau, N., Tasson, C. (2009). An Explicit Formula for the Free Exponential Modality of Linear Logic. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds) Automata, Languages and Programming. ICALP 2009. Lecture Notes in Computer Science, vol 5556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02930-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-02930-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02929-5
Online ISBN: 978-3-642-02930-1
eBook Packages: Computer ScienceComputer Science (R0)