×

Linear logic in normed cones: probabilistic coherence spaces and beyond. (English) Zbl 07527569

Summary: Th. Ehrhard et al. [“Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming”, in: Proceedings of the ACM on Programming Languages, POPL 2. New York, NY: ACM. Article No. 59, 28 p. (2018; doi:10.1145/3158147)] 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.

MSC:

03F52 Proof-theoretic aspects of linear logic and other substructural logics

Software:

QPL

References:

[1] Banach, S. (1955). Théorie des opérations linéaires, Chelsea Publishing Co. · Zbl 0067.08902
[2] Blute, R., Ehrhard, T. and Tasson, C. (2012). A convenient differential category. Cahiers de Topologie et Geometrie Differentielle53211-232. · Zbl 1281.46061
[3] 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. · Zbl 1509.18020
[4] Bourbaki, N. (1981). Espaces vectoriels topologiques, Eléments de mathématique, vol. 5, Masson. · Zbl 0482.46001
[5] Conway, J. (2000). A Course in Operator Theory, Graduate Studies in Mathematics, vol. 21, American Mathematical Society. · Zbl 0936.47001
[6] 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. · Zbl 1486.03104
[7] Dahlqvist, F. and Kozen, D. (2019). Semantics of higher-order probabilistic programs with conditioning. CoRR, abs/1902.11189.
[8] Danos, V. and Ehrhard, T. (2011). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation209 (6) 966-991. · Zbl 1267.68085
[9] Davies, E. (1968). The structure and ideal theory of the predual of a Banach lattice. Transactions of the American Mathematical Society131544-555. · Zbl 0159.41503
[10] Ehrhard, T. (2002) On Koethe sequence spaces and linear logic. Mathematical Structures in Computer Science12579-623.
[11] 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-383 · Zbl 1498.03157
[12] 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. · Zbl 1426.68035
[13] Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science3091-41. · Zbl 1070.68020
[14] Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science364166-195. · Zbl 1113.03054
[15] Einsiedler, M. and Ward, T. (2017). Functional Analysis, Spectral Theory, and Applications , Graduate Texts in Mathematics, vol. 276, Springer. · Zbl 1387.46001
[16] Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science501-102.
[17] 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. · Zbl 0828.03003
[18] Girard, J.-Y. (1999) Coherent Banach spaces: a continuous denotational semantics. Theoretical Computer Science227275-297.
[19] 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. · Zbl 1073.03036
[20] 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 Programming84155-184. · Zbl 1304.68026
[21] Himmelberg, C. (1966). Quotient uniformities. Transactions of the American Mathematical Society171385-1388.
[22] Keimel, K. and Plotkin, G. (2017). Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science13 (1). · Zbl 1448.06002
[23] Kelley, J. (1975). General Topology, Graduate Texts in Mathematics, vol. 27, Springer-Verlag. · Zbl 0306.54002
[24] Kerjean, M. (2016). Weak topologies for linear logic. Logical Methods in Computer Science12 (1). · Zbl 1448.03014
[25] 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. · Zbl 1206.03052
[26] Namioka, I. (1957). Partially Ordered Linear Topological Spaces, Memoirs of the American Mathematical Society, vol. 24, American Mathematical Society. · Zbl 0105.08901
[27] Ng, K. (1971). A duality theorem on partially ordered normed spaces. Journal of the London Mathematical Society2-3403-404.
[28] 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. · Zbl 0674.03007
[29] 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.
[30] Schaefer, H. and Wolff, M. (1999). Topological Vector Spaces, Graduate Texts in Mathematics, vol. 3, Springer. · Zbl 0983.46002
[31] Sherman, S. (1951). Order in operator algebras. American Journal of Mathematics73227-232. · Zbl 0042.35001
[32] Slavnov, S. (2019). On Banach spaces of sequences and free linear logic exponential modality. Mathematical Structures in Computer Science29 (2) 215-242. · Zbl 1456.03106
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.