论文标题
锥体积分
Integration in Cones
论文作者
论文摘要
可测量的锥体，具有线性和可测量的函数作为形态，是直觉的线性逻辑的模型和逐名概率PCF的模型，可容纳“连续数据类型”，例如真实线。然而，到目前为止，他们缺乏使它们成为更通用的概率编程语言模型（尤其是逐个呼叫和逐个通话语言）的模型：一种集成理论的函数的集成理论，该功能是代码域是锥体的功能，这是解释采样编程原始人的关键成分。本文的目的是发展这样的理论：我们对积分的定义是对拓扑矢量空间中Pettis积分锥的适应。我们证明，具有整体保护的线性图作为形态学，形成了线性逻辑的模型，我们开发了两个指数式的comoNADS：第一个基于稳定和可测量功能的概念，而第二个基于较早的工作的概念，第二个基于第二个基于整合性分析函数的概念。
Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates "continuous data types" such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theory of integration for functions whose codomain is a cone, which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that such integrable cones, with integral-preserving linear maps as morphisms, form a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable and measurable functions introduced in earlier work and the second based on a new notion of integrable analytic function on cones.
