Document Open Access Logo

Classical Linear Logic in Perfect Banach Lattices

Authors Pedro H. Azevedo de Amorim , Leon Witzman , Dexter Kozen

PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.44.pdf
  • Filesize: 0.89 MB
  • 21 pages

Document Identifiers

Author Details

Pedro H. Azevedo de Amorim
  • Oxford University, UK
Leon Witzman
  • Nanyang Technological University, Singapore
Dexter Kozen
  • Cornell University, Ithaca, NY, USA

Funding

  • Azevedo de Amorim, Pedro H.: Pedro H. Azevedo de Amorim was funded by the National Science Foundation under grant CCF-2008083. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.
  • Kozen, Dexter: Dexter Kozen was funded by the National Science Foundation under grants AitF-1637532, SaTC-1717581, and CCF-2008083. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

Acknowledgements

The authors would like to thank Raphaëlle Crubillé, Christine Tasson, Thomas Ehrhard and Fredrik Dahlqvist for lively discussions on the subject. We would also like to thank Arthur Azevedo de Amorim and Michael Roberts for reading an earlier draft of this work.

Cite As Get BibTex

Pedro H. Azevedo de Amorim, Leon Witzman, and Dexter Kozen. Classical Linear Logic in Perfect Banach Lattices. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 44:1-44:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.44

Abstract

In recent years, researchers have proposed various models of linear logic with strong connections to measure theory, with probabilistic coherence spaces (PCoh) being one of the most prominent. One of the main limitations of the PCoh model is that it cannot interpret continuous measures. To overcome this obstacle, Ehrhard has extended PCoh to a category of positive cones and linear Scott-continuous functions and shown that it is a model of intuitionistic linear logic. In this work we show that the category PBanLat₁ of perfect Banach lattices and positive linear functions of norm at most 1 can serve the same purpose, with some added benefits. We show that PBanLat₁ is a model of classical linear logic (without exponential) and that PCoh embeds fully and faithfully in PBanLat₁ while preserving the monoidal and *-autonomous structures. Finally, we show how PBanLat₁ can be used to give semantics to a higher-order probabilistic programming language.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Linear logic
  • Theory of computation → Denotational semantics
  • Theory of computation → Probabilistic computation
Keywords
  • Probabilistic Semantics
  • Linear Logic
  • Categorical Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Charalambos D Aliprantis and Owen Burkinshaw. Positive operators. Springer, 2006. URL: https://doi.org/10.1007/978-1-4020-5008-4.
  2. Pedro H. Azevedo de Amorim. A higher-order language for markov kernels and linear operators. In Foundations of Software Science and Computation Structures (FoSSaCS), 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_5.
  3. Francis Borceux. Handbook of categorical algebra: volume 1, Basic category theory, volume 1. Cambridge University Press, 1994. Google Scholar
  4. Francis Borceux. Handbook of categorical algebra: volume 2, Categories and Structures, volume 2. Cambridge University Press, 1994. Google Scholar
  5. Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 2019. Google Scholar
  6. Raphaëlle Crubillé. Probabilistic stable functions on discrete cones are power series. In Logic in Computer Science (LICS), 2018. Google Scholar
  7. Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. In Principles of Programming Languages (POPL), 2019. Google Scholar
  8. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 209(6):966-991, 2011. URL: https://doi.org/10.1016/J.IC.2011.02.001.
  9. Thomas Ehrhard. On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, 12(5):579-623, 2002. URL: https://doi.org/10.1017/S0960129502003729.
  10. Thomas Ehrhard. Differentials and distances in probabilistic coherence spaces. arXiv preprint, 2019. URL: https://arxiv.org/abs/1902.04836.
  11. Thomas Ehrhard. On the linear structure of cones. In Logic in Computer Science (LICS), 2020. Google Scholar
  12. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. In Principles of Programming Languages (POPL), 2017. Google Scholar
  13. Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Principles of Programming Languages (POPL), 2014. Google Scholar
  14. David H Fremlin. Measure theory. Torres Fremlin, 2000. Google Scholar
  15. DH Fremlin. Abstract Köthe spaces IV. In Mathematical Proceedings of the Cambridge Philosophical Society, pages 45-52. Cambridge University Press, 1968. Google Scholar
  16. Tobias Fritz. A synthetic approach to markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020. Google Scholar
  17. Jean-Yves Girard. Coherent banach spaces: a continuous denotational semantics. Theoretical Computer Science, 227(1-2):275-297, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00056-0.
  18. Klaus Keimel and Gordon D Plotkin. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science, 2017. Google Scholar
  19. Marie Kerjean and Christine Tasson. Mackey-complete spaces and power series-a topological model of differential linear logic. Mathematical Structures in Computer Science, 28(4):472-507, 2018. URL: https://doi.org/10.1017/S0960129516000281.
  20. Dexter Kozen. Semantics of probabilistic programs. In Symposium on Foundations of Computer Science (SFCS), 1979. Google Scholar
  21. WAJ Luxemberg and AC Zaanen. Notes on Banach function spaces VI-XIII. Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, Series A, 66:251-263, 1963. Google Scholar
  22. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  23. Peter Selinger. Towards a semantics for higher-order quantum computation. In Quantum Programming Languages (QPL), 2004. Google Scholar
  24. Sergey Slavnov. Linear logic in normed cones: probabilistic coherence spaces and beyond. Mathematical Structures in Computer Science, 31(5):495-534, 2021. URL: https://doi.org/10.1017/S0960129521000177.
  25. Christine Tasson and Thomas Ehrhard. Probabilistic call by push value. Logical Methods in Computer Science, 15, 2019. URL: https://doi.org/10.23638/LMCS-15(1:3)2019.
  26. Adriaan C Zaanen. Introduction to operator theory in Riesz spaces. Springer, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact