Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of probabilistic PCF which accommodates ''continuous data types'' such as the real line. So far they lacked however a major feature to make them a model of other probabilistic programming languages: a general and vesatile theory of integration which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory based on a notion of integrable cones and of integrable linear maps. We prove that we obtain again in that way a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable functions introduced in earlier work and the second based on a new notion of integrable analytic function on cones.
翻译:可计量的锥体具有线性、可测量的形态性功能,是直观线性逻辑和概率PCF的模型,它包含“连续数据类型”等真实线条。但迄今为止,它们缺乏一个主要特征,无法使它们成为其他概率性编程语言的模型:一个通用和微小集成理论,这是解释抽样编程原始数据的关键成分。本文件的目标是根据可探测锥体和不可探测线性地图的概念发展这样一个理论。我们证明,我们以这种方式又获得了一种线性逻辑模型,我们为此开发了两种指数共鸣词:第一个基于先前工作中引入的稳定功能概念,第二个基于对锥体的不可探测分析功能的新概念。