Extensional Denotational Semantics of Higher-Order Probabilistic Programs, Beyond the Discrete Case

2021/04/13 by Geoffroy, Guillaume
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2104.06016

Abstract

We describe a mathematical structure that can give extensional denotational semantics to higher-order probabilistic programs. It is not limited to discrete probabilities, and it is compatible with integration in a way the models that have been proposed before are not. It is organised as a model of propositional linear logic in which all the connectives have intuitive probabilistic interpretations. In addition, it has least fixed points for all maps, so it can interpret recursion.

Related

• Semantics of higher-order probabilistic programs with conditioning
• ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
• A Higher-Order Language for Markov Kernels and Linear Operators
• Probabilistic Logic: Many-valuedness and Intensionality
• Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability