Hostname: page-component-78c5997874-8bhkd Total loading time: 0 Render date: 2024-11-10T18:52:57.277Z Has data issue: false hasContentIssue false
  • English
  • Français

Mackey-complete spaces and power series – a topological model of differential linear logic

Published online by Cambridge University Press:  21 October 2016

MARIE KERJEAN  and
CHRISTINE TASSON
MARIE KERJEAN
Affiliation:
Laboratory PPS, Université Paris Diderot, Paris, France Emails: [email protected], [email protected]
CHRISTINE TASSON
Affiliation:
Laboratory PPS, Université Paris Diderot, Paris, France Emails: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we describe a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted as bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we use a notion of power series between Mackey-complete spaces, generalizing entire functions in $\mathbb{C}$ . Finally, we get a quantitative model of Intuitionist Differential Linear Logic, with usual syntactic differentiation and where interpretations of proofs decompose as a Taylor expansion.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 28 , Issue 4 , April 2018 , pp. 472 - 507
Copyright
Copyright © Cambridge University Press 2016 

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

Abramsky, S., Jagadeesan, R. and Malacaria, P. (2000). Full abstraction for PCF. Information and Computation 163 (2) 409–470.CrossRefGoogle Scholar
Barr, M. (1979). *-Autonomous Categories, Lecture Notes in Mathematics, volume 752, Springer, Berlin, With an appendix by Po Hsiang Chu.Google Scholar
Blute, R., Cockett, J.R.B. and Seely, R.A.G. (2015). Cartesian differential storage categories. Theory and Applications of Categories 30 (18) 620–687.Google Scholar
Blute, R., Panangaden, P. and Seely, R. (1994). Fock space: A model of linear exponential types. Manuscript, revised version of the MFPS paper Holomorphic Models of Exponential Types in Linear Logic, 474–512.Google Scholar
Blute, R., Cockett, R. and Seely, R. (2006). Differential categories. Mathematical Structures in Computer Science 16 (6) 1049–1083.Google Scholar
Blute, R., Cockett, R. and Seely, R. (2009). Cartesian differential categories. Theory and Applications of Categories 22 (23) 622–672.Google Scholar
Blute, R., Ehrhard, T. and Tasson, C. (2012). A convenient differential category. Cahiers de Topologie et Géométrie Différentielle Catégoriques 53 (3) 211–232. ISSN .Google Scholar
Bochnak, J. and Siciak, J. (1971). Analytic functions in topological vector spaces. Studia Mathematica 39 77–112.Google Scholar
Boman, J. (1967). Differentiability of a function and of its compositions with functions of one variable. Mathematics Scandinavica 20 249–268.CrossRefGoogle Scholar
Danos, V. and Ehrhard, T. (2016). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209 (6) 966–991.CrossRefGoogle Scholar
Ehrhard, T. (2002). On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 (5) 579–623.CrossRefGoogle Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 (4) 615–646.Google Scholar
Ehrhard, T. (2007). On finiteness spaces and extensional presheaves over the lawvere theory of polynomials. Journal of Pure and Applied Algebra, To appear.Google Scholar
Ehrhard, T. (2016). An introduction to differential linear logic: proof-nets, models and antiderivatives. CoRR abs/1606.01642Google Scholar
Ehrhard, T. and Regnier, L. (2003a). The differential lambda-calculus. Theoretical Computer Science 309 (1–3) 1–41.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2003b). The differential lambda-calculus. Theoretical Computer Science 309 (1–3) 1–41.Google Scholar
Ehrhard, T., Pagani, L. and Tasson, C. (2014). Probabilistic coherence spaces are fully abstract for probabilistic PCF. In: Sewell, P. (ed.), The 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL14, San Diego, USA. ACM.Google Scholar
Escardó, M. and Heckmann, R. (2001/02). Topologies on spaces of continuous functions. In: Proceedings of the 16th Summer Conference on General Topology and its Applications (New York), volume 26, 545–564.Google Scholar
Fiore, M. (2007). Differential structure in models of multiplicative biadditive intuitionistic linear logic. In: Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26–28, 2007 163–177.Google Scholar
Fiore, M., Gambino, N., Hyland, M. and Winskel, G. (2008). The Cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society. Second Series 77 (1) 203–220.Google Scholar
Frölicher, A. and Kriegl, A. (1988). Linear Spaces and Differentiation Theory, Wiley.Google Scholar
Girard, J.-Y. (1986). The system F of variable types, fifteen years later. Theoretical Computer Science 45 (2) 159–192.CrossRefGoogle Scholar
Girard, J.-Y. (1988). Normal functors, power series and λ-calculus. Annals of Pure and Applied Logic 37 (2) 129–177.CrossRefGoogle Scholar
Girard, J.-Y. (1999). Coherent Banach spaces: a continuous denotational semantics. Theoretical Computer Science 227 (1–2) 275–297. ISSN . Linear logic, I (Tokyo, 1996).Google Scholar
Grothendieck, A. (1953). Sur certains espaces de fonctions holomorphes. I. Journal für die Reine und Angewandte Mathematik 192 35–64.Google Scholar
Hasegawa, R. (2002). Two applications of analytic functors. Theoretical Computer Science 272 (1) 113–175.CrossRefGoogle Scholar
Hogbe-Nlend, H. (1970). Sur le “problème de hahn-banach” en bornologie. Comptes Rendus de l'Académie des Sciences Paris Séries A-B 270 A1320–A1322.Google Scholar
Hogbe-Nlend, H. (1977). Bornologies and Functional Analysis. Mathematics Studies, volume 26, North Holland, Amsterdam.Google Scholar
Hyland, M. and Ong, L. (2000). On full abstraction for PCF. Information and Computation 163 (2) 285–408.CrossRefGoogle Scholar
Iglesias-Zemmour, P. (2013). Diffeology, Mathematical Surveys and Monographs, volume 185, American Mathematical Society, Providence, RI.CrossRefGoogle Scholar
Jarchow, H. (1981). Locally convex spaces. Teubner, B. G., Stuttgart. Mathematical Textbooks.Google Scholar
Kriegl, A. and Michor, P.W. (1997). The Convenient Setting of Global Analysis, Mathematical Surveys and Monographs, volume 53, American Mathematical Society, Providence, RI.CrossRefGoogle Scholar
Laird, J., Manzonetto, G. and McCusker, G. (2013a). Constructing differential categories and deconstructing categories of games. Information and Computation 222 (C) 247–264.Google Scholar
Laird, J., Manzonetto, G., McCusker, G. and Pagani, M. (2013b). Weighted relational models of typed lambda-calculi. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), 25–28 June 2013, New Orleans, USA 301–310.Google Scholar
Manzonetto, G. (2012). What is a categorical model of the differential and the resource λ-calculi? Mathematical Structures in Computer Science 22 (3) 451–520.Google Scholar
Pagani, M., Selinger, P. and Valiron, B. (2014). Applying quantitative semantics to higher-order quantum computing. In: Sewell, P. (ed.), The 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL14, San Diego, USA. ACM.Google Scholar
Robertson, A.P. (1970). On bornological products. Glasgow Mathematical Journal 11 37–40.Google Scholar
Robin, J., Cockett, B. and Cruttwell, G.S.H. (2014). Differential structure, tangent structure, and SDG. Applied Categorical Structures 22 (2) 331–417.Google Scholar
Schaefer, H.H. (1971). Topological Vector Spaces, Graduate Texts in Mathematics, volume 3, Springer-Verlag, New York-Berlin. Third printing corrected.Google Scholar
Ulam, S. (1930). Zur masstheorie in der allgemeinen mengenlehre. Fundamenta Mathematicae 16 (1) 140–150.Google Scholar