A Sampling-Aware Interpretation of Linear Logic: Syntax and Categorical Semantics

The usual resource interpretation of linear logic says that variables have to be used exactly once. However, there are models of linear logic where this interpretation is too restrictive. In this work we show how in probabilistic models of linear logic the correct resource interpretation should be sampling, i.e. the linear arrow should be read as "the output may only sample once from its input". We accommodate this new interpretation by defining a multilanguage syntax and its categorical semantics that bridges the Markov kernel and linear logic interpretations of probabilistic programs.