Article contents
On Banach spaces of sequences and free linear logic exponential modality
Published online by Cambridge University Press: 18 December 2017
Abstract
We introduce a category of vector spaces modelling full propositional linear logic, similar to probabilistic coherence spaces and to Koethe sequences spaces. Its objects are rigged sequence spaces, Banach spaces of sequences, with norms defined from pairing with finite sequences, and morphisms are bounded linear maps, continuous in a suitable topology. The main interest of the work is that our model gives a realization of the free linear logic exponentials construction.
- Type
- Paper
- Information
- Copyright
- Copyright © Cambridge University Press 2017
References
Blute, R., Ehrhard, T. and Tasson, C. (2012). A convenient differential category. Cahiers de Topologie et Geometrie Differentielle 53 (3) 211–232.Google Scholar
Blute, R., Panangaden, P. and Seely, R. (1993). Old foundations for linear logic. In: Proceedings of the 9th Symposium on Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, vol. 802, Springer-Verlag, 474–512.Google Scholar
Crubillé, R., Ehrhard, T., Pagani, M. and Tasson, C. (2017). The free exponential modality of probabilistic coherence spaces. In: Esparza, J. and Murawski, A. (eds.) Foundations of Software Science and Computation Structures. FoSSaCS 2017, Lecture Notes in Computer Science, vol. 10203, Springer, Berlin, Heidelberg, 20–35.Google Scholar
Danos, V. and Ehrhard, T. (2011). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209 (6) 966–991.Google Scholar
Ehrhard, T. (2002). On Koethe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 579–623.Google Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 1–41.Google Scholar
Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science 364 166–195.Google Scholar
Gelfand, I. and Vilenkin, N. (1964). Generalized Functions, vol. 4: Some Applications of Harmonic Analysis. Rigged Hilbert Spaces, Academic Press.Google Scholar
Girard, J.-Y. (1995). Linear logic: Its syntax and semantics. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, London Mathematical Society Lecture Note Series, vol. 222, Cambridge University Press, 1–42.Google Scholar
Girard, J.-Y. (1999). Coherent Banach spaces: A continuous denotational semantics. Theoretical Computer Science 227 275–297.Google Scholar
Girard, J.-Y. (2004). Between logic and quantic: A tract. In: Ehrhard, Th., Girard, J.-Y., Ruet, P. and Scott, Ph. (eds.) Linear Logic in Computer Science, London Mathematical Society Lecture Note Series, vol. 316, Cambridge University Press, pp. 346–381.Google Scholar
Lafont, Y. (1988). Logique, catégories et machines. Thèse de doctorat, Université de Paris 7, Denis Diderot.Google Scholar
Melliés, P.-A. (2009). Categorical semantics of linear logic. In: Curien, P.-L., Herbelin, H., Krivine, J.-L. and Melliés, P.-A. (eds.) Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses, vol. 27, Société Mathématique de France, 1–196.Google Scholar
Melliés, P.-A., Tabareau, N. and Tasson, C. (2009). An explicit formula for the free exponential modality of linear logic. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S. and Thomas, W. (eds.) Automata, Languages and Programming. ICALP 2009, Lecture Notes in Computer Science, vol. 5556, 247–260.Google Scholar
Rudin, W. (1991). Functional analysis. In: International Series in Pure and Applied Mathematics, McGraw-Hill Science/Engineering/Math.Google Scholar
Seely, R.A.G. (1989). Linear logic, *-autonomous categories and cofree coalgebras. In: Gray, J. and Scedrov, A. (eds.) Categories in Computer Science and Logic, Contemporary Mathematics, vol. 92, American Mathematical Society, 371–382.Google Scholar
- 1
- Cited by