Hostname: page-component-7bb8b95d7b-pwrkn Total loading time: 0 Render date: 2024-09-17T21:49:42.610Z Has data issue: false hasContentIssue false

On Banach spaces of sequences and free linear logic exponential modality

Published online by Cambridge University Press:  18 December 2017

SERGEY SLAVNOV*
Affiliation:
National Research University Higher School of Economics, Tallinskaya-24, Moscow 123458, Russia Email: [email protected]

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
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

Blute, R., Ehrhard, T. and Tasson, C. (2012). A convenient differential category. Cahiers de Topologie et Geometrie Differentielle 53 (3) 211232.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, 2035.Google Scholar
Danos, V. and Ehrhard, T. (2011). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209 (6) 966991.Google Scholar
Ehrhard, T. (2002). On Koethe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 579623.Google Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 141.Google Scholar
Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science 364 166195.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. (1987). Linear logic. Theoretical Computer Science 50 1102.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, 142.Google Scholar
Girard, J.-Y. (1999). Coherent Banach spaces: A continuous denotational semantics. Theoretical Computer Science 227 275297.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. 346381.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, 1196.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, 247260.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, 371382.Google Scholar