Classical Linear Logic in Perfect Banach Lattices

Reference. Classical Linear Logic in Perfect Banach Lattices

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.

Cite

Cite as @amorim_witzman_kozen_2025 (helia, typst) · \cite{amorim_witzman_kozen_2025} (LaTeX)

BibTeX

bibtex · 10 lines

@inproceedings{amorim_witzman_kozen_2025,
 title = {Classical Linear Logic in Perfect Banach Lattices},
 author = {Amorim, Pedro H. Azevedo de and Witzman, Leon and Kozen, Dexter},
 year = {2025},
 doi = {10.4230/LIPIcs.CSL.2025.44},
 url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.44},
 booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
 series = {LIPIcs},
 publisher = {Schloss Dagstuhl}
}

hayagriva YAML (typst)

yaml · 18 lines

amorim_witzman_kozen_2025:
  type: article
  title: Classical Linear Logic in Perfect Banach Lattices
  author:
  - Amorim, Pedro H. Azevedo de
  - Witzman, Leon
  - Kozen, Dexter
  date: 2025
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.44
  serial-number:
    doi: 10.4230/LIPIcs.CSL.2025.44
  parent:
    type: proceedings
    title: 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)
    publisher: Schloss Dagstuhl
    parent:
      type: proceedings
      title: LIPIcs

Download: amorim_witzman_kozen_2025.bib · amorim_witzman_kozen_2025.yml

Cites 34 works (2 here)

With notes (2)

A Higher-Order Language for Markov Kernels and Linear Operators amorim_2023_fossacsFoSSaCS · 2023

Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators.

Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strengths and weaknesses. Though it is believed that there is a connection between them there are no languages that can handle both styles of programming.

In this work we address these questions by defining a two-level calculus and its categorical semantics which makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, where the resource being kept track of is sampling instead of variable use.

DOI

A convenient category for higher-order probability theory heunen-2017-aLICS · 2017

DOI · arXiv

External (32)

Affine monads and lazy structures for bayesian programming (2023)
Sppl: probabilistic programming with fast exact symbolic inference (2021)
Linear logic in normed cones: probabilistic coherence spaces and beyond (2021)
Compositional semantics for probabilistic programs with exact conditioning (2021)
On the linear structure of cones (2020)
A synthetic approach to markov kernels, conditional independence and theorems on sufficient statistics (2020)
Scaling exact inference for discrete probabilistic programs (2020)
Symbolic disintegration with a variety of base measures (2020)
Semantics of higher-order probabilistic programs with conditioning (2019)
Differentials and distances in probabilistic coherence spaces (2019)
Trace types and denotational semantics for sound programmable inference in probabilistic languages (2019)
Probabilistic call by push value (2019)
Probabilistic stable functions on discrete cones are power series (2018)
Mackey-complete spaces and power series–a topological model of differential linear logic (2018)
Probabilistic programming with programmable inference (2018)
Stan: A probabilistic programming language (2017)
Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming (2017)
Exact bayesian inference by symbolic disintegration (2017)
Psi: Exact symbolic inference for probabilistic programs (2016)
Probabilistic inference by program transformation in hakaru (system description) (2016)
Design and implementation of probabilistic programming language anglican (2016)
Probabilistic coherence spaces are fully abstract for probabilistic PCF (2014)
Introduction to operator theory in Riesz spaces (2012)
Probabilistic coherence spaces as a model of higher-order probabilistic computation (2011)
Categorical semantics of linear logic (2009)
Church: a language for generative models (2008)
On Köthe sequence spaces and linear logic (2002)
Coherent banach spaces: a continuous denotational semantics (1999)
Semantics of probabilistic programs (1979)
Abstract Köthe spaces IV (1968)
Notes on Banach function spaces VI-XIII (1963)
Borel structures for function spaces (1961)