Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-08T14:30:23.015Z Has data issue: false hasContentIssue false
  • English
  • Français

Linear logic in normed cones: probabilistic coherence spaces and beyond

Published online by Cambridge University Press:  16 November 2021

Sergey Slavnov Open the ORCID record for Sergey Slavnov [Opens in a new window]
Sergey Slavnov*
Affiliation:
National Research University Higher School of Economics, Moscow, Russia
*
Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Ehrhard et al. (2018. Proceedings of the ACM on Programming Languages, POPL 2, Article 59.) proposed a model of probabilistic functional programming in a category of normed positive cones and stable measurable cone maps, which can be seen as a coordinate-free generalization of probabilistic coherence spaces (PCSs). However, unlike the case of PCSs, it remained unclear if the model could be refined to a model of classical linear logic. In this work, we consider a somewhat similar category which gives indeed a coordinate-free model of full propositional linear logic with nondegenerate interpretation of additives and sound interpretation of exponentials. Objects are dual pairs of normed cones satisfying certain specific completeness properties, such as existence of norm-bounded monotone weak limits, and morphisms are bounded (adjointable) positive maps. Norms allow us a distinct interpretation of dual additive connectives as product and coproduct. Exponential connectives are modeled using real analytic functions and distributions that have representations as power series with positive coefficients. Unlike the familiar case of PCSs, there is no reference or need for a preferred basis; in this sense the model is invariant. PCSs form a full subcategory, whose objects, seen as posets, are lattices. Thus, we get a model fitting in the tradition of interpreting linear logic in a linear algebraic setting, which arguably is free from the drawbacks of its predecessors.

Keywords

Linear logicdenotational semanticsprobabilistic coherence spaces
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Issue 5 , May 2021 , pp. 495 - 534
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

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

Banach, S. (1955). Théorie des opérations linéaires, Chelsea Publishing Co.Google Scholar
Blute, R., Ehrhard, T. and Tasson, C. (2012). A convenient differential category. Cahiers de Topologie et Geometrie Differentielle 53 211–232.Google Scholar
Blute, R., Panangaden, P. and Seely, R. (1993). Holomorhpic models of exponential types in 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
Bourbaki, N. (1981). Espaces vectoriels topologiques, Eléments de mathématique, vol. 5, Masson.Google Scholar
Conway, J. (2000). A Course in Operator Theory, Graduate Studies in Mathematics, vol. 21, American Mathematical Society.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, Berlin, Heidelberg, Springer, 20–35.Google Scholar
Dahlqvist, F. and Kozen, D. (2019). Semantics of higher-order probabilistic programs with conditioning. CoRR, abs/1902.11189.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.CrossRefGoogle Scholar
Davies, E. (1968). The structure and ideal theory of the predual of a Banach lattice. Transactions of the American Mathematical Society 131 544–555.CrossRefGoogle Scholar
Ehrhard, T. (2002) On Koethe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 579–623.CrossRefGoogle Scholar
Ehrhard, T. (2020) Cones as a model of intuitionistic linear logic. In: LICS’20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Association for Computing Machinery, 370–383CrossRefGoogle Scholar
Ehrhard, T., Pagani, M. and Tasson, C. (2018) Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. In: Proceedings of the ACM on Programming Languages, POPL 2, Article 59.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 1–41.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science 364 166–195.CrossRefGoogle Scholar
Einsiedler, M. and Ward, T. (2017). Functional Analysis, Spectral Theory, and Applications , Graduate Texts in Mathematics, vol. 276, Springer.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle 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.CrossRefGoogle Scholar
Girard, J.-Y. (1999) Coherent Banach spaces: a continuous denotational semantics. Theoretical Computer Science 227 275–297.CrossRefGoogle 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, 346–381.CrossRefGoogle Scholar
Goubault-Larrecq, J. (2015). Full abstraction for non-deterministic and probabilistic extensions of PCF I: the angelic cases. Journal of Logical and Algebraic Methods in Programming 84 155–184.CrossRefGoogle Scholar
Himmelberg, C. (1966). Quotient uniformities. Transactions of the American Mathematical Society 17 1385–1388.Google Scholar
Keimel, K. and Plotkin, G. (2017). Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science 13 (1).Google Scholar
Kelley, J. (1975). General Topology, Graduate Texts in Mathematics, vol. 27, Springer-Verlag.Google Scholar
Kerjean, M. (2016). Weak topologies for linear logic. Logical Methods in Computer Science 12 (1).CrossRefGoogle Scholar
Melliés, P.-A. (2009). Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses, vol. 27, Société Mathématique de France, 1–196.Google Scholar
Namioka, I. (1957). Partially Ordered Linear Topological Spaces, Memoirs of the American Mathematical Society, vol. 24, American Mathematical Society.Google Scholar
Ng, K. (1971). A duality theorem on partially ordered normed spaces. Journal of the London Mathematical Society 2–3 403–404.CrossRefGoogle 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.CrossRefGoogle Scholar
Selinger, P. (2004). Toward a semantics for higher-order quantum computation. In: Selinger, P. (ed.) Proceedings of the 2nd International Workshop on Quantum Programming Languages, TUCS General Publication, vol. 33, 127–143.Google Scholar
Schaefer, H. and Wolff, M. (1999). Topological Vector Spaces , Graduate Texts in Mathematics, vol. 3, Springer.Google Scholar
Sherman, S. (1951). Order in operator algebras. American Journal of Mathematics 73 227–232.CrossRefGoogle Scholar
Slavnov, S. (2019). On Banach spaces of sequences and free linear logic exponential modality. Mathematical Structures in Computer Science 29 (2) 215–242.CrossRefGoogle Scholar